MAYBE
Time: 0.002758
TRS:
 {  +(x, +(y, z)) -> +(+(x, y), z),
        +(x, 0()) -> x,
        +(x, s y) -> s +(x, y),
        +(0(), y) -> y,
        +(s x, y) -> s +(x, y),
  f h(x, h(y, z)) -> f h(+(x, y), z),
          f g f x -> f h(s 0(), x),
      f g h(x, y) -> f h(s x, y)}
 DP:
  DP:
   {  +#(x, +(y, z)) -> +#(x, y),
      +#(x, +(y, z)) -> +#(+(x, y), z),
          +#(x, s y) -> +#(x, y),
          +#(s x, y) -> +#(x, y),
    f# h(x, h(y, z)) -> +#(x, y),
    f# h(x, h(y, z)) -> f# h(+(x, y), z),
            f# g f x -> f# h(s 0(), x),
        f# g h(x, y) -> f# h(s x, y)}
  TRS:
  {  +(x, +(y, z)) -> +(+(x, y), z),
         +(x, 0()) -> x,
         +(x, s y) -> s +(x, y),
         +(0(), y) -> y,
         +(s x, y) -> s +(x, y),
   f h(x, h(y, z)) -> f h(+(x, y), z),
           f g f x -> f h(s 0(), x),
       f g h(x, y) -> f h(s x, y)}
  UR:
   {+(x, +(y, z)) -> +(+(x, y), z),
        +(x, 0()) -> x,
        +(x, s y) -> s +(x, y),
        +(0(), y) -> y,
        +(s x, y) -> s +(x, y)}
   EDG:
    {(+#(x, s y) -> +#(x, y), +#(s x, y) -> +#(x, y))
     (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (+#(x, s y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
     (+#(x, s y) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
     (f# h(x, h(y, z)) -> +#(x, y), +#(s x, y) -> +#(x, y))
     (f# h(x, h(y, z)) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (f# h(x, h(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
     (f# h(x, h(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
     (f# g f x -> f# h(s 0(), x), f# h(x, h(y, z)) -> f# h(+(x, y), z))
     (f# g f x -> f# h(s 0(), x), f# h(x, h(y, z)) -> +#(x, y))
     (+#(x, +(y, z)) -> +#(+(x, y), z), +#(s x, y) -> +#(x, y))
     (+#(x, +(y, z)) -> +#(+(x, y), z), +#(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)) -> +#(x, y))
     (f# g h(x, y) -> f# h(s x, y), f# h(x, h(y, z)) -> +#(x, y))
     (f# g h(x, y) -> f# h(s x, y), f# h(x, h(y, z)) -> f# h(+(x, y), z))
     (f# h(x, h(y, z)) -> f# h(+(x, y), z), f# h(x, h(y, z)) -> +#(x, y))
     (f# h(x, h(y, z)) -> f# h(+(x, y), z), f# h(x, h(y, z)) -> f# h(+(x, y), z))
     (+#(s x, y) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
     (+#(s x, y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
     (+#(s x, y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (+#(x, +(y, z)) -> +#(x, y), +#(s x, y) -> +#(x, y))}
    STATUS:
     arrows: 0.593750
     SCCS (2):
      Scc:
       {f# h(x, h(y, z)) -> f# h(+(x, y), z)}
      Scc:
       {+#(x, +(y, z)) -> +#(x, y),
        +#(x, +(y, z)) -> +#(+(x, y), z),
            +#(x, s y) -> +#(x, y),
            +#(s x, y) -> +#(x, y)}
      
      
      
      SCC (1):
       Strict:
        {f# h(x, h(y, z)) -> f# h(+(x, y), z)}
       Weak:
       {  +(x, +(y, z)) -> +(+(x, y), z),
              +(x, 0()) -> x,
              +(x, s y) -> s +(x, y),
              +(0(), y) -> y,
              +(s x, y) -> s +(x, y),
        f h(x, h(y, z)) -> f h(+(x, y), z),
                f g f x -> f h(s 0(), x),
            f g h(x, y) -> f h(s x, y)}
       Open
      
      SCC (4):
       Strict:
        {+#(x, +(y, z)) -> +#(x, y),
         +#(x, +(y, z)) -> +#(+(x, y), z),
             +#(x, s y) -> +#(x, y),
             +#(s x, y) -> +#(x, y)}
       Weak:
       {  +(x, +(y, z)) -> +(+(x, y), z),
              +(x, 0()) -> x,
              +(x, s y) -> s +(x, y),
              +(0(), y) -> y,
              +(s x, y) -> s +(x, y),
        f h(x, h(y, z)) -> f h(+(x, y), z),
                f g f x -> f h(s 0(), x),
            f g h(x, y) -> f h(s x, y)}
       Open