MAYBE
(ignored inputs)COMMENT translated from Cops 261
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ -(?x,?x) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     +(?x,?y) -> +(?y,?x),
     +(0,?x) -> ?x,
     +(?x,0) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)),
     +(p(?x),?y) -> p(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?y,?x)),
     s(p(?x)) -> ?x,
     p(s(?x)) -> ?x ]
Constructors: {+,-,0,p,s}
Defined function symbols: {}
Constructor subsystem:
   [ -(s(?x),s(?y)) -> -(?x,?y),
     +(0,?x) -> ?x,
     +(?x,0) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)),
     +(p(?x),?y) -> p(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?y,?x)),
     s(p(?x)) -> ?x,
     p(s(?x)) -> ?x ]
Rule part & Conj Part:
   [ -(s(?x),s(?y)) -> -(?x,?y),
     +(0,?x) -> ?x,
     +(?x,0) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)),
     +(p(?x),?y) -> p(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?y,?x)),
     s(p(?x)) -> ?x,
     p(s(?x)) -> ?x ]
   [ -(?x,?x) -> 0,
     +(?x,?y) -> +(?y,?x) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Int}
Signature:
   [ + : Int,Int -> Int,
     - : Int,Int -> Int,
     0 : Int,
     p : Int -> Int,
     s : Int -> Int ]
Rule Part:
   [ -(s(?x),s(?y)) -> -(?x,?y),
     +(0,?x) -> ?x,
     +(?x,0) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)),
     +(p(?x),?y) -> p(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?y,?x)),
     s(p(?x)) -> ?x,
     p(s(?x)) -> ?x ]
Conjecture Part:
   [ -(?x,?x) = 0,
     +(?x,?y) = +(?y,?x) ]
Precedence (by weight): {(+,5),(-,2),(0,3),(p,1),(s,4)}
Rule part is not confluent.
Check ground confluence of Rule part (R0) by basic RI.
Rules:
   [ -(s(?x),s(?y)) -> -(?x,?y),
     +(0,?x) -> ?x,
     +(?x,0) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)),
     +(p(?x),?y) -> p(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?y,?x)),
     s(p(?x)) -> ?x,
     p(s(?x)) -> ?x ]
Conjectures:
   [ -(?x_7,s(?y)) = -(p(?x_7),?y),
     -(s(?x),?x_7) = -(?x,p(?x_7)),
     s(s(+(?x_3,?y_4))) = s(s(+(?y_4,?x_3))),
     +(?x_3,?y_6) = +(?y_6,?x_3),
     +(?y_4,?x_5) = +(?x_5,?y_4),
     +(?x_4,?x_7) = +(?x_7,?x_4),
     p(p(+(?x_5,?y_6))) = p(p(+(?y_6,?x_5))),
     +(?x_6,?x_8) = +(?x_8,?x_6) ]
STEP 0
ES:
   [ -(?x_7,s(?y)) = -(p(?x_7),?y),
     -(s(?x),?x_7) = -(?x,p(?x_7)),
     s(s(+(?x_3,?y_4))) = s(s(+(?y_4,?x_3))),
     +(?x_3,?y_6) = +(?y_6,?x_3),
     +(?y_4,?x_5) = +(?x_5,?y_4),
     +(?x_4,?x_7) = +(?x_7,?x_4),
     p(p(+(?x_5,?y_6))) = p(p(+(?y_6,?x_5))),
     +(?x_6,?x_8) = +(?x_8,?x_6) ]
HS:
   [ ]
ES0:
   [ -(?x_7,s(?y)) = -(p(?x_7),?y),
     -(s(?x),?x_7) = -(?x,p(?x_7)),
     s(s(+(?x_3,?y_4))) = s(s(+(?y_4,?x_3))),
     +(?x_3,?y_6) = +(?y_6,?x_3),
     +(?y_4,?x_5) = +(?x_5,?y_4),
     +(?x_4,?x_7) = +(?x_7,?x_4),
     p(p(+(?x_5,?y_6))) = p(p(+(?y_6,?x_5))),
     +(?x_6,?x_8) = +(?x_8,?x_6) ]
HS0:
   [ ]
ES1:
   [ -(?x_7,s(?y)) = -(p(?x_7),?y),
     -(s(?x),?x_7) = -(?x,p(?x_7)),
     s(s(+(?x_3,?y_4))) = s(s(+(?y_4,?x_3))),
     +(?x_3,?y_6) = +(?y_6,?x_3),
     +(?y_4,?x_5) = +(?x_5,?y_4),
     +(?x_4,?x_7) = +(?x_7,?x_4),
     p(p(+(?x_5,?y_6))) = p(p(+(?y_6,?x_5))),
     +(?x_6,?x_8) = +(?x_8,?x_6) ]
HS1:
   [ ]
No equation to expand
Failed to prove ground confluece R0.
examples/fromCops/noncr/261.trs: Failure(unknown)
(35 msec.)