MAYBE
Time: 0.011843
TRS:
 {                *(0(), x) -> 0(),
                  *(1(), x) -> x,
              *(.(x, y), z) -> .(*(x, z), *(y, z)),
                *(2(), 2()) -> .(1(), 0()),
              *(2(), min()) -> .(min(), 2()),
            *(min(), min()) -> 1(),
                  *(3(), x) -> .(x, *(min(), x)),
              *(+(y, z), x) -> +(*(x, y), *(x, z)),
              .(x, .(y, z)) -> .(+(x, y), z),
                .(x, min()) -> .(+(min(), x), 3()),
                  .(0(), x) -> x,
              .(min(), 3()) -> min(),
                    +(x, x) -> *(2(), x),
                  +(0(), x) -> x,
            +(*(2(), x), x) -> *(3(), x),
  +(*(2(), v), *(min(), v)) -> v,
          +(*(min(), x), x) -> 0(),
                +(1(), 2()) -> 3(),
              +(1(), min()) -> 0(),
              +(.(x, y), z) -> .(x, +(y, z)),
              +(2(), min()) -> 1(),
                  +(3(), x) -> .(1(), +(min(), x))}
 DP:
  DP:
   {  *#(.(x, y), z) -> *#(x, z),
      *#(.(x, y), z) -> *#(y, z),
      *#(.(x, y), z) -> .#(*(x, z), *(y, z)),
        *#(2(), 2()) -> .#(1(), 0()),
      *#(2(), min()) -> .#(min(), 2()),
          *#(3(), x) -> *#(min(), x),
          *#(3(), x) -> .#(x, *(min(), x)),
      *#(+(y, z), x) -> *#(x, z),
      *#(+(y, z), x) -> *#(x, y),
      *#(+(y, z), x) -> +#(*(x, y), *(x, z)),
      .#(x, .(y, z)) -> .#(+(x, y), z),
      .#(x, .(y, z)) -> +#(x, y),
        .#(x, min()) -> .#(+(min(), x), 3()),
        .#(x, min()) -> +#(min(), x),
            +#(x, x) -> *#(2(), x),
    +#(*(2(), x), x) -> *#(3(), x),
      +#(.(x, y), z) -> .#(x, +(y, z)),
      +#(.(x, y), z) -> +#(y, z),
          +#(3(), x) -> .#(1(), +(min(), x)),
          +#(3(), x) -> +#(min(), x)}
  TRS:
  {                *(0(), x) -> 0(),
                   *(1(), x) -> x,
               *(.(x, y), z) -> .(*(x, z), *(y, z)),
                 *(2(), 2()) -> .(1(), 0()),
               *(2(), min()) -> .(min(), 2()),
             *(min(), min()) -> 1(),
                   *(3(), x) -> .(x, *(min(), x)),
               *(+(y, z), x) -> +(*(x, y), *(x, z)),
               .(x, .(y, z)) -> .(+(x, y), z),
                 .(x, min()) -> .(+(min(), x), 3()),
                   .(0(), x) -> x,
               .(min(), 3()) -> min(),
                     +(x, x) -> *(2(), x),
                   +(0(), x) -> x,
             +(*(2(), x), x) -> *(3(), x),
   +(*(2(), v), *(min(), v)) -> v,
           +(*(min(), x), x) -> 0(),
                 +(1(), 2()) -> 3(),
               +(1(), min()) -> 0(),
               +(.(x, y), z) -> .(x, +(y, z)),
               +(2(), min()) -> 1(),
                   +(3(), x) -> .(1(), +(min(), x))}
  EDG:
   {(.#(x, min()) -> +#(min(), x), +#(x, x) -> *#(2(), x))
    (+#(*(2(), x), x) -> *#(3(), x), *#(3(), x) -> .#(x, *(min(), x)))
    (+#(*(2(), x), x) -> *#(3(), x), *#(3(), x) -> *#(min(), 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))
    (*#(.(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))
    (*#(+(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, y), *(x, z)), +#(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)) -> +#(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), +#(x, x) -> *#(2(), 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), *#(3(), x) -> .#(x, *(min(), x)))
    (*#(.(x, y), z) -> *#(y, z), *#(3(), x) -> *#(min(), x))
    (*#(.(x, y), z) -> *#(y, z), *#(2(), min()) -> .#(min(), 2()))
    (*#(.(x, y), z) -> *#(y, z), *#(2(), 2()) -> .#(1(), 0()))
    (*#(.(x, y), z) -> *#(y, z), *#(.(x, y), z) -> .#(*(x, z), *(y, z)))
    (*#(.(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), +#(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) -> +#(y, z), +#(x, x) -> *#(2(), x))
    (*#(+(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), *#(.(x, y), z) -> .#(*(x, z), *(y, z)))
    (*#(+(y, z), x) -> *#(x, z), *#(2(), 2()) -> .#(1(), 0()))
    (*#(+(y, z), x) -> *#(x, z), *#(2(), min()) -> .#(min(), 2()))
    (*#(+(y, z), x) -> *#(x, z), *#(3(), x) -> *#(min(), x))
    (*#(+(y, z), x) -> *#(x, z), *#(3(), x) -> .#(x, *(min(), x)))
    (*#(+(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)))
    (*#(.(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), *#(.(x, y), z) -> .#(*(x, z), *(y, z)))
    (*#(.(x, y), z) -> *#(x, z), *#(2(), 2()) -> .#(1(), 0()))
    (*#(.(x, y), z) -> *#(x, z), *#(2(), min()) -> .#(min(), 2()))
    (*#(.(x, y), z) -> *#(x, z), *#(3(), x) -> *#(min(), x))
    (*#(.(x, y), z) -> *#(x, z), *#(3(), x) -> .#(x, *(min(), x)))
    (*#(.(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)))
    (*#(+(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), *#(.(x, y), z) -> .#(*(x, z), *(y, z)))
    (*#(+(y, z), x) -> *#(x, y), *#(2(), 2()) -> .#(1(), 0()))
    (*#(+(y, z), x) -> *#(x, y), *#(2(), min()) -> .#(min(), 2()))
    (*#(+(y, z), x) -> *#(x, y), *#(3(), x) -> *#(min(), x))
    (*#(+(y, z), x) -> *#(x, y), *#(3(), x) -> .#(x, *(min(), x)))
    (*#(+(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)))
    (+#(.(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))
    (*#(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), +#(x, x) -> *#(2(), x))
    (+#(x, x) -> *#(2(), x), *#(2(), 2()) -> .#(1(), 0()))
    (+#(x, x) -> *#(2(), x), *#(2(), min()) -> .#(min(), 2()))}
   STATUS:
    arrows: 0.790000
    SCCS (2):
     Scc:
      {*#(.(x, y), z) -> *#(x, z),
       *#(.(x, y), z) -> *#(y, z),
       *#(+(y, z), x) -> *#(x, z),
       *#(+(y, z), x) -> *#(x, y)}
     Scc:
      {      *#(3(), x) -> .#(x, *(min(), x)),
         .#(x, .(y, z)) -> .#(+(x, y), z),
         .#(x, .(y, z)) -> +#(x, y),
       +#(*(2(), x), x) -> *#(3(), x),
         +#(.(x, y), z) -> .#(x, +(y, z)),
         +#(.(x, y), z) -> +#(y, z),
             +#(3(), x) -> .#(1(), +(min(), x))}
     
     SCC (4):
      Strict:
       {*#(.(x, y), z) -> *#(x, z),
        *#(.(x, y), z) -> *#(y, z),
        *#(+(y, z), x) -> *#(x, z),
        *#(+(y, z), x) -> *#(x, y)}
      Weak:
      {                *(0(), x) -> 0(),
                       *(1(), x) -> x,
                   *(.(x, y), z) -> .(*(x, z), *(y, z)),
                     *(2(), 2()) -> .(1(), 0()),
                   *(2(), min()) -> .(min(), 2()),
                 *(min(), min()) -> 1(),
                       *(3(), x) -> .(x, *(min(), x)),
                   *(+(y, z), x) -> +(*(x, y), *(x, z)),
                   .(x, .(y, z)) -> .(+(x, y), z),
                     .(x, min()) -> .(+(min(), x), 3()),
                       .(0(), x) -> x,
                   .(min(), 3()) -> min(),
                         +(x, x) -> *(2(), x),
                       +(0(), x) -> x,
                 +(*(2(), x), x) -> *(3(), x),
       +(*(2(), v), *(min(), v)) -> v,
               +(*(min(), x), x) -> 0(),
                     +(1(), 2()) -> 3(),
                   +(1(), min()) -> 0(),
                   +(.(x, y), z) -> .(x, +(y, z)),
                   +(2(), min()) -> 1(),
                       +(3(), x) -> .(1(), +(min(), x))}
      Open
     
     
     SCC (7):
      Strict:
       {      *#(3(), x) -> .#(x, *(min(), x)),
          .#(x, .(y, z)) -> .#(+(x, y), z),
          .#(x, .(y, z)) -> +#(x, y),
        +#(*(2(), x), x) -> *#(3(), x),
          +#(.(x, y), z) -> .#(x, +(y, z)),
          +#(.(x, y), z) -> +#(y, z),
              +#(3(), x) -> .#(1(), +(min(), x))}
      Weak:
      {                *(0(), x) -> 0(),
                       *(1(), x) -> x,
                   *(.(x, y), z) -> .(*(x, z), *(y, z)),
                     *(2(), 2()) -> .(1(), 0()),
                   *(2(), min()) -> .(min(), 2()),
                 *(min(), min()) -> 1(),
                       *(3(), x) -> .(x, *(min(), x)),
                   *(+(y, z), x) -> +(*(x, y), *(x, z)),
                   .(x, .(y, z)) -> .(+(x, y), z),
                     .(x, min()) -> .(+(min(), x), 3()),
                       .(0(), x) -> x,
                   .(min(), 3()) -> min(),
                         +(x, x) -> *(2(), x),
                       +(0(), x) -> x,
                 +(*(2(), x), x) -> *(3(), x),
       +(*(2(), v), *(min(), v)) -> v,
               +(*(min(), x), x) -> 0(),
                     +(1(), 2()) -> 3(),
                   +(1(), min()) -> 0(),
                   +(.(x, y), z) -> .(x, +(y, z)),
                   +(2(), min()) -> 1(),
                       +(3(), x) -> .(1(), +(min(), x))}
      Open