MAYBE
Time: 0.009589
TRS:
 {              s h() -> 1(),
    a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
    a(l, x, s y, h()) -> a(l, x, y, s h()),
    a(l, s x, h(), z) -> a(l, x, z, z),
  a(s l, h(), h(), z) -> a(l, z, h(), z),
  a(h(), h(), h(), x) -> s x,
            +(x, h()) -> x,
          +(s x, s y) -> s s +(x, y),
            +(h(), x) -> x,
        +(+(x, y), z) -> +(x, +(y, z)),
            *(x, h()) -> h(),
          *(s x, s y) -> s +(+(*(x, y), x), y),
            *(h(), x) -> h()}
 DP:
  DP:
   {  a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)),
      a#(l, x, s y, s z) -> a#(l, x, s y, z),
      a#(l, x, s y, h()) -> s# h(),
      a#(l, x, s y, h()) -> a#(l, x, y, s h()),
      a#(l, s x, h(), z) -> a#(l, x, z, z),
    a#(s l, h(), h(), z) -> a#(l, z, h(), z),
    a#(h(), h(), h(), x) -> s# x,
            +#(s x, s y) -> s# s +(x, y),
            +#(s x, s y) -> s# +(x, y),
            +#(s x, s y) -> +#(x, y),
          +#(+(x, y), z) -> +#(x, +(y, z)),
          +#(+(x, y), z) -> +#(y, z),
            *#(s x, s y) -> s# +(+(*(x, y), x), y),
            *#(s x, s y) -> +#(+(*(x, y), x), y),
            *#(s x, s y) -> +#(*(x, y), x),
            *#(s x, s y) -> *#(x, y)}
  TRS:
  {              s h() -> 1(),
     a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
     a(l, x, s y, h()) -> a(l, x, y, s h()),
     a(l, s x, h(), z) -> a(l, x, z, z),
   a(s l, h(), h(), z) -> a(l, z, h(), z),
   a(h(), h(), h(), x) -> s x,
             +(x, h()) -> x,
           +(s x, s y) -> s s +(x, y),
             +(h(), x) -> x,
         +(+(x, y), z) -> +(x, +(y, z)),
             *(x, h()) -> h(),
           *(s x, s y) -> s +(+(*(x, y), x), y),
             *(h(), x) -> h()}
  UR:
   {              s h() -> 1(),
      a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
      a(l, x, s y, h()) -> a(l, x, y, s h()),
      a(l, s x, h(), z) -> a(l, x, z, z),
    a(s l, h(), h(), z) -> a(l, z, h(), z),
    a(h(), h(), h(), x) -> s x,
              +(x, h()) -> x,
            +(s x, s y) -> s s +(x, y),
              +(h(), x) -> x,
          +(+(x, y), z) -> +(x, +(y, z)),
              *(x, h()) -> h(),
            *(s x, s y) -> s +(+(*(x, y), x), y),
              *(h(), x) -> h(),
                b(w, v) -> w,
                b(w, v) -> v}
   EDG:
    {(a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(h(), h(), h(), x) -> s# x)
     (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(s l, h(), h(), z) -> a#(l, z, h(), z))
     (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, s x, h(), z) -> a#(l, x, z, z))
     (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, s z) -> a#(l, x, s y, z))
     (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)))
     (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> a#(l, x, y, s h()))
     (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> s# h())
     (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, s z) -> a#(l, x, s y, z))
     (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)))
     (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(h(), h(), h(), x) -> s# x)
     (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(s l, h(), h(), z) -> a#(l, z, h(), z))
     (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(l, s x, h(), z) -> a#(l, x, z, z))
     (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(h(), h(), h(), x) -> s# x)
     (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(s l, h(), h(), z) -> a#(l, z, h(), z))
     (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, s x, h(), z) -> a#(l, x, z, z))
     (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z))
     (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)))
     (*#(s x, s y) -> +#(*(x, y), x), +#(s x, s y) -> +#(x, y))
     (*#(s x, s y) -> +#(*(x, y), x), +#(s x, s y) -> s# +(x, y))
     (*#(s x, s y) -> +#(*(x, y), x), +#(s x, s y) -> s# s +(x, y))
     (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> *#(x, y))
     (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> +#(*(x, y), x))
     (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> +#(+(*(x, y), x), y))
     (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> s# +(+(*(x, y), x), y))
     (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> s# s +(x, y))
     (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> s# +(x, y))
     (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y))
     (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> s# s +(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> s# +(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
     (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> s# s +(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> s# +(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)))
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, s z) -> a#(l, x, s y, z))
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, h()) -> s# h())
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, h()) -> a#(l, x, y, s h()))
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, s x, h(), z) -> a#(l, x, z, z))
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(s l, h(), h(), z) -> a#(l, z, h(), z))
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(h(), h(), h(), x) -> s# x)
     (*#(s x, s y) -> +#(+(*(x, y), x), y), +#(s x, s y) -> s# s +(x, y))
     (*#(s x, s y) -> +#(+(*(x, y), x), y), +#(s x, s y) -> s# +(x, y))
     (*#(s x, s y) -> +#(+(*(x, y), x), y), +#(s x, s y) -> +#(x, y))
     (*#(s x, s y) -> +#(+(*(x, y), x), y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (*#(s x, s y) -> +#(+(*(x, y), x), y), +#(+(x, y), z) -> +#(y, z))}
    STATUS:
     arrows: 0.800781
     SCCS (3):
      Scc:
       {*#(s x, s y) -> *#(x, y)}
      Scc:
       {  a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)),
          a#(l, x, s y, s z) -> a#(l, x, s y, z),
          a#(l, x, s y, h()) -> a#(l, x, y, s h()),
          a#(l, s x, h(), z) -> a#(l, x, z, z),
        a#(s l, h(), h(), z) -> a#(l, z, h(), z)}
      Scc:
       {  +#(s x, s y) -> +#(x, y),
        +#(+(x, y), z) -> +#(x, +(y, z)),
        +#(+(x, y), z) -> +#(y, z)}
      
      SCC (1):
       Strict:
        {*#(s x, s y) -> *#(x, y)}
       Weak:
       {              s h() -> 1(),
          a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
          a(l, x, s y, h()) -> a(l, x, y, s h()),
          a(l, s x, h(), z) -> a(l, x, z, z),
        a(s l, h(), h(), z) -> a(l, z, h(), z),
        a(h(), h(), h(), x) -> s x,
                  +(x, h()) -> x,
                +(s x, s y) -> s s +(x, y),
                  +(h(), x) -> x,
              +(+(x, y), z) -> +(x, +(y, z)),
                  *(x, h()) -> h(),
                *(s x, s y) -> s +(+(*(x, y), x), y),
                  *(h(), x) -> h()}
       Open
      
      SCC (5):
       Strict:
        {  a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)),
           a#(l, x, s y, s z) -> a#(l, x, s y, z),
           a#(l, x, s y, h()) -> a#(l, x, y, s h()),
           a#(l, s x, h(), z) -> a#(l, x, z, z),
         a#(s l, h(), h(), z) -> a#(l, z, h(), z)}
       Weak:
       {              s h() -> 1(),
          a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
          a(l, x, s y, h()) -> a(l, x, y, s h()),
          a(l, s x, h(), z) -> a(l, x, z, z),
        a(s l, h(), h(), z) -> a(l, z, h(), z),
        a(h(), h(), h(), x) -> s x,
                  +(x, h()) -> x,
                +(s x, s y) -> s s +(x, y),
                  +(h(), x) -> x,
              +(+(x, y), z) -> +(x, +(y, z)),
                  *(x, h()) -> h(),
                *(s x, s y) -> s +(+(*(x, y), x), y),
                  *(h(), x) -> h()}
       Open
      
      SCC (3):
       Strict:
        {  +#(s x, s y) -> +#(x, y),
         +#(+(x, y), z) -> +#(x, +(y, z)),
         +#(+(x, y), z) -> +#(y, z)}
       Weak:
       {              s h() -> 1(),
          a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
          a(l, x, s y, h()) -> a(l, x, y, s h()),
          a(l, s x, h(), z) -> a(l, x, z, z),
        a(s l, h(), h(), z) -> a(l, z, h(), z),
        a(h(), h(), h(), x) -> s x,
                  +(x, h()) -> x,
                +(s x, s y) -> s s +(x, y),
                  +(h(), x) -> x,
              +(+(x, y), z) -> +(x, +(y, z)),
                  *(x, h()) -> h(),
                *(s x, s y) -> s +(+(*(x, y), x), y),
                  *(h(), x) -> h()}
       Open