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