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