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