MAYBE
TRS:
 {f(x, f(s(s(y)), f(z, w))) -> f(s(x), f(y, f(s(z), w))),
    f(x, f(s(s(y)), nil())) -> f(s(x), f(y, f(s(0()), nil()))),
     L(f(s(s(y)), f(z, w))) -> L(f(s(0()), f(y, f(s(z), w))))}
 DP:
  Strict:
   {f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)),
    f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))),
    f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w),
      f#(x, f(s(s(y)), nil())) -> f#(y, f(s(0()), nil())),
      f#(x, f(s(s(y)), nil())) -> f#(s(x), f(y, f(s(0()), nil()))),
      f#(x, f(s(s(y)), nil())) -> f#(s(0()), nil()),
       L#(f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)),
       L#(f(s(s(y)), f(z, w))) -> f#(s(z), w),
       L#(f(s(s(y)), f(z, w))) -> f#(s(0()), f(y, f(s(z), w))),
       L#(f(s(s(y)), f(z, w))) -> L#(f(s(0()), f(y, f(s(z), w))))}
  Weak:
  {f(x, f(s(s(y)), f(z, w))) -> f(s(x), f(y, f(s(z), w))),
     f(x, f(s(s(y)), nil())) -> f(s(x), f(y, f(s(0()), nil()))),
      L(f(s(s(y)), f(z, w))) -> L(f(s(0()), f(y, f(s(z), w))))}
  EDG:
   {(L#(f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)), f#(x, f(s(s(y)), nil())) -> f#(s(0()), nil()))
    (L#(f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)), f#(x, f(s(s(y)), nil())) -> f#(s(x), f(y, f(s(0()), nil()))))
    (L#(f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)), f#(x, f(s(s(y)), nil())) -> f#(y, f(s(0()), nil())))
    (L#(f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)), f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w))
    (L#(f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)), f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))))
    (L#(f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)), f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)))
    (f#(x, f(s(s(y)), nil())) -> f#(s(x), f(y, f(s(0()), nil()))), f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w))
    (f#(x, f(s(s(y)), nil())) -> f#(s(x), f(y, f(s(0()), nil()))), f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))))
    (f#(x, f(s(s(y)), nil())) -> f#(s(x), f(y, f(s(0()), nil()))), f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)))
    (L#(f(s(s(y)), f(z, w))) -> f#(s(z), w), f#(x, f(s(s(y)), nil())) -> f#(s(0()), nil()))
    (L#(f(s(s(y)), f(z, w))) -> f#(s(z), w), f#(x, f(s(s(y)), nil())) -> f#(s(x), f(y, f(s(0()), nil()))))
    (L#(f(s(s(y)), f(z, w))) -> f#(s(z), w), f#(x, f(s(s(y)), nil())) -> f#(y, f(s(0()), nil())))
    (L#(f(s(s(y)), f(z, w))) -> f#(s(z), w), f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w))
    (L#(f(s(s(y)), f(z, w))) -> f#(s(z), w), f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))))
    (L#(f(s(s(y)), f(z, w))) -> f#(s(z), w), f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)))
    (L#(f(s(s(y)), f(z, w))) -> L#(f(s(0()), f(y, f(s(z), w)))), L#(f(s(s(y)), f(z, w))) -> L#(f(s(0()), f(y, f(s(z), w)))))
    (L#(f(s(s(y)), f(z, w))) -> L#(f(s(0()), f(y, f(s(z), w)))), L#(f(s(s(y)), f(z, w))) -> f#(s(0()), f(y, f(s(z), w))))
    (L#(f(s(s(y)), f(z, w))) -> L#(f(s(0()), f(y, f(s(z), w)))), L#(f(s(s(y)), f(z, w))) -> f#(s(z), w))
    (L#(f(s(s(y)), f(z, w))) -> L#(f(s(0()), f(y, f(s(z), w)))), L#(f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w), f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w), f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w), f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w), f#(x, f(s(s(y)), nil())) -> f#(y, f(s(0()), nil())))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w), f#(x, f(s(s(y)), nil())) -> f#(s(x), f(y, f(s(0()), nil()))))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w), f#(x, f(s(s(y)), nil())) -> f#(s(0()), nil()))
    (L#(f(s(s(y)), f(z, w))) -> f#(s(0()), f(y, f(s(z), w))), f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)))
    (L#(f(s(s(y)), f(z, w))) -> f#(s(0()), f(y, f(s(z), w))), f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))))
    (L#(f(s(s(y)), f(z, w))) -> f#(s(0()), f(y, f(s(z), w))), f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))), f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))), f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))), f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)), f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)), f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)), f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)), f#(x, f(s(s(y)), nil())) -> f#(y, f(s(0()), nil())))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)), f#(x, f(s(s(y)), nil())) -> f#(s(x), f(y, f(s(0()), nil()))))
    (f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)), f#(x, f(s(s(y)), nil())) -> f#(s(0()), nil()))}
   SCCS:
    Scc:
     {L#(f(s(s(y)), f(z, w))) -> L#(f(s(0()), f(y, f(s(z), w))))}
    Scc:
     {f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)),
      f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))),
      f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w),
        f#(x, f(s(s(y)), nil())) -> f#(s(x), f(y, f(s(0()), nil())))}
    SCC:
     Strict:
      {L#(f(s(s(y)), f(z, w))) -> L#(f(s(0()), f(y, f(s(z), w))))}
     Weak:
     {f(x, f(s(s(y)), f(z, w))) -> f(s(x), f(y, f(s(z), w))),
        f(x, f(s(s(y)), nil())) -> f(s(x), f(y, f(s(0()), nil()))),
         L(f(s(s(y)), f(z, w))) -> L(f(s(0()), f(y, f(s(z), w))))}
     Fail
    SCC:
     Strict:
      {f#(x, f(s(s(y)), f(z, w))) -> f#(y, f(s(z), w)),
       f#(x, f(s(s(y)), f(z, w))) -> f#(s(x), f(y, f(s(z), w))),
       f#(x, f(s(s(y)), f(z, w))) -> f#(s(z), w),
         f#(x, f(s(s(y)), nil())) -> f#(s(x), f(y, f(s(0()), nil())))}
     Weak:
     {f(x, f(s(s(y)), f(z, w))) -> f(s(x), f(y, f(s(z), w))),
        f(x, f(s(s(y)), nil())) -> f(s(x), f(y, f(s(0()), nil()))),
         L(f(s(s(y)), f(z, w))) -> L(f(s(0()), f(y, f(s(z), w))))}
     POLY:
      Argument Filtering:
       pi(nil) = [], pi(0) = [], pi(L) = [], pi(s) = [0], pi(f#) = 1, pi(f) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [f](x0, x1) = x0 + x1,
       [s](x0) = x0 + 1,
       [nil] = 0,
       [0] = 0
      Strict:
       {}
      Weak:
       {f(x, f(s(s(y)), f(z, w))) -> f(s(x), f(y, f(s(z), w))),
          f(x, f(s(s(y)), nil())) -> f(s(x), f(y, f(s(0()), nil()))),
           L(f(s(s(y)), f(z, w))) -> L(f(s(0()), f(y, f(s(z), w))))}
      Qed