YES
(ignored inputs)COMMENT translated from Cops 51
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ *(e,?x) -> ?x,
     *(-(?x),?x) -> e,
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(-(?x),*(?x,?y)) -> ?y,
     *(?x,e) -> ?x,
     -(e) -> e,
     -(-(?x)) -> ?x,
     *(?x,-(?x)) -> e,
     *(?x,*(-(?x),?y)) -> ?y,
     -(*(?x,?y)) -> *(-(?y),-(?x)) ]
Constructors: {e}
Defined function symbols: {*,-}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ *(?x,e) -> ?x,
     -(e) -> e ]
   [ *(e,?x) -> ?x,
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     -(-(?x)) -> ?x,
     -(*(?x,?y)) -> *(-(?y),-(?x)),
     *(-(?x),?x) -> e,
     *(-(?x),*(?x,?y)) -> ?y,
     *(?x,-(?x)) -> e,
     *(?x,*(-(?x),?y)) -> ?y ]
Rule part & Conj Part:
   [ *(e,?x) -> ?x,
     -(e) -> e ]
   [ *(?x,e) -> ?x,
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     -(-(?x)) -> ?x,
     -(*(?x,?y)) -> *(-(?y),-(?x)),
     *(-(?x),?x) -> e,
     *(-(?x),*(?x,?y)) -> ?y,
     *(?x,-(?x)) -> e,
     *(?x,*(-(?x),?y)) -> ?y ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Elem}
Signature:
   [ * : Elem,Elem -> Elem,
     - : Elem -> Elem,
     e : Elem ]
Rule Part:
   [ *(?x,e) -> ?x,
     -(e) -> e ]
Conjecture Part:
   [ *(e,?x) = ?x,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(-(?x)) = ?x,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(-(?x),?x) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(?x,-(?x)) = e,
     *(?x,*(-(?x),?y)) = ?y ]
Precedence (by weight): {(*,0),(-,2),(e,1)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ *(?x,e) -> ?x,
     -(e) -> e ]
Conjectures:
   [ *(e,?x) = ?x,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(-(?x)) = ?x,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(-(?x),?x) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(?x,-(?x)) = e,
     *(?x,*(-(?x),?y)) = ?y ]
STEP 0
ES:
   [ *(e,?x) = ?x,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(-(?x)) = ?x,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(-(?x),?x) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(?x,-(?x)) = e,
     *(?x,*(-(?x),?y)) = ?y ]
HS:
   [ ]
ES0:
   [ *(e,?x) = ?x,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(-(?x)) = ?x,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(-(?x),?x) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(?x,-(?x)) = e,
     *(?x,*(-(?x),?y)) = ?y ]
HS0:
   [ ]
ES1:
   [ *(e,?x) = ?x,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(-(?x)) = ?x,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(-(?x),?x) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(?x,-(?x)) = e,
     *(?x,*(-(?x),?y)) = ?y ]
HS1:
   [ ]
Expand *(e,?x) = ?x
   [ e = e ]
