MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ len(nil) -> 0,
     len(cons(?x,?xs)) -> s(len(?xs)),
     qrev(nil,?ys) -> ?ys,
     qrev(cons(?x,?xs),?ys) -> qrev(?xs,cons(?x,?ys)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     len(qrev(?xs,?ys)) -> +(len(?xs),len(?ys)) ]
Constructors: {0,s,nil,cons}
Defined function symbols: {+,len,qrev}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ len(nil) -> 0,
     len(cons(?x,?xs)) -> s(len(?xs)),
     qrev(nil,?ys) -> ?ys,
     qrev(cons(?x,?xs),?ys) -> qrev(?xs,cons(?x,?ys)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
   [ len(qrev(?xs,?ys)) -> +(len(?xs),len(?ys)) ]
Trying with:
R:
   [ len(nil) -> 0,
     len(cons(?x,?xs)) -> s(len(?xs)),
     qrev(nil,?ys) -> ?ys,
     qrev(cons(?x,?xs),?ys) -> qrev(?xs,cons(?x,?ys)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
E:
   [ len(qrev(?xs,?ys)) = +(len(?xs),len(?ys)) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,List}
Signature:
   [ len : List -> Nat,
     qrev : List,List -> List,
     + : Nat,Nat -> Nat,
     cons : Nat,List -> List,
     nil : List,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ len(nil) -> 0,
     len(cons(?x,?xs)) -> s(len(?xs)),
     qrev(nil,?ys) -> ?ys,
     qrev(cons(?x,?xs),?ys) -> qrev(?xs,cons(?x,?ys)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Conjecture Part:
   [ len(qrev(?xs,?ys)) = +(len(?xs),len(?ys)) ]
Termination proof failed.
new/len-qrev.trs: Failure(unknown)
(19 msec.)