MAYBE
Time: 2.029402
TRS:
 {f(true(), x, y) -> f(gt(x, y), x, round s y),
     gt(s u, s v) -> gt(u, v),
     gt(s u, 0()) -> true(),
       gt(0(), v) -> false(),
      round s s x -> s s round x,
      round s 0() -> s s 0(),
        round 0() -> 0()}
 DP:
  DP:
   {f#(true(), x, y) -> f#(gt(x, y), x, round s y),
    f#(true(), x, y) -> gt#(x, y),
    f#(true(), x, y) -> round# s y,
       gt#(s u, s v) -> gt#(u, v),
        round# s s x -> round# x}
  TRS:
  {f(true(), x, y) -> f(gt(x, y), x, round s y),
      gt(s u, s v) -> gt(u, v),
      gt(s u, 0()) -> true(),
        gt(0(), v) -> false(),
       round s s x -> s s round x,
       round s 0() -> s s 0(),
         round 0() -> 0()}
  UR:
   {gt(s u, s v) -> gt(u, v),
    gt(s u, 0()) -> true(),
      gt(0(), v) -> false(),
     round s s x -> s s round x,
     round s 0() -> s s 0(),
       round 0() -> 0(),
         a(z, w) -> z,
         a(z, w) -> w}
   EDG:
    {(f#(true(), x, y) -> f#(gt(x, y), x, round s y), f#(true(), x, y) -> round# s y)
     (f#(true(), x, y) -> f#(gt(x, y), x, round s y), f#(true(), x, y) -> gt#(x, y))
     (f#(true(), x, y) -> f#(gt(x, y), x, round s y), f#(true(), x, y) -> f#(gt(x, y), x, round s y))
     (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))
     (round# s s x -> round# x, round# s s x -> round# x)
     (f#(true(), x, y) -> round# s y, round# s s x -> round# 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), x, round s y)}
      Scc:
       {round# s s x -> round# x}
      Scc:
       {gt#(s u, s v) -> gt#(u, v)}
      
      SCC (1):
       Strict:
        {f#(true(), x, y) -> f#(gt(x, y), x, round s y)}
       Weak:
       {f(true(), x, y) -> f(gt(x, y), x, round s y),
           gt(s u, s v) -> gt(u, v),
           gt(s u, 0()) -> true(),
             gt(0(), v) -> false(),
            round s s x -> s s round x,
            round s 0() -> s s 0(),
              round 0() -> 0()}
       Fail
      
      SCC (1):
       Strict:
        {round# s s x -> round# x}
       Weak:
       {f(true(), x, y) -> f(gt(x, y), x, round s y),
           gt(s u, s v) -> gt(u, v),
           gt(s u, 0()) -> true(),
             gt(0(), v) -> false(),
            round s s x -> s s round x,
            round s 0() -> s s 0(),
              round 0() -> 0()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0, x1, x2) = x0 + x1 + x2 + 1,
         
         [gt](x0, x1) = x0 + x1 + 1,
         
         [round](x0) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [true] = 1,
         
         [0] = 0,
         
         [false] = 0,
         
         [round#](x0) = x0
        Strict:
         round# s s x -> round# x
         2 + 1x >= 0 + 1x
        Weak:
         round 0() -> 0()
         1 >= 0
         round s 0() -> s s 0()
         2 >= 2
         round s s x -> s s round x
         3 + 1x >= 3 + 1x
         gt(0(), v) -> false()
         1 + 1v >= 0
         gt(s u, 0()) -> true()
         2 + 1u >= 1
         gt(s u, s v) -> gt(u, v)
         3 + 1v + 1u >= 1 + 1v + 1u
         f(true(), x, y) -> f(gt(x, y), x, round s y)
         2 + 1x + 1y >= 4 + 2x + 2y
       Qed
     
     SCC (1):
      Strict:
       {gt#(s u, s v) -> gt#(u, v)}
      Weak:
      {f(true(), x, y) -> f(gt(x, y), x, round s y),
          gt(s u, s v) -> gt(u, v),
          gt(s u, 0()) -> true(),
            gt(0(), v) -> false(),
           round s s x -> s s round x,
           round s 0() -> s s 0(),
             round 0() -> 0()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [f](x0, x1, x2) = x0 + x1 + 1,
        
        [gt](x0, x1) = x0,
        
        [round](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [true] = 1,
        
        [0] = 0,
        
        [false] = 0,
        
        [gt#](x0, x1) = x0 + 1
       Strict:
        gt#(s u, s v) -> gt#(u, v)
        2 + 0v + 1u >= 1 + 0v + 1u
       Weak:
        round 0() -> 0()
        0 >= 0
        round s 0() -> s s 0()
        0 >= 2
        round s s x -> s s round x
        0 + 0x >= 2 + 0x
        gt(0(), v) -> false()
        0 + 0v >= 0
        gt(s u, 0()) -> true()
        1 + 1u >= 1
        gt(s u, s v) -> gt(u, v)
        1 + 0v + 1u >= 0 + 0v + 1u
        f(true(), x, y) -> f(gt(x, y), x, round s y)
        2 + 1x + 0y >= 1 + 2x + 0y
      Qed