MAYBE
Time: 0.345747
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:
  DP:
   {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)))}
  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)))}
  UR:
   {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())))}
   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, nil())) -> 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 x, 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#(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, 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)) -> 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#(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))))
     (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))
     (L# f(s s y, f(z, w)) -> f#(s 0(), 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#(s 0(), 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#(s 0(), f(y, f(s z, w))), f#(x, f(s s y, nil())) -> 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, 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#(s x, 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#(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#(s x, f(y, f(s z, w))), f#(x, f(s s y, nil())) -> 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, 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()))}
    STATUS:
     arrows: 0.540000
     SCCS (2):
      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 (1):
       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)))}
       Open
      
      
      
      SCC (4):
       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)))}
       Open