YES
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/and-or.trs
Input rules:
   [ not(true) -> false,
     not(false) -> true,
     or(true,?y:Bool) -> true,
     or(?x:Bool,true) -> true,
     or(false,false) -> false,
     and(true,true) -> true,
     and(?x:Bool,true) -> ?x:Bool,
     and(true,?y:Bool) -> ?y:Bool,
     and(false,false) -> false,
     not(and(?x:Bool,?y:Bool)) -> or(not(?x:Bool),not(?y:Bool)),
     not(or(?x:Bool,?y:Bool)) -> and(not(?x:Bool),not(?y:Bool)) ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ not(true) -> false,
     not(false) -> true,
     or(true,?y:Bool) -> true,
     or(?x:Bool,true) -> true,
     or(false,false) -> false,
     and(true,true) -> true,
     and(?x:Bool,true) -> ?x:Bool,
     and(true,?y:Bool) -> ?y:Bool,
     and(false,false) -> false,
     not(and(?x:Bool,?y:Bool)) -> or(not(?x:Bool),not(?y:Bool)),
     not(or(?x:Bool,?y:Bool)) -> and(not(?x:Bool),not(?y:Bool)) ]
Constructor pattern: [true,false]
Defined pattern: [or(?x_2,?x_3),and(?x_2,?x_3),not(?x_1)]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for or(?x_2,?x_3):
   [ or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false ]
candidate for and(?x_2,?x_3):
   [ and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false ]
candidate for not(?x_1):
   [ not(true) -> false,
     not(false) -> true ]
Find a quasi-ordering ...
order successfully found
Precedence:
 and : Mul;
 false : Mul,  true : Mul;
 or : Mul;
 not : Mul;
Rules:
   [ or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false,
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false,
     not(true) -> false,
     not(false) -> true ]
Conjectures:
   [ not(and(?x,?y)) = or(not(?x),not(?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)),
     and(true,true) = true,
     true = true,
     true = true ]
STEP 0
ES:
   [ not(and(?x,?y)) = or(not(?x),not(?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)),
     and(true,true) = true,
     true = true,
     true = true ]
HS:
   [ ]
ES0:
   [ not(and(?x,?y)) = or(not(?x),not(?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)),
     true = true,
     true = true,
     true = true ]
HS0:
   [ ]
