============================== Prover9 ===============================
Prover9 (32) version August-2006A, August 2006.
Process 11452 was started by mccune on cleo.thornwood,
Sat Aug 12 21:01:21 2006
The command was "/home/mccune/bin/prover9 -f head.in t2_23.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file head.in

clear(auto_inference).
    % clear(auto_inference) -> clear(predicate_elim).
    % clear(auto_inference) -> assign(eq_defs, pass).
set(predicate_elim).
set(paramodulation).
    % set(paramodulation) -> set(back_demod).
set(hyper_resolution).

formulas(sos).
x ^ y = y ^ x # label("commutativity_meet").
x v y = y v x # label("commutativity_join").
(x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet").
(x v y) v z = x v (y v z) # label("associativity_join").
(x v y) ^ x = x # label("absorption_1").
(x ^ y) v x = x # label("absorption_2").
end_of_list.

formulas(sos).
(all xa all xx all xb (A(xa,xx,xb) <-> xa <= xx & xx <= xb | xb <= xx & xx <= xa)).
(all xa all xx all xb (B(xa,xx,xb) <-> (xa ^ xx) v (xx ^ xb) = xx & (xa v xx) ^ (xx v xb) = xx)).
(all xa all xx all xb (C(xa,xx,xb) <-> (xa ^ xx) v (xx ^ xb) = xx & (xa ^ xb) v xx = xx)).
(all xa all xx all xb (CS(xa,xx,xb) <-> (xa v xx) ^ (xx v xb) = xx & (xa v xb) ^ xx = xx)).
(all xa all xx all xb (D(xa,xx,xb) <-> xa ^ xb <= xx & xx <= xa v xb)).
(all x all y (x <= y <-> x ^ y = x)).
end_of_list.

% Reading from file t2_23.in


formulas(sos).
-D(x,y,z) | A(x,y,z).
B(ca,cx,cb).
B(cx,cb,cy).
cx != cb.
-B(ca,cb,cy).
end_of_list.

============================== end of input ==========================

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:
1 (all xa all xx all xb (A(xa,xx,xb) <-> xa <= xx & xx <= xb | xb <= xx & xx <= xa)).  [assumption].
2 (all xa all xx all xb (B(xa,xx,xb) <-> (xa ^ xx) v (xx ^ xb) = xx & (xa v xx) ^ (xx v xb) = xx)).  [assumption].
3 (all xa all xx all xb (C(xa,xx,xb) <-> (xa ^ xx) v (xx ^ xb) = xx & (xa ^ xb) v xx = xx)).  [assumption].
4 (all xa all xx all xb (CS(xa,xx,xb) <-> (xa v xx) ^ (xx v xb) = xx & (xa v xb) ^ xx = xx)).  [assumption].
5 (all xa all xx all xb (D(xa,xx,xb) <-> xa ^ xb <= xx & xx <= xa v xb)).  [assumption].
6 (all x all y (x <= y <-> x ^ y = x)).  [assumption].

============================== end of process non-clausal formulas ===

============================== PROCESS INITIAL CLAUSES ===============

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
x ^ y = y ^ x # label("commutativity_meet").  [assumption].
x v y = y v x # label("commutativity_join").  [assumption].
(x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet").  [assumption].
(x v y) v z = x v (y v z) # label("associativity_join").  [assumption].
(x v y) ^ x = x # label("absorption_1").  [assumption].
(x ^ y) v x = x # label("absorption_2").  [assumption].
-A(x,y,z) | x <= y | z <= y.  [clausify(1)].
-A(x,y,z) | x <= y | y <= x.  [clausify(1)].
-A(x,y,z) | y <= z | z <= y.  [clausify(1)].
-A(x,y,z) | y <= z | y <= x.  [clausify(1)].
A(x,y,z) | -(x <= y) | -(y <= z).  [clausify(1)].
A(x,y,z) | -(z <= y) | -(y <= x).  [clausify(1)].
-B(x,y,z) | (x ^ y) v (y ^ z) = y.  [clausify(2)].
-B(x,y,z) | (x v y) ^ (y v z) = y.  [clausify(2)].
B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y.  [clausify(2)].
-C(x,y,z) | (x ^ y) v (y ^ z) = y.  [clausify(3)].
-C(x,y,z) | (x ^ z) v y = y.  [clausify(3)].
C(x,y,z) | (x ^ y) v (y ^ z) != y | (x ^ z) v y != y.  [clausify(3)].
-CS(x,y,z) | (x v y) ^ (y v z) = y.  [clausify(4)].
-CS(x,y,z) | (x v z) ^ y = y.  [clausify(4)].
CS(x,y,z) | (x v y) ^ (y v z) != y | (x v z) ^ y != y.  [clausify(4)].
-D(x,y,z) | x ^ z <= y.  [clausify(5)].
-D(x,y,z) | y <= x v z.  [clausify(5)].
D(x,y,z) | -(x ^ z <= y) | -(y <= x v z).  [clausify(5)].
-(x <= y) | x ^ y = x.  [clausify(6)].
x <= y | x ^ y != x.  [clausify(6)].
-D(x,y,z) | A(x,y,z).  [assumption].
B(ca,cx,cb).  [assumption].
B(cx,cb,cy).  [assumption].
cx != cb.  [assumption].
-B(ca,cb,cy).  [assumption].
end_of_list.

formulas(demodulators).
end_of_list.

============================== PREDICATE ELIMINATION =================

Eliminating A/3
7 A(x,y,z) | -(x <= y) | -(y <= z).  [clausify(1)].
8 -A(x,y,z) | x <= y | z <= y.  [clausify(1)].
9 -A(x,y,z) | x <= y | y <= x.  [clausify(1)].
10 -A(x,y,z) | y <= z | z <= y.  [clausify(1)].
11 -A(x,y,z) | y <= z | y <= x.  [clausify(1)].
12 A(x,y,z) | -(z <= y) | -(y <= x).  [clausify(1)].
13 -D(x,y,z) | A(x,y,z).  [assumption].
Derived: -D(x,y,z) | x <= y | z <= y.  [resolve(13,b,8,a)].
Derived: -D(x,y,z) | x <= y | y <= x.  [resolve(13,b,9,a)].
Derived: -D(x,y,z) | y <= z | z <= y.  [resolve(13,b,10,a)].
Derived: -D(x,y,z) | y <= z | y <= x.  [resolve(13,b,11,a)].

Eliminating C/3
14 C(x,y,z) | (x ^ y) v (y ^ z) != y | (x ^ z) v y != y.  [clausify(3)].
15 -C(x,y,z) | (x ^ y) v (y ^ z) = y.  [clausify(3)].
16 -C(x,y,z) | (x ^ z) v y = y.  [clausify(3)].

Eliminating CS/3
17 CS(x,y,z) | (x v y) ^ (y v z) != y | (x v z) ^ y != y.  [clausify(4)].
18 -CS(x,y,z) | (x v y) ^ (y v z) = y.  [clausify(4)].
19 -CS(x,y,z) | (x v z) ^ y = y.  [clausify(4)].

Eliminating D/3
20 D(x,y,z) | -(x ^ z <= y) | -(y <= x v z).  [clausify(5)].
21 -D(x,y,z) | x ^ z <= y.  [clausify(5)].
22 -D(x,y,z) | y <= x v z.  [clausify(5)].
23 -D(x,y,z) | x <= y | z <= y.  [resolve(13,b,8,a)].
Derived: x <= y | z <= y | -(x ^ z <= y) | -(y <= x v z).  [resolve(23,a,20,a)].
24 -D(x,y,z) | x <= y | y <= x.  [resolve(13,b,9,a)].
Derived: x <= y | y <= x | -(x ^ z <= y) | -(y <= x v z).  [resolve(24,a,20,a)].
25 -D(x,y,z) | y <= z | z <= y.  [resolve(13,b,10,a)].
Derived: x <= y | y <= x | -(z ^ y <= x) | -(x <= z v y).  [resolve(25,a,20,a)].
26 -D(x,y,z) | y <= z | y <= x.  [resolve(13,b,11,a)].
Derived: x <= y | x <= z | -(z ^ y <= x) | -(x <= z v y).  [resolve(26,a,20,a)].

============================== end predicate elimination =============

Auto_denials:  (no changes).

Term ordering decisions:
Relation symbol precedence:  lex([ <=, B, =, D, CS, C, A ]).
Function symbol precedence:  lex([ cb, cx, ca, cy, ^, v ]).
After inverse_order:  (no changes).

Auto_process settings:
  % set(factor).  % (non-Horn)
  % set(back_unit_deletion).  % (non-Horn)
    % set(back_unit_deletion) -> set(unit_deletion).

% Operation ^ is commutative; C redundancy checks enabled.

% Operation v is commutative; C redundancy checks enabled.

============================== end of process initial clauses ========

============================== CLAUSES FOR SEARCH ====================

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
27 x ^ y = y ^ x # label("commutativity_meet").  [assumption].
28 x v y = y v x # label("commutativity_join").  [assumption].
29 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet").  [assumption].
30 (x v y) v z = x v (y v z) # label("associativity_join").  [assumption].
32 x ^ (x v y) = x.  [copy(31),rewrite(27(2))].
34 x v (x ^ y) = x.  [copy(33),rewrite(28(2))].
35 -B(x,y,z) | (x ^ y) v (y ^ z) = y.  [clausify(2)].
36 -B(x,y,z) | (x v y) ^ (y v z) = y.  [clausify(2)].
37 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y.  [clausify(2)].
38 -(x <= y) | x ^ y = x.  [clausify(6)].
39 x <= y | x ^ y != x.  [clausify(6)].
40 B(ca,cx,cb).  [assumption].
41 B(cx,cb,cy).  [assumption].
42 cx != cb.  [assumption].
43 -B(ca,cb,cy).  [assumption].
44 x <= y | z <= y | -(x ^ z <= y) | -(y <= x v z).  [resolve(23,a,20,a)].
45 x <= y | y <= x | -(x ^ z <= y) | -(y <= x v z).  [resolve(24,a,20,a)].
46 x <= y | y <= x | -(z ^ y <= x) | -(x <= z v y).  [resolve(25,a,20,a)].
47 x <= y | x <= z | -(z ^ y <= x) | -(x <= z v y).  [resolve(26,a,20,a)].
48 x <= y | -(x ^ x <= y) | -(y <= x v x).  [factor(44,a,b)].
49 x <= x | -(x ^ y <= x) | -(x <= x v y).  [factor(45,a,b)].
50 x <= x | -(y ^ x <= x) | -(x <= y v x).  [factor(46,a,b)].
51 x <= y | -(y ^ y <= x) | -(x <= y v y).  [factor(47,a,b)].
end_of_list.

formulas(demodulators).
27 x ^ y = y ^ x # label("commutativity_meet").  [assumption].
        % (lex-dep)
28 x v y = y v x # label("commutativity_join").  [assumption].
        % (lex-dep)
29 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet").  [assumption].
30 (x v y) v z = x v (y v z) # label("associativity_join").  [assumption].
32 x ^ (x v y) = x.  [copy(31),rewrite(27(2))].
34 x v (x ^ y) = x.  [copy(33),rewrite(28(2))].
end_of_list.

============================== end of clauses for search =============

============================== SEARCH ================================

% Starting search at 0.00 seconds.

given #1 (I,wt=7): 27 x ^ y = y ^ x # label("commutativity_meet").  [assumption].

given #2 (I,wt=7): 28 x v y = y v x # label("commutativity_join").  [assumption].

given #3 (I,wt=11): 29 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet").  [assumption].

% Operation ^ is associative-commutative; CAC redundancy checks enabled.
% back CAC tautology: 52 x ^ (y ^ z) = z ^ (x ^ y).  [para(29(a,1),27(a,1))].

given #4 (I,wt=11): 30 (x v y) v z = x v (y v z) # label("associativity_join").  [assumption].

% Operation v is associative-commutative; CAC redundancy checks enabled.
% back CAC tautology: 54 x v (y v z) = z v (x v y).  [para(30(a,1),28(a,1))].

given #5 (I,wt=7): 32 x ^ (x v y) = x.  [copy(31),rewrite(27(2))].

given #6 (I,wt=7): 34 x v (x ^ y) = x.  [copy(33),rewrite(28(2))].

given #7 (I,wt=13): 35 -B(x,y,z) | (x ^ y) v (y ^ z) = y.  [clausify(2)].

given #8 (I,wt=13): 36 -B(x,y,z) | (x v y) ^ (y v z) = y.  [clausify(2)].

given #9 (I,wt=22): 37 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y.  [clausify(2)].

given #10 (I,wt=8): 38 -(x <= y) | x ^ y = x.  [clausify(6)].

given #11 (I,wt=8): 39 x <= y | x ^ y != x.  [clausify(6)].

given #12 (I,wt=4): 40 B(ca,cx,cb).  [assumption].

given #13 (I,wt=4): 41 B(cx,cb,cy).  [assumption].

given #14 (I,wt=3): 42 cx != cb.  [assumption].

given #15 (I,wt=4): 43 -B(ca,cb,cy).  [assumption].

given #16 (I,wt=16): 44 x <= y | z <= y | -(x ^ z <= y) | -(y <= x v z).  [resolve(23,a,20,a)].

given #17 (I,wt=16): 45 x <= y | y <= x | -(x ^ z <= y) | -(y <= x v z).  [resolve(24,a,20,a)].

given #18 (I,wt=16): 46 x <= y | y <= x | -(z ^ y <= x) | -(x <= z v y).  [resolve(25,a,20,a)].

given #19 (I,wt=16): 47 x <= y | x <= z | -(z ^ y <= x) | -(x <= z v y).  [resolve(26,a,20,a)].

given #20 (T,wt=5): 64 x ^ x = x.  [para(34(a,1),32(a,1,2))].

given #21 (A,wt=11): 53 x ^ (y ^ z) = y ^ (x ^ z).  [para(27(a,1),29(a,1,1)),rewrite(29(2))].

given #22 (F,wt=3): 110 x <= x.  [hyper(39,b,64,a)].

given #23 (F,wt=4): 114 B(x,x,y).  [para(64(a,1),37(b,1,1)),rewrite(34(3),65(3),32(4)),xx(b),xx(c)].

given #24 (T,wt=4): 115 B(x,y,y).  [para(64(a,1),37(b,1,2)),rewrite(28(3),60(3),65(4),27(4),56(4)),xx(b),xx(c)].

given #25 (T,wt=5): 65 x v x = x.  [para(32(a,1),34(a,1,2))].

given #26 (A,wt=11): 55 x v (y v z) = y v (x v z).  [para(28(a,1),30(a,1,1)),rewrite(30(2))].

given #27 (F,wt=5): 80 x <= x v y.  [hyper(39,b,32,a)].

given #28 (F,wt=5): 140 x <= y v x.  [para(28(a,1),80(a,2))].

given #29 (T,wt=5): 144 x ^ y <= x.  [para(34(a,1),140(a,2))].

given #30 (T,wt=5): 147 x ^ y <= y.  [para(27(a,1),144(a,1))].

given #31 (A,wt=7): 56 x ^ (y v x) = x.  [para(28(a,1),32(a,1,2))].

given #32 (F,wt=6): 146 x <= y | y <= x.  [hyper(46,c,144,a,d,80,a)].

given #33 (F,wt=7): 60 x v (y ^ x) = x.  [para(27(a,1),34(a,1,2))].

given #34 (T,wt=7): 142 x <= y v (x v z).  [para(55(a,1),80(a,2))].

given #35 (T,wt=7): 143 x <= y v (z v x).  [para(30(a,1),140(a,2))].

given #36 (A,wt=11): 57 x ^ ((x v y) ^ z) = x ^ z.  [para(32(a,1),29(a,1,1)),flip(a)].

given #37 (F,wt=7): 149 x ^ (y ^ z) <= y.  [para(53(a,1),144(a,1))].

given #38 (F,wt=7): 150 x ^ (y ^ z) <= z.  [para(29(a,1),147(a,1))].

given #39 (T,wt=7): 190 x ^ y <= z v x.  [para(34(a,1),143(a,2,2))].

given #40 (T,wt=7): 192 x ^ y <= z v y.  [para(60(a,1),143(a,2,2))].

given #41 (A,wt=13): 58 x ^ (y ^ ((x ^ y) v z)) = x ^ y.  [para(32(a,1),29(a,1)),flip(a)].

given #42 (F,wt=7): 210 x ^ y <= x v z.  [para(57(a,1),149(a,1))].

given #43 (F,wt=7): 216 x ^ y <= y v z.  [para(32(a,1),150(a,1,2))].

given #44 (T,wt=8): 81 x <= y | y ^ x != x.  [para(27(a,1),39(b,1))].

given #45 (T,wt=8): 172 x ^ y = x | y <= x.  [hyper(38,a,146,a)].

given #46 (A,wt=13): 59 (x v y) ^ (x v (y v z)) = x v y.  [para(30(a,1),32(a,1,2))].

given #47 (F,wt=6): 287 x <= y | y != x.  [para(172(a,1),81(b,1)),merge(b)].

given #48 (F,wt=7): 304 x v y <= y v x.  [hyper(287,b,28,a)].

given #49 (T,wt=7): 305 x ^ y <= y ^ x.  [hyper(287,b,27,a)].

given #50 (T,wt=8): 269 x <= y | x ^ y = y.  [para(172(a,1),27(a,1)),flip(b)].

given #51 (A,wt=13): 61 (x ^ y) v (x ^ (y ^ z)) = x ^ y.  [para(29(a,1),34(a,1,2))].

given #52 (F,wt=8): 279 x <= y | x v y = x.  [para(172(a,1),60(a,1,2))].

given #53 (F,wt=8): 282 x ^ y <= z | z <= x.  [para(172(a,1),149(a,1))].

given #54 (T,wt=8): 283 x <= y | z ^ y <= x.  [para(172(a,1),150(a,1,2))].

given #55 (T,wt=8): 284 x <= y | y <= z v x.  [para(172(a,1),192(a,1))].

given #56 (A,wt=11): 62 x v ((x ^ y) v z) = x v z.  [para(34(a,1),30(a,1,1)),flip(a)].

given #57 (F,wt=8): 286 x <= y | y <= x v z.  [para(172(a,1),216(a,1))].

given #58 (F,wt=8): 301 x <= x ^ y | y <= x.  [hyper(287,b,172,a)].

given #59 (T,wt=8): 313 x <= y | y <= x ^ y.  [para(172(a,1),305(a,1))].

given #60 (T,wt=8): 338 x v y <= x | x <= y.  [hyper(287,b,279,b(flip))].

given #61 (A,wt=13): 63 x v (y v ((x v y) ^ z)) = x v y.  [para(34(a,1),30(a,1)),flip(a)].

given #62 (F,wt=8): 339 x <= y | y v x = x.  [para(279(b,1),28(a,1)),flip(b)].

given #63 (F,wt=8): 350 x <= y | y v x <= x.  [para(279(b,1),304(a,2))].

given #64 (T,wt=9): 84 (cb v cx) ^ (cx v ca) = cx.  [hyper(36,a,40,a),rewrite(28(3),28(6),27(7))].

given #65 (T,wt=4): 576 B(cb,cx,ca).  [para(84(a,1),37(c,1)),rewrite(85(11)),xx(b),xx(c)].

given #66 (A,wt=22): 66 B(x,y,z) | (y ^ x) v (y ^ z) != y | (x v y) ^ (y v z) != y.  [para(27(a,1),37(b,1,1))].

given #67 (F,wt=9): 85 (cb ^ cx) v (cx ^ ca) = cx.  [hyper(35,a,40,a),rewrite(27(3),27(6),28(7))].

given #68 (F,wt=9): 86 (cb v cx) ^ (cb v cy) = cb.  [hyper(36,a,41,a),rewrite(28(3))].

given #69 (T,wt=9): 87 (cb ^ cx) v (cb ^ cy) = cb.  [hyper(35,a,41,a),rewrite(27(3))].

given #70 (T,wt=9): 111 x ^ (x ^ y) = x ^ y.  [para(64(a,1),29(a,1,1)),flip(a)].

given #71 (A,wt=22): 67 B(x,y,z) | (x ^ y) v (z ^ y) != y | (x v y) ^ (y v z) != y.  [para(27(a,1),37(b,1,2))].

given #72 (F,wt=9): 113 x ^ (y ^ x) = y ^ x.  [para(64(a,1),29(a,2,2)),rewrite(27(2))].

given #73 (F,wt=9): 119 x v (y ^ (x ^ z)) = x.  [para(53(a,1),34(a,1,2))].

given #74 (T,wt=9): 127 x v (x v y) = x v y.  [para(65(a,1),30(a,1,1)),flip(a)].

given #75 (T,wt=9): 129 x v (y v x) = y v x.  [para(65(a,1),30(a,2,2)),rewrite(28(2))].

given #76 (A,wt=22): 68 B(x,y,z) | (x ^ y) v (y ^ z) != y | (y v z) ^ (x v y) != y.  [para(27(a,1),37(c,1))].

given #77 (F,wt=9): 132 x ^ (y v (x v z)) = x.  [para(55(a,1),32(a,1,2))].

given #78 (F,wt=9): 141 x v y <= x v (y v z).  [para(30(a,1),80(a,2))].

given #79 (T,wt=9): 145 x v y <= x v (z v y).  [para(55(a,1),140(a,2))].

given #80 (T,wt=9): 148 x ^ (y ^ z) <= x ^ y.  [para(29(a,1),144(a,1))].

given #81 (A,wt=22): 69 B(x,y,z) | (y ^ z) v (x ^ y) != y | (x v y) ^ (y v z) != y.  [para(28(a,1),37(b,1))].

given #82 (F,wt=9): 151 x ^ (y ^ z) <= x ^ z.  [para(53(a,1),147(a,1))].

given #83 (F,wt=9): 154 x ^ (y v (z v x)) = x.  [para(30(a,1),56(a,1,2))].

given #84 (T,wt=9): 173 x v (y ^ (z ^ x)) = x.  [para(29(a,1),60(a,1,2))].

given #85 (T,wt=9): 185 x <= y v (z v (x v u)).  [para(30(a,1),142(a,2))].

given #86 (A,wt=22): 70 B(x,y,z) | (x ^ y) v (y ^ z) != y | (y v x) ^ (y v z) != y.  [para(28(a,1),37(c,1,1))].

given #87 (F,wt=9): 189 x <= y v (z v (u v x)).  [para(30(a,1),143(a,2,2))].

given #88 (F,wt=9): 202 x ^ y <= (x v z) ^ y.  [para(57(a,1),147(a,1))].

given #89 (T,wt=9): 209 x ^ (y ^ (z ^ u)) <= z.  [para(29(a,1),149(a,1))].

given #90 (T,wt=9): 215 x ^ (y ^ (z ^ u)) <= u.  [para(29(a,1),150(a,1,2))].

given #91 (A,wt=22): 71 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (z v y) != y.  [para(28(a,1),37(c,1,2))].

given #92 (F,wt=9): 222 x ^ y <= z v (u v x).  [para(30(a,1),190(a,2))].

given #93 (F,wt=9): 223 x ^ (y ^ z) <= u v y.  [para(53(a,1),190(a,1))].

given #94 (T,wt=9): 229 x ^ (y ^ z) <= u v z.  [para(29(a,1),192(a,1))].

given #95 (T,wt=9): 230 x ^ y <= z v (u v y).  [para(30(a,1),192(a,2))].

given #96 (A,wt=28): 72 B(x ^ y,z,u) | (x ^ (y ^ z)) v (z ^ u) != z | ((x ^ y) v z) ^ (z v u) != z.  [para(29(a,1),37(b,1,1))].

given #97 (F,wt=9): 253 x ^ (y ^ z) <= y v u.  [para(53(a,1),210(a,1))].

given #98 (F,wt=9): 254 x ^ y <= z v (x v u).  [para(55(a,1),210(a,2))].

given #99 (T,wt=9): 257 x ^ (y ^ z) <= z v u.  [para(29(a,1),216(a,1))].

given #100 (T,wt=9): 260 x ^ y <= z v (y v u).  [para(55(a,1),216(a,2))].

given #101 (A,wt=36): 73 B(x,y ^ z,u) | (x ^ (y ^ z)) v (y ^ (z ^ u)) != y ^ z | (x v (y ^ z)) ^ ((y ^ z) v u) != y ^ z.  [para(29(a,1),37(b,1,2))].

given #102 (F,wt=9): 381 x <= y | y <= z | z <= x.  [para(269(b,1),282(a,1))].

given #103 (F,wt=9): 446 (x ^ y) v z <= x v z.  [para(62(a,1),140(a,2))].

given #104 (T,wt=9): 581 cb ^ (cx v ca) = cb ^ cx.  [para(84(a,1),57(a,1,2)),flip(a)].

given #105 (T,wt=9): 638 cb v (cx ^ ca) = cb v cx.  [para(85(a,1),62(a,1,2)),flip(a)].

given #106 (A,wt=28): 74 B(x v y,z,u) | ((x v y) ^ z) v (z ^ u) != z | (x v (y v z)) ^ (z v u) != z.  [para(30(a,1),37(c,1,1))].

given #107 (F,wt=9): 781 x v y <= y v (x v z).  [para(28(a,1),141(a,1))].

given #108 (F,wt=9): 782 x v y <= y v (z v x).  [para(28(a,1),141(a,2)),rewrite(30(3))].

given #109 (T,wt=9): 798 x v y <= z v (y v x).  [para(28(a,1),145(a,2)),rewrite(30(3))].

given #110 (T,wt=9): 801 x v (y ^ z) <= x v y.  [para(34(a,1),145(a,2,2))].

given #111 (A,wt=36): 75 B(x,y v z,u) | (x ^ (y v z)) v ((y v z) ^ u) != y v z | (x v (y v z)) ^ (y v (z v u)) != y v z.  [para(30(a,1),37(c,1,2))].

given #112 (F,wt=9): 803 x v (y ^ z) <= x v z.  [para(60(a,1),145(a,2,2))].

given #113 (F,wt=7): 1527 cx <= ca v (cb ^ cx).  [para(85(a,1),803(a,1)),rewrite(28(6))].

given #114 (T,wt=7): 1529 cb <= cy v (cb ^ cx).  [para(87(a,1),803(a,1)),rewrite(28(6))].

given #115 (T,wt=7): 1533 cb v cx <= cb v ca.  [para(638(a,1),803(a,1))].

given #116 (A,wt=14): 82 x ^ y <= z | x ^ (y ^ z) != x ^ y.  [para(29(a,1),39(b,1))].

given #117 (F,wt=8): 1538 cx <= cb ^ cx | cx <= ca.  [hyper(47,c,283,b,d,1527,a),merge(c)].

given #118 (F,wt=6): 1580 cx <= cb | cx <= ca.  [para(172(a,1),1538(a,2)),merge(b)].

given #119 (T,wt=8): 1540 cx <= cb | cx <= cb v ca.  [para(172(a,1),1527(a,2,2)),rewrite(28(7))].

given #120 (T,wt=6): 1583 cb <= ca | cx <= cb.  [para(279(b,1),1540(b,2)),merge(c)].

given #121 (A,wt=16): 88 x <= y | z <= y | -(z ^ x <= y) | -(y <= x v z).  [para(27(a,1),44(c,1))].

given #122 (F,wt=8): 1541 ca <= cb ^ cx | cx <= ca.  [para(279(b,1),1527(a,2))].

given #123 (F,wt=8): 1547 cb <= cb ^ cx | cb <= cy.  [hyper(47,c,283,b,d,1529,a),merge(c)].

given #124 (T,wt=6): 1615 cb <= cx | cb <= cy.  [para(269(b,1),1547(a,2)),merge(b)].

given #125 (T,wt=8): 1549 cb <= cx | cb <= cx v cy.  [para(269(b,1),1529(a,2,2)),rewrite(28(7))].

given #126 (A,wt=22): 89 x ^ y <= z | u <= z | -(x ^ (y ^ u) <= z) | -(z <= (x ^ y) v u).  [para(29(a,1),44(c,1))].

given #127 (F,wt=6): 1618 cx <= cy | cb <= cx.  [para(279(b,1),1549(b,2)),merge(c)].

given #128 (F,wt=8): 1550 cy <= cb ^ cx | cb <= cy.  [para(279(b,1),1529(a,2))].

given #129 (T,wt=8): 1560 cb <= ca | cb v cx <= cb.  [para(279(b,1),1533(a,2))].

given #130 (T,wt=8): 1561 ca <= cb | cb v cx <= ca.  [para(339(b,1),1533(a,2))].

given #131 (A,wt=22): 90 x v y <= z | u <= z | -((x v y) ^ u <= z) | -(z <= x v (y v u)).  [para(30(a,1),44(d,2))].

given #132 (F,wt=8): 1579 cb ^ cx = cx | cx <= ca.  [hyper(38,a,1538,a),rewrite(113(5))].

given #133 (F,wt=6): 1925 cx <= ca | ca <= cb.  [factor(1890,a,b)].

given #134 (T,wt=8): 1581 cx ^ ca = cx | cx <= cb.  [hyper(38,a,1580,b)].

given #135 (T,wt=8): 1584 cb ^ cx = cx | cb <= ca.  [hyper(38,a,1583,b),rewrite(27(3))].

given #136 (A,wt=16): 105 x <= y | x <= z | -(y ^ z <= x) | -(x <= z v y).  [para(27(a,1),47(c,1))].

given #137 (F,wt=8): 1614 cb ^ cx = cb | cb <= cy.  [hyper(38,a,1547,a),rewrite(111(5))].

given #138 (F,wt=6): 2074 cb <= cy | cx <= ca.  [para(1614(a,1),1579(a,1)),flip(b),unit_del(b,42)].

given #139 (T,wt=6): 2075 cb <= cy | cb <= ca.  [para(1614(a,1),1584(a,1)),flip(b),unit_del(b,42)].

given #140 (T,wt=6): 2076 cb <= cy | cy <= cx.  [factor(2045,a,c)].

given #141 (A,wt=22): 106 x <= y | x <= z ^ u | -(z ^ (u ^ y) <= x) | -(x <= (z ^ u) v y).  [para(29(a,1),47(c,1))].

given #142 (F,wt=8): 1616 cb ^ cy = cb | cb <= cx.  [hyper(38,a,1615,b)].

given #143 (F,wt=8): 1800 cx ^ cy = cx | cb <= cx.  [hyper(38,a,1618,a)].

given #144 (T,wt=8): 1802 cb v cx = cb | cb <= ca.  [hyper(38,a,1560,b),rewrite(27(5),32(5)),flip(a)].

given #145 (T,wt=8): 1881 cx <= ca | cb v cx = cb.  [para(1579(a,1),34(a,1,2))].

given #146 (A,wt=22): 107 x <= y | x <= z v u | -((z v u) ^ y <= x) | -(x <= z v (u v y)).  [para(30(a,1),47(d,2))].

given #147 (F,wt=8): 1886 cx <= ca | x ^ cx <= cb.  [para(1579(a,1),149(a,1,2))].

given #148 (F,wt=8): 1887 cx <= ca | cx <= x v cb.  [para(1579(a,1),190(a,1))].

given #149 (T,wt=8): 1888 cx <= ca | cx <= cb v x.  [para(1579(a,1),210(a,1))].

given #150 (T,wt=8): 1919 cx <= ca | cb <= cx v cy.  [para(1579(a,1),1529(a,2,2)),rewrite(28(7))].

given #151 (A,wt=15): 116 B(x,y,y ^ z) | (x ^ y) v (y ^ z) != y.  [back_rewrite(79),rewrite(111(5))].

given #152 (F,wt=6): 2557 B(cb,cx,cx ^ ca).  [hyper(116,b,85,a)].

given #153 (F,wt=8): 1927 cb ^ ca = ca | cx <= ca.  [hyper(38,a,1925,b),rewrite(27(3))].

given #154 (T,wt=8): 1928 cx <= cx ^ ca | cx <= cb.  [hyper(287,b,1581,a)].

given #155 (T,wt=8): 1935 cx <= cb | cx v ca = ca.  [para(1581(a,1),60(a,1,2)),rewrite(28(6))].

given #156 (A,wt=17): 117 B(x,x ^ y,z) | x ^ ((x ^ y) v z) != x ^ y.  [back_rewrite(78),rewrite(111(4),61(6)),xx(b)].

given #157 (F,wt=8): 1936 cx <= cb | x ^ cx <= ca.  [para(1581(a,1),150(a,1,2))].

given #158 (F,wt=8): 1937 cx <= cb | cx <= x v ca.  [para(1581(a,1),192(a,1))].

given #159 (T,wt=8): 1938 cx <= cb | cx <= ca v x.  [para(1581(a,1),216(a,1))].

given #160 (T,wt=8): 1968 cx <= cb ^ cx | cb <= ca.  [hyper(287,b,1584,a)].

given #161 (A,wt=11): 118 x ^ (y ^ (x v z)) = y ^ x.  [para(32(a,1),53(a,1,2)),flip(a)].

given #162 (F,wt=8): 1975 cb <= ca | x ^ cx <= cb.  [para(1584(a,1),149(a,1,2))].

given #163 (F,wt=8): 1976 cb <= ca | cx <= x v cb.  [para(1584(a,1),190(a,1))].

given #164 (T,wt=8): 1977 cb <= ca | cx <= cb v x.  [para(1584(a,1),210(a,1))].

given #165 (T,wt=8): 2008 cb <= ca | cb <= cx v cy.  [para(1584(a,1),1529(a,2,2)),rewrite(28(7))].

given #166 (A,wt=36): 120 B(x,y ^ z,u) | (y ^ (x ^ z)) v (y ^ (z ^ u)) != y ^ z | (x v (y ^ z)) ^ ((y ^ z) v u) != y ^ z.  [para(53(a,1),37(b,1,1)),rewrite(29(6))].

given #167 (F,wt=8): 2041 cb <= cy | cb v cx = cx.  [para(1614(a,1),60(a,1,2)),rewrite(28(6))].

given #168 (F,wt=8): 2042 cb <= cy | x ^ cb <= cx.  [para(1614(a,1),150(a,1,2))].

given #169 (T,wt=8): 2043 cb <= cy | cb <= x v cx.  [para(1614(a,1),192(a,1))].

given #170 (T,wt=8): 2044 cb <= cy | cb <= cx v x.  [para(1614(a,1),216(a,1))].

given #171 (A,wt=28): 121 B(x,y,z ^ u) | (x ^ y) v (z ^ (y ^ u)) != y | (x v y) ^ (y v (z ^ u)) != y.  [para(53(a,1),37(b,1,2))].

given #172 (F,wt=8): 2071 cb <= cy | cx <= cb v ca.  [para(1614(a,1),1527(a,2,2)),rewrite(28(7))].

given #173 (F,wt=8): 2077 cx ^ ca = cx | cb <= cy.  [hyper(38,a,2074,b)].

given #174 (T,wt=8): 2078 cb ^ cy = cb | cb <= ca.  [hyper(38,a,2075,a)].

given #175 (T,wt=6): 3110 cb <= ca | ca <= cy.  [factor(3068,a,c)].

given #176 (A,wt=12): 122 x <= y ^ z | y ^ (x ^ z) != x.  [para(53(a,1),39(b,1))].

given #177 (F,wt=8): 2079 cx ^ cy = cy | cb <= cy.  [hyper(38,a,2076,b),rewrite(27(3))].

given #178 (F,wt=8): 2155 cb <= cb ^ cy | cb <= cx.  [hyper(287,b,1616,a)].

given #179 (T,wt=8): 2162 cb <= cx | cb v cy = cy.  [para(1616(a,1),60(a,1,2)),rewrite(28(6))].

given #180 (T,wt=8): 2163 cb <= cx | x ^ cb <= cy.  [para(1616(a,1),150(a,1,2))].

given #181 (A,wt=22): 123 x <= y | z ^ u <= y | -(z ^ (x ^ u) <= y) | -(y <= x v (z ^ u)).  [para(53(a,1),44(c,1))].

given #182 (F,wt=8): 2164 cb <= cx | cb <= x v cy.  [para(1616(a,1),192(a,1))].

given #183 (F,wt=8): 2165 cb <= cx | cb <= cy v x.  [para(1616(a,1),216(a,1))].

given #184 (T,wt=8): 2198 cx <= cx ^ cy | cb <= cx.  [hyper(287,b,1800,a)].

given #185 (T,wt=8): 2205 cb <= cx | cx v cy = cy.  [para(1800(a,1),60(a,1,2)),rewrite(28(6))].

given #186 (A,wt=22): 126 x <= y ^ z | x <= u | -(y ^ (u ^ z) <= x) | -(x <= u v (y ^ z)).  [para(53(a,1),47(c,1))].

given #187 (F,wt=8): 2206 cb <= cx | x ^ cx <= cy.  [para(1800(a,1),150(a,1,2))].

given #188 (F,wt=8): 2207 cb <= cx | cx <= x v cy.  [para(1800(a,1),192(a,1))].

given #189 (T,wt=8): 2208 cb <= cx | cx <= cy v x.  [para(1800(a,1),216(a,1))].

given #190 (T,wt=8): 2246 cb <= ca | cx ^ x <= cb.  [para(1802(a,1),190(a,2))].

given #191 (A,wt=15): 130 B(x,y,y v z) | (x v y) ^ (y v z) != y.  [back_rewrite(77),rewrite(127(5))].

given #192 (F,wt=6): 3562 B(cb,cx,cx v ca).  [hyper(130,b,84,a)].

given #193 (F,wt=8): 2275 cb v cx <= cb | cx <= ca.  [hyper(287,b,1881,b(flip))].

given #194 (T,wt=8): 2281 cx <= ca | cx ^ x <= cb.  [para(1881(b,1),190(a,2))].

given #195 (T,wt=8): 2591 ca <= cb ^ ca | cx <= ca.  [hyper(287,b,1927,a)].

given #196 (A,wt=17): 131 B(x,x v y,z) | x v ((x v y) ^ z) != x v y.  [back_rewrite(76),rewrite(127(9),59(11)),xx(c)].

given #197 (F,wt=8): 2594 cx <= ca | cb v ca = cb.  [para(1927(a,1),34(a,1,2))].

given #198 (F,wt=8): 2599 cx <= ca | x ^ ca <= cb.  [para(1927(a,1),149(a,1,2))].

given #199 (T,wt=8): 2600 cx <= ca | ca <= x v cb.  [para(1927(a,1),190(a,1))].

given #200 (T,wt=8): 2601 cx <= ca | ca <= cb v x.  [para(1927(a,1),210(a,1))].

given #201 (A,wt=11): 133 x v (y v (x ^ z)) = y v x.  [para(34(a,1),55(a,1,2)),flip(a)].

given #202 (F,wt=8): 2641 cx v ca <= ca | cx <= cb.  [hyper(287,b,1935,b(flip))].

given #203 (F,wt=8): 2648 cx <= cb | cx ^ x <= ca.  [para(1935(b,1),210(a,2))].

given #204 (T,wt=8): 2701 B(cb,cb ^ cx,cx ^ ca).  [para(85(a,1),117(b,1,2)),xx(b)].

given #205 (T,wt=8): 2884 cb v cx <= cx | cb <= cy.  [hyper(287,b,2041,b(flip))].

given #206 (A,wt=36): 134 B(x,y v z,u) | (x ^ (y v z)) v ((y v z) ^ u) != y v z | (y v (x v z)) ^ (y v (z v u)) != y v z.  [para(55(a,1),37(c,1,1)),rewrite(30(13))].

given #207 (F,wt=8): 2891 cb <= cy | cb ^ x <= cx.  [para(2041(b,1),210(a,2))].

given #208 (F,wt=8): 3000 cx <= cx ^ ca | cb <= cy.  [hyper(287,b,2077,a)].

given #209 (T,wt=8): 3007 cb <= cy | cx v ca = ca.  [para(2077(a,1),60(a,1,2)),rewrite(28(6))].

given #210 (T,wt=8): 3008 cb <= cy | x ^ cx <= ca.  [para(2077(a,1),150(a,1,2))].

given #211 (A,wt=28): 135 B(x,y,z v u) | (x ^ y) v (y ^ (z v u)) != y | (x v y) ^ (z v (y v u)) != y.  [para(55(a,1),37(c,1,2))].

given #212 (F,wt=8): 3009 cb <= cy | cx <= x v ca.  [para(2077(a,1),192(a,1))].

given #213 (F,wt=8): 3010 cb <= cy | cx <= ca v x.  [para(2077(a,1),216(a,1))].

given #214 (T,wt=8): 3056 cb <= cb ^ cy | cb <= ca.  [hyper(287,b,2078,a)].

given #215 (T,wt=8): 3063 cb <= ca | cb v cy = cy.  [para(2078(a,1),60(a,1,2)),rewrite(28(6))].

given #216 (A,wt=22): 136 x <= y | z v u <= y | -(x ^ (z v u) <= y) | -(y <= z v (x v u)).  [para(55(a,1),44(d,2))].

given #217 (F,wt=6): 4003 cb <= ca | cx <= cy.  [para(3063(b,1),1977(b,2)),merge(b)].

given #218 (F,wt=8): 3064 cb <= ca | x ^ cb <= cy.  [para(2078(a,1),150(a,1,2))].

given #219 (T,wt=8): 3065 cb <= ca | cb <= x v cy.  [para(2078(a,1),192(a,1))].

given #220 (T,wt=8): 3066 cb <= ca | cb <= cy v x.  [para(2078(a,1),216(a,1))].

given #221 (A,wt=22): 139 x <= y v z | x <= u | -(u ^ (y v z) <= x) | -(x <= y v (u v z)).  [para(55(a,1),47(d,2))].

given #222 (F,wt=8): 3112 ca ^ cy = ca | cb <= ca.  [hyper(38,a,3110,b)].

given #223 (F,wt=8): 3137 cy <= cx ^ cy | cb <= cy.  [hyper(287,b,2079,a)].

given #224 (T,wt=8): 3140 cb <= cy | cx v cy = cx.  [para(2079(a,1),34(a,1,2))].

given #225 (T,wt=8): 3145 cb <= cy | x ^ cy <= cx.  [para(2079(a,1),149(a,1,2))].

given #226 (A,wt=11): 152 x ^ ((y v x) ^ z) = x ^ z.  [para(56(a,1),29(a,1,1)),flip(a)].

given #227 (F,wt=8): 3146 cb <= cy | cy <= x v cx.  [para(2079(a,1),190(a,1))].

given #228 (F,wt=8): 3147 cb <= cy | cy <= cx v x.  [para(2079(a,1),210(a,1))].

given #229 (T,wt=6): 4555 cb <= cy | cy <= ca.  [para(3007(b,1),3147(b,2)),merge(b)].

given #230 (T,wt=8): 3197 cb v cy <= cy | cb <= cx.  [hyper(287,b,2162,b(flip))].

given #231 (A,wt=13): 153 x ^ (y ^ (z v (x ^ y))) = x ^ y.  [para(56(a,1),29(a,1)),flip(a)].

given #232 (F,wt=8): 3204 cb <= cx | cb ^ x <= cy.  [para(2162(b,1),210(a,2))].

given #233 (F,wt=8): 3448 cx v cy <= cy | cb <= cx.  [hyper(287,b,2205,b(flip))].

given #234 (T,wt=8): 3455 cb <= cx | cx ^ x <= cy.  [para(2205(b,1),210(a,2))].

given #235 (T,wt=8): 3611 B(cb,cb v cx,cx v ca).  [para(84(a,1),131(b,1,2)),xx(b)].

given #236 (A,wt=17): 155 B(x,y v x,z) | x v ((y v x) ^ z) != y v x.  [para(56(a,1),37(b,1,1)),rewrite(129(9),30(10),59(11)),xx(c)].

given #237 (F,wt=8): 3631 cb v ca <= cb | cx <= ca.  [hyper(287,b,2594,b(flip))].

given #238 (F,wt=8): 3637 cx <= ca | ca ^ x <= cb.  [para(2594(b,1),190(a,2))].

given #239 (T,wt=8): 3831 cx v ca <= ca | cb <= cy.  [hyper(287,b,3007,b(flip))].

given #240 (T,wt=8): 3838 cb <= cy | cx ^ x <= ca.  [para(3007(b,1),210(a,2))].

given #241 (A,wt=15): 156 B(x,y,z v y) | (x v y) ^ (z v y) != y.  [para(56(a,1),37(b,1,2)),rewrite(28(4),60(4),129(6)),xx(b)].

given #242 (F,wt=8): 3963 cb v cy <= cy | cb <= ca.  [hyper(287,b,3063,b(flip))].

given #243 (F,wt=8): 3970 cb <= ca | cb ^ x <= cy.  [para(3063(b,1),210(a,2))].

given #244 (T,wt=8): 4095 cx ^ cy = cx | cb <= ca.  [hyper(38,a,4003,b)].

given #245 (T,wt=8): 4371 ca <= ca ^ cy | cb <= ca.  [hyper(287,b,3112,a)].

given #246 (A,wt=11): 157 B(x,y,x v y) | x v y != y.  [para(56(a,1),37(c,1)),rewrite(56(5),28(4),60(4)),xx(b)].

given #247 (F,wt=8): 4378 cb <= ca | ca v cy = cy.  [para(3112(a,1),60(a,1,2)),rewrite(28(6))].

given #248 (F,wt=8): 4379 cb <= ca | x ^ ca <= cy.  [para(3112(a,1),150(a,1,2))].

given #249 (T,wt=8): 4380 cb <= ca | ca <= x v cy.  [para(3112(a,1),192(a,1))].

given #250 (T,wt=8): 4381 cb <= ca | ca <= cy v x.  [para(3112(a,1),216(a,1))].

given #251 (A,wt=11): 158 x ^ (y ^ (z v x)) = y ^ x.  [para(56(a,1),53(a,1,2)),flip(a)].

given #252 (F,wt=8): 4433 cx v cy <= cx | cb <= cy.  [hyper(287,b,3140,b(flip))].

given #253 (F,wt=8): 4438 cb <= cy | cy ^ x <= cx.  [para(3140(b,1),190(a,2))].

given #254 (T,wt=8): 4556 ca ^ cy = cy | cb <= cy.  [hyper(38,a,4555,b),rewrite(27(3))].

given #255 (T,wt=8): 4644 B(cx,cb v cx,cb v cy).  [para(86(a,1),155(b,1,2)),rewrite(28(11)),xx(b)].

given #256 (A,wt=13): 159 (x v y) ^ (x v (z v y)) = x v y.  [para(55(a,1),56(a,1,2))].

given #257 (F,wt=8): 4717 cx <= cx ^ cy | cb <= ca.  [hyper(287,b,4095,a)].

given #258 (F,wt=8): 4724 cb <= ca | cx v cy = cy.  [para(4095(a,1),60(a,1,2)),rewrite(28(6))].

given #259 (T,wt=8): 4725 cb <= ca | x ^ cx <= cy.  [para(4095(a,1),150(a,1,2))].

given #260 (T,wt=8): 4726 cb <= ca | cx <= x v cy.  [para(4095(a,1),192(a,1))].

given #261 (A,wt=11): 174 x v ((y ^ x) v z) = x v z.  [para(60(a,1),30(a,1,1)),flip(a)].

given #262 (F,wt=8): 4727 cb <= ca | cx <= cy v x.  [para(4095(a,1),216(a,1))].

given #263 (F,wt=8): 4795 ca v cy <= cy | cb <= ca.  [hyper(287,b,4378,b(flip))].

given #264 (T,wt=8): 4802 cb <= ca | ca ^ x <= cy.  [para(4378(b,1),210(a,2))].

given #265 (T,wt=8): 4954 cy <= ca ^ cy | cb <= cy.  [hyper(287,b,4556,a)].

given #266 (A,wt=13): 175 x v (y v (z ^ (x v y))) = x v y.  [para(60(a,1),30(a,1)),flip(a)].

given #267 (F,wt=8): 4957 cb <= cy | ca v cy = ca.  [para(4556(a,1),34(a,1,2))].

given #268 (F,wt=8): 4962 cb <= cy | x ^ cy <= ca.  [para(4556(a,1),149(a,1,2))].

given #269 (T,wt=8): 4963 cb <= cy | cy <= x v ca.  [para(4556(a,1),190(a,1))].

given #270 (T,wt=8): 4964 cb <= cy | cy <= ca v x.  [para(4556(a,1),210(a,1))].

given #271 (A,wt=11): 176 B(x,y,x ^ y) | x ^ y != y.  [para(60(a,1),37(b,1)),rewrite(60(7),27(6),56(6)),xx(c)].

given #272 (F,wt=8): 5074 cx v cy <= cy | cb <= ca.  [hyper(287,b,4724,b(flip))].

given #273 (F,wt=8): 5081 cb <= ca | cx ^ x <= cy.  [para(4724(b,1),210(a,2))].

given #274 (T,wt=8): 5282 ca v cy <= ca | cb <= cy.  [hyper(287,b,4957,b(flip))].

given #275 (T,wt=8): 5287 cb <= cy | cy ^ x <= ca.  [para(4957(b,1),190(a,2))].

given #276 (A,wt=17): 177 B(x,y ^ x,z) | x ^ ((y ^ x) v z) != y ^ x.  [para(60(a,1),37(c,1,1)),rewrite(113(4),29(5),61(6)),xx(b)].

given #277 (F,wt=8): 5388 B(cx,cb ^ cx,cb ^ cy).  [para(87(a,1),177(b,1,2)),rewrite(27(11)),xx(b)].

given #278 (F,wt=9): 813 x ^ (y ^ z) <= z ^ x.  [para(27(a,1),148(a,1)),rewrite(29(2))].

given #279 (T,wt=9): 814 x ^ (y ^ z) <= y ^ x.  [para(27(a,1),148(a,2))].

given #280 (T,wt=9): 854 x ^ (y ^ z) <= z ^ y.  [para(27(a,1),151(a,1)),rewrite(29(2))].

given #281 (A,wt=15): 178 B(x,y,z ^ y) | (x ^ y) v (z ^ y) != y.  [para(60(a,1),37(c,1,2)),rewrite(113(5),27(8),56(8)),xx(c)].

given #282 (F,wt=9): 857 x ^ y <= x ^ (y v z).  [para(32(a,1),151(a,1,2))].

given #283 (F,wt=9): 859 x ^ y <= x ^ (z v y).  [para(56(a,1),151(a,1,2))].

given #284 (T,wt=7): 5661 cb ^ ca <= cb ^ cx.  [para(581(a,1),859(a,2))].

given #285 (T,wt=8): 5686 ca <= cb | cb <= cb ^ cx.  [para(172(a,1),5661(a,1))].

given #286 (A,wt=13): 179 (x ^ y) v (x ^ (z ^ y)) = x ^ y.  [para(53(a,1),60(a,1,2))].

given #287 (F,wt=8): 5687 cb <= ca | ca <= cb ^ cx.  [para(269(b,1),5661(a,1))].

given #288 (F,wt=6): 5749 cb <= ca | ca <= cx.  [para(1584(a,1),5687(b,2)),merge(b)].

given #289 (T,wt=8): 5688 cb <= cx | cb ^ ca <= cx.  [para(269(b,1),5661(a,2))].

given #290 (T,wt=6): 5753 ca <= cx | cb <= cx.  [hyper(88,c,5688,b,d,286,b),merge(c),merge(d)].

given #291 (A,wt=11): 180 x v (y v (z ^ x)) = y v x.  [para(60(a,1),55(a,1,2)),flip(a)].

given #292 (F,wt=6): 5754 ca <= cb | cb <= cx.  [para(172(a,1),5688(b,1)),merge(c)].

given #293 (F,wt=8): 5689 cb <= ca | cb ^ ca <= cx.  [para(1584(a,1),5661(a,2))].

given #294 (T,wt=8): 5750 cx ^ ca = ca | cb <= ca.  [hyper(38,a,5749,b),rewrite(27(3))].

given #295 (T,wt=8): 5755 cx ^ ca = ca | cb <= cx.  [hyper(38,a,5753,a),rewrite(27(3))].

given #296 (A,wt=11): 184 x v y <= z v (x v (y v u)).  [para(30(a,1),142(a,2,2))].

given #297 (F,wt=6): 6002 cb <= cx | ca <= cy.  [para(5755(a,1),3455(b,1)),merge(b)].

given #298 (F,wt=8): 5858 cb ^ ca = ca | cb <= cx.  [hyper(38,a,5754,a),rewrite(27(3))].

given #299 (T,wt=8): 5859 ca <= cx ^ ca | cb <= ca.  [hyper(287,b,5750,a)].

given #300 (T,wt=8): 5863 cb <= ca | cx v ca = cx.  [para(5750(a,1),34(a,1,2))].

given #301 (A,wt=11): 191 x v y <= z v (x v (u v y)).  [para(55(a,1),143(a,2,2))].

given #302 (F,wt=8): 5868 cb <= ca | x ^ ca <= cx.  [para(5750(a,1),149(a,1,2))].

given #303 (F,wt=8): 5869 cb <= ca | ca <= x v cx.  [para(5750(a,1),190(a,1))].

given #304 (T,wt=8): 5870 cb <= ca | ca <= cx v x.  [para(5750(a,1),210(a,1))].

given #305 (T,wt=8): 5936 ca <= cx ^ ca | cb <= cx.  [hyper(287,b,5755,a)].

given #306 (A,wt=17): 193 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u).  [para(57(a,1),29(a,1)),rewrite(29(2)),flip(a)].

given #307 (F,wt=8): 5940 cb <= cx | cx v ca = cx.  [para(5755(a,1),34(a,1,2))].

given #308 (F,wt=8): 5945 cb <= cx | x ^ ca <= cx.  [para(5755(a,1),149(a,1,2))].

given #309 (T,wt=8): 5946 cb <= cx | ca <= x v cx.  [para(5755(a,1),190(a,1))].

given #310 (T,wt=8): 5947 cb <= cx | ca <= cx v x.  [para(5755(a,1),210(a,1))].

given #311 (A,wt=17): 194 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u.  [para(30(a,1),57(a,1,2,1))].

given #312 (F,wt=8): 6047 ca ^ cy = ca | cb <= cx.  [hyper(38,a,6002,b)].

given #313 (F,wt=8): 6048 ca <= cb ^ ca | cb <= cx.  [hyper(287,b,5858,a)].

given #314 (T,wt=8): 6052 cb <= cx | cb v ca = cb.  [para(5858(a,1),34(a,1,2))].

given #315 (T,wt=8): 6057 cb <= cx | x ^ ca <= cb.  [para(5858(a,1),149(a,1,2))].

given #316 (A,wt=46): 195 B(x,(x v y) ^ z,u) | (x ^ z) v ((x v y) ^ (z ^ u)) != (x v y) ^ z | (x v ((x v y) ^ z)) ^ (((x v y) ^ z) v u) != (x v y) ^ z.  [para(57(a,1),37(b,1,1)),rewrite(29(7))].

given #317 (F,wt=8): 6058 cb <= cx | ca <= x v cb.  [para(5858(a,1),190(a,1))].

given #318 (F,wt=8): 6059 cb <= cx | ca <= cb v x.  [para(5858(a,1),210(a,1))].

given #319 (T,wt=8): 6120 cb <= cx | ca <= cb ^ cx.  [para(5858(a,1),5661(a,1))].

given #320 (T,wt=8): 6123 cx v ca <= cx | cb <= ca.  [hyper(287,b,5863,b(flip))].

given #321 (A,wt=30): 196 B(x,y,(y v z) ^ u) | (x ^ y) v (y ^ u) != y | (x v y) ^ (y v ((y v z) ^ u)) != y.  [para(57(a,1),37(b,1,2))].

given #322 (F,wt=8): 6128 cb <= ca | ca ^ x <= cx.  [para(5863(b,1),190(a,2))].

given #323 (F,wt=8): 6334 cx v ca <= cx | cb <= cx.  [hyper(287,b,5940,b(flip))].

given #324 (T,wt=8): 6339 cb <= cx | ca ^ x <= cx.  [para(5940(b,1),190(a,2))].

given #325 (T,wt=8): 6495 ca <= ca ^ cy | cb <= cx.  [hyper(287,b,6047,a)].

given #326 (A,wt=12): 197 x <= (x v y) ^ z | x ^ z != x.  [para(57(a,1),39(b,1))].

given #327 (F,wt=8): 6502 cb <= cx | ca v cy = cy.  [para(6047(a,1),60(a,1,2)),rewrite(28(6))].

given #328 (F,wt=8): 6503 cb <= cx | x ^ ca <= cy.  [para(6047(a,1),150(a,1,2))].

given #329 (T,wt=8): 6504 cb <= cx | ca <= x v cy.  [para(6047(a,1),192(a,1))].

given #330 (T,wt=8): 6505 cb <= cx | ca <= cy v x.  [para(6047(a,1),216(a,1))].

given #331 (A,wt=24): 198 x <= y | (x v z) ^ u <= y | -(x ^ u <= y) | -(y <= x v ((x v z) ^ u)).  [para(57(a,1),44(c,1))].

given #332 (F,wt=8): 6569 cb v ca <= cb | cb <= cx.  [hyper(287,b,6052,b(flip))].

given #333 (F,wt=8): 6574 cb <= cx | ca ^ x <= cb.  [para(6052(b,1),190(a,2))].

given #334 (T,wt=8): 6920 ca v cy <= cy | cb <= cx.  [hyper(287,b,6502,b(flip))].

given #335 (T,wt=8): 6925 cb <= cx | ca ^ x <= cy.  [para(6502(b,1),210(a,2))].

given #336 (A,wt=24): 199 x <= (y v z) ^ u | x <= y | -(y ^ u <= x) | -(x <= y v ((y v z) ^ u)).  [para(57(a,1),47(c,1))].

given #337 (F,wt=9): 963 x ^ y <= (y v z) ^ x.  [para(27(a,1),202(a,1))].

given #338 (F,wt=9): 964 x ^ y <= y ^ (x v z).  [para(27(a,1),202(a,2))].

given #339 (T,wt=9): 965 x ^ y <= (z v x) ^ y.  [para(28(a,1),202(a,2,1))].

given #340 (T,wt=9): 968 x <= (x v y) ^ (x v z).  [para(32(a,1),202(a,1))].

given #341 (A,wt=15): 200 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u).  [para(57(a,1),53(a,1,2)),flip(a)].

given #342 (F,wt=9): 972 x <= (x v y) ^ (z v x).  [para(56(a,1),202(a,1))].

given #343 (F,wt=9): 1260 (x ^ y) v z <= y v z.  [para(27(a,1),446(a,1,1))].

given #344 (T,wt=9): 1261 x v (y ^ z) <= y v x.  [para(28(a,1),446(a,1))].

given #345 (T,wt=9): 1262 (x ^ y) v z <= z v x.  [para(28(a,1),446(a,2))].

given #346 (A,wt=13): 201 x ^ ((y v (x v z)) ^ u) = x ^ u.  [para(55(a,1),57(a,1,2,1))].

given #347 (F,wt=9): 1265 (x ^ y) v (x ^ z) <= x.  [para(34(a,1),446(a,2))].

given #348 (F,wt=9): 1269 (x ^ y) v (z ^ x) <= x.  [para(60(a,1),446(a,2))].

given #349 (T,wt=9): 1421 (x ^ y) v z <= z v y.  [para(60(a,1),782(a,2,2))].

given #350 (T,wt=9): 1517 x v (y ^ z) <= z v x.  [para(28(a,1),803(a,2))].

given #351 (A,wt=15): 203 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y.  [para(57(a,1),60(a,1,2)),rewrite(28(4))].

given #352 (F,wt=9): 1890 cx <= ca | cx <= x | x <= cb.  [para(1579(a,1),282(a,1))].

given #353 (F,wt=9): 1939 cx <= cb | ca <= cx | ca != cx.  [para(1581(a,1),81(b,1)),flip(c)].

given #354 (T,wt=9): 1940 cx <= cb | x <= ca | cx <= x.  [para(1581(a,1),283(b,1))].

given #355 (T,wt=8): 8258 cb ^ ca = cb | cx <= cb.  [factor(8191,b,c)].

given #356 (A,wt=13): 207 x ^ (y ^ (x ^ z)) = y ^ (x ^ z).  [hyper(38,a,149,a),rewrite(27(3))].

given #357 (F,wt=8): 8270 cb <= cb ^ ca | cx <= cb.  [hyper(287,b,8258,a)].

given #358 (F,wt=8): 8278 cx <= cb | cb v ca = ca.  [para(8258(a,1),60(a,1,2)),rewrite(28(6))].

given #359 (T,wt=8): 8279 cx <= cb | x ^ cb <= ca.  [para(8258(a,1),150(a,1,2))].

given #360 (T,wt=8): 8280 cx <= cb | cb <= x v ca.  [para(8258(a,1),192(a,1))].

given #361 (A,wt=11): 208 x ^ (y ^ (z ^ u)) <= y ^ z.  [para(29(a,1),149(a,1,2))].

given #362 (F,wt=8): 8281 cx <= cb | cb <= ca v x.  [para(8258(a,1),216(a,1))].

given #363 (F,wt=8): 8363 cb v ca <= ca | cx <= cb.  [hyper(287,b,8278,b(flip))].

given #364 (T,wt=8): 8368 cx <= cb | cb ^ x <= ca.  [para(8278(b,1),210(a,2))].

given #365 (T,wt=8): 8387 cx <= cb | cb v cx <= ca.  [para(8278(b,1),1533(a,2))].

given #366 (A,wt=13): 214 x ^ (y ^ (z ^ x)) = y ^ (z ^ x).  [hyper(38,a,150,a),rewrite(27(3))].

given #367 (F,wt=9): 1979 cb <= ca | cx <= x | x <= cb.  [para(1584(a,1),282(a,1))].

given #368 (F,wt=9): 2045 cb <= cy | x <= cx | cb <= x.  [para(1614(a,1),283(b,1))].

given #369 (T,wt=9): 2166 cb <= cx | cy <= cb | cy != cb.  [para(1616(a,1),81(b,1)),flip(c)].

given #370 (T,wt=9): 2167 cb <= cx | x <= cy | cb <= x.  [para(1616(a,1),283(b,1))].

given #371 (A,wt=11): 217 x ^ (y ^ (z ^ u)) <= y ^ u.  [para(53(a,1),150(a,1,2))].

given #372 (F,wt=9): 2209 cb <= cx | cy <= cx | cy != cx.  [para(1800(a,1),81(b,1)),flip(c)].

given #373 (F,wt=9): 2210 cb <= cx | x <= cy | cx <= x.  [para(1800(a,1),283(b,1))].

given #374 (T,wt=9): 2566 x <= y | B(z,y,y ^ x).  [para(172(a,1),116(b,1,2)),rewrite(28(5),60(5)),xx(c)].

given #375 (T,wt=9): 2568 x <= y | B(x,y,y ^ z).  [para(269(b,1),116(b,1,1)),rewrite(34(5)),xx(c)].

given #376 (A,wt=11): 218 x ^ (y ^ z) <= (y v u) ^ z.  [para(57(a,1),150(a,1,2))].

given #377 (F,wt=9): 2579 cx <= ca | B(cb,cx,cx ^ x).  [para(1579(a,1),116(b,1,1)),rewrite(34(12)),xx(c)].

given #378 (F,wt=9): 2582 cx <= cb | B(x,cx,cx ^ ca).  [para(1581(a,1),116(b,1,2)),rewrite(28(12),60(12)),xx(c)].

given #379 (T,wt=9): 2583 cb <= ca | B(cb,cx,cx ^ x).  [para(1584(a,1),116(b,1,1)),rewrite(34(12)),xx(c)].

given #380 (T,wt=9): 2586 cb <= cy | B(x,cb,cb ^ cx).  [para(1614(a,1),116(b,1,2)),rewrite(28(12),60(12)),xx(c)].

given #381 (A,wt=11): 221 x ^ (y ^ z) <= u v (x ^ y).  [para(29(a,1),190(a,1))].

given #382 (F,wt=9): 2588 cb <= cx | B(x,cb,cb ^ cy).  [para(1616(a,1),116(b,1,2)),rewrite(28(12),60(12)),xx(c)].

given #383 (F,wt=9): 2590 cb <= cx | B(x,cx,cx ^ cy).  [para(1800(a,1),116(b,1,2)),rewrite(28(12),60(12)),xx(c)].

given #384 (T,wt=9): 2603 cx <= ca | ca <= x | x <= cb.  [para(1927(a,1),282(a,1))].

given #385 (T,wt=9): 2637 cx <= ca | B(cb,ca,ca ^ x).  [para(1927(a,1),116(b,1,1)),rewrite(34(12)),xx(c)].

given #386 (A,wt=11): 224 (x v y) ^ z <= x v (u v y).  [para(55(a,1),190(a,2))].

given #387 (F,wt=9): 3011 cb <= cy | ca <= cx | ca != cx.  [para(2077(a,1),81(b,1)),flip(c)].

given #388 (F,wt=9): 3012 cb <= cy | x <= ca | cx <= x.  [para(2077(a,1),283(b,1))].

given #389 (T,wt=9): 3043 cb <= cy | B(x,cx,cx ^ ca).  [para(2077(a,1),116(b,1,2)),rewrite(28(12),60(12)),xx(c)].

given #390 (T,wt=9): 3067 cb <= ca | cy <= cb | cy != cb.  [para(2078(a,1),81(b,1)),flip(c)].

given #391 (A,wt=10): 226 x v y <= y | x v y <= x.  [hyper(47,c,192,a,d,110,a)].

given #392 (F,wt=9): 3068 cb <= ca | x <= cy | cb <= x.  [para(2078(a,1),283(b,1))].

given #393 (F,wt=9): 3099 cb <= ca | B(x,cb,cb ^ cy).  [para(2078(a,1),116(b,1,2)),rewrite(28(12),60(12)),xx(c)].

given #394 (T,wt=9): 3149 cb <= cy | cy <= x | x <= cx.  [para(2079(a,1),282(a,1))].

given #395 (T,wt=9): 3183 cb <= cy | B(cx,cy,cy ^ x).  [para(2079(a,1),116(b,1,1)),rewrite(34(12)),xx(c)].

given #396 (A,wt=10): 228 x <= x ^ y | y <= x ^ y.  [hyper(44,c,110,a,d,192,a)].

given #397 (F,wt=9): 3571 x <= y | B(z,x,x v y).  [para(279(b,1),130(b,1,2)),rewrite(27(5),56(5)),xx(c)].

given #398 (F,wt=9): 3574 x <= y | B(y,x,x v z).  [para(339(b,1),130(b,1,1)),rewrite(32(5)),xx(c)].

given #399 (T,wt=3): 9709 cb <= ca.  [factor(9702,a,b),unit_del(b,43)].

given #400 (T,wt=5): 9711 cb ^ ca = cb.  [hyper(38,a,9709,a)].

given #401 (A,wt=11): 231 x ^ (y ^ z) <= u v (x ^ z).  [para(53(a,1),192(a,1))].

given #402 (F,wt=3): 9875 cb <= cx.  [para(9711(a,1),5945(b,1)),merge(b)].

given #403 (F,wt=3): 10069 cx <= ca.  [back_rewrite(1579),rewrite(9901(3)),flip(a),unit_del(a,42)].

given #404 (T,wt=5): 9837 cb v ca = ca.  [para(9711(a,1),60(a,1,2)),rewrite(28(3))].

given #405 (T,wt=5): 9838 x ^ cb <= ca.  [para(9711(a,1),150(a,1,2))].

given #406 (A,wt=11): 232 x ^ (y v z) <= y v (u v z).  [para(55(a,1),192(a,2))].

given #407 (F,wt=5): 9839 cb <= x v ca.  [para(9711(a,1),192(a,1))].

given #408 (F,wt=5): 9840 cb <= ca v x.  [para(9711(a,1),216(a,1))].

given #409 (T,wt=5): 9901 cb ^ cx = cb.  [back_rewrite(9794),rewrite(9836(5),27(3))].

given #410 (T,wt=5): 10004 cx v ca = ca.  [back_rewrite(5768),rewrite(9901(4),28(3),9837(3)),flip(a)].

given #411 (A,wt=11): 233 x ^ y <= z v ((x v u) ^ y).  [para(57(a,1),192(a,1))].

given #412 (F,wt=5): 10084 cx ^ ca = cx.  [back_rewrite(85),rewrite(9901(3),638(5),9962(3))].

given #413 (F,wt=5): 10166 x ^ cx <= ca.  [back_rewrite(1574),rewrite(9962(3),10084(3),10004(5),9962(7),10084(7)),xx(b)].

given #414 (T,wt=5): 10186 cb v cy <= cx.  [back_rewrite(651),rewrite(9962(3),10084(3),9962(9),10084(9)),unit_del(a,42)].

given #415 (T,wt=5): 10240 cb v cx = cx.  [back_rewrite(9962),rewrite(10084(6))].

given #416 (A,wt=13): 234 x ^ (y ^ ((y ^ x) v z)) = x ^ y.  [para(27(a,1),58(a,1,2,2,1))].

given #417 (F,wt=5): 10323 cb ^ x <= ca.  [para(9837(a,1),210(a,2))].

given #418 (F,wt=5): 10394 x ^ cb <= cx.  [para(9901(a,1),150(a,1,2))].

given #419 (T,wt=5): 10395 cb <= x v cx.  [para(9901(a,1),192(a,1))].

given #420 (T,wt=5): 10396 cb <= cx v x.  [para(9901(a,1),216(a,1))].

given #421 (A,wt=19): 235 x ^ (y ^ (z ^ ((x ^ (y ^ z)) v u))) = x ^ (y ^ z).  [para(58(a,1),29(a,1)),rewrite(29(2),29(4)),flip(a)].

given #422 (F,wt=5): 10439 cx <= x v ca.  [para(10004(a,1),142(a,2,2))].

given #423 (F,wt=5): 10440 cx ^ x <= ca.  [para(10004(a,1),210(a,2))].

given #424 (T,wt=5): 10561 cx <= ca v x.  [para(10084(a,1),216(a,1))].

given #425 (T,wt=5): 10575 cb v cy = cb.  [hyper(38,a,10186,a),rewrite(27(5),10012(5)),flip(a)].

given #426 (A,wt=58): 236 B(x,y ^ ((x ^ y) v z),u) | (x ^ y) v (y ^ (((x ^ y) v z) ^ u)) != y ^ ((x ^ y) v z) | (x v (y ^ ((x ^ y) v z))) ^ ((y ^ ((x ^ y) v z)) v u) != y ^ ((x ^ y) v z).  [para(58(a,1),37(b,1,1)),rewrite(29(9))].

given #427 (F,wt=3): 10856 cy <= cb.  [para(10575(a,1),140(a,2))].

given #428 (F,wt=5): 10597 cb ^ x <= cx.  [para(10240(a,1),210(a,2))].

given #429 (T,wt=5): 10857 cb ^ cy = cy.  [para(10575(a,1),56(a,1,2)),rewrite(27(3))].

given #430 (T,wt=3): 11091 cy <= ca.  [para(10857(a,1),10323(a,1))].

given #431 (A,wt=34): 237 B(x,y,z ^ ((y ^ z) v u)) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v (z ^ ((y ^ z) v u))) != y.  [para(58(a,1),37(b,1,2))].

given #432 (F,wt=3): 11092 cy <= cx.  [para(10857(a,1),10597(a,1))].

given #433 (F,wt=5): 10858 cy <= x v cb.  [para(10575(a,1),143(a,2,2))].

given #434 (T,wt=5): 10859 cy ^ x <= cb.  [para(10575(a,1),190(a,2))].

given #435 (T,wt=5): 10860 x ^ cy <= cb.  [para(10575(a,1),192(a,2))].

given #436 (A,wt=14): 238 x <= y ^ ((x ^ y) v z) | x ^ y != x.  [para(58(a,1),39(b,1))].

given #437 (F,wt=5): 10922 cx ^ cy = cy.  [back_rewrite(10129),rewrite(10857(6))].

given #438 (F,wt=5): 10923 cx v cy = cx.  [back_rewrite(10128),rewrite(10857(4))].

given #439 (T,wt=5): 11060 cy <= cb v x.  [para(10857(a,1),210(a,1))].

given #440 (T,wt=5): 11093 ca ^ cy = cy.  [hyper(38,a,11091,a),rewrite(27(3))].

given #441 (A,wt=28): 239 x <= y | z ^ ((x ^ z) v u) <= y | -(x ^ z <= y) | -(y <= x v (z ^ ((x ^ z) v u))).  [para(58(a,1),44(c,1))].

given #442 (F,wt=5): 11193 x ^ cy <= cx.  [para(10922(a,1),149(a,1,2))].

given #443 (F,wt=5): 11194 cy <= x v cx.  [para(10922(a,1),190(a,1))].

given #444 (T,wt=5): 11195 cy <= cx v x.  [para(10922(a,1),210(a,1))].

given #445 (T,wt=5): 11246 cy ^ x <= cx.  [para(10923(a,1),190(a,2))].

given #446 (A,wt=28): 240 x <= y ^ ((z ^ y) v u) | x <= z | -(z ^ y <= x) | -(x <= z v (y ^ ((z ^ y) v u))).  [para(58(a,1),47(c,1))].

given #447 (F,wt=5): 11267 ca v cy = ca.  [para(11093(a,1),34(a,1,2))].

given #448 (F,wt=5): 11271 x ^ cy <= ca.  [para(11093(a,1),149(a,1,2))].

given #449 (T,wt=5): 11272 cy <= x v ca.  [para(11093(a,1),190(a,1))].

given #450 (T,wt=5): 11273 cy <= ca v x.  [para(11093(a,1),210(a,1))].

given #451 (A,wt=17): 241 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z).  [para(58(a,1),53(a,1,2)),flip(a)].

given #452 (F,wt=5): 11613 cy ^ x <= ca.  [para(11267(a,1),190(a,2))].

given #453 (F,wt=6): 9841 ca <= cb | ca != cb.  [para(9711(a,1),81(b,1)),flip(b)].

given #454 (T,wt=6): 9842 x <= ca | cb <= x.  [para(9711(a,1),283(b,1))].

given #455 (T,wt=6): 9990 x <= ca | cx <= x.  [back_rewrite(8154),rewrite(9901(3)),flip(a),unit_del(a,42)].

given #456 (A,wt=19): 242 x ^ (y ^ (z ^ ((y ^ (x ^ z)) v u))) = x ^ (y ^ z).  [para(53(a,1),58(a,1,2,2,1)),rewrite(29(5))].

given #457 (F,wt=6): 10130 B(cb,cx,x v cx).  [back_rewrite(4693),rewrite(10084(4),10084(5),9962(8),10084(8),10084(9),56(9),10084(9)),xx(b)].

given #458 (F,wt=6): 10145 B(cb,cx,cx v x).  [back_rewrite(3582),rewrite(10084(4),10084(5),9962(8),10084(8),10084(9),32(9),10084(9)),xx(b)].

given #459 (T,wt=6): 10193 ca <= cx | ca != cx.  [back_rewrite(582),rewrite(10004(3),9962(4),10084(4),10004(6))].

given #460 (T,wt=6): 10335 B(cb,ca,ca v x).  [para(9837(a,1),130(b,1,1)),rewrite(32(9)),xx(b)].

given #461 (A,wt=15): 243 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y.  [para(55(a,1),58(a,1,2,2))].

given #462 (F,wt=6): 10339 B(cb,ca,x v ca).  [para(9837(a,1),156(b,1,1)),rewrite(56(9)),xx(b)].

given #463 (F,wt=6): 10397 x <= cx | cb <= x.  [para(9901(a,1),283(b,1))].

given #464 (T,wt=6): 10458 B(cx,ca,ca v x).  [para(10004(a,1),130(b,1,1)),rewrite(32(9)),xx(b)].

given #465 (T,wt=6): 10462 B(cx,ca,x v ca).  [para(10004(a,1),156(b,1,1)),rewrite(56(9)),xx(b)].

given #466 (A,wt=11): 244 x ^ y <= y ^ ((x ^ y) v z).  [para(58(a,1),147(a,1))].

given #467 (F,wt=6): 10589 B(cx,cb,cb ^ x).  [back_rewrite(10159),rewrite(10575(4),10575(5),10575(9),34(9),10575(9)),xx(b)].

given #468 (F,wt=6): 10594 B(cx,cb,x ^ cb).  [back_rewrite(10123),rewrite(10575(4),10575(5),10575(9),60(9),10575(9)),xx(b)].

given #469 (T,wt=6): 10861 cy <= x | x <= cb.  [para(10575(a,1),284(b,2))].

given #470 (T,wt=6): 11072 B(cb,cy,cy ^ x).  [para(10857(a,1),116(b,1,1)),rewrite(34(9)),xx(b)].

given #471 (A,wt=19): 245 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z).  [para(58(a,1),60(a,1,2)),rewrite(28(5))].

given #472 (F,wt=6): 11077 B(cb,cy,x ^ cy).  [para(10857(a,1),178(b,1,1)),rewrite(60(9)),xx(b)].

given #473 (F,wt=6): 11197 cy <= x | x <= cx.  [para(10922(a,1),282(a,1))].

given #474 (T,wt=6): 11219 B(cx,cy,cy ^ x).  [para(10922(a,1),116(b,1,1)),rewrite(34(9)),xx(b)].

given #475 (T,wt=6): 11226 B(cx,cy,x ^ cy).  [para(10922(a,1),178(b,1,1)),rewrite(60(9)),xx(b)].

given #476 (A,wt=15): 246 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y.  [para(58(a,1),57(a,1,2)),rewrite(57(3)),flip(a)].

given #477 (F,wt=6): 11275 cy <= x | x <= ca.  [para(11093(a,1),282(a,1))].

given #478 (F,wt=6): 11297 B(ca,cy,cy ^ x).  [para(11093(a,1),116(b,1,1)),rewrite(34(9)),xx(b)].

given #479 (T,wt=6): 11304 B(ca,cy,x ^ cy).  [para(11093(a,1),178(b,1,1)),rewrite(60(9)),xx(b)].

given #480 (T,wt=7): 9830 cb <= ca ^ (cb v x).  [hyper(197,b,9711,a),rewrite(27(5))].

given #481 (A,wt=13): 247 x ^ (y ^ z) <= z ^ ((y ^ z) v u).  [para(58(a,1),150(a,1,2))].

given #482 (F,wt=7): 9848 x ^ cb <= x ^ ca.  [para(9711(a,1),151(a,1,2))].

given #483 (F,wt=7): 9849 ca v (x ^ cb) = ca.  [para(9711(a,1),173(a,1,2,2))].

given #484 (T,wt=7): 9851 x ^ (y ^ cb) <= ca.  [para(9711(a,1),215(a,1,2,2))].

given #485 (T,wt=7): 9852 x ^ cb <= y v ca.  [para(9711(a,1),229(a,1,2))].

given #486 (A,wt=13): 248 x ^ y <= z v (y ^ ((x ^ y) v u)).  [para(58(a,1),192(a,1))].

given #487 (F,wt=7): 9853 cb <= x v (y v ca).  [para(9711(a,1),230(a,1))].

given #488 (F,wt=7): 9855 x ^ cb <= ca v y.  [para(9711(a,1),257(a,1,2))].

given #489 (T,wt=7): 9856 cb <= x v (ca v y).  [para(9711(a,1),260(a,1))].

given #490 (T,wt=7): 9859 x v cb <= x v ca.  [para(9711(a,1),803(a,1,2))].

given #491 (A,wt=11): 251 x ^ (y ^ z) <= (x ^ y) v u.  [para(29(a,1),210(a,1))].

given #492 (F,wt=7): 9868 B(cb,ca,cb) | ca != cb.  [para(9711(a,1),176(b,1)),rewrite(9711(5)),flip(b)].

given #493 (F,wt=7): 9869 x ^ cb <= ca ^ x.  [para(9711(a,1),813(a,1,2))].

given #494 (T,wt=7): 9880 cb <= ca ^ (x v cb).  [para(9711(a,1),965(a,1)),rewrite(27(5))].

given #495 (T,wt=7): 9881 cb v x <= ca v x.  [para(9711(a,1),1260(a,1,1))].

given #496 (A,wt=11): 252 (x v y) ^ z <= x v (y v u).  [para(30(a,1),210(a,2))].

given #497 (F,wt=7): 9882 cb v (ca ^ x) <= ca.  [para(9711(a,1),1269(a,1,2)),rewrite(28(4))].

given #498 (F,wt=7): 9883 cb v x <= x v ca.  [para(9711(a,1),1421(a,1,1))].

given #499 (T,wt=7): 9884 x v cb <= ca v x.  [para(9711(a,1),1517(a,1,2))].

given #500 (T,wt=7): 9985 cb <= x | B(x,cb,cx).  [back_rewrite(9695),rewrite(9901(3),9901(5))].

given #501 (A,wt=11): 258 x ^ (y v z) <= y v (z v u).  [para(30(a,1),216(a,2))].

given #502 (F,wt=7): 10107 x <= cx | B(x,cx,cb).  [back_rewrite(8985),rewrite(9962(3),10084(3),9962(5),10084(5))].

given #503 (F,wt=7): 10112 cx v (cb ^ x) <= cx.  [back_rewrite(7723),rewrite(10084(3),9962(7),10084(7))].

given #504 (T,wt=7): 10118 cx <= ca ^ (cx v x).  [back_rewrite(6904),rewrite(9962(3),10084(3),10083(5),10004(6),27(5),9962(9),10084(9)),xx(b)].

given #505 (T,wt=7): 10127 B(cx,ca,cx) | ca != cx.  [back_rewrite(5353),rewrite(9962(3),10084(3),10004(4),10004(7))].

given #506 (A,wt=11): 259 x ^ (y ^ z) <= (x ^ z) v u.  [para(53(a,1),216(a,1))].

given #507 (F,wt=7): 10325 cb ^ (x v ca) = cb.  [para(9837(a,1),132(a,1,2,2))].

given #508 (F,wt=7): 10326 cb ^ x <= ca ^ x.  [para(9837(a,1),202(a,2,1))].

given #509 (T,wt=7): 10327 x ^ (cb ^ y) <= ca.  [para(9837(a,1),253(a,2))].

given #510 (T,wt=7): 10328 cb ^ x <= y v ca.  [para(9837(a,1),254(a,2,2))].

given #511 (A,wt=11): 261 x ^ y <= ((x v z) ^ y) v u.  [para(57(a,1),216(a,1))].

given #512 (F,wt=7): 10332 cb v (x ^ ca) <= ca.  [para(9837(a,1),803(a,2))].

given #513 (F,wt=7): 10346 cb ^ x <= x ^ ca.  [para(9837(a,1),964(a,2,2))].

given #514 (T,wt=7): 10351 cb <= x | B(x,cb,ca).  [para(9837(a,1),3574(b,3))].

given #515 (T,wt=7): 10390 cb ^ (ca v x) = cb.  [hyper(38,a,9840,a)].

given #516 (A,wt=13): 262 x ^ y <= (y ^ ((x ^ y) v z)) v u.  [para(58(a,1),216(a,1))].

given #517 (F,wt=7): 10391 cb <= cx ^ (cb v x).  [hyper(197,b,9901,a),rewrite(27(5))].

given #518 (F,wt=7): 10398 x ^ cb <= x ^ cx.  [para(9901(a,1),151(a,1,2))].

given #519 (T,wt=7): 10399 cx v (x ^ cb) = cx.  [para(9901(a,1),173(a,1,2,2))].

given #520 (T,wt=7): 10400 x ^ (y ^ cb) <= cx.  [para(9901(a,1),215(a,1,2,2))].

given #521 (A,wt=12): 263 x <= y ^ z | y ^ (z ^ x) != x.  [para(29(a,1),81(b,1))].

given #522 (F,wt=7): 10401 x ^ cb <= y v cx.  [para(9901(a,1),229(a,1,2))].

given #523 (F,wt=7): 10402 cb <= x v (y v cx).  [para(9901(a,1),230(a,1))].

given #524 (T,wt=7): 10404 x ^ cb <= cx v y.  [para(9901(a,1),257(a,1,2))].

given #525 (T,wt=7): 10405 cb <= x v (cx v y).  [para(9901(a,1),260(a,1))].

given #526 (A,wt=10): 264 x v y <= x | x v y != x.  [para(32(a,1),81(b,1)),flip(b)].

given #527 (F,wt=7): 10407 x v cb <= x v cx.  [para(9901(a,1),803(a,1,2))].

given #528 (F,wt=7): 10414 x ^ cb <= cx ^ x.  [para(9901(a,1),813(a,1,2))].

given #529 (T,wt=7): 10424 cb <= cx ^ (x v cb).  [para(9901(a,1),965(a,1)),rewrite(27(5))].

given #530 (T,wt=7): 10425 cb v x <= cx v x.  [para(9901(a,1),1260(a,1,1))].

given #531 (A,wt=14): 265 x ^ y <= z | x ^ (z ^ y) != x ^ y.  [para(53(a,1),81(b,1))].

given #532 (F,wt=7): 10426 cb v (cx ^ x) <= cx.  [para(9901(a,1),1269(a,1,2)),rewrite(28(4))].

given #533 (F,wt=7): 10427 cb v x <= x v cx.  [para(9901(a,1),1421(a,1,1))].

given #534 (T,wt=7): 10428 x v cb <= cx v x.  [para(9901(a,1),1517(a,1,2))].

given #535 (T,wt=7): 10442 cx ^ (x v ca) = cx.  [para(10004(a,1),132(a,1,2,2))].

given #536 (A,wt=10): 266 x v y <= y | x v y != y.  [para(56(a,1),81(b,1)),flip(b)].

given #537 (F,wt=7): 10443 x v cx <= x v ca.  [para(10004(a,1),141(a,2,2))].

given #538 (F,wt=7): 10444 cx <= x v (y v ca).  [para(10004(a,1),185(a,2,2,2))].

given #539 (T,wt=7): 10445 cx ^ x <= ca ^ x.  [para(10004(a,1),202(a,2,1))].

given #540 (T,wt=7): 10446 x ^ (cx ^ y) <= ca.  [para(10004(a,1),253(a,2))].

given #541 (A,wt=16): 267 (x v y) ^ z <= x | (x v y) ^ z != x ^ z.  [para(57(a,1),81(b,1)),flip(b)].

given #542 (F,wt=7): 10447 cx ^ x <= y v ca.  [para(10004(a,1),254(a,2,2))].

given #543 (F,wt=7): 10448 x ^ (y ^ cx) <= ca.  [para(10004(a,1),257(a,2))].

given #544 (T,wt=7): 10449 x ^ cx <= y v ca.  [para(10004(a,1),260(a,2,2))].

given #545 (T,wt=7): 10450 ca v (cx ^ x) <= ca.  [para(10004(a,1),446(a,2)),rewrite(28(4))].

given #546 (A,wt=20): 268 x ^ ((y ^ x) v z) <= y | x ^ ((y ^ x) v z) != y ^ x.  [para(58(a,1),81(b,1)),flip(b)].

given #547 (F,wt=7): 10452 cx v x <= x v ca.  [para(10004(a,1),781(a,2,2))].

given #548 (F,wt=7): 10453 cx v (ca ^ x) <= ca.  [para(10004(a,1),801(a,2))].

given #549 (T,wt=7): 10455 cx v (x ^ ca) <= ca.  [para(10004(a,1),803(a,2))].

given #550 (T,wt=7): 10463 x ^ cx <= x ^ ca.  [para(10004(a,1),857(a,2,2))].

given #551 (A,wt=12): 270 x <= y | y ^ (x ^ z) = y ^ z.  [para(172(a,1),29(a,1,1)),flip(b)].

given #552 (F,wt=7): 10471 x ^ cx <= ca ^ x.  [para(10004(a,1),963(a,2,1))].

given #553 (F,wt=7): 10472 cx ^ x <= x ^ ca.  [para(10004(a,1),964(a,2,2))].

given #554 (T,wt=7): 10474 cx <= ca ^ (x v cx).  [para(10004(a,1),972(a,2,1))].

given #555 (T,wt=7): 10479 cx <= x | B(x,cx,ca).  [para(10004(a,1),3574(b,3))].

given #556 (A,wt=14): 271 x <= y ^ z | y ^ (z ^ x) = y ^ z.  [para(172(a,1),29(a,1)),flip(b)].

given #557 (F,wt=7): 10562 ca v (x ^ cx) = ca.  [para(10084(a,1),173(a,1,2,2))].

given #558 (F,wt=7): 10563 x ^ cx <= ca v y.  [para(10084(a,1),257(a,1,2))].

given #559 (T,wt=7): 10564 cx <= x v (ca v y).  [para(10084(a,1),260(a,1))].

given #560 (T,wt=7): 10570 cx v x <= ca v x.  [para(10084(a,1),1260(a,1,1))].

given #561 (A,wt=12): 272 x <= y | z ^ (y ^ x) = z ^ y.  [para(172(a,1),29(a,2,2)),rewrite(29(3))].

given #562 (F,wt=7): 10571 x v cx <= ca v x.  [para(10084(a,1),1517(a,1,2))].

given #563 (F,wt=7): 10599 cb ^ (x v cx) = cb.  [para(10240(a,1),132(a,1,2,2))].

given #564 (T,wt=7): 10600 cb ^ x <= cx ^ x.  [para(10240(a,1),202(a,2,1))].

given #565 (T,wt=7): 10601 x ^ (cb ^ y) <= cx.  [para(10240(a,1),253(a,2))].

given #566 (A,wt=23): 273 x <= y | B(y,x,z) | y v (x ^ z) != x | (y v x) ^ (x v z) != x.  [para(172(a,1),37(b,1,1))].

given #567 (F,wt=7): 10602 cb ^ x <= y v cx.  [para(10240(a,1),254(a,2,2))].

given #568 (F,wt=7): 10603 cb v (x ^ cx) <= cx.  [para(10240(a,1),803(a,2))].

given #569 (T,wt=7): 10610 cb ^ x <= x ^ cx.  [para(10240(a,1),964(a,2,2))].

given #570 (T,wt=7): 10728 cb ^ (cx v x) = cb.  [hyper(38,a,10396,a)].

given #571 (A,wt=16): 274 x <= y | B(z,y,x) | (z v y) ^ (y v x) != y.  [para(172(a,1),37(b,1,2)),rewrite(28(4),60(4)),xx(c)].

given #572 (F,wt=7): 10849 cx ^ (ca v x) = cx.  [hyper(38,a,10561,a)].

given #573 (F,wt=7): 10865 x v cy <= x v cb.  [para(10575(a,1),145(a,2,2))].

given #574 (T,wt=7): 10866 cy ^ (x v cb) = cy.  [para(10575(a,1),154(a,1,2,2))].

given #575 (T,wt=7): 10868 cy <= x v (y v cb).  [para(10575(a,1),189(a,2,2,2))].

given #576 (A,wt=25): 275 x v y <= z v x | B(z,x,y) | (z ^ x) v (x ^ y) != x | z v x != x.  [para(172(a,1),37(c,1))].

given #577 (F,wt=7): 10871 cy ^ x <= y v cb.  [para(10575(a,1),222(a,2,2))].

given #578 (F,wt=7): 10872 x ^ (cy ^ y) <= cb.  [para(10575(a,1),223(a,2))].

given #579 (T,wt=7): 10873 x ^ (y ^ cy) <= cb.  [para(10575(a,1),229(a,2))].

given #580 (T,wt=7): 10874 x ^ cy <= y v cb.  [para(10575(a,1),230(a,2,2))].

given #581 (A,wt=17): 276 x <= y | z <= x | z <= y | -(y <= z) | -(z <= y v x).  [para(172(a,1),47(c,1))].

given #582 (F,wt=7): 10876 cy v (cb ^ x) <= cb.  [para(10575(a,1),446(a,2)),rewrite(28(4))].

given #583 (F,wt=7): 10878 cy v x <= x v cb.  [para(10575(a,1),782(a,2,2))].

given #584 (T,wt=7): 10879 cb v (cy ^ x) <= cb.  [para(10575(a,1),801(a,2))].

given #585 (T,wt=7): 10890 B(cb,cy,cb) | cy != cb.  [para(10575(a,1),157(b,1)),rewrite(10575(5)),flip(b)].

given #586 (A,wt=12): 277 x <= y | y ^ (z ^ x) = z ^ y.  [para(172(a,1),53(a,1,2)),flip(b)].

given #587 (F,wt=7): 10893 x ^ cy <= x ^ cb.  [para(10575(a,1),859(a,2,2))].

given #588 (F,wt=7): 10895 cy ^ x <= cb ^ x.  [para(10575(a,1),965(a,2,1))].

given #589 (T,wt=7): 10896 cy <= cb ^ (cy v x).  [para(10575(a,1),972(a,2,2)),rewrite(27(5))].

given #590 (T,wt=7): 10897 cy v (x ^ cb) <= cb.  [para(10575(a,1),1260(a,2)),rewrite(28(4))].

given #591 (A,wt=12): 278 x ^ y <= z | x ^ (z ^ y) = z.  [para(172(a,1),53(a,1)),flip(b)].

given #592 (F,wt=7): 11062 cb v (x ^ cy) = cb.  [para(10857(a,1),119(a,1,2,2))].

given #593 (F,wt=7): 11065 x ^ cy <= cb v y.  [para(10857(a,1),253(a,1,2))].

given #594 (T,wt=7): 11066 cy <= x v (cb v y).  [para(10857(a,1),254(a,1))].

given #595 (T,wt=7): 11068 cy v x <= cb v x.  [para(10857(a,1),446(a,1,1))].

given #596 (A,wt=10): 280 x <= y v z | y ^ x = y.  [para(172(a,1),57(a,1,2)),rewrite(32(4)),flip(b)].

given #597 (F,wt=7): 11076 x ^ cy <= cb ^ x.  [para(10857(a,1),814(a,1,2))].

given #598 (F,wt=7): 11078 cy <= cb ^ (x v cy).  [para(10857(a,1),859(a,1))].

given #599 (T,wt=7): 11086 x v cy <= cb v x.  [para(10857(a,1),1261(a,1,2))].

given #600 (T,wt=7): 11087 cy ^ (cb v x) = cy.  [para(10857(a,1),203(a,1,1)),rewrite(27(5),34(6),27(5)),flip(a)].

given #601 (A,wt=13): 288 (x v y) ^ (y v (x v z)) = y v x.  [para(28(a,1),59(a,1,1))].

given #602 (F,wt=7): 11089 x <= cb | B(x,cb,cy).  [para(10857(a,1),2568(b,3))].

given #603 (F,wt=3): 16657 ca <= cb.  [hyper(43,a,11089,b)].

============================== PROOF =================================

% Proof 1 at 10.46 (+ 0.04) seconds.
% Length of proof is 109.
% Level of proof is 26.
% Maximum clause weight is 22.
% Given clauses 603.

1 (all xa all xx all xb (A(xa,xx,xb) <-> xa <= xx & xx <= xb | xb <= xx & xx <= xa)) # label(non_clause).  [assumption].
2 (all xa all xx all xb (B(xa,xx,xb) <-> (xa ^ xx) v (xx ^ xb) = xx & (xa v xx) ^ (xx v xb) = xx)) # label(non_clause).  [assumption].
5 (all xa all xx all xb (D(xa,xx,xb) <-> xa ^ xb <= xx & xx <= xa v xb)) # label(non_clause).  [assumption].
6 (all x all y (x <= y <-> x ^ y = x)) # label(non_clause).  [assumption].
10 -A(x,y,z) | y <= z | z <= y.  [clausify(1)].
11 -A(x,y,z) | y <= z | y <= x.  [clausify(1)].
13 -D(x,y,z) | A(x,y,z).  [assumption].
20 D(x,y,z) | -(x ^ z <= y) | -(y <= x v z).  [clausify(5)].
25 -D(x,y,z) | y <= z | z <= y.  [resolve(13,b,10,a)].
26 -D(x,y,z) | y <= z | y <= x.  [resolve(13,b,11,a)].
27 x ^ y = y ^ x # label("commutativity_meet").  [assumption].
28 x v y = y v x # label("commutativity_join").  [assumption].
29 (x ^ y) ^ z = x ^ (y ^ z) # label("associativity_meet").  [assumption].
30 (x v y) v z = x v (y v z) # label("associativity_join").  [assumption].
31 (x v y) ^ x = x # label("absorption_1").  [assumption].
32 x ^ (x v y) = x.  [copy(31),rewrite(27(2))].
33 (x ^ y) v x = x # label("absorption_2").  [assumption].
34 x v (x ^ y) = x.  [copy(33),rewrite(28(2))].
35 -B(x,y,z) | (x ^ y) v (y ^ z) = y.  [clausify(2)].
36 -B(x,y,z) | (x v y) ^ (y v z) = y.  [clausify(2)].
37 B(x,y,z) | (x ^ y) v (y ^ z) != y | (x v y) ^ (y v z) != y.  [clausify(2)].
38 -(x <= y) | x ^ y = x.  [clausify(6)].
39 x <= y | x ^ y != x.  [clausify(6)].
40 B(ca,cx,cb).  [assumption].
41 B(cx,cb,cy).  [assumption].
42 cx != cb.  [assumption].
43 -B(ca,cb,cy).  [assumption].
46 x <= y | y <= x | -(z ^ y <= x) | -(x <= z v y).  [resolve(25,a,20,a)].
47 x <= y | x <= z | -(z ^ y <= x) | -(x <= z v y).  [resolve(26,a,20,a)].
53 x ^ (y ^ z) = y ^ (x ^ z).  [para(27(a,1),29(a,1,1)),rewrite(29(2))].
55 x v (y v z) = y v (x v z).  [para(28(a,1),30(a,1,1)),rewrite(30(2))].
56 x ^ (y v x) = x.  [para(28(a,1),32(a,1,2))].
57 x ^ ((x v y) ^ z) = x ^ z.  [para(32(a,1),29(a,1,1)),flip(a)].
60 x v (y ^ x) = x.  [para(27(a,1),34(a,1,2))].
62 x v ((x ^ y) v z) = x v z.  [para(34(a,1),30(a,1,1)),flip(a)].
64 x ^ x = x.  [para(34(a,1),32(a,1,2))].
65 x v x = x.  [para(32(a,1),34(a,1,2))].
77 B(x,y,y v z) | (x v y) ^ (y v (y v z)) != y.  [para(32(a,1),37(b,1,2)),rewrite(28(4),60(4)),xx(b)].
79 B(x,y,y ^ z) | (x ^ y) v (y ^ (y ^ z)) != y.  [para(34(a,1),37(c,1,2)),rewrite(27(9),56(9)),xx(c)].
80 x <= x v y.  [hyper(39,b,32,a)].
84 (cb v cx) ^ (cx v ca) = cx.  [hyper(36,a,40,a),rewrite(28(3),28(6),27(7))].
85 (cb ^ cx) v (cx ^ ca) = cx.  [hyper(35,a,40,a),rewrite(27(3),27(6),28(7))].
86 (cb v cx) ^ (cb v cy) = cb.  [hyper(36,a,41,a),rewrite(28(3))].
87 (cb ^ cx) v (cb ^ cy) = cb.  [hyper(35,a,41,a),rewrite(27(3))].
111 x ^ (x ^ y) = x ^ y.  [para(64(a,1),29(a,1,1)),flip(a)].
116 B(x,y,y ^ z) | (x ^ y) v (y ^ z) != y.  [back_rewrite(79),rewrite(111(5))].
127 x v (x v y) = x v y.  [para(65(a,1),30(a,1,1)),flip(a)].
130 B(x,y,y v z) | (x v y) ^ (y v z) != y.  [back_rewrite(77),rewrite(127(5))].
132 x ^ (y v (x v z)) = x.  [para(55(a,1),32(a,1,2))].
140 x <= y v x.  [para(28(a,1),80(a,2))].
144 x ^ y <= x.  [para(34(a,1),140(a,2))].
145 x v y <= x v (z v y).  [para(55(a,1),140(a,2))].
146 x <= y | y <= x.  [hyper(46,c,144,a,d,80,a)].
147 x ^ y <= y.  [para(27(a,1),144(a,1))].
150 x ^ (y ^ z) <= z.  [para(29(a,1),147(a,1))].
152 x ^ ((y v x) ^ z) = x ^ z.  [para(56(a,1),29(a,1,1)),flip(a)].
158 x ^ (y ^ (z v x)) = y ^ x.  [para(56(a,1),53(a,1,2)),flip(a)].
172 x ^ y = x | y <= x.  [hyper(38,a,146,a)].
180 x v (y v (z ^ x)) = y v x.  [para(60(a,1),55(a,1,2)),flip(a)].
203 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y.  [para(57(a,1),60(a,1,2)),rewrite(28(4))].
269 x <= y | x ^ y = y.  [para(172(a,1),27(a,1)),flip(b)].
279 x <= y | x v y = x.  [para(172(a,1),60(a,1,2))].
283 x <= y | z ^ y <= x.  [para(172(a,1),150(a,1,2))].
339 x <= y | y v x = x.  [para(279(b,1),28(a,1)),flip(b)].
581 cb ^ (cx v ca) = cb ^ cx.  [para(84(a,1),57(a,1,2)),flip(a)].
638 cb v (cx ^ ca) = cb v cx.  [para(85(a,1),62(a,1,2)),flip(a)].
651 cb v cx = cb | cb v cy <= cb v cx.  [para(86(a,1),172(a,1)),flip(a)].
803 x v (y ^ z) <= x v z.  [para(60(a,1),145(a,2,2))].
1527 cx <= ca v (cb ^ cx).  [para(85(a,1),803(a,1)),rewrite(28(6))].
1529 cb <= cy v (cb ^ cx).  [para(87(a,1),803(a,1)),rewrite(28(6))].
1533 cb v cx <= cb v ca.  [para(638(a,1),803(a,1))].
1540 cx <= cb | cx <= cb v ca.  [para(172(a,1),1527(a,2,2)),rewrite(28(7))].
1547 cb <= cb ^ cx | cb <= cy.  [hyper(47,c,283,b,d,1529,a),merge(c)].
1559 (cb v cx) ^ (cb v ca) = cb v cx.  [hyper(38,a,1533,a)].
1583 cb <= ca | cx <= cb.  [para(279(b,1),1540(b,2)),merge(c)].
1584 cb ^ cx = cx | cb <= ca.  [hyper(38,a,1583,b),rewrite(27(3))].
1614 cb ^ cx = cb | cb <= cy.  [hyper(38,a,1547,a),rewrite(111(5))].
2075 cb <= cy | cb <= ca.  [para(1614(a,1),1584(a,1)),flip(b),unit_del(b,42)].
2078 cb ^ cy = cb | cb <= ca.  [hyper(38,a,2075,a)].
2568 x <= y | B(x,y,y ^ z).  [para(269(b,1),116(b,1,1)),rewrite(34(5)),xx(c)].
3063 cb <= ca | cb v cy = cy.  [para(2078(a,1),60(a,1,2)),rewrite(28(6))].
3574 x <= y | B(y,x,x v z).  [para(339(b,1),130(b,1,1)),rewrite(32(5)),xx(c)].
4505 cx ^ (cb v cy) = cb ^ cx.  [para(86(a,1),152(a,1,2)),rewrite(27(3)),flip(a)].
4871 ca ^ (cb v cx) = cx ^ ca.  [para(84(a,1),158(a,1,2)),rewrite(27(3),27(8)),flip(a)].
4894 cb ^ (cx ^ ca) = cb ^ ca.  [para(581(a,1),158(a,1,2)),rewrite(53(5),27(4))].
5768 ca v (cb ^ cx) = cx v ca.  [para(85(a,1),180(a,1,2)),rewrite(28(3),28(8)),flip(a)].
9702 cb <= ca | cb <= x | B(x,cb,cy).  [para(3063(b,1),3574(b,3))].
9709 cb <= ca.  [factor(9702,a,b),unit_del(b,43)].
9711 cb ^ ca = cb.  [hyper(38,a,9709,a)].
9794 cb ^ (cx ^ ca) = cb.  [back_rewrite(4894),rewrite(9711(8))].
9836 cb ^ (x ^ ca) = x ^ cb.  [para(9711(a,1),53(a,1,2)),flip(a)].
9837 cb v ca = ca.  [para(9711(a,1),60(a,1,2)),rewrite(28(3))].
9901 cb ^ cx = cb.  [back_rewrite(9794),rewrite(9836(5),27(3))].
9962 cb v cx = cx ^ ca.  [back_rewrite(1559),rewrite(9837(6),27(5),4871(5)),flip(a)].
10004 cx v ca = ca.  [back_rewrite(5768),rewrite(9901(4),28(3),9837(3)),flip(a)].
10012 cx ^ (cb v cy) = cb.  [back_rewrite(4505),rewrite(9901(8))].
10084 cx ^ ca = cx.  [back_rewrite(85),rewrite(9901(3),638(5),9962(3))].
10186 cb v cy <= cx.  [back_rewrite(651),rewrite(9962(3),10084(3),9962(9),10084(9)),unit_del(a,42)].
10240 cb v cx = cx.  [back_rewrite(9962),rewrite(10084(6))].
10442 cx ^ (x v ca) = cx.  [para(10004(a,1),132(a,1,2,2))].
10477 (cx ^ x) v (ca ^ x) = ca ^ x.  [para(10004(a,1),203(a,1,2,1)),rewrite(10004(8))].
10575 cb v cy = cb.  [hyper(38,a,10186,a),rewrite(27(5),10012(5)),flip(a)].
10613 (cb ^ x) v (cx ^ x) = cx ^ x.  [para(10240(a,1),203(a,1,2,1)),rewrite(10240(8))].
10857 cb ^ cy = cy.  [para(10575(a,1),56(a,1,2)),rewrite(27(3))].
11089 x <= cb | B(x,cb,cy).  [para(10857(a,1),2568(b,3))].
16657 ca <= cb.  [hyper(43,a,11089,b)].
16659 ca = cb.  [hyper(38,a,16657,a),rewrite(27(3),9711(3)),flip(a)].
16931 cx ^ x = cb ^ x.  [back_rewrite(10477),rewrite(16659(3),28(5),10613(5),16659(3))].
16939 $F.  [back_rewrite(10442),rewrite(16659(2),16931(4),56(4)),flip(a),unit_del(a,42)].

============================== end of proof ==========================

============================== STATISTICS ============================

Given=603. Generated=134869. Kept=16910. proofs=1.
Usable=336. Sos=7305. Demods=627. Limbo=280, Disabled=9028. Hints=0.
Weight_deleted=64. Literals_deleted=0.
Forward_subsumed=112563. Back_subsumed=6316.
Sos_limit_deleted=5331. Sos_displaced=0. Sos_removed=0.
New_demodulators=767 (7 lex), Back_demodulated=2661. Back_unit_deleted=10.
Demod_attempts=1958305. Demod_rewrites=148145.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=6335754. Nonunit_bsub_feature_tests=818756.
Megabytes=8.80.
User_CPU=10.46, System_CPU=0.04, Wall_clock=11.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 11452 exit (max_proofs) Sat Aug 12 21:01:32 2006