MAYBE
Time: 0.002938
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))}
    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))}
     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))}
      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()}
          Open
         
         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()}
          Open
         
         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()}
          Open