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