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