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