MAYBE

Problem:
 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)))

Proof:
 DP Processor:
  DPs:
   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)))
  Usable Rule Processor:
   DPs:
    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:
    f6(x,y) -> x
    f6(x,y) -> y
   CDG Processor:
    DPs:
     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:
     f6(x,y) -> x
     f6(x,y) -> y
    graph:
     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,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),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,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)))
    Restore Modifier:
     DPs:
      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)))
     SCC Processor:
      #sccs: 1
      #rules: 3
      #arcs: 6/9
      DPs:
       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)
      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)))
      Open