MAYBE

Problem:
 *(0(),x) -> 0()
 *(1(),x) -> x
 *(2(),2()) -> .(1(),0())
 *(3(),x) -> .(x,*(min(),x))
 *(min(),min()) -> 1()
 *(2(),min()) -> .(min(),2())
 *(.(x,y),z) -> .(*(x,z),*(y,z))
 *(+(y,z),x) -> +(*(x,y),*(x,z))
 +(0(),x) -> x
 +(x,x) -> *(2(),x)
 +(1(),2()) -> 3()
 +(1(),min()) -> 0()
 +(2(),min()) -> 1()
 +(3(),x) -> .(1(),+(min(),x))
 +(.(x,y),z) -> .(x,+(y,z))
 +(*(2(),x),x) -> *(3(),x)
 +(*(min(),x),x) -> 0()
 +(*(2(),v),*(min(),v)) -> v
 .(min(),3()) -> min()
 .(x,min()) -> .(+(min(),x),3())
 .(0(),x) -> x
 .(x,.(y,z)) -> .(+(x,y),z)

Proof:
 DP Processor:
  DPs:
   *#(2(),2()) -> .#(1(),0())
   *#(3(),x) -> *#(min(),x)
   *#(3(),x) -> .#(x,*(min(),x))
   *#(2(),min()) -> .#(min(),2())
   *#(.(x,y),z) -> *#(y,z)
   *#(.(x,y),z) -> *#(x,z)
   *#(.(x,y),z) -> .#(*(x,z),*(y,z))
   *#(+(y,z),x) -> *#(x,z)
   *#(+(y,z),x) -> *#(x,y)
   *#(+(y,z),x) -> +#(*(x,y),*(x,z))
   +#(x,x) -> *#(2(),x)
   +#(3(),x) -> +#(min(),x)
   +#(3(),x) -> .#(1(),+(min(),x))
   +#(.(x,y),z) -> +#(y,z)
   +#(.(x,y),z) -> .#(x,+(y,z))
   +#(*(2(),x),x) -> *#(3(),x)
   .#(x,min()) -> +#(min(),x)
   .#(x,min()) -> .#(+(min(),x),3())
   .#(x,.(y,z)) -> +#(x,y)
   .#(x,.(y,z)) -> .#(+(x,y),z)
  TRS:
   *(0(),x) -> 0()
   *(1(),x) -> x
   *(2(),2()) -> .(1(),0())
   *(3(),x) -> .(x,*(min(),x))
   *(min(),min()) -> 1()
   *(2(),min()) -> .(min(),2())
   *(.(x,y),z) -> .(*(x,z),*(y,z))
   *(+(y,z),x) -> +(*(x,y),*(x,z))
   +(0(),x) -> x
   +(x,x) -> *(2(),x)
   +(1(),2()) -> 3()
   +(1(),min()) -> 0()
   +(2(),min()) -> 1()
   +(3(),x) -> .(1(),+(min(),x))
   +(.(x,y),z) -> .(x,+(y,z))
   +(*(2(),x),x) -> *(3(),x)
   +(*(min(),x),x) -> 0()
   +(*(2(),v),*(min(),v)) -> v
   .(min(),3()) -> min()
   .(x,min()) -> .(+(min(),x),3())
   .(0(),x) -> x
   .(x,.(y,z)) -> .(+(x,y),z)
  TDG Processor:
   DPs:
    *#(2(),2()) -> .#(1(),0())
    *#(3(),x) -> *#(min(),x)
    *#(3(),x) -> .#(x,*(min(),x))
    *#(2(),min()) -> .#(min(),2())
    *#(.(x,y),z) -> *#(y,z)
    *#(.(x,y),z) -> *#(x,z)
    *#(.(x,y),z) -> .#(*(x,z),*(y,z))
    *#(+(y,z),x) -> *#(x,z)
    *#(+(y,z),x) -> *#(x,y)
    *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    +#(x,x) -> *#(2(),x)
    +#(3(),x) -> +#(min(),x)
    +#(3(),x) -> .#(1(),+(min(),x))
    +#(.(x,y),z) -> +#(y,z)
    +#(.(x,y),z) -> .#(x,+(y,z))
    +#(*(2(),x),x) -> *#(3(),x)
    .#(x,min()) -> +#(min(),x)
    .#(x,min()) -> .#(+(min(),x),3())
    .#(x,.(y,z)) -> +#(x,y)
    .#(x,.(y,z)) -> .#(+(x,y),z)
   TRS:
    *(0(),x) -> 0()
    *(1(),x) -> x
    *(2(),2()) -> .(1(),0())
    *(3(),x) -> .(x,*(min(),x))
    *(min(),min()) -> 1()
    *(2(),min()) -> .(min(),2())
    *(.(x,y),z) -> .(*(x,z),*(y,z))
    *(+(y,z),x) -> +(*(x,y),*(x,z))
    +(0(),x) -> x
    +(x,x) -> *(2(),x)
    +(1(),2()) -> 3()
    +(1(),min()) -> 0()
    +(2(),min()) -> 1()
    +(3(),x) -> .(1(),+(min(),x))
    +(.(x,y),z) -> .(x,+(y,z))
    +(*(2(),x),x) -> *(3(),x)
    +(*(min(),x),x) -> 0()
    +(*(2(),v),*(min(),v)) -> v
    .(min(),3()) -> min()
    .(x,min()) -> .(+(min(),x),3())
    .(0(),x) -> x
    .(x,.(y,z)) -> .(+(x,y),z)
   graph:
    +#(3(),x) -> +#(min(),x) -> +#(*(2(),x),x) -> *#(3(),x)
    +#(3(),x) -> +#(min(),x) -> +#(.(x,y),z) -> .#(x,+(y,z))
    +#(3(),x) -> +#(min(),x) -> +#(.(x,y),z) -> +#(y,z)
    +#(3(),x) -> +#(min(),x) -> +#(3(),x) -> .#(1(),+(min(),x))
    +#(3(),x) -> +#(min(),x) -> +#(3(),x) -> +#(min(),x)
    +#(3(),x) -> +#(min(),x) -> +#(x,x) -> *#(2(),x)
    +#(3(),x) -> .#(1(),+(min(),x)) -> .#(x,.(y,z)) -> .#(+(x,y),z)
    +#(3(),x) -> .#(1(),+(min(),x)) -> .#(x,.(y,z)) -> +#(x,y)
    +#(3(),x) -> .#(1(),+(min(),x)) ->
    .#(x,min()) -> .#(+(min(),x),3())
    +#(3(),x) -> .#(1(),+(min(),x)) -> .#(x,min()) -> +#(min(),x)
    +#(.(x,y),z) -> +#(y,z) -> +#(*(2(),x),x) -> *#(3(),x)
    +#(.(x,y),z) -> +#(y,z) -> +#(.(x,y),z) -> .#(x,+(y,z))
    +#(.(x,y),z) -> +#(y,z) -> +#(.(x,y),z) -> +#(y,z)
    +#(.(x,y),z) -> +#(y,z) -> +#(3(),x) -> .#(1(),+(min(),x))
    +#(.(x,y),z) -> +#(y,z) -> +#(3(),x) -> +#(min(),x)
    +#(.(x,y),z) -> +#(y,z) -> +#(x,x) -> *#(2(),x)
    +#(.(x,y),z) -> .#(x,+(y,z)) -> .#(x,.(y,z)) -> .#(+(x,y),z)
    +#(.(x,y),z) -> .#(x,+(y,z)) -> .#(x,.(y,z)) -> +#(x,y)
    +#(.(x,y),z) -> .#(x,+(y,z)) -> .#(x,min()) -> .#(+(min(),x),3())
    +#(.(x,y),z) -> .#(x,+(y,z)) -> .#(x,min()) -> +#(min(),x)
    +#(*(2(),x),x) -> *#(3(),x) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    +#(*(2(),x),x) -> *#(3(),x) -> *#(+(y,z),x) -> *#(x,y)
    +#(*(2(),x),x) -> *#(3(),x) -> *#(+(y,z),x) -> *#(x,z)
    +#(*(2(),x),x) -> *#(3(),x) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
    +#(*(2(),x),x) -> *#(3(),x) -> *#(.(x,y),z) -> *#(x,z)
    +#(*(2(),x),x) -> *#(3(),x) -> *#(.(x,y),z) -> *#(y,z)
    +#(*(2(),x),x) -> *#(3(),x) -> *#(2(),min()) -> .#(min(),2())
    +#(*(2(),x),x) -> *#(3(),x) -> *#(3(),x) -> .#(x,*(min(),x))
    +#(*(2(),x),x) -> *#(3(),x) -> *#(3(),x) -> *#(min(),x)
    +#(*(2(),x),x) -> *#(3(),x) -> *#(2(),2()) -> .#(1(),0())
    +#(x,x) -> *#(2(),x) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    +#(x,x) -> *#(2(),x) -> *#(+(y,z),x) -> *#(x,y)
    +#(x,x) -> *#(2(),x) -> *#(+(y,z),x) -> *#(x,z)
    +#(x,x) -> *#(2(),x) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
    +#(x,x) -> *#(2(),x) -> *#(.(x,y),z) -> *#(x,z)
    +#(x,x) -> *#(2(),x) -> *#(.(x,y),z) -> *#(y,z)
    +#(x,x) -> *#(2(),x) -> *#(2(),min()) -> .#(min(),2())
    +#(x,x) -> *#(2(),x) -> *#(3(),x) -> .#(x,*(min(),x))
    +#(x,x) -> *#(2(),x) -> *#(3(),x) -> *#(min(),x)
    +#(x,x) -> *#(2(),x) -> *#(2(),2()) -> .#(1(),0())
    .#(x,min()) -> +#(min(),x) -> +#(*(2(),x),x) -> *#(3(),x)
    .#(x,min()) -> +#(min(),x) -> +#(.(x,y),z) -> .#(x,+(y,z))
    .#(x,min()) -> +#(min(),x) -> +#(.(x,y),z) -> +#(y,z)
    .#(x,min()) -> +#(min(),x) -> +#(3(),x) -> .#(1(),+(min(),x))
    .#(x,min()) -> +#(min(),x) -> +#(3(),x) -> +#(min(),x)
    .#(x,min()) -> +#(min(),x) -> +#(x,x) -> *#(2(),x)
    .#(x,min()) -> .#(+(min(),x),3()) ->
    .#(x,.(y,z)) -> .#(+(x,y),z)
    .#(x,min()) -> .#(+(min(),x),3()) -> .#(x,.(y,z)) -> +#(x,y)
    .#(x,min()) -> .#(+(min(),x),3()) ->
    .#(x,min()) -> .#(+(min(),x),3())
    .#(x,min()) -> .#(+(min(),x),3()) -> .#(x,min()) -> +#(min(),x)
    .#(x,.(y,z)) -> +#(x,y) -> +#(*(2(),x),x) -> *#(3(),x)
    .#(x,.(y,z)) -> +#(x,y) -> +#(.(x,y),z) -> .#(x,+(y,z))
    .#(x,.(y,z)) -> +#(x,y) -> +#(.(x,y),z) -> +#(y,z)
    .#(x,.(y,z)) -> +#(x,y) -> +#(3(),x) -> .#(1(),+(min(),x))
    .#(x,.(y,z)) -> +#(x,y) -> +#(3(),x) -> +#(min(),x)
    .#(x,.(y,z)) -> +#(x,y) -> +#(x,x) -> *#(2(),x)
    .#(x,.(y,z)) -> .#(+(x,y),z) -> .#(x,.(y,z)) -> .#(+(x,y),z)
    .#(x,.(y,z)) -> .#(+(x,y),z) -> .#(x,.(y,z)) -> +#(x,y)
    .#(x,.(y,z)) -> .#(+(x,y),z) -> .#(x,min()) -> .#(+(min(),x),3())
    .#(x,.(y,z)) -> .#(+(x,y),z) -> .#(x,min()) -> +#(min(),x)
    *#(+(y,z),x) -> +#(*(x,y),*(x,z)) ->
    +#(*(2(),x),x) -> *#(3(),x)
    *#(+(y,z),x) -> +#(*(x,y),*(x,z)) ->
    +#(.(x,y),z) -> .#(x,+(y,z))
    *#(+(y,z),x) -> +#(*(x,y),*(x,z)) -> +#(.(x,y),z) -> +#(y,z)
    *#(+(y,z),x) -> +#(*(x,y),*(x,z)) ->
    +#(3(),x) -> .#(1(),+(min(),x))
    *#(+(y,z),x) -> +#(*(x,y),*(x,z)) -> +#(3(),x) -> +#(min(),x)
    *#(+(y,z),x) -> +#(*(x,y),*(x,z)) -> +#(x,x) -> *#(2(),x)
    *#(+(y,z),x) -> *#(x,z) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    *#(+(y,z),x) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,y)
    *#(+(y,z),x) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,z)
    *#(+(y,z),x) -> *#(x,z) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
    *#(+(y,z),x) -> *#(x,z) -> *#(.(x,y),z) -> *#(x,z)
    *#(+(y,z),x) -> *#(x,z) -> *#(.(x,y),z) -> *#(y,z)
    *#(+(y,z),x) -> *#(x,z) -> *#(2(),min()) -> .#(min(),2())
    *#(+(y,z),x) -> *#(x,z) -> *#(3(),x) -> .#(x,*(min(),x))
    *#(+(y,z),x) -> *#(x,z) -> *#(3(),x) -> *#(min(),x)
    *#(+(y,z),x) -> *#(x,z) -> *#(2(),2()) -> .#(1(),0())
    *#(+(y,z),x) -> *#(x,y) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    *#(+(y,z),x) -> *#(x,y) -> *#(+(y,z),x) -> *#(x,y)
    *#(+(y,z),x) -> *#(x,y) -> *#(+(y,z),x) -> *#(x,z)
    *#(+(y,z),x) -> *#(x,y) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
    *#(+(y,z),x) -> *#(x,y) -> *#(.(x,y),z) -> *#(x,z)
    *#(+(y,z),x) -> *#(x,y) -> *#(.(x,y),z) -> *#(y,z)
    *#(+(y,z),x) -> *#(x,y) -> *#(2(),min()) -> .#(min(),2())
    *#(+(y,z),x) -> *#(x,y) -> *#(3(),x) -> .#(x,*(min(),x))
    *#(+(y,z),x) -> *#(x,y) -> *#(3(),x) -> *#(min(),x)
    *#(+(y,z),x) -> *#(x,y) -> *#(2(),2()) -> .#(1(),0())
    *#(3(),x) -> .#(x,*(min(),x)) -> .#(x,.(y,z)) -> .#(+(x,y),z)
    *#(3(),x) -> .#(x,*(min(),x)) -> .#(x,.(y,z)) -> +#(x,y)
    *#(3(),x) -> .#(x,*(min(),x)) -> .#(x,min()) -> .#(+(min(),x),3())
    *#(3(),x) -> .#(x,*(min(),x)) -> .#(x,min()) -> +#(min(),x)
    *#(3(),x) -> *#(min(),x) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    *#(3(),x) -> *#(min(),x) -> *#(+(y,z),x) -> *#(x,y)
    *#(3(),x) -> *#(min(),x) -> *#(+(y,z),x) -> *#(x,z)
    *#(3(),x) -> *#(min(),x) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
    *#(3(),x) -> *#(min(),x) -> *#(.(x,y),z) -> *#(x,z)
    *#(3(),x) -> *#(min(),x) -> *#(.(x,y),z) -> *#(y,z)
    *#(3(),x) -> *#(min(),x) -> *#(2(),min()) -> .#(min(),2())
    *#(3(),x) -> *#(min(),x) -> *#(3(),x) -> .#(x,*(min(),x))
    *#(3(),x) -> *#(min(),x) -> *#(3(),x) -> *#(min(),x)
    *#(3(),x) -> *#(min(),x) -> *#(2(),2()) -> .#(1(),0())
    *#(.(x,y),z) -> .#(*(x,z),*(y,z)) ->
    .#(x,.(y,z)) -> .#(+(x,y),z)
    *#(.(x,y),z) -> .#(*(x,z),*(y,z)) -> .#(x,.(y,z)) -> +#(x,y)
    *#(.(x,y),z) -> .#(*(x,z),*(y,z)) ->
    .#(x,min()) -> .#(+(min(),x),3())
    *#(.(x,y),z) -> .#(*(x,z),*(y,z)) -> .#(x,min()) -> +#(min(),x)
    *#(.(x,y),z) -> *#(y,z) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    *#(.(x,y),z) -> *#(y,z) -> *#(+(y,z),x) -> *#(x,y)
    *#(.(x,y),z) -> *#(y,z) -> *#(+(y,z),x) -> *#(x,z)
    *#(.(x,y),z) -> *#(y,z) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
    *#(.(x,y),z) -> *#(y,z) -> *#(.(x,y),z) -> *#(x,z)
    *#(.(x,y),z) -> *#(y,z) -> *#(.(x,y),z) -> *#(y,z)
    *#(.(x,y),z) -> *#(y,z) -> *#(2(),min()) -> .#(min(),2())
    *#(.(x,y),z) -> *#(y,z) -> *#(3(),x) -> .#(x,*(min(),x))
    *#(.(x,y),z) -> *#(y,z) -> *#(3(),x) -> *#(min(),x)
    *#(.(x,y),z) -> *#(y,z) -> *#(2(),2()) -> .#(1(),0())
    *#(.(x,y),z) -> *#(x,z) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    *#(.(x,y),z) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,y)
    *#(.(x,y),z) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,z)
    *#(.(x,y),z) -> *#(x,z) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
    *#(.(x,y),z) -> *#(x,z) -> *#(.(x,y),z) -> *#(x,z)
    *#(.(x,y),z) -> *#(x,z) -> *#(.(x,y),z) -> *#(y,z)
    *#(.(x,y),z) -> *#(x,z) -> *#(2(),min()) -> .#(min(),2())
    *#(.(x,y),z) -> *#(x,z) -> *#(3(),x) -> .#(x,*(min(),x))
    *#(.(x,y),z) -> *#(x,z) -> *#(3(),x) -> *#(min(),x)
    *#(.(x,y),z) -> *#(x,z) -> *#(2(),2()) -> .#(1(),0())
    *#(2(),min()) -> .#(min(),2()) -> .#(x,.(y,z)) -> .#(+(x,y),z)
    *#(2(),min()) -> .#(min(),2()) -> .#(x,.(y,z)) -> +#(x,y)
    *#(2(),min()) -> .#(min(),2()) ->
    .#(x,min()) -> .#(+(min(),x),3())
    *#(2(),min()) -> .#(min(),2()) -> .#(x,min()) -> +#(min(),x)
    *#(2(),2()) -> .#(1(),0()) -> .#(x,.(y,z)) -> .#(+(x,y),z)
    *#(2(),2()) -> .#(1(),0()) -> .#(x,.(y,z)) -> +#(x,y)
    *#(2(),2()) -> .#(1(),0()) -> .#(x,min()) -> .#(+(min(),x),3())
    *#(2(),2()) -> .#(1(),0()) -> .#(x,min()) -> +#(min(),x)
   EDG Processor:
    DPs:
     *#(2(),2()) -> .#(1(),0())
     *#(3(),x) -> *#(min(),x)
     *#(3(),x) -> .#(x,*(min(),x))
     *#(2(),min()) -> .#(min(),2())
     *#(.(x,y),z) -> *#(y,z)
     *#(.(x,y),z) -> *#(x,z)
     *#(.(x,y),z) -> .#(*(x,z),*(y,z))
     *#(+(y,z),x) -> *#(x,z)
     *#(+(y,z),x) -> *#(x,y)
     *#(+(y,z),x) -> +#(*(x,y),*(x,z))
     +#(x,x) -> *#(2(),x)
     +#(3(),x) -> +#(min(),x)
     +#(3(),x) -> .#(1(),+(min(),x))
     +#(.(x,y),z) -> +#(y,z)
     +#(.(x,y),z) -> .#(x,+(y,z))
     +#(*(2(),x),x) -> *#(3(),x)
     .#(x,min()) -> +#(min(),x)
     .#(x,min()) -> .#(+(min(),x),3())
     .#(x,.(y,z)) -> +#(x,y)
     .#(x,.(y,z)) -> .#(+(x,y),z)
    TRS:
     *(0(),x) -> 0()
     *(1(),x) -> x
     *(2(),2()) -> .(1(),0())
     *(3(),x) -> .(x,*(min(),x))
     *(min(),min()) -> 1()
     *(2(),min()) -> .(min(),2())
     *(.(x,y),z) -> .(*(x,z),*(y,z))
     *(+(y,z),x) -> +(*(x,y),*(x,z))
     +(0(),x) -> x
     +(x,x) -> *(2(),x)
     +(1(),2()) -> 3()
     +(1(),min()) -> 0()
     +(2(),min()) -> 1()
     +(3(),x) -> .(1(),+(min(),x))
     +(.(x,y),z) -> .(x,+(y,z))
     +(*(2(),x),x) -> *(3(),x)
     +(*(min(),x),x) -> 0()
     +(*(2(),v),*(min(),v)) -> v
     .(min(),3()) -> min()
     .(x,min()) -> .(+(min(),x),3())
     .(0(),x) -> x
     .(x,.(y,z)) -> .(+(x,y),z)
    graph:
     +#(3(),x) -> +#(min(),x) -> +#(x,x) -> *#(2(),x)
     +#(3(),x) -> .#(1(),+(min(),x)) -> .#(x,min()) -> +#(min(),x)
     +#(3(),x) -> .#(1(),+(min(),x)) ->
     .#(x,min()) -> .#(+(min(),x),3())
     +#(3(),x) -> .#(1(),+(min(),x)) -> .#(x,.(y,z)) -> +#(x,y)
     +#(3(),x) -> .#(1(),+(min(),x)) -> .#(x,.(y,z)) -> .#(+(x,y),z)
     +#(.(x,y),z) -> +#(y,z) -> +#(x,x) -> *#(2(),x)
     +#(.(x,y),z) -> +#(y,z) -> +#(3(),x) -> +#(min(),x)
     +#(.(x,y),z) -> +#(y,z) -> +#(3(),x) -> .#(1(),+(min(),x))
     +#(.(x,y),z) -> +#(y,z) -> +#(.(x,y),z) -> +#(y,z)
     +#(.(x,y),z) -> +#(y,z) -> +#(.(x,y),z) -> .#(x,+(y,z))
     +#(.(x,y),z) -> +#(y,z) -> +#(*(2(),x),x) -> *#(3(),x)
     +#(.(x,y),z) -> .#(x,+(y,z)) -> .#(x,min()) -> +#(min(),x)
     +#(.(x,y),z) -> .#(x,+(y,z)) -> .#(x,min()) -> .#(+(min(),x),3())
     +#(.(x,y),z) -> .#(x,+(y,z)) -> .#(x,.(y,z)) -> +#(x,y)
     +#(.(x,y),z) -> .#(x,+(y,z)) -> .#(x,.(y,z)) -> .#(+(x,y),z)
     +#(*(2(),x),x) -> *#(3(),x) -> *#(3(),x) -> *#(min(),x)
     +#(*(2(),x),x) -> *#(3(),x) -> *#(3(),x) -> .#(x,*(min(),x))
     +#(x,x) -> *#(2(),x) -> *#(2(),2()) -> .#(1(),0())
     +#(x,x) -> *#(2(),x) -> *#(2(),min()) -> .#(min(),2())
     .#(x,min()) -> +#(min(),x) -> +#(x,x) -> *#(2(),x)
     .#(x,.(y,z)) -> +#(x,y) -> +#(x,x) -> *#(2(),x)
     .#(x,.(y,z)) -> +#(x,y) -> +#(3(),x) -> +#(min(),x)
     .#(x,.(y,z)) -> +#(x,y) -> +#(3(),x) -> .#(1(),+(min(),x))
     .#(x,.(y,z)) -> +#(x,y) -> +#(.(x,y),z) -> +#(y,z)
     .#(x,.(y,z)) -> +#(x,y) -> +#(.(x,y),z) -> .#(x,+(y,z))
     .#(x,.(y,z)) -> +#(x,y) -> +#(*(2(),x),x) -> *#(3(),x)
     .#(x,.(y,z)) -> .#(+(x,y),z) -> .#(x,min()) -> +#(min(),x)
     .#(x,.(y,z)) -> .#(+(x,y),z) -> .#(x,min()) -> .#(+(min(),x),3())
     .#(x,.(y,z)) -> .#(+(x,y),z) -> .#(x,.(y,z)) -> +#(x,y)
     .#(x,.(y,z)) -> .#(+(x,y),z) -> .#(x,.(y,z)) -> .#(+(x,y),z)
     *#(+(y,z),x) -> +#(*(x,y),*(x,z)) -> +#(x,x) -> *#(2(),x)
     *#(+(y,z),x) -> +#(*(x,y),*(x,z)) -> +#(3(),x) -> +#(min(),x)
     *#(+(y,z),x) -> +#(*(x,y),*(x,z)) ->
     +#(3(),x) -> .#(1(),+(min(),x))
     *#(+(y,z),x) -> +#(*(x,y),*(x,z)) -> +#(.(x,y),z) -> +#(y,z)
     *#(+(y,z),x) -> +#(*(x,y),*(x,z)) ->
     +#(.(x,y),z) -> .#(x,+(y,z))
     *#(+(y,z),x) -> +#(*(x,y),*(x,z)) -> +#(*(2(),x),x) -> *#(3(),x)
     *#(+(y,z),x) -> *#(x,z) -> *#(2(),2()) -> .#(1(),0())
     *#(+(y,z),x) -> *#(x,z) -> *#(3(),x) -> *#(min(),x)
     *#(+(y,z),x) -> *#(x,z) -> *#(3(),x) -> .#(x,*(min(),x))
     *#(+(y,z),x) -> *#(x,z) -> *#(2(),min()) -> .#(min(),2())
     *#(+(y,z),x) -> *#(x,z) -> *#(.(x,y),z) -> *#(y,z)
     *#(+(y,z),x) -> *#(x,z) -> *#(.(x,y),z) -> *#(x,z)
     *#(+(y,z),x) -> *#(x,z) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
     *#(+(y,z),x) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,z)
     *#(+(y,z),x) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,y)
     *#(+(y,z),x) -> *#(x,z) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
     *#(+(y,z),x) -> *#(x,y) -> *#(2(),2()) -> .#(1(),0())
     *#(+(y,z),x) -> *#(x,y) -> *#(3(),x) -> *#(min(),x)
     *#(+(y,z),x) -> *#(x,y) -> *#(3(),x) -> .#(x,*(min(),x))
     *#(+(y,z),x) -> *#(x,y) -> *#(2(),min()) -> .#(min(),2())
     *#(+(y,z),x) -> *#(x,y) -> *#(.(x,y),z) -> *#(y,z)
     *#(+(y,z),x) -> *#(x,y) -> *#(.(x,y),z) -> *#(x,z)
     *#(+(y,z),x) -> *#(x,y) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
     *#(+(y,z),x) -> *#(x,y) -> *#(+(y,z),x) -> *#(x,z)
     *#(+(y,z),x) -> *#(x,y) -> *#(+(y,z),x) -> *#(x,y)
     *#(+(y,z),x) -> *#(x,y) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
     *#(3(),x) -> .#(x,*(min(),x)) -> .#(x,min()) -> +#(min(),x)
     *#(3(),x) -> .#(x,*(min(),x)) ->
     .#(x,min()) -> .#(+(min(),x),3())
     *#(3(),x) -> .#(x,*(min(),x)) -> .#(x,.(y,z)) -> +#(x,y)
     *#(3(),x) -> .#(x,*(min(),x)) -> .#(x,.(y,z)) -> .#(+(x,y),z)
     *#(.(x,y),z) -> .#(*(x,z),*(y,z)) ->
     .#(x,min()) -> +#(min(),x)
     *#(.(x,y),z) -> .#(*(x,z),*(y,z)) ->
     .#(x,min()) -> .#(+(min(),x),3())
     *#(.(x,y),z) -> .#(*(x,z),*(y,z)) -> .#(x,.(y,z)) -> +#(x,y)
     *#(.(x,y),z) -> .#(*(x,z),*(y,z)) -> .#(x,.(y,z)) -> .#(+(x,y),z)
     *#(.(x,y),z) -> *#(y,z) -> *#(2(),2()) -> .#(1(),0())
     *#(.(x,y),z) -> *#(y,z) -> *#(3(),x) -> *#(min(),x)
     *#(.(x,y),z) -> *#(y,z) -> *#(3(),x) -> .#(x,*(min(),x))
     *#(.(x,y),z) -> *#(y,z) -> *#(2(),min()) -> .#(min(),2())
     *#(.(x,y),z) -> *#(y,z) -> *#(.(x,y),z) -> *#(y,z)
     *#(.(x,y),z) -> *#(y,z) -> *#(.(x,y),z) -> *#(x,z)
     *#(.(x,y),z) -> *#(y,z) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
     *#(.(x,y),z) -> *#(y,z) -> *#(+(y,z),x) -> *#(x,z)
     *#(.(x,y),z) -> *#(y,z) -> *#(+(y,z),x) -> *#(x,y)
     *#(.(x,y),z) -> *#(y,z) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
     *#(.(x,y),z) -> *#(x,z) -> *#(2(),2()) -> .#(1(),0())
     *#(.(x,y),z) -> *#(x,z) -> *#(3(),x) -> *#(min(),x)
     *#(.(x,y),z) -> *#(x,z) -> *#(3(),x) -> .#(x,*(min(),x))
     *#(.(x,y),z) -> *#(x,z) -> *#(2(),min()) -> .#(min(),2())
     *#(.(x,y),z) -> *#(x,z) -> *#(.(x,y),z) -> *#(y,z)
     *#(.(x,y),z) -> *#(x,z) -> *#(.(x,y),z) -> *#(x,z)
     *#(.(x,y),z) -> *#(x,z) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
     *#(.(x,y),z) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,z)
     *#(.(x,y),z) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,y)
     *#(.(x,y),z) -> *#(x,z) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    CDG Processor:
     DPs:
      *#(2(),2()) -> .#(1(),0())
      *#(3(),x) -> *#(min(),x)
      *#(3(),x) -> .#(x,*(min(),x))
      *#(2(),min()) -> .#(min(),2())
      *#(.(x,y),z) -> *#(y,z)
      *#(.(x,y),z) -> *#(x,z)
      *#(.(x,y),z) -> .#(*(x,z),*(y,z))
      *#(+(y,z),x) -> *#(x,z)
      *#(+(y,z),x) -> *#(x,y)
      *#(+(y,z),x) -> +#(*(x,y),*(x,z))
      +#(x,x) -> *#(2(),x)
      +#(3(),x) -> +#(min(),x)
      +#(3(),x) -> .#(1(),+(min(),x))
      +#(.(x,y),z) -> +#(y,z)
      +#(.(x,y),z) -> .#(x,+(y,z))
      +#(*(2(),x),x) -> *#(3(),x)
      .#(x,min()) -> +#(min(),x)
      .#(x,min()) -> .#(+(min(),x),3())
      .#(x,.(y,z)) -> +#(x,y)
      .#(x,.(y,z)) -> .#(+(x,y),z)
     TRS:
      *(0(),x) -> 0()
      *(1(),x) -> x
      *(2(),2()) -> .(1(),0())
      *(3(),x) -> .(x,*(min(),x))
      *(min(),min()) -> 1()
      *(2(),min()) -> .(min(),2())
      *(.(x,y),z) -> .(*(x,z),*(y,z))
      *(+(y,z),x) -> +(*(x,y),*(x,z))
      +(0(),x) -> x
      +(x,x) -> *(2(),x)
      +(1(),2()) -> 3()
      +(1(),min()) -> 0()
      +(2(),min()) -> 1()
      +(3(),x) -> .(1(),+(min(),x))
      +(.(x,y),z) -> .(x,+(y,z))
      +(*(2(),x),x) -> *(3(),x)
      +(*(min(),x),x) -> 0()
      +(*(2(),v),*(min(),v)) -> v
      .(min(),3()) -> min()
      .(x,min()) -> .(+(min(),x),3())
      .(0(),x) -> x
      .(x,.(y,z)) -> .(+(x,y),z)
     graph:
      +#(3(),x) -> +#(min(),x) -> +#(x,x) -> *#(2(),x)
      +#(3(),x) -> .#(1(),+(min(),x)) ->
      .#(x,.(y,z)) -> .#(+(x,y),z)
      +#(3(),x) -> .#(1(),+(min(),x)) -> .#(x,.(y,z)) -> +#(x,y)
      +#(3(),x) -> .#(1(),+(min(),x)) ->
      .#(x,min()) -> .#(+(min(),x),3())
      +#(3(),x) -> .#(1(),+(min(),x)) -> .#(x,min()) -> +#(min(),x)
      +#(.(x,y),z) -> +#(y,z) -> +#(*(2(),x),x) -> *#(3(),x)
      +#(.(x,y),z) -> +#(y,z) -> +#(.(x,y),z) -> .#(x,+(y,z))
      +#(.(x,y),z) -> +#(y,z) -> +#(.(x,y),z) -> +#(y,z)
      +#(.(x,y),z) -> +#(y,z) -> +#(3(),x) -> .#(1(),+(min(),x))
      +#(.(x,y),z) -> +#(y,z) -> +#(3(),x) -> +#(min(),x)
      +#(.(x,y),z) -> +#(y,z) -> +#(x,x) -> *#(2(),x)
      +#(.(x,y),z) -> .#(x,+(y,z)) -> .#(x,.(y,z)) -> .#(+(x,y),z)
      +#(.(x,y),z) -> .#(x,+(y,z)) -> .#(x,.(y,z)) -> +#(x,y)
      +#(.(x,y),z) -> .#(x,+(y,z)) -> .#(x,min()) -> .#(+(min(),x),3())
      +#(.(x,y),z) -> .#(x,+(y,z)) -> .#(x,min()) -> +#(min(),x)
      +#(*(2(),x),x) -> *#(3(),x) -> *#(3(),x) -> .#(x,*(min(),x))
      +#(*(2(),x),x) -> *#(3(),x) -> *#(3(),x) -> *#(min(),x)
      +#(x,x) -> *#(2(),x) -> *#(2(),min()) -> .#(min(),2())
      +#(x,x) -> *#(2(),x) -> *#(2(),2()) -> .#(1(),0())
      .#(x,min()) -> +#(min(),x) -> +#(x,x) -> *#(2(),x)
      .#(x,.(y,z)) -> +#(x,y) -> +#(*(2(),x),x) -> *#(3(),x)
      .#(x,.(y,z)) -> +#(x,y) -> +#(.(x,y),z) -> .#(x,+(y,z))
      .#(x,.(y,z)) -> +#(x,y) -> +#(.(x,y),z) -> +#(y,z)
      .#(x,.(y,z)) -> +#(x,y) -> +#(3(),x) -> .#(1(),+(min(),x))
      .#(x,.(y,z)) -> +#(x,y) -> +#(3(),x) -> +#(min(),x)
      .#(x,.(y,z)) -> +#(x,y) -> +#(x,x) -> *#(2(),x)
      .#(x,.(y,z)) -> .#(+(x,y),z) -> .#(x,.(y,z)) -> .#(+(x,y),z)
      .#(x,.(y,z)) -> .#(+(x,y),z) -> .#(x,.(y,z)) -> +#(x,y)
      .#(x,.(y,z)) -> .#(+(x,y),z) -> .#(x,min()) -> .#(+(min(),x),3())
      .#(x,.(y,z)) -> .#(+(x,y),z) -> .#(x,min()) -> +#(min(),x)
      *#(+(y,z),x) -> +#(*(x,y),*(x,z)) ->
      +#(*(2(),x),x) -> *#(3(),x)
      *#(+(y,z),x) -> +#(*(x,y),*(x,z)) ->
      +#(.(x,y),z) -> .#(x,+(y,z))
      *#(+(y,z),x) -> +#(*(x,y),*(x,z)) -> +#(.(x,y),z) -> +#(y,z)
      *#(+(y,z),x) -> +#(*(x,y),*(x,z)) ->
      +#(3(),x) -> .#(1(),+(min(),x))
      *#(+(y,z),x) -> +#(*(x,y),*(x,z)) ->
      +#(3(),x) -> +#(min(),x)
      *#(+(y,z),x) -> +#(*(x,y),*(x,z)) -> +#(x,x) -> *#(2(),x)
      *#(+(y,z),x) -> *#(x,z) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
      *#(+(y,z),x) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,y)
      *#(+(y,z),x) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,z)
      *#(+(y,z),x) -> *#(x,z) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
      *#(+(y,z),x) -> *#(x,z) -> *#(.(x,y),z) -> *#(x,z)
      *#(+(y,z),x) -> *#(x,z) -> *#(.(x,y),z) -> *#(y,z)
      *#(+(y,z),x) -> *#(x,z) -> *#(2(),min()) -> .#(min(),2())
      *#(+(y,z),x) -> *#(x,z) -> *#(3(),x) -> .#(x,*(min(),x))
      *#(+(y,z),x) -> *#(x,z) -> *#(3(),x) -> *#(min(),x)
      *#(+(y,z),x) -> *#(x,z) -> *#(2(),2()) -> .#(1(),0())
      *#(+(y,z),x) -> *#(x,y) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
      *#(+(y,z),x) -> *#(x,y) -> *#(+(y,z),x) -> *#(x,y)
      *#(+(y,z),x) -> *#(x,y) -> *#(+(y,z),x) -> *#(x,z)
      *#(+(y,z),x) -> *#(x,y) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
      *#(+(y,z),x) -> *#(x,y) -> *#(.(x,y),z) -> *#(x,z)
      *#(+(y,z),x) -> *#(x,y) -> *#(.(x,y),z) -> *#(y,z)
      *#(+(y,z),x) -> *#(x,y) -> *#(2(),min()) -> .#(min(),2())
      *#(+(y,z),x) -> *#(x,y) -> *#(3(),x) -> .#(x,*(min(),x))
      *#(+(y,z),x) -> *#(x,y) -> *#(3(),x) -> *#(min(),x)
      *#(+(y,z),x) -> *#(x,y) -> *#(2(),2()) -> .#(1(),0())
      *#(.(x,y),z) -> .#(*(x,z),*(y,z)) ->
      .#(x,.(y,z)) -> .#(+(x,y),z)
      *#(.(x,y),z) -> .#(*(x,z),*(y,z)) -> .#(x,.(y,z)) -> +#(x,y)
      *#(.(x,y),z) -> .#(*(x,z),*(y,z)) ->
      .#(x,min()) -> .#(+(min(),x),3())
      *#(.(x,y),z) -> .#(*(x,z),*(y,z)) -> .#(x,min()) -> +#(min(),x)
      *#(.(x,y),z) -> *#(y,z) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
      *#(.(x,y),z) -> *#(y,z) -> *#(+(y,z),x) -> *#(x,y)
      *#(.(x,y),z) -> *#(y,z) -> *#(+(y,z),x) -> *#(x,z)
      *#(.(x,y),z) -> *#(y,z) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
      *#(.(x,y),z) -> *#(y,z) -> *#(.(x,y),z) -> *#(x,z)
      *#(.(x,y),z) -> *#(y,z) -> *#(.(x,y),z) -> *#(y,z)
      *#(.(x,y),z) -> *#(y,z) -> *#(2(),min()) -> .#(min(),2())
      *#(.(x,y),z) -> *#(y,z) -> *#(3(),x) -> .#(x,*(min(),x))
      *#(.(x,y),z) -> *#(y,z) -> *#(3(),x) -> *#(min(),x)
      *#(.(x,y),z) -> *#(y,z) -> *#(2(),2()) -> .#(1(),0())
      *#(.(x,y),z) -> *#(x,z) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
      *#(.(x,y),z) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,y)
      *#(.(x,y),z) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,z)
      *#(.(x,y),z) -> *#(x,z) -> *#(.(x,y),z) -> .#(*(x,z),*(y,z))
      *#(.(x,y),z) -> *#(x,z) -> *#(.(x,y),z) -> *#(x,z)
      *#(.(x,y),z) -> *#(x,z) -> *#(.(x,y),z) -> *#(y,z)
      *#(.(x,y),z) -> *#(x,z) -> *#(2(),min()) -> .#(min(),2())
      *#(.(x,y),z) -> *#(x,z) -> *#(3(),x) -> .#(x,*(min(),x))
      *#(.(x,y),z) -> *#(x,z) -> *#(3(),x) -> *#(min(),x)
      *#(.(x,y),z) -> *#(x,z) -> *#(2(),2()) -> .#(1(),0())
     SCC Processor:
      #sccs: 2
      #rules: 9
      #arcs: 80/400
      DPs:
       *#(+(y,z),x) -> *#(x,z)
       *#(.(x,y),z) -> *#(y,z)
       *#(.(x,y),z) -> *#(x,z)
       *#(+(y,z),x) -> *#(x,y)
      TRS:
       *(0(),x) -> 0()
       *(1(),x) -> x
       *(2(),2()) -> .(1(),0())
       *(3(),x) -> .(x,*(min(),x))
       *(min(),min()) -> 1()
       *(2(),min()) -> .(min(),2())
       *(.(x,y),z) -> .(*(x,z),*(y,z))
       *(+(y,z),x) -> +(*(x,y),*(x,z))
       +(0(),x) -> x
       +(x,x) -> *(2(),x)
       +(1(),2()) -> 3()
       +(1(),min()) -> 0()
       +(2(),min()) -> 1()
       +(3(),x) -> .(1(),+(min(),x))
       +(.(x,y),z) -> .(x,+(y,z))
       +(*(2(),x),x) -> *(3(),x)
       +(*(min(),x),x) -> 0()
       +(*(2(),v),*(min(),v)) -> v
       .(min(),3()) -> min()
       .(x,min()) -> .(+(min(),x),3())
       .(0(),x) -> x
       .(x,.(y,z)) -> .(+(x,y),z)
      Open
      
      DPs:
       +#(3(),x) -> .#(1(),+(min(),x))
       .#(x,.(y,z)) -> +#(x,y)
       +#(.(x,y),z) -> +#(y,z)
       +#(.(x,y),z) -> .#(x,+(y,z))
       .#(x,.(y,z)) -> .#(+(x,y),z)
      TRS:
       *(0(),x) -> 0()
       *(1(),x) -> x
       *(2(),2()) -> .(1(),0())
       *(3(),x) -> .(x,*(min(),x))
       *(min(),min()) -> 1()
       *(2(),min()) -> .(min(),2())
       *(.(x,y),z) -> .(*(x,z),*(y,z))
       *(+(y,z),x) -> +(*(x,y),*(x,z))
       +(0(),x) -> x
       +(x,x) -> *(2(),x)
       +(1(),2()) -> 3()
       +(1(),min()) -> 0()
       +(2(),min()) -> 1()
       +(3(),x) -> .(1(),+(min(),x))
       +(.(x,y),z) -> .(x,+(y,z))
       +(*(2(),x),x) -> *(3(),x)
       +(*(min(),x),x) -> 0()
       +(*(2(),v),*(min(),v)) -> v
       .(min(),3()) -> min()
       .(x,min()) -> .(+(min(),x),3())
       .(0(),x) -> x
       .(x,.(y,z)) -> .(+(x,y),z)
      Open