MAYBE
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:
  Strict:
   {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)}
  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)}
  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))}
   SCCS:
    Scc:
     {gt#(s(u), s(v)) -> gt#(u, v)}
    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:
     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)}
     SPSC:
      Simple Projection:
       pi(gt#) = 0
      Strict:
       {}
      Qed
    SCC:
     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)}
     Fail