MAYBE
Time: 0.822730
TRS:
 {f(a x, y, s z, u) -> f(a b(), y, z, g(x, y, s z, u)),
              a b() -> c(),
      g(x, y, z, u) -> h(x, y, z, u),
    h(b(), y, z, u) -> f(y, y, z, u)}
 DP:
  DP:
   {f#(a x, y, s z, u) -> f#(a b(), y, z, g(x, y, s z, u)),
    f#(a x, y, s z, u) -> a# b(),
    f#(a x, y, s z, u) -> g#(x, y, s z, u),
        g#(x, y, z, u) -> h#(x, y, z, u),
      h#(b(), y, z, u) -> f#(y, y, z, u)}
  TRS:
  {f(a x, y, s z, u) -> f(a b(), y, z, g(x, y, s z, u)),
               a b() -> c(),
       g(x, y, z, u) -> h(x, y, z, u),
     h(b(), y, z, u) -> f(y, y, z, u)}
  EDG:
   {(g#(x, y, z, u) -> h#(x, y, z, u), h#(b(), y, z, u) -> f#(y, y, z, u))
    (h#(b(), y, z, u) -> f#(y, y, z, u), f#(a x, y, s z, u) -> f#(a b(), y, z, g(x, y, s z, u)))
    (h#(b(), y, z, u) -> f#(y, y, z, u), f#(a x, y, s z, u) -> a# b())
    (h#(b(), y, z, u) -> f#(y, y, z, u), f#(a x, y, s z, u) -> g#(x, y, s z, u))
    (f#(a x, y, s z, u) -> g#(x, y, s z, u), g#(x, y, z, u) -> h#(x, y, z, u))
    (f#(a x, y, s z, u) -> f#(a b(), y, z, g(x, y, s z, u)), f#(a x, y, s z, u) -> f#(a b(), y, z, g(x, y, s z, u)))
    (f#(a x, y, s z, u) -> f#(a b(), y, z, g(x, y, s z, u)), f#(a x, y, s z, u) -> a# b())
    (f#(a x, y, s z, u) -> f#(a b(), y, z, g(x, y, s z, u)), f#(a x, y, s z, u) -> g#(x, y, s z, u))}
   STATUS:
    arrows: 0.680000
    SCCS (1):
     Scc:
      {f#(a x, y, s z, u) -> f#(a b(), y, z, g(x, y, s z, u)),
       f#(a x, y, s z, u) -> g#(x, y, s z, u),
           g#(x, y, z, u) -> h#(x, y, z, u),
         h#(b(), y, z, u) -> f#(y, y, z, u)}
     
     SCC (4):
      Strict:
       {f#(a x, y, s z, u) -> f#(a b(), y, z, g(x, y, s z, u)),
        f#(a x, y, s z, u) -> g#(x, y, s z, u),
            g#(x, y, z, u) -> h#(x, y, z, u),
          h#(b(), y, z, u) -> f#(y, y, z, u)}
      Weak:
      {f(a x, y, s z, u) -> f(a b(), y, z, g(x, y, s z, u)),
                   a b() -> c(),
           g(x, y, z, u) -> h(x, y, z, u),
         h(b(), y, z, u) -> f(y, y, z, u)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [f](x0, x1, x2, x3) = x0 + x1 + x2 + x3,
        
        [g](x0, x1, x2, x3) = x0,
        
        [h](x0, x1, x2, x3) = 0,
        
        [a](x0) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [b] = 1,
        
        [c] = 0,
        
        [f#](x0, x1, x2, x3) = x0,
        
        [g#](x0, x1, x2, x3) = x0,
        
        [h#](x0, x1, x2, x3) = x0
       Strict:
        h#(b(), y, z, u) -> f#(y, y, z, u)
        0 + 0y + 1z + 0u >= 0 + 0y + 1z + 0u
        g#(x, y, z, u) -> h#(x, y, z, u)
        0 + 0y + 1z + 0x + 0u >= 0 + 0y + 1z + 0x + 0u
        f#(a x, y, s z, u) -> g#(x, y, s z, u)
        1 + 0y + 1z + 0x + 0u >= 1 + 0y + 1z + 0x + 0u
        f#(a x, y, s z, u) -> f#(a b(), y, z, g(x, y, s z, u))
        1 + 0y + 1z + 0x + 0u >= 0 + 0y + 1z + 0x + 0u
       Weak:
        h(b(), y, z, u) -> f(y, y, z, u)
        0 + 0y + 0z + 0u >= 0 + 2y + 1z + 1u
        g(x, y, z, u) -> h(x, y, z, u)
        0 + 1y + 0z + 0x + 0u >= 0 + 0y + 0z + 0x + 0u
        a b() -> c()
        2 >= 0
        f(a x, y, s z, u) -> f(a b(), y, z, g(x, y, s z, u))
        2 + 1y + 1z + 1x + 1u >= 2 + 2y + 1z + 0x + 0u
      SCCS (1):
       Scc:
        {f#(a x, y, s z, u) -> g#(x, y, s z, u),
             g#(x, y, z, u) -> h#(x, y, z, u),
           h#(b(), y, z, u) -> f#(y, y, z, u)}
       
       SCC (3):
        Strict:
         {f#(a x, y, s z, u) -> g#(x, y, s z, u),
              g#(x, y, z, u) -> h#(x, y, z, u),
            h#(b(), y, z, u) -> f#(y, y, z, u)}
        Weak:
        {f(a x, y, s z, u) -> f(a b(), y, z, g(x, y, s z, u)),
                     a b() -> c(),
             g(x, y, z, u) -> h(x, y, z, u),
           h(b(), y, z, u) -> f(y, y, z, u)}
        Fail