MAYBE
Time: 0.001001
TRS:
 {f(true(), x, y) -> f(gt(x, y), trunc x, s y),
     gt(s u, s v) -> gt(u, v),
     gt(s u, 0()) -> true(),
       gt(0(), v) -> false(),
      trunc s s x -> s s trunc x,
      trunc s 0() -> 0(),
        trunc 0() -> 0()}
 DP:
  DP:
   {f#(true(), x, y) -> f#(gt(x, y), trunc x, s y),
    f#(true(), x, y) -> gt#(x, y),
    f#(true(), x, y) -> trunc# x,
       gt#(s u, s v) -> gt#(u, v),
        trunc# s s x -> trunc# x}
  TRS:
  {f(true(), x, y) -> f(gt(x, y), trunc x, s y),
      gt(s u, s v) -> gt(u, v),
      gt(s u, 0()) -> true(),
        gt(0(), v) -> false(),
       trunc s s x -> s s trunc x,
       trunc s 0() -> 0(),
         trunc 0() -> 0()}
  UR:
   {gt(s u, s v) -> gt(u, v),
    gt(s u, 0()) -> true(),
      gt(0(), v) -> false(),
     trunc s s x -> s s trunc x,
     trunc s 0() -> 0(),
       trunc 0() -> 0(),
         a(z, w) -> z,
         a(z, w) -> w}
   EDG:
    {(f#(true(), x, y) -> f#(gt(x, y), trunc x, s y), f#(true(), x, y) -> trunc# x)
     (f#(true(), x, y) -> f#(gt(x, y), trunc x, s y), f#(true(), x, y) -> gt#(x, y))
     (f#(true(), x, y) -> f#(gt(x, y), trunc x, s y), f#(true(), x, y) -> f#(gt(x, y), trunc x, s y))
     (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))
     (trunc# s s x -> trunc# x, trunc# s s x -> trunc# x)
     (f#(true(), x, y) -> trunc# x, trunc# s s x -> trunc# x)
     (f#(true(), x, y) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))}
    STATUS:
     arrows: 0.720000
     SCCS (3):
      Scc:
       {f#(true(), x, y) -> f#(gt(x, y), trunc x, s y)}
      Scc:
       {trunc# s s x -> trunc# x}
      Scc:
       {gt#(s u, s v) -> gt#(u, v)}
      
      SCC (1):
       Strict:
        {f#(true(), x, y) -> f#(gt(x, y), trunc x, s y)}
       Weak:
       {f(true(), x, y) -> f(gt(x, y), trunc x, s y),
           gt(s u, s v) -> gt(u, v),
           gt(s u, 0()) -> true(),
             gt(0(), v) -> false(),
            trunc s s x -> s s trunc x,
            trunc s 0() -> 0(),
              trunc 0() -> 0()}
       Open
      
      SCC (1):
       Strict:
        {trunc# s s x -> trunc# x}
       Weak:
       {f(true(), x, y) -> f(gt(x, y), trunc x, s y),
           gt(s u, s v) -> gt(u, v),
           gt(s u, 0()) -> true(),
             gt(0(), v) -> false(),
            trunc s s x -> s s trunc x,
            trunc s 0() -> 0(),
              trunc 0() -> 0()}
       Open
      
      SCC (1):
       Strict:
        {gt#(s u, s v) -> gt#(u, v)}
       Weak:
       {f(true(), x, y) -> f(gt(x, y), trunc x, s y),
           gt(s u, s v) -> gt(u, v),
           gt(s u, 0()) -> true(),
             gt(0(), v) -> false(),
            trunc s s x -> s s trunc x,
            trunc s 0() -> 0(),
              trunc 0() -> 0()}
       Open