ES1:
   [ not(and(?x,?y)) = or(not(?x),not(?y)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS1:
   [ ]
Expand not(and(?x,?y)) = or(not(?x),not(?y))
   [ not(?x_3) = or(not(?x_3),not(true)),
     not(?y_4) = or(not(true),not(?y_4)),
     not(false) = or(not(false),not(false)) ]
ES2:
   [ not(?x_3) = or(not(?x_3),not(true)),
     not(?y_4) = or(not(true),not(?y_4)),
     true = or(not(false),not(false)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS2:
   [ not(and(?x,?y)) -> or(not(?x),not(?y)) ]
STEP 1
ES:
   [ not(?x_3) = or(not(?x_3),not(true)),
     not(?y_4) = or(not(true),not(?y_4)),
     true = or(not(false),not(false)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS:
   [ not(and(?x,?y)) -> or(not(?x),not(?y)) ]
ES0:
   [ not(?x_3) = or(not(?x_3),false),
     not(?y_4) = or(false,not(?y_4)),
     true = true,
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS0:
   [ not(and(?x,?y)) -> or(not(?x),not(?y)) ]
ES1:
   [ not(?x_3) = or(not(?x_3),false),
     not(?y_4) = or(false,not(?y_4)),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS1:
   [ not(and(?x,?y)) -> or(not(?x),not(?y)) ]
Expand or(not(?x_3),false) = not(?x_3)
   [ or(false,false) = not(true),
     or(true,false) = not(false) ]
ES2:
   [ false = not(true),
     true = not(false),
     not(or(?x,?y)) = and(not(?x),not(?y)),
     not(?y_4) = or(false,not(?y_4)) ]
HS2:
   [ or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
STEP 2
ES:
   [ false = not(true),
     true = not(false),
     not(or(?x,?y)) = and(not(?x),not(?y)),
     not(?y_4) = or(false,not(?y_4)) ]
HS:
   [ or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
ES0:
   [ false = false,
     true = true,
     not(or(?x,?y)) = and(not(?x),not(?y)),
     not(?y_4) = or(false,not(?y_4)) ]
HS0:
   [ or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
ES1:
   [ not(or(?x,?y)) = and(not(?x),not(?y)),
     not(?y_4) = or(false,not(?y_4)) ]
HS1:
   [ or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
Expand or(false,not(?y_4)) = not(?y_4)
   [ 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_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
STEP 3
ES:
   [ false = not(true),
     true = not(false),
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS:
   [ or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
ES0:
   [ false = false,
     true = true,
     not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS0:
   [ or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
ES1:
   [ not(or(?x,?y)) = and(not(?x),not(?y)) ]
HS1:
   [ or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
Expand and(not(?x),not(?y)) = not(or(?x,?y))
   [ and(false,not(?y)) = not(or(true,?y)),
     and(true,not(?y)) = not(or(false,?y)) ]
ES2:
   [ and(false,not(?y)) = not(or(true,?y)),
     not(?y) = not(or(false,?y)) ]
HS2:
   [ and(not(?x),not(?y)) -> not(or(?x,?y)),
     or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
STEP 4
ES:
   [ and(false,not(?y)) = not(or(true,?y)),
     not(?y) = not(or(false,?y)) ]
HS:
   [ and(not(?x),not(?y)) -> not(or(?x,?y)),
     or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
ES0:
   [ and(false,not(?y)) = false,
     not(?y) = not(or(false,?y)) ]
HS0:
   [ and(not(?x),not(?y)) -> not(or(?x,?y)),
     or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
ES1:
   [ and(false,not(?y)) = false,
     not(?y) = not(or(false,?y)) ]
HS1:
   [ and(not(?x),not(?y)) -> not(or(?x,?y)),
     or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
Expand and(false,not(?y)) = false
   [ and(false,false) = false,
     and(false,true) = false ]
ES2:
   [ false = false,
     false = false,
     not(?y) = not(or(false,?y)) ]
HS2:
   [ and(false,not(?y)) -> false,
     and(not(?x),not(?y)) -> not(or(?x,?y)),
     or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
STEP 5
ES:
   [ false = false,
     false = false,
     not(?y) = not(or(false,?y)) ]
HS:
   [ and(false,not(?y)) -> false,
     and(not(?x),not(?y)) -> not(or(?x,?y)),
     or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
ES0:
   [ false = false,
     false = false,
     not(?y) = not(or(false,?y)) ]
HS0:
   [ and(false,not(?y)) -> false,
     and(not(?x),not(?y)) -> not(or(?x,?y)),
     or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
ES1:
   [ not(?y) = not(or(false,?y)) ]
HS1:
   [ and(false,not(?y)) -> false,
     and(not(?x),not(?y)) -> not(or(?x,?y)),
     or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
Expand not(or(false,?y)) = not(?y)
   [ not(true) = not(true),
     not(false) = not(false) ]
ES2:
   [ false = not(true),
     true = not(false) ]
HS2:
   [ not(or(false,?y)) -> not(?y),
     and(false,not(?y)) -> false,
     and(not(?x),not(?y)) -> not(or(?x,?y)),
     or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
STEP 6
ES:
   [ false = not(true),
     true = not(false) ]
HS:
   [ not(or(false,?y)) -> not(?y),
     and(false,not(?y)) -> false,
     and(not(?x),not(?y)) -> not(or(?x,?y)),
     or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
ES0:
   [ false = false,
     true = true ]
HS0:
   [ not(or(false,?y)) -> not(?y),
     and(false,not(?y)) -> false,
     and(not(?x),not(?y)) -> not(or(?x,?y)),
     or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
ES1:
   [ ]
HS1:
   [ not(or(false,?y)) -> not(?y),
     and(false,not(?y)) -> false,
     and(not(?x),not(?y)) -> not(or(?x,?y)),
     or(false,not(?y_4)) -> not(?y_4),
     or(not(?x_3),false) -> not(?x_3),
     not(and(?x,?y)) -> or(not(?x),not(?y)) ]
: Success(GCR)
(22 msec.)