MAYBE
Time: 2.796999
TRS:
 {f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, y, s z),
  f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, s y, z),
        gt(s u, s v) -> gt(u, v),
        gt(s u, 0()) -> true(),
          gt(0(), v) -> false(),
        plus(n, s m) -> s plus(n, m),
        plus(n, 0()) -> n}
 DP:
  DP:
   {f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, y, s z),
    f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, s y, z),
    f#(true(), x, y, z) -> gt#(x, plus(y, z)),
    f#(true(), x, y, z) -> plus#(y, z),
          gt#(s u, s v) -> gt#(u, v),
          plus#(n, s m) -> plus#(n, m)}
  TRS:
  {f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, y, s z),
   f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, s y, z),
         gt(s u, s v) -> gt(u, v),
         gt(s u, 0()) -> true(),
           gt(0(), v) -> false(),
         plus(n, s m) -> s plus(n, m),
         plus(n, 0()) -> n}
  UR:
   {gt(s u, s v) -> gt(u, v),
    gt(s u, 0()) -> true(),
      gt(0(), v) -> false(),
    plus(n, s m) -> s plus(n, m),
    plus(n, 0()) -> n,
         a(w, t) -> w,
         a(w, t) -> t}
   EDG:
    {(f#(true(), x, y, z) -> gt#(x, plus(y, z)), gt#(s u, s v) -> gt#(u, v))
     (f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, y, s z), f#(true(), x, y, z) -> plus#(y, z))
     (f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, y, s z), f#(true(), x, y, z) -> gt#(x, plus(y, z)))
     (f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, y, s z), f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, s y, z))
     (f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, y, s z), f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, y, s z))
     (plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
     (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))
     (f#(true(), x, y, z) -> plus#(y, z), plus#(n, s m) -> plus#(n, m))
     (f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, s y, z), f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, y, s z))
     (f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, s y, z), f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, s y, z))
     (f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, s y, z), f#(true(), x, y, z) -> gt#(x, plus(y, z)))
     (f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, s y, z), f#(true(), x, y, z) -> plus#(y, z))}
    STATUS:
     arrows: 0.666667
     SCCS (3):
      Scc:
       {f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, y, s z),
        f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, s y, z)}
      Scc:
       {plus#(n, s m) -> plus#(n, m)}
      Scc:
       {gt#(s u, s v) -> gt#(u, v)}
      
      SCC (2):
       Strict:
        {f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, y, s z),
         f#(true(), x, y, z) -> f#(gt(x, plus(y, z)), x, s y, z)}
       Weak:
       {f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, y, s z),
        f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, s y, z),
              gt(s u, s v) -> gt(u, v),
              gt(s u, 0()) -> true(),
                gt(0(), v) -> false(),
              plus(n, s m) -> s plus(n, m),
              plus(n, 0()) -> n}
       Open
      
      SCC (1):
       Strict:
        {plus#(n, s m) -> plus#(n, m)}
       Weak:
       {f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, y, s z),
        f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, s y, z),
              gt(s u, s v) -> gt(u, v),
              gt(s u, 0()) -> true(),
                gt(0(), v) -> false(),
              plus(n, s m) -> s plus(n, m),
              plus(n, 0()) -> n}
       Open
      
      SCC (1):
       Strict:
        {gt#(s u, s v) -> gt#(u, v)}
       Weak:
       {f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, y, s z),
        f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, s y, z),
              gt(s u, s v) -> gt(u, v),
              gt(s u, 0()) -> true(),
                gt(0(), v) -> false(),
              plus(n, s m) -> s plus(n, m),
              plus(n, 0()) -> n}
       Open