MAYBE
Time: 0.061053
TRS:
 {f(s s s s s s s s x, y, y) -> f(id s s s s s s s s x, y, y),
                      id s x -> s id x,
                      id 0() -> 0()}
 DP:
  DP:
   {f#(s s s s s s s s x, y, y) -> f#(id s s s s s s s s x, y, y),
    f#(s s s s s s s s x, y, y) -> id# s s s s s s s s x,
                        id# s x -> id# x}
  TRS:
  {f(s s s s s s s s x, y, y) -> f(id s s s s s s s s x, y, y),
                       id s x -> s id x,
                       id 0() -> 0()}
  UR:
   {id s x -> s id x,
    id 0() -> 0()}
   EDG:
    {(f#(s s s s s s s s x, y, y) -> f#(id s s s s s s s s x, y, y), f#(s s s s s s s s x, y, y) -> id# s s s s s s s s x)
     (f#(s s s s s s s s x, y, y) -> f#(id s s s s s s s s x, y, y), f#(s s s s s s s s x, y, y) -> f#(id s s s s s s s s x, y, y))
     (f#(s s s s s s s s x, y, y) -> id# s s s s s s s s x, id# s x -> id# x)
     (id# s x -> id# x, id# s x -> id# x)}
    STATUS:
     arrows: 0.555556
     SCCS (2):
      Scc:
       {f#(s s s s s s s s x, y, y) -> f#(id s s s s s s s s x, y, y)}
      Scc:
       {id# s x -> id# x}
      
      SCC (1):
       Strict:
        {f#(s s s s s s s s x, y, y) -> f#(id s s s s s s s s x, y, y)}
       Weak:
       {f(s s s s s s s s x, y, y) -> f(id s s s s s s s s x, y, y),
                            id s x -> s id x,
                            id 0() -> 0()}
       Fail
      
      SCC (1):
       Strict:
        {id# s x -> id# x}
       Weak:
       {f(s s s s s s s s x, y, y) -> f(id s s s s s s s s x, y, y),
                            id s x -> s id x,
                            id 0() -> 0()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0, x1, x2) = x0,
         
         [id](x0) = x0,
         
         [s](x0) = x0 + 1,
         
         [0] = 0,
         
         [id#](x0) = x0
        Strict:
         id# s x -> id# x
         1 + 1x >= 0 + 1x
        Weak:
         id 0() -> 0()
         0 >= 0
         id s x -> s id x
         1 + 1x >= 1 + 1x
         f(s s s s s s s s x, y, y) -> f(id s s s s s s s s x, y, y)
         8 + 1x + 0y >= 8 + 1x + 0y
       Qed