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