MAYBE
Time: 0.002028
TRS:
 {g(true(), x, y, z) -> f(gt(x, z), x, y, s z),
  g(true(), x, y, z) -> f(gt(x, z), x, s y, z),
        gt(s u, s v) -> gt(u, v),
        gt(s u, 0()) -> true(),
          gt(0(), v) -> false(),
  f(true(), x, y, z) -> g(gt(x, y), x, y, z)}
 DP:
  DP:
   {g#(true(), x, y, z) -> gt#(x, z),
    g#(true(), x, y, z) -> f#(gt(x, z), x, y, s z),
    g#(true(), x, y, z) -> f#(gt(x, z), x, s y, z),
          gt#(s u, s v) -> gt#(u, v),
    f#(true(), x, y, z) -> g#(gt(x, y), x, y, z),
    f#(true(), x, y, z) -> gt#(x, y)}
  TRS:
  {g(true(), x, y, z) -> f(gt(x, z), x, y, s z),
   g(true(), x, y, z) -> f(gt(x, z), x, s y, z),
         gt(s u, s v) -> gt(u, v),
         gt(s u, 0()) -> true(),
           gt(0(), v) -> false(),
   f(true(), x, y, z) -> g(gt(x, y), x, y, z)}
  EDG:
   {(g#(true(), x, y, z) -> gt#(x, z), gt#(s u, s v) -> gt#(u, v))
    (f#(true(), x, y, z) -> g#(gt(x, y), x, y, z), g#(true(), x, y, z) -> f#(gt(x, z), x, s y, z))
    (f#(true(), x, y, z) -> g#(gt(x, y), x, y, z), g#(true(), x, y, z) -> f#(gt(x, z), x, y, s z))
    (f#(true(), x, y, z) -> g#(gt(x, y), x, y, z), g#(true(), x, y, z) -> gt#(x, z))
    (g#(true(), x, y, z) -> f#(gt(x, z), x, y, s z), f#(true(), x, y, z) -> gt#(x, y))
    (g#(true(), x, y, z) -> f#(gt(x, z), x, y, s z), f#(true(), x, y, z) -> g#(gt(x, y), x, y, z))
    (f#(true(), x, y, z) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
    (g#(true(), x, y, z) -> f#(gt(x, z), x, s y, z), f#(true(), x, y, z) -> g#(gt(x, y), x, y, z))
    (g#(true(), x, y, z) -> f#(gt(x, z), x, s y, z), f#(true(), x, y, z) -> gt#(x, y))
    (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))}
   STATUS:
    arrows: 0.722222
    SCCS (2):
     Scc:
      {g#(true(), x, y, z) -> f#(gt(x, z), x, y, s z),
       g#(true(), x, y, z) -> f#(gt(x, z), x, s y, z),
       f#(true(), x, y, z) -> g#(gt(x, y), x, y, z)}
     Scc:
      {gt#(s u, s v) -> gt#(u, v)}
     
     SCC (3):
      Strict:
       {g#(true(), x, y, z) -> f#(gt(x, z), x, y, s z),
        g#(true(), x, y, z) -> f#(gt(x, z), x, s y, z),
        f#(true(), x, y, z) -> g#(gt(x, y), x, y, z)}
      Weak:
      {g(true(), x, y, z) -> f(gt(x, z), x, y, s z),
       g(true(), x, y, z) -> f(gt(x, z), x, s y, z),
             gt(s u, s v) -> gt(u, v),
             gt(s u, 0()) -> true(),
               gt(0(), v) -> false(),
       f(true(), x, y, z) -> g(gt(x, y), x, y, z)}
      Open
     
     
     SCC (1):
      Strict:
       {gt#(s u, s v) -> gt#(u, v)}
      Weak:
      {g(true(), x, y, z) -> f(gt(x, z), x, y, s z),
       g(true(), x, y, z) -> f(gt(x, z), x, s y, z),
             gt(s u, s v) -> gt(u, v),
             gt(s u, 0()) -> true(),
               gt(0(), v) -> false(),
       f(true(), x, y, z) -> g(gt(x, y), x, y, z)}
      Open