ES2:
   [ e = e,
     *(?x,*(-(?x),?y)) = ?y,
     *(?x,-(?x)) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(-(?x),?x) = e,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     -(-(?x)) = ?x,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS2:
   [ *(e,?x) -> ?x ]
STEP 1
ES:
   [ e = e,
     *(?x,*(-(?x),?y)) = ?y,
     *(?x,-(?x)) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(-(?x),?x) = e,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     -(-(?x)) = ?x,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS:
   [ *(e,?x) -> ?x ]
ES0:
   [ e = e,
     *(?x,*(-(?x),?y)) = ?y,
     *(?x,-(?x)) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(-(?x),?x) = e,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     -(-(?x)) = ?x,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS0:
   [ *(e,?x) -> ?x ]
ES1:
   [ *(?x,*(-(?x),?y)) = ?y,
     *(?x,-(?x)) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(-(?x),?x) = e,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     -(-(?x)) = ?x,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS1:
   [ *(e,?x) -> ?x ]
Expand -(-(?x)) = ?x
   [ -(e) = e ]
ES2:
   [ e = e,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     *(?x,-(?x)) = e,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(-(?x),?x) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(?x,*(-(?x),?y)) = ?y ]
HS2:
   [ -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
STEP 2
ES:
   [ e = e,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     *(?x,-(?x)) = e,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(-(?x),?x) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(?x,*(-(?x),?y)) = ?y ]
HS:
   [ -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES0:
   [ e = e,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     *(?x,-(?x)) = e,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(-(?x),?x) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(?x,*(-(?x),?y)) = ?y ]
HS0:
   [ -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES1:
   [ *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     *(?x,-(?x)) = e,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(-(?x),?x) = e,
     *(-(?x),*(?x,?y)) = ?y,
     *(?x,*(-(?x),?y)) = ?y ]
HS1:
   [ -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
Expand *(?x,-(?x)) = e
   [ *(e,e) = e ]
ES2:
   [ e = e,
     *(?x,*(-(?x),?y)) = ?y,
     *(-(?x),*(?x,?y)) = ?y,
     *(-(?x),?x) = e,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS2:
   [ *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
STEP 3
ES:
   [ e = e,
     *(?x,*(-(?x),?y)) = ?y,
     *(-(?x),*(?x,?y)) = ?y,
     *(-(?x),?x) = e,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS:
   [ *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES0:
   [ e = e,
     *(?x,*(-(?x),?y)) = ?y,
     *(-(?x),*(?x,?y)) = ?y,
     *(-(?x),?x) = e,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS0:
   [ *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES1:
   [ *(?x,*(-(?x),?y)) = ?y,
     *(-(?x),*(?x,?y)) = ?y,
     *(-(?x),?x) = e,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS1:
   [ *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
Expand *(-(?x),?x) = e
   [ *(e,e) = e ]
ES2:
   [ e = e,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(?x,*(-(?x),?y)) = ?y,
     *(-(?x),*(?x,?y)) = ?y ]
HS2:
   [ *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
STEP 4
ES:
   [ e = e,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(?x,*(-(?x),?y)) = ?y,
     *(-(?x),*(?x,?y)) = ?y ]
HS:
   [ *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES0:
   [ e = e,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(?x,*(-(?x),?y)) = ?y,
     *(-(?x),*(?x,?y)) = ?y ]
HS0:
   [ *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES1:
   [ *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(?x,*(-(?x),?y)) = ?y,
     *(-(?x),*(?x,?y)) = ?y ]
HS1:
   [ *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
Expand *(?x,*(-(?x),?y)) = ?y
   [ *(e,*(e,?y)) = ?y ]
ES2:
   [ ?y = ?y,
     *(-(?x),*(?x,?y)) = ?y,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS2:
   [ *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
STEP 5
ES:
   [ ?y = ?y,
     *(-(?x),*(?x,?y)) = ?y,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS:
   [ *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES0:
   [ ?y = ?y,
     *(-(?x),*(?x,?y)) = ?y,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS0:
   [ *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES1:
   [ *(-(?x),*(?x,?y)) = ?y,
     -(*(?x,?y)) = *(-(?y),-(?x)),
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS1:
   [ *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
Expand *(-(?x),*(?x,?y)) = ?y
   [ *(e,*(e,?y)) = ?y ]
ES2:
   [ ?y = ?y,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(*(?x,?y)) = *(-(?y),-(?x)) ]
HS2:
   [ *(-(?x),*(?x,?y)) -> ?y,
     *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
STEP 6
ES:
   [ ?y = ?y,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(*(?x,?y)) = *(-(?y),-(?x)) ]
HS:
   [ *(-(?x),*(?x,?y)) -> ?y,
     *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES0:
   [ ?y = ?y,
     *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(*(?x,?y)) = *(-(?y),-(?x)) ]
HS0:
   [ *(-(?x),*(?x,?y)) -> ?y,
     *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES1:
   [ *(*(?x,?y),?z) = *(?x,*(?y,?z)),
     -(*(?x,?y)) = *(-(?y),-(?x)) ]
HS1:
   [ *(-(?x),*(?x,?y)) -> ?y,
     *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
Expand -(*(?x,?y)) = *(-(?y),-(?x))
   [ -(?x_1) = *(-(e),-(?x_1)) ]
ES2:
   [ -(?x_1) = *(-(e),-(?x_1)),
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS2:
   [ -(*(?x,?y)) -> *(-(?y),-(?x)),
     *(-(?x),*(?x,?y)) -> ?y,
     *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
STEP 7
ES:
   [ -(?x_1) = *(-(e),-(?x_1)),
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS:
   [ -(*(?x,?y)) -> *(-(?y),-(?x)),
     *(-(?x),*(?x,?y)) -> ?y,
     *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES0:
   [ -(?x_1) = -(?x_1),
     *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS0:
   [ -(*(?x,?y)) -> *(-(?y),-(?x)),
     *(-(?x),*(?x,?y)) -> ?y,
     *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES1:
   [ *(*(?x,?y),?z) = *(?x,*(?y,?z)) ]
HS1:
   [ -(*(?x,?y)) -> *(-(?y),-(?x)),
     *(-(?x),*(?x,?y)) -> ?y,
     *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
Expand *(*(?x,?y),?z) = *(?x,*(?y,?z))
   [ *(?x_1,?z) = *(?x_1,*(e,?z)) ]
ES2:
   [ *(?x_1,?z) = *(?x_1,*(e,?z)) ]
HS2:
   [ *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     -(*(?x,?y)) -> *(-(?y),-(?x)),
     *(-(?x),*(?x,?y)) -> ?y,
     *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
STEP 8
ES:
   [ *(?x_1,?z) = *(?x_1,*(e,?z)) ]
HS:
   [ *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     -(*(?x,?y)) -> *(-(?y),-(?x)),
     *(-(?x),*(?x,?y)) -> ?y,
     *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES0:
   [ *(?x_1,?z) = *(?x_1,?z) ]
HS0:
   [ *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     -(*(?x,?y)) -> *(-(?y),-(?x)),
     *(-(?x),*(?x,?y)) -> ?y,
     *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
ES1:
   [ ]
HS1:
   [ *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     -(*(?x,?y)) -> *(-(?y),-(?x)),
     *(-(?x),*(?x,?y)) -> ?y,
     *(?x,*(-(?x),?y)) -> ?y,
     *(-(?x),?x) -> e,
     *(?x,-(?x)) -> e,
     -(-(?x)) -> ?x,
     *(e,?x) -> ?x ]
Conj part consisits of inductive theorems of R0.
examples/fromCops/cr/51.trs: Success(GCR)
(7 msec.)