MAYBE
Time: 0.013181
TRS:
 {                        r(xs, ys, zs, nil()) -> xs,
                 r(xs, nil(), zs, cons(w, ws)) -> r(xs, xs, cons(succ zero(), zs), ws),
        r(xs, cons(y, ys), nil(), cons(w, ws)) -> r(xs, xs, cons(succ zero(), nil()), ws),
  r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) -> r(ys, cons(y, ys), zs, cons(succ zero(), cons(w, ws)))}
 DP:
  DP:
   {               r#(xs, nil(), zs, cons(w, ws)) -> r#(xs, xs, cons(succ zero(), zs), ws),
          r#(xs, cons(y, ys), nil(), cons(w, ws)) -> r#(xs, xs, cons(succ zero(), nil()), ws),
    r#(xs, cons(y, ys), cons(z, zs), cons(w, ws)) -> r#(ys, cons(y, ys), zs, cons(succ zero(), cons(w, ws)))}
  TRS:
  {                        r(xs, ys, zs, nil()) -> xs,
                  r(xs, nil(), zs, cons(w, ws)) -> r(xs, xs, cons(succ zero(), zs), ws),
         r(xs, cons(y, ys), nil(), cons(w, ws)) -> r(xs, xs, cons(succ zero(), nil()), ws),
   r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) -> r(ys, cons(y, ys), zs, cons(succ zero(), cons(w, ws)))}
  UR:
   {a(x, v) -> x,
    a(x, v) -> v}
   EDG:
    {(r#(xs, cons(y, ys), nil(), cons(w, ws)) -> r#(xs, xs, cons(succ zero(), nil()), ws), r#(xs, cons(y, ys), cons(z, zs), cons(w, ws)) -> r#(ys, cons(y, ys), zs, cons(succ zero(), cons(w, ws))))
     (r#(xs, cons(y, ys), nil(), cons(w, ws)) -> r#(xs, xs, cons(succ zero(), nil()), ws), r#(xs, nil(), zs, cons(w, ws)) -> r#(xs, xs, cons(succ zero(), zs), ws))
     (r#(xs, cons(y, ys), cons(z, zs), cons(w, ws)) -> r#(ys, cons(y, ys), zs, cons(succ zero(), cons(w, ws))), r#(xs, cons(y, ys), nil(), cons(w, ws)) -> r#(xs, xs, cons(succ zero(), nil()), ws))
     (r#(xs, cons(y, ys), cons(z, zs), cons(w, ws)) -> r#(ys, cons(y, ys), zs, cons(succ zero(), cons(w, ws))), r#(xs, cons(y, ys), cons(z, zs), cons(w, ws)) -> r#(ys, cons(y, ys), zs, cons(succ zero(), cons(w, ws))))
     (r#(xs, nil(), zs, cons(w, ws)) -> r#(xs, xs, cons(succ zero(), zs), ws), r#(xs, nil(), zs, cons(w, ws)) -> r#(xs, xs, cons(succ zero(), zs), ws))
     (r#(xs, nil(), zs, cons(w, ws)) -> r#(xs, xs, cons(succ zero(), zs), ws), r#(xs, cons(y, ys), cons(z, zs), cons(w, ws)) -> r#(ys, cons(y, ys), zs, cons(succ zero(), cons(w, ws))))}
    STATUS:
     arrows: 0.333333
     SCCS (1):
      Scc:
       {               r#(xs, nil(), zs, cons(w, ws)) -> r#(xs, xs, cons(succ zero(), zs), ws),
              r#(xs, cons(y, ys), nil(), cons(w, ws)) -> r#(xs, xs, cons(succ zero(), nil()), ws),
        r#(xs, cons(y, ys), cons(z, zs), cons(w, ws)) -> r#(ys, cons(y, ys), zs, cons(succ zero(), cons(w, ws)))}
      
      SCC (3):
       Strict:
        {               r#(xs, nil(), zs, cons(w, ws)) -> r#(xs, xs, cons(succ zero(), zs), ws),
               r#(xs, cons(y, ys), nil(), cons(w, ws)) -> r#(xs, xs, cons(succ zero(), nil()), ws),
         r#(xs, cons(y, ys), cons(z, zs), cons(w, ws)) -> r#(ys, cons(y, ys), zs, cons(succ zero(), cons(w, ws)))}
       Weak:
       {                        r(xs, ys, zs, nil()) -> xs,
                       r(xs, nil(), zs, cons(w, ws)) -> r(xs, xs, cons(succ zero(), zs), ws),
              r(xs, cons(y, ys), nil(), cons(w, ws)) -> r(xs, xs, cons(succ zero(), nil()), ws),
        r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) -> r(ys, cons(y, ys), zs, cons(succ zero(), cons(w, ws)))}
       Fail