YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ not(true) -> false,
     not(false) -> true,
     or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false,
     and(true,true) -> true,
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false,
     not(and(?x,?y)) -> or(not(?x),not(?y)),
     not(or(?x,?y)) -> and(not(?x),not(?y)) ]
Constructors: {true,false}
Defined function symbols: {or,and,not}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ not(true) -> false,
     not(false) -> true,
     or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false,
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false ]
   [ and(true,true) -> true,
     not(and(?x,?y)) -> or(not(?x),not(?y)),
     not(or(?x,?y)) -> and(not(?x),not(?y)) ]
Trying with:
R:
   [ not(true) -> false,
     not(false) -> true,
     or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false,
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false ]
E:
   [ and(true,true) = true,
     not(and(?x,?y)) = or(not(?x),not(?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Bool}
Signature:
   [ not : Bool -> Bool,
     and : Bool,Bool -> Bool,
     or : Bool,Bool -> Bool,
     true : Bool,
     false : Bool ]
Rule Part:
   [ not(true) -> false,
     not(false) -> true,
     or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false,
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false ]
Conjecture Part:
   [ and(true,true) = true,
     not(and(?x,?y)) = or(not(?x),not(?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
Precedence (by weight): {(or,7),(and,6),(not,4),(true,1),(false,0)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ not(true) -> false,
     not(false) -> true,
     or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false,
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false ]
Conjectures:
   [ and(true,true) = true,
     not(and(?x,?y)) = or(not(?x),not(?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
STEP 0
ES:
   [ and(true,true) = true,
     not(and(?x,?y)) = or(not(?x),not(?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS:
   [ ]
ES0:
   [ true = true,
     not(and(?x,?y)) = or(not(?x),not(?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS0:
   [ ]
ES1:
   [ not(and(?x,?y)) = or(not(?x),not(?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS1:
   [ ]
Expand or(not(?x),not(?y)) = not(and(?x,?y))
   [ or(false,not(?y)) = not(and(true,?y)),
     or(true,not(?y)) = not(and(false,?y)) ]
ES2:
   [ or(false,not(?y)) = not(and(true,?y)),
     true = not(and(false,?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS2:
   [ or(not(?x),not(?y)) -> not(and(?x,?y)) ]
STEP 1
ES:
   [ or(false,not(?y)) = not(and(true,?y)),
     true = not(and(false,?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS:
   [ or(not(?x),not(?y)) -> not(and(?x,?y)) ]
ES0:
   [ or(false,not(?y)) = not(?y),
     true = not(and(false,?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS0:
   [ or(not(?x),not(?y)) -> not(and(?x,?y)) ]
ES1:
   [ or(false,not(?y)) = not(?y),
     true = not(and(false,?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS1:
   [ or(not(?x),not(?y)) -> not(and(?x,?y)) ]
Expand not(and(false,?y)) = true
   [ not(false) = true,
     not(false) = true ]
ES2:
   [ true = true,
     true = true,
     not(or(?x,?y)) = and(not(?x),not(?y)),
     or(false,not(?y)) = not(?y) ]
HS2:
   [ not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
STEP 2
ES:
   [ true = true,
     true = true,
     not(or(?x,?y)) = and(not(?x),not(?y)),
     or(false,not(?y)) = not(?y) ]
HS:
   [ not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
ES0:
   [ true = true,
     true = true,
     not(or(?x,?y)) = and(not(?x),not(?y)),
     or(false,not(?y)) = not(?y) ]
HS0:
   [ not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
ES1:
   [ not(or(?x,?y)) = and(not(?x),not(?y)),
     or(false,not(?y)) = not(?y) ]
HS1:
   [ not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
Expand or(false,not(?y)) = not(?y)
   [ or(false,false) = not(true),
     or(false,true) = not(false) ]
ES2:
   [ false = not(true),
     true = not(false),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS2:
   [ or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
STEP 3
ES:
   [ false = not(true),
     true = not(false),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS:
   [ or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
ES0:
   [ false = false,
     true = true,
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS0:
   [ or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
ES1:
   [ not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS1:
   [ or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
Expand not(or(?x,?y)) = and(not(?x),not(?y))
   [ not(true) = and(not(true),not(?y_1)),
     not(true) = and(not(?x_2),not(true)),
     not(false) = and(not(false),not(false)) ]
ES2:
   [ false = and(not(true),not(?y_1)),
     false = and(not(?x_2),not(true)),
     true = and(not(false),not(false)) ]
HS2:
   [ not(or(?x,?y)) -> and(not(?x),not(?y)),
     or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
STEP 4
ES:
   [ false = and(not(true),not(?y_1)),
     false = and(not(?x_2),not(true)),
     true = and(not(false),not(false)) ]
HS:
   [ not(or(?x,?y)) -> and(not(?x),not(?y)),
     or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
ES0:
   [ false = and(false,not(?y_1)),
     false = and(not(?x_2),false),
     true = true ]
HS0:
   [ not(or(?x,?y)) -> and(not(?x),not(?y)),
     or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
ES1:
   [ false = and(false,not(?y_1)),
     false = and(not(?x_2),false) ]
HS1:
   [ not(or(?x,?y)) -> and(not(?x),not(?y)),
     or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
Expand and(false,not(?y_1)) = false
   [ and(false,false) = false,
     and(false,true) = false ]
ES2:
   [ false = false,
     false = false,
     false = and(not(?x_2),false) ]
HS2:
   [ and(false,not(?y_1)) -> false,
     not(or(?x,?y)) -> and(not(?x),not(?y)),
     or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
STEP 5
ES:
   [ false = false,
     false = false,
     false = and(not(?x_2),false) ]
HS:
   [ and(false,not(?y_1)) -> false,
     not(or(?x,?y)) -> and(not(?x),not(?y)),
     or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
ES0:
   [ false = false,
     false = false,
     false = and(not(?x_2),false) ]
HS0:
   [ and(false,not(?y_1)) -> false,
     not(or(?x,?y)) -> and(not(?x),not(?y)),
     or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
ES1:
   [ false = and(not(?x_2),false) ]
HS1:
   [ and(false,not(?y_1)) -> false,
     not(or(?x,?y)) -> and(not(?x),not(?y)),
     or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
Expand and(not(?x_2),false) = false
   [ and(false,false) = false,
     and(true,false) = false ]
ES2:
   [ false = false,
     false = false ]
HS2:
   [ and(not(?x_2),false) -> false,
     and(false,not(?y_1)) -> false,
     not(or(?x,?y)) -> and(not(?x),not(?y)),
     or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
STEP 6
ES:
   [ false = false,
     false = false ]
HS:
   [ and(not(?x_2),false) -> false,
     and(false,not(?y_1)) -> false,
     not(or(?x,?y)) -> and(not(?x),not(?y)),
     or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
ES0:
   [ false = false,
     false = false ]
HS0:
   [ and(not(?x_2),false) -> false,
     and(false,not(?y_1)) -> false,
     not(or(?x,?y)) -> and(not(?x),not(?y)),
     or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
ES1:
   [ ]
HS1:
   [ and(not(?x_2),false) -> false,
     and(false,not(?y_1)) -> false,
     not(or(?x,?y)) -> and(not(?x),not(?y)),
     or(false,not(?y)) -> not(?y),
     not(and(false,?y)) -> true,
     or(not(?x),not(?y)) -> not(and(?x,?y)) ]
Conj part consisits of inductive theorems of R0.
new/and-or.trs: Success(GCR)
(34 msec.)