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