MAYBE
(ignored inputs)COMMENT translated from Cops 181
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(k,0) -> 0,
     *(k,s(?y)) -> +(k,*(k,?y)),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(k,+(?x,?y)) -> +(*(k,?x),*(k,?y)) ]
Constructors: {*,+,0,k,s}
Defined function symbols: {}
Constructor subsystem:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(k,0) -> 0,
     *(k,s(?y)) -> +(k,*(k,?y)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(k,+(?x,?y)) -> +(*(k,?x),*(k,?y)) ]
Rule part & Conj Part:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(k,0) -> 0,
     *(k,s(?y)) -> +(k,*(k,?y)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(k,+(?x,?y)) -> +(*(k,?x),*(k,?y)) ]
   [ +(?x,?y) -> +(?y,?x) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat}
Signature:
   [ * : Nat,Nat -> Nat,
     + : Nat,Nat -> Nat,
     0 : Nat,
     k : Nat,
     s : Nat -> Nat ]
Rule Part:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(k,0) -> 0,
     *(k,s(?y)) -> +(k,*(k,?y)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(k,+(?x,?y)) -> +(*(k,?x),*(k,?y)) ]
Conjecture Part:
   [ +(?x,?y) = +(?y,?x) ]
Termination proof failed.
examples/fromCops/cr/181.trs: Failure(unknown)
(24 msec.)