============================== Prover9 ===============================
Prover9 (32) version March-2007, March 2007.
Process 21276 was started by mccune on cleo,
Mon Mar 19 17:11:02 2007
The command was "/home/mccune/bin/prover9 -f lt.in uc.in H78b.in".
============================== end of head ===========================

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

% Reading from file lt.in


formulas(sos).
x v y = y v x.
(x v y) v z = x v (y v z).
x ^ y = y ^ x.
(x ^ y) ^ z = x ^ (y ^ z).
x ^ (x v y) = x.
x v (x ^ y) = x.
end_of_list.

% Reading from file uc.in


formulas(sos).
x v x' = 1.
x ^ x' = 0.
x v y != 1 | x ^ y != 0 | x' = y.
end_of_list.

% Reading from file H78b.in


list(weights).
weight(x') = weight(x).
weight(x v (y v (z v u))) = 1000.
weight(x ^ (y ^ (z ^ u))) = 1000.
end_of_list.

formulas(sos).
x ^ (y v (z ^ (y v u))) = x ^ (y v (z ^ (u v (y ^ (x v u))))) # label(H78).
end_of_list.

formulas(goals).
(all x all y (x ^ y = x -> x' v y' = x')).
end_of_list.

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

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

% Formulas that are not ordinary clauses:
1 (all x all y (x ^ y = x -> x' v y' = x')) # label(goal).  [goal].

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

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

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
x v y = y v x.  [assumption].
(x v y) v z = x v (y v z).  [assumption].
x ^ y = y ^ x.  [assumption].
(x ^ y) ^ z = x ^ (y ^ z).  [assumption].
x ^ (x v y) = x.  [assumption].
x v (x ^ y) = x.  [assumption].
x v x' = 1.  [assumption].
x ^ x' = 0.  [assumption].
x v y != 1 | x ^ y != 0 | x' = y.  [assumption].
x ^ (y v (z ^ (y v u))) = x ^ (y v (z ^ (u v (y ^ (x v u))))) # label(H78).  [assumption].
c1 ^ c2 = c1.  [deny(1)].
c1' != c1' v c2'.  [deny(1)].
end_of_list.

formulas(demodulators).
end_of_list.

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

No predicates eliminated.

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

Auto_denials:  (no changes).

Term ordering decisions:
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ 0, 1, c1, c2, ^, v, ' ]).
After inverse_order: Function symbol precedence:  lex([ 0, 1, c1, c2, ^, v, ' ]).
Unfolding symbols: (none).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).
  % set(hyper_resolution).  % (nonunit Horn with equality)
  % set(neg_ur_resolution).  % (nonunit Horn with equality)
  % assign(para_lit_limit, 3).  % (nonunit Horn with equality)

Auto_process settings:  (no changes).

% Operation v is commutative; C redundancy checks enabled.

% Operation ^ 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).
2 x v y = y v x.  [assumption].
3 (x v y) v z = x v (y v z).  [assumption].
4 x ^ y = y ^ x.  [assumption].
5 (x ^ y) ^ z = x ^ (y ^ z).  [assumption].
6 x ^ (x v y) = x.  [assumption].
7 x v (x ^ y) = x.  [assumption].
8 x v x' = 1.  [assumption].
9 x ^ x' = 0.  [assumption].
10 x v y != 1 | x ^ y != 0 | x' = y.  [assumption].
12 x ^ (y v (z ^ (u v (y ^ (x v u))))) = x ^ (y v (z ^ (y v u))).  [copy(11),flip(a)].
13 c1 ^ c2 = c1.  [deny(1)].
15 c1' v c2' != c1'.  [copy(14),flip(a)].
end_of_list.

formulas(demodulators).
2 x v y = y v x.  [assumption].
        % (lex-dep)
3 (x v y) v z = x v (y v z).  [assumption].
4 x ^ y = y ^ x.  [assumption].
        % (lex-dep)
5 (x ^ y) ^ z = x ^ (y ^ z).  [assumption].
6 x ^ (x v y) = x.  [assumption].
7 x v (x ^ y) = x.  [assumption].
8 x v x' = 1.  [assumption].
9 x ^ x' = 0.  [assumption].
13 c1 ^ c2 = c1.  [deny(1)].
end_of_list.

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

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

% Starting search at 0.00 seconds.

given #1 (I,wt=7): 2 x v y = y v x.  [assumption].

given #2 (I,wt=11): 3 (x v y) v z = x v (y v z).  [assumption].

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

given #3 (I,wt=7): 4 x ^ y = y ^ x.  [assumption].

given #4 (I,wt=11): 5 (x ^ y) ^ z = x ^ (y ^ z).  [assumption].

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

given #5 (I,wt=7): 6 x ^ (x v y) = x.  [assumption].

given #6 (I,wt=7): 7 x v (x ^ y) = x.  [assumption].

given #7 (I,wt=5): 8 x v x' = 1.  [assumption].

given #8 (I,wt=5): 9 x ^ x' = 0.  [assumption].

given #9 (I,wt=13): 10 x v y != 1 | x ^ y != 0 | x' = y.  [assumption].

given #10 (I,wt=23): 12 x ^ (y v (z ^ (u v (y ^ (x v u))))) = x ^ (y v (z ^ (y v u))).  [copy(11),flip(a)].

given #11 (I,wt=5): 13 c1 ^ c2 = c1.  [deny(1)].

given #12 (I,wt=5): 15 c1' v c2' != c1'.  [copy(14),flip(a)].

given #13 (A,wt=11): 17 x v (y v z) = y v (x v z).  [para(2(a,1),3(a,1,1)),rewrite(3(2))].

given #14 (T,wt=5): 28 x ^ x = x.  [para(7(a,1),6(a,1,2))].

given #15 (T,wt=5): 29 x v x = x.  [para(6(a,1),7(a,1,2))].

given #16 (T,wt=5): 32 x ^ 1 = x.  [para(8(a,1),6(a,1,2))].

given #17 (T,wt=5): 35 x v 0 = x.  [para(9(a,1),7(a,1,2))].

given #18 (A,wt=11): 19 x ^ (y ^ z) = y ^ (x ^ z).  [para(4(a,1),5(a,1,1)),rewrite(5(2))].

given #19 (T,wt=5): 73 1 ^ x = x.  [para(32(a,1),4(a,1)),flip(a)].

given #20 (T,wt=3): 82 1' = 0.  [hyper(10,a,35,a,b,73,a)].

given #21 (T,wt=5): 75 0 v x = x.  [para(35(a,1),2(a,1)),flip(a)].

given #22 (T,wt=3): 85 0' = 1.  [hyper(10,a,75,a,b,32,a)].

given #23 (A,wt=7): 20 x ^ (y v x) = x.  [para(2(a,1),6(a,1,2))].

given #24 (T,wt=5): 83 1 v x = 1.  [para(73(a,1),6(a,1))].

given #25 (T,wt=5): 86 0 ^ x = 0.  [para(75(a,1),6(a,1,2))].

given #26 (T,wt=5): 94 x v 1 = 1.  [para(20(a,1),73(a,1)),flip(a)].

given #27 (T,wt=5): 97 x ^ 0 = 0.  [para(86(a,1),4(a,1)),flip(a)].

given #28 (A,wt=13): 21 (x v y) ^ (x v (y v z)) = x v y.  [para(3(a,1),6(a,1,2))].

given #29 (T,wt=6): 95 0 != x | x' = 1.  [back_rewrite(74),rewrite(94(2)),xx(a)].

given #30 (T,wt=6): 99 1 != x | x' = 0.  [back_rewrite(76),rewrite(97(4)),xx(b)].

given #31 (T,wt=7): 26 x v (y ^ x) = x.  [para(4(a,1),7(a,1,2))].

given #32 (T,wt=5): 108 c1 v c2 = c2.  [para(13(a,1),26(a,1,2)),rewrite(2(3))].

given #33 (A,wt=11): 22 x ^ ((x v y) ^ z) = x ^ z.  [para(6(a,1),5(a,1,1)),flip(a)].

given #34 (T,wt=7): 84 x v (x' v y) = 1.  [back_rewrite(30),rewrite(83(5))].

given #35 (T,wt=7): 87 x ^ (x' ^ y) = 0.  [back_rewrite(33),rewrite(86(5))].

given #36 (T,wt=7): 96 x v (y v x') = 1.  [back_rewrite(64),rewrite(94(5))].

given #37 (T,wt=7): 98 x ^ (y ^ x') = 0.  [back_rewrite(79),rewrite(97(5))].

given #38 (A,wt=13): 23 x ^ (y ^ ((x ^ y) v z)) = x ^ y.  [para(6(a,1),5(a,1)),flip(a)].

given #39 (F,wt=7): 120 c1 ^ (c1' v c2') != 0.  [ur(10,a,84,a,c,15,a(flip))].

given #40 (T,wt=7): 116 x ^ (x v y)' = 0.  [para(9(a,1),22(a,1,2)),rewrite(97(2)),flip(a)].

given #41 (T,wt=5): 137 c1 ^ c2' = 0.  [para(108(a,1),116(a,1,2,1))].

given #42 (T,wt=7): 132 x ^ (y v x)' = 0.  [para(2(a,1),116(a,1,2,1))].

given #43 (T,wt=7): 138 c1 ^ (c2' ^ x) = 0.  [para(137(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #44 (A,wt=11): 24 x v ((x ^ y) v z) = x v z.  [para(7(a,1),3(a,1,1)),flip(a)].

given #45 (T,wt=7): 140 c1 ^ (x ^ c2') = 0.  [para(137(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #46 (T,wt=7): 149 x v (x ^ y)' = 1.  [para(8(a,1),24(a,1,2)),rewrite(94(2)),flip(a)].

given #47 (T,wt=7): 158 x v (y ^ x)' = 1.  [para(4(a,1),149(a,1,2,1))].

given #48 (T,wt=5): 166 c2 v c1' = 1.  [para(13(a,1),158(a,1,2,1))].

given #49 (A,wt=13): 25 x v (y v ((x v y) ^ z)) = x v y.  [para(7(a,1),3(a,1)),flip(a)].

given #50 (T,wt=7): 171 c2 v (c1' v x) = 1.  [para(166(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #51 (T,wt=7): 173 c2 v (x v c1') = 1.  [para(166(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #52 (T,wt=8): 139 c1 v c2' != 1 | c2' = c1'.  [para(137(a,1),10(b,1)),flip(c),xx(b)].

given #53 (T,wt=8): 172 c2 ^ c1' != 0 | c2' = c1'.  [para(166(a,1),10(a,1)),xx(a)].

given #54 (A,wt=13): 27 (x ^ y) v (x ^ (y ^ z)) = x ^ y.  [para(5(a,1),7(a,1,2))].

given #55 (T,wt=9): 31 x v (y v (x v y)') = 1.  [para(8(a,1),3(a,1)),flip(a)].

given #56 (T,wt=9): 34 x ^ (y ^ (x ^ y)') = 0.  [para(9(a,1),5(a,1)),flip(a)].

given #57 (T,wt=9): 59 c1 ^ (c2 ^ x) = c1 ^ x.  [para(13(a,1),5(a,1,1)),flip(a)].

given #58 (T,wt=7): 191 c1 ^ (c2 v x) = c1.  [para(6(a,1),59(a,1,2)),rewrite(13(3)),flip(a)].

given #59 (A,wt=13): 36 x v y != 1 | y ^ x != 0 | y' = x.  [para(2(a,1),10(a,1))].

given #60 (T,wt=3): 208 x'' = x.  [para(8(a,1),36(a,1)),rewrite(4(5),9(5)),xx(a),xx(b)].

given #61 (T,wt=7): 193 c1 ^ (x v c2) = c1.  [para(20(a,1),59(a,1,2)),rewrite(13(3)),flip(a)].

given #62 (T,wt=7): 197 c1 ^ (c2 v x)' = 0.  [para(116(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #63 (T,wt=7): 198 c1 ^ (x v c2)' = 0.  [para(132(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #64 (A,wt=19): 37 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y)' = z.  [para(3(a,1),10(a,1))].

given #65 (T,wt=7): 223 x' v (y v x) = 1.  [para(208(a,1),96(a,1,2,2))].

given #66 (T,wt=7): 224 x' ^ (y ^ x) = 0.  [para(208(a,1),98(a,1,2,2))].

given #67 (T,wt=8): 218 c2 ^ c1' != 0 | c2 = c1.  [para(166(a,1),36(a,1)),rewrite(4(7),208(12)),flip(c),xx(a)].

given #68 (T,wt=9): 60 c2 ^ (x ^ c1) = x ^ c1.  [para(13(a,1),5(a,2,2)),rewrite(4(4))].

given #69 (A,wt=13): 38 x v y != 1 | y ^ x != 0 | x' = y.  [para(4(a,1),10(b,1))].

given #70 (T,wt=7): 276 c2 v (x ^ c1) = c2.  [para(60(a,1),7(a,1,2))].

given #71 (T,wt=7): 279 c2 v (x ^ c1)' = 1.  [para(60(a,1),149(a,1,2,1))].

given #72 (T,wt=7): 304 c2 v (c1 ^ x) = c2.  [para(4(a,1),276(a,1,2))].

given #73 (T,wt=7): 309 c2 v (c1 ^ x)' = 1.  [para(4(a,1),279(a,1,2,1))].

given #74 (A,wt=19): 39 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z.  [para(5(a,1),10(b,1))].

given #75 (T,wt=8): 291 c1 v c2' != 1 | c2 = c1.  [para(137(a,1),38(b,1)),rewrite(2(4),208(12)),xx(b)].

given #76 (T,wt=9): 62 x ^ (y v (x v z)) = x.  [para(17(a,1),6(a,1,2))].

given #77 (T,wt=9): 66 x ^ (x ^ y) = x ^ y.  [para(28(a,1),5(a,1,1)),flip(a)].

given #78 (T,wt=9): 67 x ^ (y ^ x) = y ^ x.  [para(28(a,1),5(a,2,2)),rewrite(4(2))].

given #79 (A,wt=23): 42 x ^ (y v (z ^ (u v (y ^ (u v x))))) = x ^ (y v (z ^ (y v u))).  [para(2(a,1),12(a,1,2,2,2,2,2))].

given #80 (T,wt=9): 68 1 != x | 0 != x | x' = x.  [para(28(a,1),10(b,1)),rewrite(29(1)),flip(a),flip(b)].

given #81 (T,wt=9): 70 x v (x v y) = x v y.  [para(29(a,1),3(a,1,1)),flip(a)].

given #82 (T,wt=9): 71 x v (y v x) = y v x.  [para(29(a,1),3(a,2,2)),rewrite(2(2))].

given #83 (T,wt=9): 78 x v (y ^ (x ^ z)) = x.  [para(19(a,1),7(a,1,2))].

given #84 (A,wt=23): 43 x ^ (y v (z ^ (u v (y ^ (x v u))))) = x ^ (y v (z ^ (u v y))).  [para(2(a,1),12(a,2,2,2,2))].

given #85 (T,wt=9): 81 c1 ^ (x ^ c2) = x ^ c1.  [para(13(a,1),19(a,1,2)),flip(a)].

given #86 (T,wt=9): 88 x ^ (y v (z v x)) = x.  [para(3(a,1),20(a,1,2))].

given #87 (T,wt=9): 106 x v (y ^ (z ^ x)) = x.  [para(5(a,1),26(a,1,2))].

given #88 (T,wt=9): 111 c2 != 1 | c1 != 0 | c1' = c2.  [back_rewrite(61),rewrite(108(3))].

given #89 (A,wt=23): 48 x ^ (y v ((z v (y ^ (x v z))) ^ u)) = x ^ (y v (u ^ (y v z))).  [para(4(a,1),12(a,1,2,2))].

given #90 (T,wt=9): 112 c1 v (c2 v x) = c2 v x.  [para(108(a,1),3(a,1,1)),flip(a)].

given #91 (T,wt=9): 113 c2 v (x v c1) = x v c2.  [para(108(a,1),3(a,2,2)),rewrite(2(4))].

given #92 (T,wt=9): 114 c1 v (x v c2) = x v c2.  [para(108(a,1),17(a,1,2)),flip(a)].

given #93 (T,wt=9): 123 x ^ ((x v y)' ^ z) = 0.  [para(87(a,1),22(a,1,2)),rewrite(97(2)),flip(a)].

given #94 (A,wt=39): 54 x v (y v (z ^ (u v (y ^ (x v u))))) != 1 | x ^ (y v (z ^ (y v u))) != 0 | x' = y v (z ^ (u v (y ^ (x v u)))).  [para(12(a,1),10(b,1))].

given #95 (T,wt=9): 126 x ^ (y ^ (x v z)') = 0.  [para(98(a,1),22(a,1,2)),rewrite(97(2)),flip(a)].

given #96 (T,wt=9): 136 x ^ (y v (x v z))' = 0.  [para(17(a,1),116(a,1,2,1))].

given #97 (T,wt=9): 141 x ^ (y v (z v x))' = 0.  [para(3(a,1),132(a,1,2,1))].

given #98 (T,wt=9): 142 x ^ ((y v x)' ^ z) = 0.  [para(132(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #99 (A,wt=31): 55 x v (y v (z ^ (y v u))) != 1 | x ^ (y v (z ^ (u v y))) != 0 | x' = y v (z ^ (y v u)).  [para(12(a,2),10(b,1)),rewrite(43(12))].

given #100 (T,wt=9): 146 x ^ (y ^ (z v x)') = 0.  [para(132(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #101 (T,wt=9): 153 x v ((x ^ y)' v z) = 1.  [para(84(a,1),24(a,1,2)),rewrite(94(2)),flip(a)].

given #102 (T,wt=9): 154 x v (y v (x ^ z)') = 1.  [para(96(a,1),24(a,1,2)),rewrite(94(2)),flip(a)].

given #103 (T,wt=9): 161 x v (y ^ (x ^ z))' = 1.  [para(19(a,1),149(a,1,2,1))].

given #104 (A,wt=43): 56 x ^ (y v (z ^ ((u ^ (v v (x ^ (y v v)))) v (y ^ (x v (u ^ (x v v))))))) = x ^ (y v (z ^ (y v (u ^ (v v (x ^ (y v v))))))).  [para(12(a,1),12(a,1,2,2,2,2))].

given #105 (T,wt=9): 162 x v ((y ^ x)' v z) = 1.  [para(158(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #106 (T,wt=9): 164 x v (y ^ (z ^ x))' = 1.  [para(5(a,1),158(a,1,2,1))].

given #107 (T,wt=9): 167 x v (y v (z ^ x)') = 1.  [para(158(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #108 (T,wt=9): 185 x v (y v (y v x)') = 1.  [para(2(a,1),31(a,1,2,2,1))].

given #109 (A,wt=35): 57 x ^ (y v (z ^ ((u ^ (x v v)) v (y ^ (x v (u ^ (v v x))))))) = x ^ (y v (z ^ (y v (u ^ (x v v))))).  [para(12(a,2),12(a,1,2,2,2,2)),rewrite(43(8))].

given #110 (T,wt=9): 188 x ^ (y ^ (y ^ x)') = 0.  [para(4(a,1),34(a,1,2,2,1))].

given #111 (T,wt=9): 199 (c2 ^ x) v (c1 ^ x)' = 1.  [para(59(a,1),158(a,1,2,1))].

given #112 (T,wt=9): 200 c1 ^ (x ^ (c2 ^ x)') = 0.  [para(34(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #113 (T,wt=9): 202 c1 ^ (x v (c2 v y)) = c1.  [para(17(a,1),191(a,1,2))].

given #114 (A,wt=17): 58 x ^ (y v (z ^ (y v x))) = x ^ (y v (z ^ x)).  [para(12(a,2),12(a,1,2,2)),rewrite(20(2),29(1),26(2)),flip(a)].

given #115 (T,wt=9): 212 c2 != 1 | c1 != 0 | c2' = c1.  [para(108(a,1),36(a,1)),rewrite(4(6),13(6))].

given #116 (T,wt=9): 225 c1 ^ (x v (y v c2)) = c1.  [para(3(a,1),193(a,1,2))].

given #117 (T,wt=9): 229 c1 ^ ((c2 v x)' ^ y) = 0.  [para(197(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #118 (T,wt=9): 231 c1 ^ (x v (c2 v y))' = 0.  [para(17(a,1),197(a,1,2,1))].

given #119 (A,wt=11): 63 x v (y v (x ^ z)) = y v x.  [para(7(a,1),17(a,1,2)),flip(a)].

given #120 (T,wt=9): 232 c1 ^ (x ^ (c2 v y)') = 0.  [para(197(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #121 (T,wt=9): 233 c1 ^ (x v (y v c2))' = 0.  [para(3(a,1),198(a,1,2,1))].

given #122 (T,wt=9): 234 c1 ^ ((x v c2)' ^ y) = 0.  [para(198(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #123 (T,wt=9): 236 c1 ^ (x ^ (y v c2)') = 0.  [para(198(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #124 (A,wt=19): 65 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z.  [para(17(a,1),10(a,1))].

given #125 (T,wt=9): 305 c2 v (x ^ (y ^ c1)) = c2.  [para(5(a,1),276(a,1,2))].

given #126 (T,wt=9): 308 c2 v ((x ^ c1)' v y) = 1.  [para(279(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #127 (T,wt=9): 310 c2 v (x ^ (y ^ c1))' = 1.  [para(5(a,1),279(a,1,2,1))].

given #128 (T,wt=9): 312 c2 v (x v (y ^ c1)') = 1.  [para(279(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #129 (A,wt=13): 69 1 != x | x ^ y != 0 | x' = x ^ y.  [back_rewrite(41),rewrite(66(4))].

given #130 (T,wt=6): 1267 c1 != 1 | c1' = 0.  [para(137(a,1),69(b,1)),rewrite(137(12)),flip(a),xx(b)].

given #131 (T,wt=6): 1269 x' != 1 | 0 = x.  [para(224(a,1),69(b,1)),rewrite(208(8),224(9)),flip(a),flip(c),xx(b)].

given #132 (T,wt=9): 318 c2 v (x ^ (c1 ^ y)) = c2.  [para(19(a,1),304(a,1,2))].

given #133 (T,wt=9): 321 c2 v ((c1 ^ x)' v y) = 1.  [para(309(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #134 (A,wt=13): 72 x v y != 1 | 0 != x | x' = x v y.  [back_rewrite(40),rewrite(70(2))].

given #135 (F,wt=7): 1273 (c1 ^ (c1' v c2'))' != 1.  [ur(1269,b,120,a(flip))].

given #136 (T,wt=6): 1301 c2 != 0 | c2' = 1.  [para(166(a,1),72(a,1)),rewrite(166(12)),flip(b),xx(a)].

given #137 (T,wt=6): 1302 x' != 0 | 1 = x.  [para(223(a,1),72(a,1)),rewrite(208(8),223(9)),flip(b),flip(c),xx(a)].

given #138 (T,wt=9): 323 c2 v (x v (c1 ^ y)') = 1.  [para(309(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #139 (T,wt=9): 324 c2 v (x ^ (c1 ^ y))' = 1.  [para(19(a,1),309(a,1,2,1))].

given #140 (A,wt=11): 77 x ^ (y ^ (x v z)) = y ^ x.  [para(6(a,1),19(a,1,2)),flip(a)].

given #141 (T,wt=9): 472 (x ^ c2) v (x ^ c1)' = 1.  [para(81(a,1),158(a,1,2,1))].

given #142 (T,wt=9): 473 x ^ (c1 ^ (x ^ c2)') = 0.  [para(81(a,1),224(a,1,2)),rewrite(4(6),5(6))].

given #143 (T,wt=9): 602 c2 v (x v c1) = c2 v x.  [para(113(a,2),2(a,1))].

given #144 (T,wt=9): 604 (x v c1) ^ (x v c2)' = 0.  [para(113(a,1),132(a,1,2,1))].

given #145 (A,wt=19): 80 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x' = y ^ z.  [para(19(a,1),10(b,1))].

given #146 (T,wt=9): 608 x v (c2 v (x v c1)') = 1.  [para(113(a,1),223(a,1,2)),rewrite(2(6),3(6))].

given #147 (T,wt=9): 1027 c1 ^ (x ^ (x ^ c2)') = 0.  [para(188(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #148 (T,wt=9): 1033 (x ^ c2) v (c1 ^ x)' = 1.  [para(4(a,1),199(a,1,1))].

given #149 (T,wt=9): 1034 (c2 ^ x) v (x ^ c1)' = 1.  [para(4(a,1),199(a,1,2,1))].

given #150 (A,wt=11): 89 x ^ ((y v x) ^ z) = x ^ z.  [para(20(a,1),5(a,1,1)),flip(a)].

given #151 (T,wt=9): 1035 (c2 ^ (c1 v x)) v c1' = 1.  [para(6(a,1),199(a,1,2,1))].

given #152 (T,wt=9): 1039 (c2 ^ (x v c1)) v c1' = 1.  [para(20(a,1),199(a,1,2,1))].

given #153 (T,wt=9): 1058 x ^ (c1 ^ (c2 ^ x)') = 0.  [para(200(a,1),19(a,1)),flip(a)].

given #154 (T,wt=9): 1059 c1 ^ (c2 ^ (c1 v x))' = 0.  [para(200(a,1),22(a,1)),flip(a)].

given #155 (A,wt=13): 90 x ^ (y ^ (z v (x ^ y))) = x ^ y.  [para(20(a,1),5(a,1)),flip(a)].

given #156 (T,wt=9): 1265 c1 != 1 | c1 != 0 | c1' = c1.  [para(13(a,1),69(b,1)),rewrite(13(11)),flip(a)].

given #157 (T,wt=9): 1303 c2 != 1 | c2 != 0 | c2' = c2.  [para(276(a,1),72(a,1)),rewrite(276(12)),flip(b)].

given #158 (T,wt=9): 1358 (x v c1) ^ (c2 v x)' = 0.  [para(602(a,1),132(a,1,2,1))].

given #159 (T,wt=9): 1361 c2 v (x v (x v c1)') = 1.  [para(602(a,1),223(a,1,2)),rewrite(2(6),3(6))].

given #160 (A,wt=13): 91 x v y != 1 | 0 != y | y' = x v y.  [para(20(a,1),10(b,1)),rewrite(71(2)),flip(b)].

given #161 (T,wt=6): 1601 c1' != 0 | c1 = 1.  [para(166(a,1),91(a,1)),rewrite(208(10),166(12)),flip(b),xx(a)].

given #162 (T,wt=9): 1376 (c1 v x) ^ (x v c2)' = 0.  [para(2(a,1),604(a,1,1))].

given #163 (T,wt=9): 1440 x v (c2 v (c1 v x)') = 1.  [para(2(a,1),608(a,1,2,2,1))].

given #164 (T,wt=9): 1504 c1 ^ (c2 ^ (x v c1))' = 0.  [para(89(a,1),200(a,1))].

given #165 (A,wt=13): 92 (x v y) ^ (x v (z v y)) = x v y.  [para(17(a,1),20(a,1,2))].

given #166 (T,wt=9): 1509 c1' v (c2 ^ (c1 v x)) = 1.  [para(1035(a,1),2(a,1)),flip(a)].

given #167 (T,wt=9): 1523 c1' v (c2 ^ (x v c1)) = 1.  [para(1039(a,1),2(a,1)),flip(a)].

given #168 (T,wt=9): 1572 (c1 v x) ^ (c2 v x)' = 0.  [para(2(a,1),1358(a,1,1))].

given #169 (T,wt=9): 1573 (c1 v (c2 ^ x)) ^ c2' = 0.  [para(7(a,1),1358(a,1,2,1)),rewrite(2(4))].

given #170 (A,wt=11): 93 x ^ (y ^ (z v x)) = y ^ x.  [para(20(a,1),19(a,1,2)),flip(a)].

given #171 (T,wt=9): 1576 (c1 v (x ^ c2)) ^ c2' = 0.  [para(26(a,1),1358(a,1,2,1)),rewrite(2(4))].

given #172 (T,wt=9): 1585 c2 v (x v (c1 v x)') = 1.  [para(2(a,1),1361(a,1,2,2,1))].

given #173 (T,wt=9): 1586 c2 v (c1 v (c2 ^ x))' = 1.  [para(1361(a,1),24(a,1)),rewrite(2(6)),flip(a)].

given #174 (T,wt=9): 1697 c2' ^ (c1 v (c2 ^ x)) = 0.  [para(1573(a,1),4(a,1)),flip(a)].

given #175 (A,wt=13): 100 (x v y) ^ (y v (x v z)) = y v x.  [para(2(a,1),21(a,1,1))].

given #176 (T,wt=6): 1769 c2' != 1 | c2 = 0.  [para(1697(a,1),69(b,1)),rewrite(208(10),1697(15)),flip(a),xx(b)].

given #177 (T,wt=9): 1723 c2' ^ (c1 v (x ^ c2)) = 0.  [para(1576(a,1),4(a,1)),flip(a)].

given #178 (T,wt=9): 1742 c2 v (c1 v (x ^ c2))' = 1.  [para(4(a,1),1586(a,1,2,1,2))].

given #179 (T,wt=10): 245 x v y != 0 | (x v y)' = 1.  [para(32(a,1),37(b,1)),rewrite(94(2),94(2)),xx(a)].

given #180 (A,wt=13): 101 (x v y) ^ (y v (z v x)) = x v y.  [para(2(a,1),21(a,1,2)),rewrite(3(3))].

given #181 (T,wt=7): 1827 c1' v (x v c2) = 1.  [para(166(a,1),101(a,1,1)),rewrite(73(7),166(9))].

given #182 (T,wt=9): 1825 (x ^ y)' v (z v x) = 1.  [para(149(a,1),101(a,1,1)),rewrite(73(6),149(7))].

given #183 (T,wt=9): 1826 (x ^ y)' v (z v y) = 1.  [para(158(a,1),101(a,1,1)),rewrite(73(6),158(7))].

given #184 (T,wt=9): 1832 (x ^ c1)' v (y v c2) = 1.  [para(279(a,1),101(a,1,1)),rewrite(73(8),279(11))].

given #185 (A,wt=17): 102 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u.  [para(21(a,1),5(a,1,1)),flip(a)].

given #186 (T,wt=9): 1834 (c1 ^ x)' v (y v c2) = 1.  [para(309(a,1),101(a,1,1)),rewrite(73(8),309(11))].

given #187 (T,wt=10): 246 x v y != 1 | (x v y)' = 0.  [para(35(a,1),37(a,1,2)),rewrite(4(6),86(6)),xx(b)].

given #188 (T,wt=6): 1949 c2 != 1 | c2' = 0.  [para(108(a,1),246(a,1)),rewrite(108(6))].

given #189 (T,wt=10): 332 x ^ y != 0 | (x ^ y)' = 1.  [para(32(a,1),39(b,1,2)),rewrite(2(3),83(3)),xx(a)].

given #190 (A,wt=17): 103 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y).  [para(21(a,1),19(a,1,2)),flip(a)].

given #191 (T,wt=6): 1951 c1 != 0 | c1' = 1.  [para(13(a,1),332(a,1)),rewrite(13(6))].

given #192 (T,wt=10): 333 x ^ y != 1 | (x ^ y)' = 0.  [para(35(a,1),39(a,1)),rewrite(97(5),97(5)),xx(b)].

given #193 (T,wt=10): 1600 (x ^ y)' != 0 | x ^ y = 1.  [para(149(a,1),91(a,1)),rewrite(208(10),149(11)),flip(b),xx(a)].

given #194 (T,wt=10): 1817 x v y != 0 | (y v x)' = 1.  [para(2(a,1),245(a,1))].

given #195 (A,wt=11): 104 x v ((y ^ x) v z) = x v z.  [para(26(a,1),3(a,1,1)),flip(a)].

given #196 (T,wt=10): 1947 x v y != 1 | (y v x)' = 0.  [para(2(a,1),246(a,1))].

given #197 (T,wt=10): 1950 x ^ y != 0 | (y ^ x)' = 1.  [para(4(a,1),332(a,1))].

given #198 (T,wt=10): 1971 x ^ y != 1 | (y ^ x)' = 0.  [para(4(a,1),333(a,1))].

given #199 (T,wt=10): 1975 (x ^ y)' != 0 | y ^ x = 1.  [para(4(a,1),1600(a,1,1))].

given #200 (A,wt=13): 105 x v (y v (z ^ (x v y))) = x v y.  [para(26(a,1),3(a,1)),flip(a)].

given #201 (T,wt=10): 1977 (x v y)' != 0 | x v y = 1.  [para(21(a,1),1600(a,1,1)),rewrite(21(8))].

given #202 (T,wt=6): 2072 c2' != 0 | c2 = 1.  [para(108(a,1),1977(a,1,1)),rewrite(108(7))].

given #203 (T,wt=10): 2070 (x v y)' != 0 | y v x = 1.  [para(2(a,1),1977(a,1,1))].

given #204 (T,wt=11): 109 x v (y v (z ^ x)) = y v x.  [para(26(a,1),17(a,1,2)),flip(a)].

given #205 (A,wt=13): 107 1 != x | y ^ x != 0 | x' = y ^ x.  [para(26(a,1),10(a,1)),rewrite(67(4)),flip(a)].

given #206 (T,wt=10): 2119 (x v y)' != 1 | x v y = 0.  [para(116(a,1),107(b,1)),rewrite(208(10),116(11)),flip(a),xx(b)].

given #207 (T,wt=10): 2140 (x v y)' != 1 | y v x = 0.  [para(2(a,1),2119(a,1,1))].

given #208 (T,wt=10): 2142 (x ^ y)' != 1 | x ^ y = 0.  [para(27(a,1),2119(a,1,1)),rewrite(27(8))].

given #209 (T,wt=6): 2146 c1' != 1 | c1 = 0.  [para(13(a,1),2142(a,1,1)),rewrite(13(7))].

given #210 (A,wt=13): 110 (x ^ y) v (x ^ (z ^ y)) = x ^ y.  [para(19(a,1),26(a,1,2))].

given #211 (T,wt=10): 2145 (x ^ y)' != 1 | y ^ x = 0.  [para(4(a,1),2142(a,1,1))].

given #212 (T,wt=11): 115 (x v c1) ^ (x v c2) = x v c1.  [para(108(a,1),21(a,1,2,2))].

given #213 (T,wt=11): 133 (x v y) ^ (x v (y v z))' = 0.  [para(3(a,1),116(a,1,2,1))].

given #214 (T,wt=9): 2213 (x v y) ^ (y v x)' = 0.  [para(71(a,1),133(a,1,2,1))].

given #215 (A,wt=21): 117 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x' = (x v y) ^ z.  [para(22(a,1),10(b,1))].

given #216 (T,wt=11): 134 x ^ (y ^ ((x ^ y) v z)') = 0.  [para(116(a,1),5(a,1)),flip(a)].

given #217 (T,wt=11): 143 x ^ (y ^ (z v (x ^ y))') = 0.  [para(132(a,1),5(a,1)),flip(a)].

given #218 (T,wt=11): 145 (x v y) ^ (x v (z v y))' = 0.  [para(17(a,1),132(a,1,2,1))].

given #219 (T,wt=11): 155 ((x ^ y) v z) ^ (x v z)' = 0.  [para(24(a,1),132(a,1,2,1))].

given #220 (A,wt=13): 118 x ^ ((y v (x v z)) ^ u) = x ^ u.  [para(17(a,1),22(a,1,2,1))].

given #221 (T,wt=11): 157 x v (y v ((x v y) ^ z)') = 1.  [para(149(a,1),3(a,1)),flip(a)].

given #222 (T,wt=11): 159 (x ^ y) v (x ^ (y ^ z))' = 1.  [para(5(a,1),149(a,1,2,1))].

given #223 (T,wt=9): 2405 (x ^ y) v (y ^ x)' = 1.  [para(67(a,1),159(a,1,2,1))].

given #224 (T,wt=11): 163 x v (y v (z ^ (x v y))') = 1.  [para(158(a,1),3(a,1)),flip(a)].

given #225 (A,wt=15): 119 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y.  [para(22(a,1),26(a,1,2)),rewrite(2(4))].

given #226 (T,wt=11): 168 (x ^ y) v (x ^ (z ^ y))' = 1.  [para(19(a,1),158(a,1,2,1))].

given #227 (T,wt=11): 169 ((x v y) ^ z) v (x ^ z)' = 1.  [para(22(a,1),158(a,1,2,1))].

given #228 (T,wt=11): 187 x v (y v ((x ^ z) v y)') = 1.  [para(31(a,1),24(a,1,2)),rewrite(94(2)),flip(a)].

given #229 (T,wt=11): 190 x ^ (y ^ ((x v z) ^ y)') = 0.  [para(34(a,1),22(a,1,2)),rewrite(97(2)),flip(a)].

given #230 (A,wt=12): 121 x ^ (x' v y) != 0 | x' v y = x'.  [para(84(a,1),10(a,1)),flip(c),xx(a)].

given #231 (T,wt=11): 194 (c1 ^ x) v (c2 ^ x) = c2 ^ x.  [para(59(a,1),26(a,1,2)),rewrite(2(5))].

given #232 (T,wt=11): 195 c1 ^ ((c2 v x) ^ y) = c1 ^ y.  [para(22(a,1),59(a,1,2)),rewrite(59(4)),flip(a)].

given #233 (T,wt=11): 203 c1 ^ (x ^ (c2 v y)) = x ^ c1.  [para(191(a,1),19(a,1,2)),flip(a)].

given #234 (T,wt=11): 226 c1 ^ ((x v c2) ^ y) = c1 ^ y.  [para(193(a,1),5(a,1,1)),flip(a)].

given #235 (A,wt=12): 122 x v (x' ^ y) != 1 | x' ^ y = x'.  [para(87(a,1),10(b,1)),flip(c),xx(b)].

given #236 (T,wt=10): 2789 c2 != 1 | c2' ^ (x ^ c1) = c2'.  [para(305(a,1),122(a,1))].

given #237 (T,wt=11): 228 c1 ^ (x ^ (y v c2)) = x ^ c1.  [para(193(a,1),19(a,1,2)),flip(a)].

given #238 (T,wt=11): 278 c2 v ((x ^ c1) v y) = c2 v y.  [para(60(a,1),24(a,1,2,1))].

given #239 (T,wt=11): 281 (c2 ^ x) v (x ^ c1) = c2 ^ x.  [para(60(a,1),27(a,1,2))].

given #240 (A,wt=12): 124 x ^ (y v x') != 0 | y v x' = x'.  [para(96(a,1),10(a,1)),flip(c),xx(a)].

given #241 (T,wt=11): 306 c2 v (x v (y ^ c1)) = x v c2.  [para(276(a,1),17(a,1,2)),flip(a)].

given #242 (T,wt=11): 315 c2 v ((c1 ^ x) v y) = c2 v y.  [para(304(a,1),3(a,1,1)),flip(a)].

given #243 (T,wt=11): 317 c2 v (x v (c1 ^ y)) = x v c2.  [para(304(a,1),17(a,1,2)),flip(a)].

given #244 (T,wt=11): 366 (x ^ y) v (y ^ x) = x ^ y.  [para(67(a,1),27(a,1,2))].

given #245 (A,wt=12): 125 x v (y ^ x') != 1 | y ^ x' = x'.  [para(98(a,1),10(b,1)),flip(c),xx(b)].

given #246 (T,wt=11): 432 (x v y) ^ (y v x) = x v y.  [para(71(a,1),21(a,1,2))].

given #247 (T,wt=11): 471 (x ^ c1) v (x ^ c2) = x ^ c2.  [para(81(a,1),26(a,1,2)),rewrite(2(5))].

given #248 (T,wt=11): 614 (c1 v x) ^ (x v c2) = c1 v x.  [para(114(a,1),21(a,1,2))].

given #249 (T,wt=11): 621 x ^ ((y v (x v z))' ^ u) = 0.  [para(17(a,1),123(a,1,2,1,1))].

given #250 (A,wt=13): 127 x ^ (y ^ ((y ^ x) v z)) = x ^ y.  [para(4(a,1),23(a,1,2,2,1))].

given #251 (T,wt=11): 707 x ^ (y ^ (z v (x v u))') = 0.  [para(17(a,1),126(a,1,2,2,1))].

given #252 (T,wt=11): 717 x ^ ((y v (z v x))' ^ u) = 0.  [para(141(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #253 (T,wt=11): 720 x ^ (y ^ (z v (u v x))') = 0.  [para(141(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #254 (T,wt=11): 765 x v ((y ^ (x ^ z))' v u) = 1.  [para(19(a,1),153(a,1,2,1,1))].

given #255 (A,wt=25): 128 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | x' = y ^ ((x ^ y) v z).  [para(23(a,1),10(b,1))].

given #256 (T,wt=11): 776 x v (y v (z ^ (x ^ u))') = 1.  [para(19(a,1),154(a,1,2,2,1))].

given #257 (T,wt=11): 894 x v ((y ^ (z ^ x))' v u) = 1.  [para(5(a,1),162(a,1,2,1,1))].

given #258 (T,wt=11): 899 (c2 ^ x) v ((c1 ^ x)' v y) = 1.  [para(59(a,1),162(a,1,2,1,1))].

given #259 (T,wt=11): 903 (x ^ c2) v ((x ^ c1)' v y) = 1.  [para(81(a,1),162(a,1,2,1,1))].

given #260 (A,wt=15): 129 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y.  [para(17(a,1),23(a,1,2,2))].

given #261 (T,wt=11): 913 x v (y v (z ^ (u ^ x))') = 1.  [para(164(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #262 (T,wt=11): 916 (c2 ^ x) v (y ^ (c1 ^ x))' = 1.  [para(59(a,1),164(a,1,2,1,2))].

given #263 (T,wt=11): 920 (x ^ c2) v (y ^ (x ^ c1))' = 1.  [para(81(a,1),164(a,1,2,1,2))].

given #264 (T,wt=11): 933 (c2 ^ x) v (y v (c1 ^ x)') = 1.  [para(59(a,1),167(a,1,2,2,1))].

given #265 (A,wt=19): 130 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z).  [para(23(a,1),26(a,1,2)),rewrite(2(5))].

given #266 (T,wt=11): 938 (x ^ c2) v (y v (x ^ c1)') = 1.  [para(81(a,1),167(a,1,2,2,1))].

given #267 (T,wt=11): 945 x v (y v (y v (x ^ z))') = 1.  [para(185(a,1),24(a,1,2)),rewrite(94(2)),flip(a)].

given #268 (T,wt=11): 1026 x ^ (y ^ (y ^ (x v z))') = 0.  [para(188(a,1),22(a,1,2)),rewrite(97(2)),flip(a)].

given #269 (T,wt=11): 1044 (c2 ^ (x v (c1 v y))) v c1' = 1.  [para(62(a,1),199(a,1,2,1))].

given #270 (A,wt=15): 131 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y.  [para(23(a,1),22(a,1,2)),rewrite(22(3)),flip(a)].

given #271 (T,wt=11): 1046 (c2 ^ (x v (y v c1))) v c1' = 1.  [para(88(a,1),199(a,1,2,1))].

given #272 (T,wt=11): 1128 c1 ^ ((x v (c2 v y))' ^ z) = 0.  [para(17(a,1),229(a,1,2,1,1))].

given #273 (T,wt=11): 1132 c1 ^ (x ^ (y v (c2 v z))') = 0.  [para(231(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #274 (T,wt=11): 1137 (x v (y ^ z)) ^ (x v y)' = 0.  [para(63(a,1),132(a,1,2,1))].

given #275 (A,wt=12): 135 x v (x v y)' != 1 | (x v y)' = x'.  [para(116(a,1),10(b,1)),flip(c),xx(b)].

given #276 (T,wt=11): 1141 x v (y v (x v (y ^ z))') = 1.  [para(63(a,1),223(a,1,2)),rewrite(2(5),3(5))].

given #277 (T,wt=11): 1165 c1 ^ ((x v (y v c2))' ^ z) = 0.  [para(233(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #278 (T,wt=11): 1167 c1 ^ (x ^ (y v (z v c2))') = 0.  [para(233(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #279 (T,wt=11): 1228 c2 v ((x ^ (y ^ c1))' v z) = 1.  [para(5(a,1),308(a,1,2,1,1))].

given #280 (A,wt=12): 144 x v (y v x)' != 1 | (y v x)' = x'.  [para(132(a,1),10(b,1)),flip(c),xx(b)].

given #281 (T,wt=11): 1243 c2 v (x v (y ^ (z ^ c1))') = 1.  [para(310(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #282 (T,wt=11): 1285 c2 v ((x ^ (c1 ^ y))' v z) = 1.  [para(19(a,1),321(a,1,2,1,1))].

given #283 (T,wt=11): 1304 c2 v (x v (y ^ (c1 ^ z))') = 1.  [para(19(a,1),323(a,1,2,2,1))].

given #284 (T,wt=11): 1326 (x ^ (y v z)) v (x ^ y)' = 1.  [para(77(a,1),158(a,1,2,1))].

given #285 (A,wt=12): 147 c1 v (c2' ^ x) != 1 | c2' ^ x = c1'.  [para(138(a,1),10(b,1)),flip(c),xx(b)].

given #286 (T,wt=10): 3803 c1 != 1 | c2' ^ (x ^ c1) = c1'.  [para(106(a,1),147(a,1))].

given #287 (T,wt=11): 1328 x ^ (y ^ (x ^ (y v z))') = 0.  [para(77(a,1),224(a,1,2)),rewrite(4(5),5(5))].

given #288 (T,wt=11): 1350 x ^ (c1 ^ (c2 ^ (x v y))') = 0.  [para(473(a,1),22(a,1,2)),rewrite(97(2),4(5)),flip(a)].

given #289 (T,wt=11): 1357 (x v c1) ^ (c2 v x) = x v c1.  [para(602(a,1),20(a,1,2))].

given #290 (A,wt=17): 148 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u.  [para(5(a,1),24(a,1,2,1))].

given #291 (T,wt=11): 1368 (x v c1) ^ (y v (c2 v x))' = 0.  [para(602(a,1),141(a,1,2,1,2))].

given #292 (T,wt=11): 1369 (x v c1) ^ ((c2 v x)' ^ y) = 0.  [para(602(a,1),142(a,1,2,1,1))].

given #293 (T,wt=11): 1370 (x v c1) ^ (y ^ (c2 v x)') = 0.  [para(602(a,1),146(a,1,2,2,1))].

given #294 (T,wt=11): 1379 (x v c1) ^ ((x v c2)' ^ y) = 0.  [para(604(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #295 (A,wt=21): 150 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x' = (x ^ z) v y.  [para(24(a,1),10(a,1))].

given #296 (T,wt=11): 1381 (x v c1) ^ (y ^ (x v c2)') = 0.  [para(604(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #297 (T,wt=11): 1442 x v (c2 v (c1 v (x ^ y))') = 1.  [para(608(a,1),24(a,1,2)),rewrite(94(2),2(5)),flip(a)].

given #298 (T,wt=11): 1459 (x ^ c2) v ((c1 ^ x)' v y) = 1.  [para(1033(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #299 (T,wt=11): 1461 (x ^ c2) v (y v (c1 ^ x)') = 1.  [para(1033(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #300 (A,wt=13): 151 x v ((y ^ (x ^ z)) v u) = x v u.  [para(19(a,1),24(a,1,2,1))].

given #301 (T,wt=11): 1471 (c2 ^ x) v ((x ^ c1)' v y) = 1.  [para(1034(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #302 (T,wt=11): 1473 (c2 ^ x) v (y v (x ^ c1)') = 1.  [para(1034(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #303 (T,wt=11): 1488 ((x v y) ^ z) v (y ^ z)' = 1.  [para(89(a,1),158(a,1,2,1))].

given #304 (T,wt=11): 1490 x ^ (y ^ ((z v x) ^ y)') = 0.  [para(34(a,1),89(a,1,2)),rewrite(97(2)),flip(a)].

given #305 (A,wt=15): 152 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y.  [para(24(a,1),20(a,1,2)),rewrite(4(4))].

given #306 (T,wt=11): 1502 x ^ (y ^ (y ^ (z v x))') = 0.  [para(188(a,1),89(a,1,2)),rewrite(97(2)),flip(a)].

given #307 (T,wt=11): 1506 x ^ (c1 ^ (c2 ^ (y v x))') = 0.  [para(473(a,1),89(a,1,2)),rewrite(97(2),4(5)),flip(a)].

given #308 (T,wt=11): 1510 (c2 ^ (c1 v x)) v (c1' v y) = 1.  [para(1035(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #309 (T,wt=11): 1512 (c2 ^ (c1 v x)) v (y v c1') = 1.  [para(1035(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #310 (A,wt=12): 156 c1 v (x ^ c2') != 1 | x ^ c2' = c1'.  [para(140(a,1),10(b,1)),flip(c),xx(b)].

given #311 (T,wt=11): 1524 (c2 ^ (x v c1)) v (c1' v y) = 1.  [para(1039(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #312 (T,wt=11): 1526 (c2 ^ (x v c1)) v (y v c1') = 1.  [para(1039(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #313 (T,wt=11): 1541 c1 ^ ((c2 ^ (c1 v x))' ^ y) = 0.  [para(1059(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #314 (T,wt=11): 1543 c1 ^ (c2 ^ (x v (c1 v y)))' = 0.  [para(17(a,1),1059(a,1,2,1,2))].

given #315 (A,wt=12): 160 x ^ (x ^ y)' != 0 | (x ^ y)' = x'.  [para(149(a,1),10(a,1)),flip(c),xx(a)].

given #316 (T,wt=11): 1544 c1 ^ (x ^ (c2 ^ (c1 v y))') = 0.  [para(1059(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #317 (T,wt=11): 1581 (c1 v (x ^ (c2 ^ y))) ^ c2' = 0.  [para(78(a,1),1358(a,1,2,1)),rewrite(2(5))].

given #318 (T,wt=11): 1582 (c1 v (x ^ (y ^ c2))) ^ c2' = 0.  [para(106(a,1),1358(a,1,2,1)),rewrite(2(5))].

given #319 (T,wt=11): 1610 (c1 v x) ^ ((x v c2)' ^ y) = 0.  [para(1376(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #320 (A,wt=12): 165 x ^ (y ^ x)' != 0 | (y ^ x)' = x'.  [para(158(a,1),10(a,1)),flip(c),xx(a)].

given #321 (T,wt=11): 1613 (c1 v x) ^ (y ^ (x v c2)') = 0.  [para(1376(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #322 (T,wt=11): 1631 c1 ^ (c2 ^ (x v (y v c1)))' = 0.  [para(3(a,1),1504(a,1,2,1,2))].

given #323 (T,wt=11): 1632 c1 ^ ((c2 ^ (x v c1))' ^ y) = 0.  [para(1504(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #324 (T,wt=11): 1634 c1 ^ (x ^ (c2 ^ (y v c1))') = 0.  [para(1504(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #325 (A,wt=13): 170 (x ^ ((y ^ x) v z)) v (y ^ x)' = 1.  [para(23(a,1),158(a,1,2,1))].

given #326 (T,wt=11): 1653 (c1 v x) ^ (c2 v x) = c1 v x.  [para(112(a,1),92(a,1,2))].

given #327 (T,wt=11): 1666 c1' v ((c2 ^ (c1 v x)) v y) = 1.  [para(1509(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #328 (T,wt=11): 1667 c1' v (x v (c2 ^ (c1 v y))) = 1.  [para(1509(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #329 (T,wt=11): 1668 c1' v (c2 ^ (x v (c1 v y))) = 1.  [para(17(a,1),1509(a,1,2,2))].

given #330 (A,wt=13): 174 x v (y v ((y v x) ^ z)) = x v y.  [para(2(a,1),25(a,1,2,2,1))].

given #331 (T,wt=11): 1679 c1' v ((c2 ^ (x v c1)) v y) = 1.  [para(1523(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #332 (T,wt=11): 1680 c1' v (c2 ^ (x v (y v c1))) = 1.  [para(3(a,1),1523(a,1,2,2))].

given #333 (T,wt=11): 1681 c1' v (x v (c2 ^ (y v c1))) = 1.  [para(1523(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #334 (T,wt=11): 1691 (c1 v x) ^ ((c2 v x)' ^ y) = 0.  [para(1572(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #335 (A,wt=25): 175 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | x' = y v ((x v y) ^ z).  [para(25(a,1),10(a,1))].

given #336 (T,wt=11): 1693 (c1 v x) ^ (y ^ (c2 v x)') = 0.  [para(1572(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #337 (T,wt=11): 1698 (c1 v (c2 ^ x)) ^ (c2' ^ y) = 0.  [para(1573(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #338 (T,wt=11): 1700 (c1 v (c2 ^ x)) ^ (y ^ c2') = 0.  [para(1573(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #339 (T,wt=11): 1707 (x ^ (y v z)) v (x ^ z)' = 1.  [para(93(a,1),158(a,1,2,1))].

given #340 (A,wt=15): 176 x v (y v (z ^ ((x v y) ^ u))) = x v y.  [para(19(a,1),25(a,1,2,2))].

given #341 (T,wt=11): 1710 x ^ (y ^ (x ^ (z v y))') = 0.  [para(93(a,1),224(a,1,2)),rewrite(4(5),5(5))].

given #342 (T,wt=11): 1724 (c1 v (x ^ c2)) ^ (c2' ^ y) = 0.  [para(1576(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #343 (T,wt=11): 1726 (c1 v (x ^ c2)) ^ (y ^ c2') = 0.  [para(1576(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #344 (T,wt=11): 1741 c2 v ((c1 v (c2 ^ x))' v y) = 1.  [para(1586(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #345 (A,wt=19): 177 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z).  [para(25(a,1),20(a,1,2)),rewrite(4(5))].

given #346 (T,wt=11): 1744 c2 v (x v (c1 v (c2 ^ y))') = 1.  [para(1586(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #347 (T,wt=11): 1745 c2 v (c1 v (x ^ (c2 ^ y)))' = 1.  [para(19(a,1),1586(a,1,2,1,2))].

given #348 (T,wt=11): 1756 c2' ^ ((c1 v (c2 ^ x)) ^ y) = 0.  [para(1697(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #349 (T,wt=11): 1757 c2' ^ (x ^ (c1 v (c2 ^ y))) = 0.  [para(1697(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #350 (A,wt=13): 178 (x v ((y v x) ^ z)) ^ (y v x)' = 0.  [para(25(a,1),132(a,1,2,1))].

given #351 (T,wt=7): 5042 c2' ^ (x ^ c1) = 0.  [para(9(a,1),1757(a,1,2,2,2)),rewrite(2(5),75(5))].

given #352 (T,wt=11): 1758 c2' ^ (c1 v (x ^ (c2 ^ y))) = 0.  [para(19(a,1),1697(a,1,2,2))].

given #353 (T,wt=11): 1779 x v (y v (z ^ (y v x))') = 1.  [para(100(a,1),161(a,1,2,1,2)),rewrite(3(5))].

given #354 (T,wt=11): 1790 c2' ^ ((c1 v (x ^ c2)) ^ y) = 0.  [para(1723(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #355 (A,wt=15): 179 x v (y v (((x ^ z) v y) ^ u)) = x v y.  [para(25(a,1),24(a,1,2)),rewrite(24(3)),flip(a)].

given #356 (T,wt=11): 1791 c2' ^ (c1 v (x ^ (y ^ c2))) = 0.  [para(5(a,1),1723(a,1,2,2))].

given #357 (T,wt=11): 1792 c2' ^ (x ^ (c1 v (y ^ c2))) = 0.  [para(1723(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #358 (T,wt=11): 1803 c2 v ((c1 v (x ^ c2))' v y) = 1.  [para(1742(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #359 (T,wt=11): 1804 c2 v (c1 v (x ^ (y ^ c2)))' = 1.  [para(5(a,1),1742(a,1,2,1,2))].

given #360 (A,wt=12): 180 c2 ^ (c1' v x) != 0 | c2' = c1' v x.  [para(171(a,1),10(a,1)),xx(a)].

given #361 (T,wt=11): 1806 c2 v (x v (c1 v (y ^ c2))') = 1.  [para(1742(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #362 (T,wt=11): 1830 (x v y) ^ (y v (z v x))' = 0.  [para(101(a,1),224(a,1,2)),rewrite(4(5))].

given #363 (T,wt=11): 1840 (x ^ (y ^ z))' v (u v y) = 1.  [para(161(a,1),101(a,1,1)),rewrite(73(7),161(9))].

given #364 (T,wt=11): 1842 (x ^ (y ^ z))' v (u v z) = 1.  [para(164(a,1),101(a,1,1)),rewrite(73(7),164(9))].

given #365 (A,wt=12): 181 c2 ^ (x v c1') != 0 | c2' = x v c1'.  [para(173(a,1),10(a,1)),xx(a)].

given #366 (T,wt=11): 1843 (c1 ^ x)' v (y v (c2 ^ x)) = 1.  [para(199(a,1),101(a,1,1)),rewrite(73(9),199(13))].

given #367 (T,wt=11): 1847 (x ^ (y ^ c1))' v (z v c2) = 1.  [para(310(a,1),101(a,1,1)),rewrite(73(9),310(13))].

given #368 (T,wt=11): 1849 (x ^ (c1 ^ y))' v (z v c2) = 1.  [para(324(a,1),101(a,1,1)),rewrite(73(9),324(13))].

given #369 (T,wt=11): 1850 (x ^ c1)' v (y v (x ^ c2)) = 1.  [para(472(a,1),101(a,1,1)),rewrite(73(9),472(13))].

given #370 (A,wt=13): 182 (x ^ y) v (y ^ (x ^ z)) = y ^ x.  [para(4(a,1),27(a,1,1))].

given #371 (T,wt=11): 1854 (c1 ^ x)' v (y v (x ^ c2)) = 1.  [para(1033(a,1),101(a,1,1)),rewrite(73(9),1033(13))].

given #372 (T,wt=11): 1855 (x ^ c1)' v (y v (c2 ^ x)) = 1.  [para(1034(a,1),101(a,1,1)),rewrite(73(9),1034(13))].

given #373 (T,wt=11): 1856 (c1 v (c2 ^ x))' v (y v c2) = 1.  [para(1586(a,1),101(a,1,1)),rewrite(73(10),1586(15))].

given #374 (T,wt=11): 1857 (c1 v (x ^ c2))' v (y v c2) = 1.  [para(1742(a,1),101(a,1,1)),rewrite(73(10),1742(15))].

given #375 (A,wt=13): 183 (x ^ y) v (y ^ (z ^ x)) = x ^ y.  [para(4(a,1),27(a,1,2)),rewrite(5(3))].

given #376 (T,wt=9): 5496 (x v y)' ^ (z ^ x) = 0.  [para(116(a,1),183(a,1,1)),rewrite(75(6),116(7))].

given #377 (T,wt=9): 5497 (x v y)' ^ (z ^ y) = 0.  [para(132(a,1),183(a,1,1)),rewrite(75(6),132(7))].

given #378 (T,wt=9): 5501 (c2 v x)' ^ (y ^ c1) = 0.  [para(197(a,1),183(a,1,1)),rewrite(75(8),197(11))].

given #379 (T,wt=9): 5502 (x v c2)' ^ (y ^ c1) = 0.  [para(198(a,1),183(a,1,1)),rewrite(75(8),198(11))].

given #380 (A,wt=17): 184 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y).  [para(27(a,1),17(a,1,2)),flip(a)].

given #381 (T,wt=11): 1883 c2 v (x v ((x v c1) ^ y)') = 1.  [para(602(a,1),1825(a,1,2)),rewrite(2(7),3(7))].

given #382 (T,wt=11): 1902 c2 v (x v (y ^ (x v c1))') = 1.  [para(602(a,1),1826(a,1,2)),rewrite(2(7),3(7))].

given #383 (T,wt=11): 1935 (c1 v x) ^ (c2 v (x v y))' = 0.  [para(1376(a,1),102(a,1,2)),rewrite(4(4),86(4),2(6)),flip(a)].

given #384 (T,wt=11): 1987 ((x ^ y) v z) ^ (y v z)' = 0.  [para(104(a,1),132(a,1,2,1))].

given #385 (A,wt=16): 186 x ^ (y v (x v y)') != 0 | y v (x v y)' = x'.  [para(31(a,1),10(a,1)),flip(c),xx(a)].

given #386 (T,wt=11): 1989 x v (y v ((z ^ x) v y)') = 1.  [para(31(a,1),104(a,1,2)),rewrite(94(2)),flip(a)].

given #387 (T,wt=11): 2008 x v (y v (y v (z ^ x))') = 1.  [para(185(a,1),104(a,1,2)),rewrite(94(2)),flip(a)].

given #388 (T,wt=11): 2012 x v (c2 v (c1 v (y ^ x))') = 1.  [para(608(a,1),104(a,1,2)),rewrite(94(2),2(5)),flip(a)].

given #389 (T,wt=11): 2078 (x v (y ^ z)) ^ (x v z)' = 0.  [para(109(a,1),132(a,1,2,1))].

given #390 (A,wt=16): 189 x v (y ^ (x ^ y)') != 1 | y ^ (x ^ y)' = x'.  [para(34(a,1),10(b,1)),flip(c),xx(b)].

given #391 (T,wt=11): 2083 x v (y v (x v (z ^ y))') = 1.  [para(109(a,1),223(a,1,2)),rewrite(2(5),3(5))].

given #392 (T,wt=11): 2204 x v (c2 v (y ^ (x v c1))') = 1.  [para(115(a,1),164(a,1,2,1,2)),rewrite(3(7))].

given #393 (T,wt=11): 2210 (x v y) ^ (y v (x v z))' = 0.  [para(2(a,1),133(a,1,1))].

given #394 (T,wt=11): 2214 (x v c1) ^ (x v (c2 v y))' = 0.  [para(112(a,1),133(a,1,2,1,2))].

given #395 (A,wt=17): 192 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | c1' = c2 ^ x.  [para(59(a,1),10(b,1))].

given #396 (T,wt=11): 2215 (x v c1) ^ (x v (y v c2))' = 0.  [para(114(a,1),133(a,1,2,1,2))].

given #397 (T,wt=11): 2218 (x v y) ^ ((y v x)' ^ z) = 0.  [para(2213(a,1),5(a,1,1)),rewrite(86(2)),flip(a)].

given #398 (T,wt=11): 2220 (x v y) ^ (z ^ (y v x)') = 0.  [para(2213(a,1),19(a,1,2)),rewrite(97(2)),flip(a)].

given #399 (T,wt=11): 2270 x ^ (y ^ ((y ^ x) v z)') = 0.  [para(4(a,1),134(a,1,2,2,1,1))].

given #400 (A,wt=13): 196 c1 ^ (x ^ ((c2 ^ x) v y)) = c1 ^ x.  [para(23(a,1),59(a,1,2)),rewrite(59(4)),flip(a)].

given #401 (T,wt=11): 2273 c1 ^ (x ^ ((c2 ^ x) v y)') = 0.  [para(134(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #402 (T,wt=11): 2285 x ^ (y ^ (z v (y ^ x))') = 0.  [para(4(a,1),143(a,1,2,2,1,2))].

given #403 (T,wt=11): 2288 c1 ^ (x ^ (y v (c2 ^ x))') = 0.  [para(143(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #404 (T,wt=11): 2299 (x v y) ^ (z v (y v x))' = 0.  [para(2(a,1),145(a,1,2,1)),rewrite(3(3))].

given #405 (A,wt=13): 201 c2 v x != 1 | c1 != 0 | c1' = c2 v x.  [para(191(a,1),10(b,1)),rewrite(112(4))].

given #406 (T,wt=11): 2306 (x v (y ^ c1)) ^ (x v c2)' = 0.  [para(276(a,1),145(a,1,2,1,2))].

given #407 (T,wt=11): 2307 (x v (c1 ^ y)) ^ (x v c2)' = 0.  [para(304(a,1),145(a,1,2,1,2))].

given #408 (T,wt=11): 2323 (x v (y ^ z)) ^ (y v x)' = 0.  [para(2(a,1),155(a,1,1))].

given #409 (T,wt=11): 2324 ((x ^ y) v z) ^ (z v x)' = 0.  [para(2(a,1),155(a,1,2,1))].

given #410 (A,wt=19): 204 x v (y v z) != 1 | z ^ (x v y) != 0 | z' = x v y.  [para(3(a,1),36(a,1))].

given #411 (T,wt=11): 2326 (x v y)' ^ ((x ^ z) v y) = 0.  [para(155(a,1),4(a,1)),flip(a)].

given #412 (T,wt=11): 2328 ((x ^ y) v (x ^ z)) ^ x' = 0.  [para(7(a,1),155(a,1,2,1))].

given #413 (T,wt=11): 2333 ((x ^ y) v (z ^ x)) ^ x' = 0.  [para(26(a,1),155(a,1,2,1))].

given #414 (T,wt=11): 2338 ((x ^ c1) v y) ^ (c2 v y)' = 0.  [para(60(a,1),155(a,1,1,1))].

given #415 (A,wt=13): 205 x v y != 1 | x ^ y != 0 | y' = x.  [para(4(a,1),36(b,1))].

given #416 (T,wt=11): 2340 ((c2 ^ x) v (y ^ c1)) ^ c2' = 0.  [para(276(a,1),155(a,1,2,1))].

given #417 (T,wt=11): 2341 ((c2 ^ x) v (c1 ^ y)) ^ c2' = 0.  [para(304(a,1),155(a,1,2,1))].

given #418 (T,wt=11): 2386 x v (y v ((y v x) ^ z)') = 1.  [para(2(a,1),157(a,1,2,2,1,1))].

given #419 (T,wt=11): 2399 c2 v (x v ((c1 v x) ^ y)') = 1.  [para(157(a,1),1440(a,1,2,2,1)),rewrite(82(8),2(8),75(8),2(7))].

given #420 (A,wt=19): 206 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | (y ^ z)' = x.  [para(5(a,1),36(b,1))].

given #421 (T,wt=11): 2400 (x ^ y) v (y ^ (x ^ z))' = 1.  [para(4(a,1),159(a,1,1))].

given #422 (T,wt=11): 2401 (x ^ y) v (y ^ (z ^ x))' = 1.  [para(4(a,1),159(a,1,2,1)),rewrite(5(3))].

given #423 (T,wt=11): 2404 (x ^ c2) v (x ^ (y ^ c1))' = 1.  [para(60(a,1),159(a,1,2,1,2))].

given #424 (T,wt=11): 2417 (x ^ y) v ((y ^ x)' v z) = 1.  [para(2405(a,1),3(a,1,1)),rewrite(83(2)),flip(a)].

given #425 (A,wt=13): 207 1 != x | x ^ y != 0 | (x ^ y)' = x.  [para(7(a,1),36(a,1)),rewrite(4(4),66(4)),flip(a)].

given #426 (T,wt=11): 2420 (x ^ y) v (z v (y ^ x)') = 1.  [para(2405(a,1),17(a,1,2)),rewrite(94(2)),flip(a)].

given #427 (T,wt=11): 2434 (x ^ y)' v (z v (y ^ x)) = 1.  [para(2405(a,1),101(a,1,1)),rewrite(73(7),2405(9))].

given #428 (T,wt=11): 2448 c2 v (x v (y ^ (c1 v x))') = 1.  [para(163(a,1),1440(a,1,2,2,1)),rewrite(82(8),2(8),75(8),2(7))].

given #429 (T,wt=11): 2468 (c2 v x) ^ (y ^ c1) = y ^ c1.  [para(60(a,1),119(a,1,1)),rewrite(26(8)),flip(a)].

given #430 (A,wt=19): 209 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z)' = y.  [para(17(a,1),36(a,1))].

given #431 (T,wt=11): 2470 (x v y) ^ (z ^ x) = z ^ x.  [para(67(a,1),119(a,1,1)),rewrite(26(5)),flip(a)].

given #432 (T,wt=11): 2533 (x ^ y) v (z ^ (y ^ x))' = 1.  [para(4(a,1),168(a,1,2,1)),rewrite(5(3))].

given #433 (T,wt=11): 2539 (x ^ (c2 v y)) v (x ^ c1)' = 1.  [para(191(a,1),168(a,1,2,1,2))].

given #434 (T,wt=11): 2541 (x ^ (y v c2)) v (x ^ c1)' = 1.  [para(193(a,1),168(a,1,2,1,2))].

given #435 (A,wt=19): 210 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z' = x ^ y.  [para(19(a,1),36(b,1))].

given #436 (T,wt=11): 2574 (x ^ y)' v ((x v z) ^ y) = 1.  [para(169(a,1),2(a,1)),flip(a)].

given #437 (T,wt=11): 2575 (x ^ (y v z)) v (y ^ x)' = 1.  [para(4(a,1),169(a,1,1))].

given #438 (T,wt=11): 2576 ((x v y) ^ z) v (z ^ x)' = 1.  [para(4(a,1),169(a,1,2,1))].

given #439 (T,wt=11): 2578 ((x v y) ^ (x v z)) v x' = 1.  [para(6(a,1),169(a,1,2,1))].

given #440 (A,wt=13): 211 1 != x | y ^ x != 0 | (y ^ x)' = x.  [para(26(a,1),36(a,1)),rewrite(4(4),67(4)),flip(a)].

given #441 (T,wt=11): 2582 ((x v y) ^ (z v x)) v x' = 1.  [para(20(a,1),169(a,1,2,1))].

given #442 (T,wt=11): 2586 ((c1 v x) ^ (c2 v y)) v c1' = 1.  [para(191(a,1),169(a,1,2,1))].

given #443 (T,wt=11): 2588 ((c1 v x) ^ (y v c2)) v c1' = 1.  [para(193(a,1),169(a,1,2,1))].

given #444 (T,wt=11): 2600 ((c2 v x) ^ y) v (c1 ^ y)' = 1.  [para(112(a,1),169(a,1,1,1))].

given #445 (A,wt=12): 213 x ^ (x' v y) != 0 | (x' v y)' = x.  [para(84(a,1),36(a,1)),rewrite(4(6)),xx(a)].

given #446 (T,wt=11): 2601 ((x v c2) ^ y) v (c1 ^ y)' = 1.  [para(114(a,1),169(a,1,1,1))].

given #447 (T,wt=11): 2628 x v (y v ((y ^ z) v x)') = 1.  [para(187(a,1),17(a,1)),flip(a)].

given #448 (T,wt=11): 2630 x v ((x ^ y) v (x ^ z))' = 1.  [para(187(a,1),24(a,1)),flip(a)].

given #449 (T,wt=11): 2634 c2 v (x v ((y ^ c1) v x)') = 1.  [para(60(a,1),187(a,1,2,2,1,1))].

given #450 (A,wt=12): 214 x ^ (y v x') != 0 | (y v x')' = x.  [para(96(a,1),36(a,1)),rewrite(4(6)),xx(a)].

given #451 (T,wt=11): 2644 c2 v (x v ((c1 ^ y) v x)') = 1.  [para(187(a,1),1440(a,1,2,2,1)),rewrite(82(8),2(8),75(8),2(7))].

given #452 (T,wt=11): 2645 x v ((x ^ y) v (z ^ x))' = 1.  [para(187(a,1),104(a,1)),flip(a)].

given #453 (T,wt=11): 2648 x ^ (y ^ ((y v z) ^ x)') = 0.  [para(190(a,1),19(a,1)),flip(a)].

given #454 (T,wt=11): 2649 x ^ ((x v y) ^ (x v z))' = 0.  [para(190(a,1),22(a,1)),flip(a)].

given #455 (A,wt=21): 215 x v y != 1 | x ^ ((x ^ z) v y) != 0 | ((x ^ z) v y)' = x.  [para(24(a,1),36(a,1)),rewrite(4(6))].

given #456 (T,wt=11): 2650 c1 ^ (x ^ ((c2 v y) ^ x)') = 0.  [para(190(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #457 (T,wt=11): 2659 c1 ^ (x ^ ((y v c2) ^ x)') = 0.  [para(114(a,1),190(a,1,2,2,1,1))].

given #458 (T,wt=11): 2664 x ^ ((x v y) ^ (z v x))' = 0.  [para(190(a,1),89(a,1)),flip(a)].

given #459 (T,wt=11): 2674 (x ^ c1) v (c2 ^ x) = c2 ^ x.  [para(4(a,1),194(a,1,1))].

given #460 (A,wt=12): 216 x ^ (x ^ y)' != 0 | x ^ y = x.  [para(149(a,1),36(a,1)),rewrite(4(6),208(11)),xx(a)].

given #461 (T,wt=11): 2675 (c1 ^ x) v (x ^ c2) = c2 ^ x.  [para(4(a,1),194(a,1,2))].

given #462 (T,wt=11): 2723 c1 ^ (x ^ (x ^ (c2 v y))') = 0.  [para(188(a,1),195(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #463 (T,wt=11): 2739 c1 ^ ((c1 v x) ^ (c2 v y))' = 0.  [para(195(a,1),190(a,1))].

given #464 (T,wt=11): 2740 x ^ (c1 ^ (x ^ (c2 v y))') = 0.  [para(203(a,1),224(a,1,2)),rewrite(4(7),5(7))].

given #465 (A,wt=12): 217 x ^ (y ^ x)' != 0 | y ^ x = x.  [para(158(a,1),36(a,1)),rewrite(4(6),208(11)),xx(a)].

given #466 (T,wt=11): 2768 c1 ^ (x ^ (x ^ (y v c2))') = 0.  [para(188(a,1),226(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #467 (T,wt=11): 2783 c1 ^ ((c1 v x) ^ (y v c2))' = 0.  [para(226(a,1),190(a,1))].

given #468 (T,wt=11): 2790 x ^ (c1 ^ (x ^ (y v c2))') = 0.  [para(228(a,1),224(a,1,2)),rewrite(4(7),5(7))].

given #469 (T,wt=11): 2826 c2 v (x v (x v (y ^ c1))') = 1.  [para(185(a,1),278(a,1,2)),rewrite(2(3),83(3)),flip(a)].

given #470 (A,wt=25): 219 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | (y v ((x v y) ^ z))' = x.  [para(25(a,1),36(a,1)),rewrite(4(7))].

given #471 (T,wt=11): 2839 c2 v ((c2 ^ x) v (y ^ c1))' = 1.  [para(278(a,1),187(a,1))].

given #472 (T,wt=11): 2858 x ^ (c1 ^ (y v (c2 ^ x))') = 0.  [para(281(a,1),141(a,1,2,1,2)),rewrite(5(7))].

given #473 (T,wt=11): 2866 (c2 ^ x) v (x ^ (c1 ^ y))' = 1.  [para(281(a,1),1825(a,1,2)),rewrite(5(3),2(7))].

given #474 (T,wt=11): 2867 (c2 ^ x) v (y ^ (x ^ c1))' = 1.  [para(281(a,1),1826(a,1,2)),rewrite(2(7))].

given #475 (A,wt=12): 220 c2 ^ (c1' v x) != 0 | (c1' v x)' = c2.  [para(171(a,1),36(a,1)),rewrite(4(8)),xx(a)].

given #476 (T,wt=11): 2875 x v (c2 v (x v (y ^ c1))') = 1.  [para(306(a,1),223(a,1,2)),rewrite(2(7),3(7))].

given #477 (T,wt=11): 2901 ((c1 ^ x) v y) ^ (c2 v y)' = 0.  [para(315(a,1),132(a,1,2,1))].

given #478 (T,wt=11): 2918 c2 v (x v (x v (c1 ^ y))') = 1.  [para(185(a,1),315(a,1,2)),rewrite(2(3),83(3)),flip(a)].

given #479 (T,wt=11): 2931 c2 v ((c2 ^ x) v (c1 ^ y))' = 1.  [para(315(a,1),187(a,1))].

given #480 (A,wt=12): 221 c2 ^ (x v c1') != 0 | (x v c1')' = c2.  [para(173(a,1),36(a,1)),rewrite(4(8)),xx(a)].

given #481 (T,wt=11): 2934 x v (c2 v (x v (c1 ^ y))') = 1.  [para(317(a,1),223(a,1,2)),rewrite(2(7),3(7))].

given #482 (T,wt=11): 3002 x ^ (c1 ^ (y v (x ^ c2))') = 0.  [para(471(a,1),136(a,1,2,1,2)),rewrite(5(7))].

given #483 (T,wt=11): 3011 (x v c2) ^ (c1 v x) = c1 v x.  [para(614(a,1),4(a,1)),flip(a)].

given #484 (T,wt=11): 3022 x v (c2 v (y ^ (c1 v x))') = 1.  [para(614(a,1),164(a,1,2,1,2)),rewrite(3(7))].

given #485 (A,wt=16): 222 x ^ (y v (x v y)') != 0 | (y v (x v y)')' = x.  [para(31(a,1),36(a,1)),rewrite(4(7)),xx(a)].

given #486 (T,wt=11): 3345 (x ^ c2) v (y ^ (c1 ^ x))' = 1.  [para(4(a,1),916(a,1,1))].

given #487 (T,wt=11): 3346 (c2 ^ x) v (c1 ^ (x ^ y))' = 1.  [para(4(a,1),916(a,1,2,1)),rewrite(5(5))].

given #488 (T,wt=11): 3347 (c2 ^ (c1 v x)) v (y ^ c1)' = 1.  [para(6(a,1),916(a,1,2,1,2))].

given #489 (T,wt=11): 3349 (c2 ^ x) v (c1 ^ (y ^ x))' = 1.  [para(19(a,1),916(a,1,2,1))].

given #490 (A,wt=13): 227 x v c2 != 1 | c1 != 0 | c1' = x v c2.  [para(193(a,1),10(b,1)),rewrite(114(4))].

given #491 (T,wt=11): 3350 (c2 ^ (x v c1)) v (y ^ c1)' = 1.  [para(20(a,1),916(a,1,2,1,2))].

given #492 (T,wt=11): 3373 (c2 ^ (x v y)) v (c1 ^ x)' = 1.  [para(77(a,1),916(a,1,2,1))].

given #493 (T,wt=11): 3378 (c2 ^ (x v y)) v (c1 ^ y)' = 1.  [para(93(a,1),916(a,1,2,1))].

given #494 (T,wt=11): 3386 (x ^ c2) v (x ^ (c1 ^ y))' = 1.  [para(4(a,1),920(a,1,2,1)),rewrite(5(5))].

given #495 (A,wt=12): 230 c1 v (c2 v x)' != 1 | (c2 v x)' = c1'.  [para(197(a,1),10(b,1)),flip(c),xx(b)].

given #496 (T,wt=11): 3388 (c2 ^ (x v y)) v (x ^ c1)' = 1.  [para(22(a,1),920(a,1,2,1)),rewrite(4(3))].

given #497 (T,wt=11): 3398 (c2 ^ (x v y)) v (y ^ c1)' = 1.  [para(89(a,1),920(a,1,2,1)),rewrite(4(3))].

given #498 (T,wt=11): 3534 x v ((y ^ x) v (x ^ z))' = 1.  [para(945(a,1),104(a,1)),flip(a)].

given #499 (T,wt=11): 3536 c2 v ((x ^ c1) v (c2 ^ y))' = 1.  [para(945(a,1),278(a,1)),flip(a)].

NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 484 (0.00 of 4.28 sec).

given #500 (A,wt=12): 235 c1 v (x v c2)' != 1 | (x v c2)' = c1'.  [para(198(a,1),10(b,1)),flip(c),xx(b)].

given #501 (T,wt=11): 3537 c2 v ((c1 ^ x) v (c2 ^ y))' = 1.  [para(945(a,1),315(a,1)),flip(a)].

given #502 (T,wt=11): 3546 x ^ ((y v x) ^ (x v z))' = 0.  [para(1026(a,1),89(a,1)),flip(a)].

given #503 (T,wt=11): 3548 c1 ^ ((c2 v x) ^ (c1 v y))' = 0.  [para(1026(a,1),195(a,1)),flip(a)].

given #504 (T,wt=11): 3550 c1 ^ ((x v c2) ^ (c1 v y))' = 0.  [para(1026(a,1),226(a,1)),flip(a)].

given #505 (A,wt=19): 237 x v (y v z) != 1 | (z v x) ^ y != 0 | (z v x)' = y.  [para(2(a,1),37(a,1)),rewrite(3(2))].

given #506 (T,wt=11): 3571 c1 ^ ((c2 ^ (c1 v x)) v y) = c1.  [para(131(a,1),59(a,1)),rewrite(13(3),4(6)),flip(a)].

given #507 (T,wt=11): 3644 (x v y)' ^ (x v (y ^ z)) = 0.  [para(1137(a,1),4(a,1)),flip(a)].

given #508 (T,wt=11): 3690 c2 v (x v (c1 v (x ^ y))') = 1.  [para(1141(a,1),1440(a,1,2,2,1)),rewrite(82(8),2(8),75(8),2(7))].

given #509 (T,wt=11): 3765 (x ^ y)' v (x ^ (y v z)) = 1.  [para(1326(a,1),2(a,1)),flip(a)].

given #510 (A,wt=19): 238 x v (y v z) != 1 | (y v x) ^ z != 0 | (x v y)' = z.  [para(2(a,1),37(b,1,1))].

given #511 (T,wt=11): 3810 c1 ^ (x ^ (c2 ^ (x v y))') = 0.  [para(1328(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #512 (T,wt=11): 3833 (c2 v x) ^ (x v c1) = x v c1.  [para(1357(a,1),4(a,1)),flip(a)].

given #513 (T,wt=11): 3916 (c1 v x) ^ (y v (c2 v x))' = 0.  [para(2(a,1),1368(a,1,1))].

given #514 (T,wt=11): 3917 (x v c1) ^ (y v (x v c2))' = 0.  [para(2(a,1),1368(a,1,2,1,2))].

given #515 (A,wt=19): 239 x v (y v z) != 1 | z ^ (x v y) != 0 | (x v y)' = z.  [para(4(a,1),37(b,1))].

given #516 (T,wt=11): 3918 (x v c1) ^ (c2 v (x v y))' = 0.  [para(2(a,1),1368(a,1,2,1)),rewrite(3(5))].

given #517 (T,wt=11): 3919 (c1 v (c2 ^ x)) ^ (y v c2)' = 0.  [para(7(a,1),1368(a,1,2,1,2)),rewrite(2(4))].

given #518 (T,wt=11): 3921 (x v c1) ^ (c2 v (y v x))' = 0.  [para(17(a,1),1368(a,1,2,1))].

given #519 (T,wt=11): 3922 (c1 v (x ^ c2)) ^ (y v c2)' = 0.  [para(26(a,1),1368(a,1,2,1,2)),rewrite(2(4))].

given #520 (A,wt=17): 240 x v y != 1 | y ^ z != 0 | (x v y)' = y ^ z.  [para(7(a,1),37(a,1,2)),rewrite(19(6),89(6))].

given #521 (T,wt=11): 3930 (c1 v (x ^ y)) ^ (c2 v x)' = 0.  [para(63(a,1),1368(a,1,2,1)),rewrite(2(3))].

given #522 (T,wt=11): 3936 (c1 v (x ^ y)) ^ (c2 v y)' = 0.  [para(109(a,1),1368(a,1,2,1)),rewrite(2(3))].

given #523 (T,wt=11): 4126 (x ^ y)' v ((z v x) ^ y) = 1.  [para(1488(a,1),2(a,1)),flip(a)].

given #524 (T,wt=11): 4128 (x ^ (y v z)) v (z ^ x)' = 1.  [para(4(a,1),1488(a,1,1))].

given #525 (A,wt=12): 241 (x v y) ^ y' != 0 | (x v y)' = y'.  [para(8(a,1),37(a,1,2)),rewrite(94(2)),xx(a)].

given #526 (T,wt=11): 4129 ((x v y) ^ z) v (z ^ y)' = 1.  [para(4(a,1),1488(a,1,2,1))].

given #527 (T,wt=11): 4131 ((x v y) ^ (y v z)) v y' = 1.  [para(6(a,1),1488(a,1,2,1))].

given #528 (T,wt=11): 4136 ((x v y) ^ (z v y)) v y' = 1.  [para(20(a,1),1488(a,1,2,1))].

given #529 (T,wt=11): 4142 ((x v c1) ^ (c2 v y)) v c1' = 1.  [para(191(a,1),1488(a,1,2,1))].

given #530 (A,wt=19): 242 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x)' = z.  [para(17(a,1),37(a,1))].

given #531 (T,wt=11): 4144 ((x v c1) ^ (y v c2)) v c1' = 1.  [para(193(a,1),1488(a,1,2,1))].

given #532 (T,wt=11): 4207 x ^ (y ^ ((z v y) ^ x)') = 0.  [para(1490(a,1),19(a,1)),flip(a)].

given #533 (T,wt=11): 4224 x ^ ((y v x) ^ (z v x))' = 0.  [para(1490(a,1),89(a,1)),flip(a)].

given #534 (T,wt=11): 4230 c1 ^ ((x v c1) ^ (c2 v y))' = 0.  [para(1490(a,1),195(a,1)),flip(a)].

given #535 (A,wt=17): 243 x v y != 1 | x v y != 0 | (x v y)' = x v y.  [para(28(a,1),37(b,1)),rewrite(71(2),70(2))].

given #536 (T,wt=11): 4232 c1 ^ ((x v c1) ^ (y v c2))' = 0.  [para(1490(a,1),226(a,1)),flip(a)].

given #537 (T,wt=11): 4257 (x ^ y) v (z v x) = z v x.  [para(71(a,1),152(a,1,1)),rewrite(20(5)),flip(a)].

given #538 (T,wt=11): 4265 (c1 ^ x) v (y v c2) = y v c2.  [para(114(a,1),152(a,1,1)),rewrite(20(8)),flip(a)].

given #539 (T,wt=11): 4333 c1 ^ ((c2 v x) ^ (y v c1))' = 0.  [para(1502(a,1),195(a,1)),flip(a)].

given #540 (A,wt=13): 244 x v y != 1 | 0 != y | (x v y)' = y.  [para(29(a,1),37(a,1,2)),rewrite(4(5),20(5)),flip(b)].

given #541 (T,wt=11): 4335 c1 ^ ((x v c2) ^ (y v c1))' = 0.  [para(1502(a,1),226(a,1)),flip(a)].

given #542 (T,wt=11): 4347 c1 ^ (x ^ (c2 ^ (y v x))') = 0.  [para(1506(a,1),19(a,1)),flip(a)].

given #543 (T,wt=11): 4515 ((c2 v x) ^ (c1 v y)) v c1' = 1.  [para(191(a,1),170(a,1,1,2,1)),rewrite(191(9))].

Low Water (keep, True_semantics): wt=65

given #544 (T,wt=11): 4517 ((x v c2) ^ (c1 v y)) v c1' = 1.  [para(193(a,1),170(a,1,1,2,1)),rewrite(193(9))].

given #545 (A,wt=25): 247 x v (y v (z ^ u)) != 1 | z ^ ((x v y) ^ u) != 0 | (x v y)' = z ^ u.  [para(19(a,1),37(b,1))].

given #546 (T,wt=11): 4590 c1' v ((c2 v x) ^ (c1 v y)) = 1.  [para(119(a,1),1666(a,1,2))].

Low Water (keep, True_semantics): wt=63

given #547 (T,wt=11): 4684 c1' v ((c2 v x) ^ (y v c1)) = 1.  [para(119(a,1),1679(a,1,2))].

given #548 (T,wt=11): 4790 (x ^ y)' v (x ^ (z v y)) = 1.  [para(1707(a,1),2(a,1)),flip(a)].

given #549 (T,wt=11): 5040 c2' ^ ((c1 ^ x) v (c2 ^ y)) = 0.  [para(152(a,1),1756(a,1,2))].

given #550 (A,wt=17): 249 x v c2 != 1 | c2 ^ (x v c1) != 0 | (x v c1)' = c2.  [para(108(a,1),37(a,1,2)),rewrite(4(8))].

given #551 (T,wt=11): 5053 ((x ^ y) v (y ^ z)) ^ y' = 0.  [para(26(a,1),178(a,1,1,2,1)),rewrite(26(5))].

given #552 (T,wt=11): 5057 ((x ^ c1) v (c2 ^ y)) ^ c2' = 0.  [para(276(a,1),178(a,1,1,2,1)),rewrite(276(9))].

given #553 (T,wt=11): 5058 ((c1 ^ x) v (c2 ^ y)) ^ c2' = 0.  [para(304(a,1),178(a,1,1,2,1)),rewrite(304(9))].

given #554 (T,wt=11): 5118 c2' ^ ((c1 ^ x) v (y ^ c2)) = 0.  [para(152(a,1),1790(a,1,2))].

given #555 (A,wt=31): 250 x v (y v ((x v (y v z)) ^ u)) != 1 | (x v y) ^ u != 0 | (x v y)' = (x v (y v z)) ^ u.  [para(22(a,1),37(b,1)),rewrite(3(2),3(15))].

Low Water (keep, True_semantics): wt=61

given #556 (T,wt=11): 5251 ((x ^ y) v z) ^ (z v y)' = 0.  [para(26(a,1),1830(a,1,2,1,2))].

given #557 (T,wt=11): 5256 ((x ^ c1) v y) ^ (y v c2)' = 0.  [para(276(a,1),1830(a,1,2,1,2))].

given #558 (T,wt=11): 5257 ((c1 ^ x) v y) ^ (y v c2)' = 0.  [para(304(a,1),1830(a,1,2,1,2))].

given #559 (T,wt=11): 5517 (x v (y v z))' ^ (u ^ y) = 0.  [para(136(a,1),183(a,1,1)),rewrite(75(7),136(9))].

given #560 (A,wt=16): 251 (x v y) ^ (y' v z) != 0 | (x v y)' = y' v z.  [para(84(a,1),37(a,1,2)),rewrite(94(2)),xx(a)].

given #561 (T,wt=11): 5518 (x v (y v z))' ^ (u ^ z) = 0.  [para(141(a,1),183(a,1,1)),rewrite(75(7),141(9))].

given #562 (T,wt=11): 5527 (x v (c2 v y))' ^ (z ^ c1) = 0.  [para(231(a,1),183(a,1,1)),rewrite(75(9),231(13))].

given #563 (T,wt=11): 5528 (x v (y v c2))' ^ (z ^ c1) = 0.  [para(233(a,1),183(a,1,1)),rewrite(75(9),233(13))].

given #564 (T,wt=11): 5532 (x v c2)' ^ (y ^ (x v c1)) = 0.  [para(604(a,1),183(a,1,1)),rewrite(75(9),604(13))].

given #565 (A,wt=20): 252 x v (y v ((x v y)' ^ z)) != 1 | (x v y)' ^ z = (x v y)'.  [para(87(a,1),37(b,1)),flip(c),xx(b)].

given #566 (T,wt=11): 5534 (c2 ^ (c1 v x))' ^ (y ^ c1) = 0.  [para(1059(a,1),183(a,1,1)),rewrite(75(10),1059(15))].

given #567 (T,wt=11): 5536 (c2 v x)' ^ (y ^ (x v c1)) = 0.  [para(1358(a,1),183(a,1,1)),rewrite(75(9),1358(13))].

given #568 (T,wt=11): 5538 (x v c2)' ^ (y ^ (c1 v x)) = 0.  [para(1376(a,1),183(a,1,1)),rewrite(75(9),1376(13))].

given #569 (T,wt=11): 5539 (c2 ^ (x v c1))' ^ (y ^ c1) = 0.  [para(1504(a,1),183(a,1,1)),rewrite(75(10),1504(15))].

given #570 (A,wt=16): 253 (x v y) ^ (z v y') != 0 | (x v y)' = z v y'.  [para(96(a,1),37(a,1,2)),rewrite(94(2)),xx(a)].

given #571 (T,wt=11): 5542 (c2 v x)' ^ (y ^ (c1 v x)) = 0.  [para(1572(a,1),183(a,1,1)),rewrite(75(9),1572(13))].

given #572 (T,wt=11): 5551 (x v y)' ^ (z ^ (y v x)) = 0.  [para(2213(a,1),183(a,1,1)),rewrite(75(7),2213(9))].

given #573 (T,wt=11): 5578 (x ^ c2) v (c1 ^ (y ^ x))' = 1.  [para(183(a,1),1843(a,1,2)),rewrite(2(7))].

given #574 (T,wt=11): 5584 x ^ (c1 ^ ((x ^ c2) v y)') = 0.  [para(81(a,1),5496(a,1,2)),rewrite(4(7),5(7))].

given #575 (A,wt=12): 254 (x v y) ^ x' != 0 | (x v y)' = x'.  [para(96(a,1),37(a,1)),xx(a)].

given #576 (T,wt=11): 5597 (c1 v x) ^ (x v (c2 v y))' = 0.  [para(614(a,1),5496(a,1,2)),rewrite(3(3),4(7))].

given #577 (T,wt=11): 5625 (c1 v x) ^ (y v (x v c2))' = 0.  [para(614(a,1),5497(a,1,2)),rewrite(4(7))].

given #578 (T,wt=11): 5701 x v (c2 v ((x v c1) ^ y)') = 1.  [para(1883(a,1),17(a,1)),flip(a)].

Low Water (keep, True_semantics): wt=59

given #579 (T,wt=11): 5702 c2 v ((c1 v (c2 ^ x)) ^ y)' = 1.  [para(1883(a,1),24(a,1)),rewrite(2(6)),flip(a)].

given #580 (A,wt=20): 255 x v (y v (z ^ (x v y)')) != 1 | z ^ (x v y)' = (x v y)'.  [para(98(a,1),37(b,1)),flip(c),xx(b)].

given #581 (T,wt=11): 5714 c2 v ((c1 v (x ^ c2)) ^ y)' = 1.  [para(1883(a,1),104(a,1)),rewrite(2(6)),flip(a)].

given #582 (T,wt=11): 5719 c2 v (x ^ (c1 v (c2 ^ y)))' = 1.  [para(1902(a,1),24(a,1)),rewrite(2(6)),flip(a)].

given #583 (T,wt=11): 5731 c2 v (x ^ (c1 v (y ^ c2)))' = 1.  [para(1902(a,1),104(a,1)),rewrite(2(6)),flip(a)].

given #584 (T,wt=11): 5734 (c1 v x) ^ (c2 v (y v x))' = 0.  [para(2(a,1),1935(a,1,2,1,2))].

given #585 (A,wt=35): 256 x v (y v (z ^ (((x v y) ^ z) v u))) != 1 | (x v y) ^ z != 0 | (x v y)' = z ^ (((x v y) ^ z) v u).  [para(23(a,1),37(b,1))].

Low Water (keep, True_semantics): wt=55

given #586 (T,wt=11): 5736 (c1 v (c2 ^ x)) ^ (c2 v y)' = 0.  [para(24(a,1),1935(a,1,2,1))].

given #587 (T,wt=11): 5741 (c1 v (x ^ c2)) ^ (c2 v y)' = 0.  [para(104(a,1),1935(a,1,2,1))].

given #588 (T,wt=11): 5749 (x v (y ^ z)) ^ (z v x)' = 0.  [para(2(a,1),1987(a,1,1))].

given #589 (T,wt=11): 5750 (x v y)' ^ ((z ^ x) v y) = 0.  [para(1987(a,1),4(a,1)),flip(a)].

given #590 (A,wt=20): 257 x v (y v (x v (y v z))') != 1 | (x v (y v z))' = (x v y)'.  [para(116(a,1),37(b,1)),rewrite(3(2),3(14)),flip(c),xx(b)].

given #591 (T,wt=11): 5755 ((x ^ y) v (z ^ y)) ^ y' = 0.  [para(26(a,1),1987(a,1,2,1))].

given #592 (T,wt=11): 5763 ((x ^ c2) v (y ^ c1)) ^ c2' = 0.  [para(276(a,1),1987(a,1,2,1))].

given #593 (T,wt=11): 5764 ((x ^ c2) v (c1 ^ y)) ^ c2' = 0.  [para(304(a,1),1987(a,1,2,1))].

given #594 (T,wt=11): 5841 x v (y v ((z ^ y) v x)') = 1.  [para(1989(a,1),17(a,1)),flip(a)].

Low Water (keep, True_semantics): wt=49

given #595 (A,wt=20): 258 x v (y v (z v (x v y))') != 1 | (z v (x v y))' = (x v y)'.  [para(132(a,1),37(b,1)),flip(c),xx(b)].

given #596 (T,wt=11): 5865 x v ((y ^ x) v (z ^ x))' = 1.  [para(1989(a,1),104(a,1)),flip(a)].

given #597 (T,wt=11): 5872 c2 v ((x ^ c2) v (y ^ c1))' = 1.  [para(1989(a,1),278(a,1)),flip(a)].

given #598 (T,wt=11): 5873 c2 v ((x ^ c2) v (c1 ^ y))' = 1.  [para(1989(a,1),315(a,1)),flip(a)].

given #599 (T,wt=11): 5912 c2 v ((x ^ c1) v (y ^ c2))' = 1.  [para(2008(a,1),278(a,1)),flip(a)].

given #600 (A,wt=27): 259 x v (y v z) != 1 | (x v y) ^ ((y ^ u) v z) != 0 | (x v y)' = (y ^ u) v z.  [para(24(a,1),37(a,1,2))].

given #601 (T,wt=11): 5913 c2 v ((c1 ^ x) v (y ^ c2))' = 1.  [para(2008(a,1),315(a,1)),flip(a)].

given #602 (T,wt=11): 5923 c2 v (x v (c1 v (y ^ x))') = 1.  [para(2012(a,1),17(a,1)),flip(a)].

given #603 (T,wt=11): 5952 (x v y)' ^ (x v (z ^ y)) = 0.  [para(2078(a,1),4(a,1)),flip(a)].

Low Water (keep, True_semantics): wt=45

given #604 (T,wt=11): 6093 (c1 v x) ^ (x v (y v c2))' = 0.  [para(114(a,1),2210(a,1,2,1,2))].

given #605 (A,wt=16): 260 (x v y) ^ (y ^ z)' != 0 | (x v y)' = (y ^ z)'.  [para(149(a,1),37(a,1,2)),rewrite(94(2)),xx(a)].

Low Water (keep, True_semantics): wt=44

given #606 (T,wt=11): 6164 c1 ^ (x ^ ((x ^ c2) v y)') = 0.  [para(2270(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #607 (T,wt=11): 6181 c1 ^ ((c2 ^ (x v c1)) v y) = c1.  [para(20(a,1),196(a,2)),rewrite(89(10))].

given #608 (T,wt=11): 6237 x ^ (c1 ^ ((c2 ^ x) v y)') = 0.  [para(2273(a,1),19(a,1)),flip(a)].

given #609 (T,wt=11): 6238 c1 ^ ((c2 ^ (c1 v x)) v y)' = 0.  [para(2273(a,1),22(a,1)),flip(a)].

given #610 (A,wt=16): 261 (x v y) ^ (z ^ y)' != 0 | (x v y)' = (z ^ y)'.  [para(158(a,1),37(a,1,2)),rewrite(94(2)),xx(a)].

given #611 (T,wt=11): 6249 c1 ^ ((c2 ^ (x v c1)) v y)' = 0.  [para(2273(a,1),89(a,1)),flip(a)].

given #612 (T,wt=11): 6258 c1 ^ (x ^ (y v (x ^ c2))') = 0.  [para(2285(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #613 (T,wt=11): 6274 c1 ^ (x v (c2 ^ (c1 v y)))' = 0.  [para(2288(a,1),22(a,1)),flip(a)].

given #614 (T,wt=11): 6285 c1 ^ (x v (c2 ^ (y v c1)))' = 0.  [para(2288(a,1),89(a,1)),flip(a)].

given #615 (A,wt=12): 262 (x v c2) ^ c1' != 0 | (x v c2)' = c1'.  [para(166(a,1),37(a,1,2)),rewrite(94(2)),xx(a)].

given #616 (T,wt=11): 6296 (x v (y ^ c1)) ^ (c2 v x)' = 0.  [para(278(a,1),2299(a,1,2,1))].

given #617 (T,wt=11): 6297 (x v (c1 ^ y)) ^ (c2 v x)' = 0.  [para(315(a,1),2299(a,1,2,1))].

given #618 (T,wt=11): 6306 (x v c2)' ^ (x v (y ^ c1)) = 0.  [para(2306(a,1),4(a,1)),flip(a)].

Low Water (keep, True_semantics): wt=41

given #619 (T,wt=11): 6315 (x v c2)' ^ (x v (c1 ^ y)) = 0.  [para(2307(a,1),4(a,1)),flip(a)].

given #620 (A,wt=31): 263 x v (y v z) != 1 | (x v y) ^ (z v ((y v z) ^ u)) != 0 | (x v y)' = z v ((y v z) ^ u).  [para(25(a,1),37(a,1,2))].

given #621 (T,wt=11): 6327 (x v y)' ^ (y v (x ^ z)) = 0.  [para(2323(a,1),4(a,1)),flip(a)].

given #622 (T,wt=11): 6367 (x v y)' ^ ((y ^ z) v x) = 0.  [para(2324(a,1),4(a,1)),flip(a)].

given #623 (T,wt=11): 6499 x' ^ ((x ^ y) v (x ^ z)) = 0.  [para(7(a,1),2326(a,1,1,1))].

Low Water (keep, True_semantics): wt=39

given #624 (T,wt=11): 6503 x' ^ ((x ^ y) v (z ^ x)) = 0.  [para(26(a,1),2326(a,1,1,1))].

Low Water (keep, True_semantics): wt=37

given #625 (A,wt=21): 264 x v y != 1 | (x v y) ^ z != 0 | (x v y)' = (x v y) ^ z.  [para(25(a,1),37(a,1)),rewrite(66(7))].

given #626 (T,wt=11): 6508 (c2 v x)' ^ ((y ^ c1) v x) = 0.  [para(60(a,1),2326(a,1,2,1))].

given #627 (T,wt=11): 6509 c2' ^ ((c2 ^ x) v (y ^ c1)) = 0.  [para(276(a,1),2326(a,1,1,1))].

given #628 (T,wt=11): 6510 c2' ^ ((c2 ^ x) v (c1 ^ y)) = 0.  [para(304(a,1),2326(a,1,1,1))].

given #629 (T,wt=11): 6554 x ^ ((x' ^ y) v (x' ^ z)) = 0.  [para(208(a,1),2328(a,1,2)),rewrite(4(6))].

given #630 (A,wt=16): 265 (x v c2) ^ (c1' v y) != 0 | (x v c2)' = c1' v y.  [para(171(a,1),37(a,1,2)),rewrite(94(2)),xx(a)].

given #631 (T,wt=11): 6572 x ^ ((x' ^ y) v (z ^ x')) = 0.  [para(208(a,1),2333(a,1,2)),rewrite(4(6))].

given #632 (T,wt=11): 6573 ((x ^ c1) v (y ^ c2)) ^ c2' = 0.  [para(60(a,1),2333(a,1,1,1))].

given #633 (T,wt=11): 6614 ((x ^ c1) v (y ^ c1)) ^ c2' = 0.  [para(276(a,1),2338(a,1,2,1))].

given #634 (T,wt=11): 6615 ((x ^ c1) v (c1 ^ y)) ^ c2' = 0.  [para(304(a,1),2338(a,1,2,1))].

given #635 (A,wt=16): 266 (x v c2) ^ (y v c1') != 0 | (x v c2)' = y v c1'.  [para(173(a,1),37(a,1,2)),rewrite(94(2)),xx(a)].

given #636 (T,wt=11): 6756 x v (c2 v ((c1 v x) ^ y)') = 1.  [para(2399(a,1),17(a,1)),flip(a)].

given #637 (T,wt=11): 6945 (c2 ^ x) v (x ^ (y ^ c1))' = 1.  [para(60(a,1),2400(a,1,2,1,2))].

Low Water (keep, True_semantics): wt=36

given #638 (T,wt=11): 6970 ((c2 v x) ^ y) v (y ^ c1)' = 1.  [para(191(a,1),2401(a,1,2,1,2))].

given #639 (T,wt=11): 6972 ((x v c2) ^ y) v (y ^ c1)' = 1.  [para(193(a,1),2401(a,1,2,1,2))].

given #640 (A,wt=12): 267 (c2 v x) ^ c1' != 0 | (c2 v x)' = c1'.  [para(173(a,1),37(a,1)),xx(a)].

given #641 (T,wt=11): 7120 (x v c2) ^ (y ^ c1) = y ^ c1.  [para(2(a,1),2468(a,1,1))].

given #642 (T,wt=11): 7299 (x v y) ^ (z ^ y) = z ^ y.  [para(2(a,1),2470(a,1,1))].

given #643 (T,wt=11): 7367 (x ^ (c2 v y)) v (c1 ^ x)' = 1.  [para(195(a,1),2533(a,1,2,1))].

Low Water (keep, True_semantics): wt=35

given #644 (T,wt=11): 7368 (x ^ (y v c2)) v (c1 ^ x)' = 1.  [para(226(a,1),2533(a,1,2,1))].

given #645 (A,wt=20): 268 (x v y) ^ (z v (y v z)') != 0 | (x v y)' = z v (y v z)'.  [para(31(a,1),37(a,1,2)),rewrite(94(2)),xx(a)].

given #646 (T,wt=11): 7375 (x ^ c1)' v (x ^ (c2 v y)) = 1.  [para(2539(a,1),2(a,1)),flip(a)].

given #647 (T,wt=11): 7394 (x ^ c1)' v (x ^ (y v c2)) = 1.  [para(2541(a,1),2(a,1)),flip(a)].

given #648 (T,wt=11): 7503 (x ^ y)' v ((y v z) ^ x) = 1.  [para(4(a,1),2574(a,1,1,1))].

given #649 (T,wt=11): 7504 (x ^ y)' v (y ^ (x v z)) = 1.  [para(4(a,1),2574(a,1,2))].

Low Water (keep, True_semantics): wt=33

given #650 (A,wt=24): 269 x v (y v (z ^ ((x v y) ^ z)')) != 1 | z ^ ((x v y) ^ z)' = (x v y)'.  [para(34(a,1),37(b,1)),flip(c),xx(b)].

given #651 (T,wt=11): 7506 x' v ((x v y) ^ (x v z)) = 1.  [para(6(a,1),2574(a,1,1,1))].

given #652 (T,wt=11): 7510 x' v ((x v y) ^ (z v x)) = 1.  [para(20(a,1),2574(a,1,1,1))].

given #653 (T,wt=11): 7515 c1' v ((c1 v x) ^ (c2 v y)) = 1.  [para(191(a,1),2574(a,1,1,1))].

given #654 (T,wt=11): 7516 c1' v ((c1 v x) ^ (y v c2)) = 1.  [para(193(a,1),2574(a,1,1,1))].

given #655 (A,wt=12): 270 x' ^ (y v x) != 0 | y v x = x.  [para(223(a,1),10(a,1)),rewrite(208(10)),flip(c),xx(a)].

given #656 (T,wt=11): 7525 (c1 ^ x)' v ((c2 v y) ^ x) = 1.  [para(112(a,1),2574(a,1,2,1))].

given #657 (T,wt=11): 7526 (c1 ^ x)' v ((y v c2) ^ x) = 1.  [para(114(a,1),2574(a,1,2,1))].

given #658 (T,wt=11): 7649 x v ((x' v y) ^ (x' v z)) = 1.  [para(208(a,1),2578(a,1,2)),rewrite(2(6))].

Low Water (keep, True_semantics): wt=32

given #659 (T,wt=11): 7698 x v ((x' v y) ^ (z v x')) = 1.  [para(208(a,1),2582(a,1,2)),rewrite(2(6))].

given #660 (A,wt=13): 271 x v (y v (y v ((x v y) ^ z))') = 1.  [para(25(a,1),223(a,1,2)),rewrite(2(6),3(6))].

given #661 (T,wt=11): 7705 ((c2 v x) ^ (y v c1)) v c1' = 1.  [para(112(a,1),2582(a,1,1,1))].

given #662 (T,wt=11): 7706 ((x v c2) ^ (y v c1)) v c1' = 1.  [para(114(a,1),2582(a,1,1,1))].

given #663 (T,wt=11): 7749 ((c2 v x) ^ (c2 v y)) v c1' = 1.  [para(112(a,1),2586(a,1,1,1))].

given #664 (T,wt=11): 7750 ((x v c2) ^ (c2 v y)) v c1' = 1.  [para(114(a,1),2586(a,1,1,1))].

given #665 (A,wt=16): 272 (x v y') ^ (z v y) != 0 | (x v y')' = z v y.  [para(223(a,1),37(a,1,2)),rewrite(94(2)),xx(a)].

given #666 (T,wt=11): 7773 ((c2 v x) ^ (y v c2)) v c1' = 1.  [para(112(a,1),2588(a,1,1,1))].

given #667 (T,wt=11): 7774 ((x v c2) ^ (y v c2)) v c1' = 1.  [para(114(a,1),2588(a,1,1,1))].

given #668 (T,wt=11): 7889 x v (c2 v ((y ^ c1) v x)') = 1.  [para(60(a,1),2628(a,1,2,2,1,1))].

given #669 (T,wt=11): 7913 c2 v ((c1 ^ x) v (c1 ^ y))' = 1.  [hyper(207,a,2630,a(flip),b,1572,a),rewrite(2630(8),73(11),208(10),2630(16))].

given #670 (A,wt=12): 273 x' v (y ^ x) != 1 | y ^ x = x.  [para(224(a,1),10(b,1)),rewrite(208(10)),flip(c),xx(b)].

given #671 (T,wt=11): 7950 c2 v ((x ^ c1) v (y ^ c1))' = 1.  [para(2634(a,1),278(a,1)),flip(a)].

Low Water (keep, True_semantics): wt=31

given #672 (T,wt=11): 7951 c2 v ((x ^ c1) v (c1 ^ y))' = 1.  [para(2634(a,1),315(a,1)),flip(a)].

given #673 (T,wt=11): 7960 x v (c2 v ((c1 ^ y) v x)') = 1.  [para(2644(a,1),17(a,1)),flip(a)].

given #674 (T,wt=11): 7972 c2 v ((c1 ^ x) v (y ^ c1))' = 1.  [para(2644(a,1),278(a,1)),flip(a)].

given #675 (A,wt=13): 274 x ^ (y ^ (y ^ ((x ^ y) v z))') = 0.  [para(23(a,1),224(a,1,2)),rewrite(4(6),5(6))].

given #676 (T,wt=11): 8053 x ^ (c1 ^ ((c2 v y) ^ x)') = 0.  [para(112(a,1),2648(a,1,2,2,1,1))].

given #677 (T,wt=11): 8054 x ^ (c1 ^ ((y v c2) ^ x)') = 0.  [para(114(a,1),2648(a,1,2,2,1,1))].

given #678 (T,wt=11): 8076 c1 ^ ((c2 v x) ^ (c2 v y))' = 0.  [para(2649(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #679 (T,wt=11): 8208 c1 ^ ((c2 v x) ^ (y v c2))' = 0.  [para(2650(a,1),226(a,1)),flip(a)].

given #680 (A,wt=12): 275 (x ^ y) v y' != 1 | x ^ y = y.  [para(224(a,1),36(b,1)),rewrite(208(10)),flip(c),xx(b)].

given #681 (T,wt=11): 8223 c1 ^ ((x v c2) ^ (c2 v y))' = 0.  [para(2659(a,1),195(a,1)),flip(a)].

given #682 (T,wt=11): 8224 c1 ^ ((x v c2) ^ (y v c2))' = 0.  [para(2659(a,1),226(a,1)),flip(a)].

given #683 (T,wt=11): 8301 (x ^ c2) v (c1 ^ x) = c2 ^ x.  [para(2675(a,1),2(a,1)),flip(a)].

given #684 (T,wt=11): 8686 (c2 v x)' ^ ((c1 ^ y) v x) = 0.  [para(2901(a,1),4(a,1)),flip(a)].

given #685 (A,wt=13): 277 c2 != 1 | x ^ c1 != 0 | c2' = x ^ c1.  [para(60(a,1),10(b,1)),rewrite(276(4))].

given #686 (T,wt=11): 8690 ((c1 ^ x) v (y ^ c2)) ^ c2' = 0.  [para(26(a,1),2901(a,1,2,1))].

given #687 (T,wt=11): 8694 ((c1 ^ x) v (y ^ c1)) ^ c2' = 0.  [para(276(a,1),2901(a,1,2,1))].

given #688 (T,wt=11): 8695 ((c1 ^ x) v (c1 ^ y)) ^ c2' = 0.  [para(304(a,1),2901(a,1,2,1))].

given #689 (T,wt=11): 8848 (x ^ c2) v (c1 ^ (x ^ y))' = 1.  [para(4(a,1),3345(a,1,2,1)),rewrite(5(5))].

given #690 (A,wt=13): 280 (x ^ c2) v (x ^ (y ^ c1)) = x ^ c2.  [para(60(a,1),27(a,1,2,2))].

given #691 (T,wt=11): 8865 (c2 ^ (c1 v x)) v (c1 ^ y)' = 1.  [para(22(a,1),3346(a,1,2,1))].

given #692 (T,wt=11): 8875 (c2 ^ (x v c1)) v (c1 ^ y)' = 1.  [para(89(a,1),3346(a,1,2,1))].

given #693 (T,wt=11): 8891 (x ^ c1)' v (c2 ^ (c1 v y)) = 1.  [para(3347(a,1),2(a,1)),flip(a)].

given #694 (T,wt=11): 8967 (x ^ c1)' v (c2 ^ (y v c1)) = 1.  [para(3350(a,1),2(a,1)),flip(a)].

given #695 (A,wt=19): 282 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | x' = y ^ z.  [para(5(a,1),38(b,1))].

given #696 (T,wt=11): 8992 (c1 ^ x)' v (c2 ^ (x v y)) = 1.  [para(3373(a,1),2(a,1)),flip(a)].

Low Water (keep, True_semantics): wt=29

given #697 (T,wt=11): 9038 (c1 ^ x)' v (c2 ^ (y v x)) = 1.  [para(3378(a,1),2(a,1)),flip(a)].

given #698 (T,wt=11): 9118 (x ^ c1)' v (c2 ^ (x v y)) = 1.  [para(3388(a,1),2(a,1)),flip(a)].

given #699 (T,wt=11): 9143 (x ^ c1)' v (c2 ^ (y v x)) = 1.  [para(3398(a,1),2(a,1)),flip(a)].

given #700 (A,wt=13): 283 x v y != 1 | 0 != x | (x v y)' = x.  [para(6(a,1),38(b,1)),rewrite(2(2),70(2)),flip(b)].

given #701 (T,wt=11): 9470 c1 ^ (x v (c2 ^ (c1 v y))) = c1.  [para(2(a,1),3571(a,1,2))].

given #702 (T,wt=11): 9993 (c1 v (x ^ y)) ^ (x v c2)' = 0.  [para(24(a,1),3917(a,1,2,1)),rewrite(2(3))].

given #703 (T,wt=11): 9997 (c1 v (x ^ y)) ^ (y v c2)' = 0.  [para(104(a,1),3917(a,1,2,1)),rewrite(2(3))].

given #704 (T,wt=11): 10217 (x v c2)' ^ (c1 v (c2 ^ y)) = 0.  [para(3919(a,1),4(a,1)),flip(a)].

given #705 (A,wt=19): 284 x v (y v z) != 1 | (x v z) ^ y != 0 | y' = x v z.  [para(17(a,1),38(a,1))].

Low Water (keep, True_semantics): wt=28

given #706 (T,wt=11): 10271 (x v c2)' ^ (c1 v (y ^ c2)) = 0.  [para(3922(a,1),4(a,1)),flip(a)].

given #707 (T,wt=11): 10328 (c2 v x)' ^ (c1 v (x ^ y)) = 0.  [para(3930(a,1),4(a,1)),flip(a)].

given #708 (T,wt=11): 10365 (c2 v x)' ^ (c1 v (y ^ x)) = 0.  [para(3936(a,1),4(a,1)),flip(a)].

given #709 (T,wt=11): 10413 (x ^ y)' v ((z v y) ^ x) = 1.  [para(4(a,1),4126(a,1,1,1))].

given #710 (A,wt=19): 285 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | (x ^ y)' = z.  [para(19(a,1),38(b,1))].

given #711 (T,wt=11): 10414 (x ^ y)' v (y ^ (z v x)) = 1.  [para(4(a,1),4126(a,1,2))].

given #712 (T,wt=11): 10415 x' v ((y v x) ^ (x v z)) = 1.  [para(6(a,1),4126(a,1,1,1))].

given #713 (T,wt=11): 10419 x' v ((y v x) ^ (z v x)) = 1.  [para(20(a,1),4126(a,1,1,1))].

given #714 (T,wt=11): 10424 c1' v ((x v c1) ^ (c2 v y)) = 1.  [para(191(a,1),4126(a,1,1,1))].

given #715 (A,wt=21): 286 x v ((x v y) ^ z) != 1 | x ^ z != 0 | ((x v y) ^ z)' = x.  [para(22(a,1),38(b,1)),rewrite(2(3))].

given #716 (T,wt=11): 10425 c1' v ((x v c1) ^ (y v c2)) = 1.  [para(193(a,1),4126(a,1,1,1))].

given #717 (T,wt=11): 10617 x v ((y v x') ^ (x' v z)) = 1.  [para(208(a,1),4131(a,1,2)),rewrite(2(6))].

given #718 (T,wt=11): 10645 x v ((y v x') ^ (z v x')) = 1.  [para(208(a,1),4136(a,1,2)),rewrite(2(6))].

given #719 (T,wt=11): 11030 (x ^ y) v (z v y) = z v y.  [para(4(a,1),4257(a,1,1))].

Low Water (keep, True_semantics): wt=27

given #720 (A,wt=12): 287 x v (x' ^ y) != 1 | (x' ^ y)' = x.  [para(87(a,1),38(b,1)),rewrite(2(3)),xx(b)].

given #721 (T,wt=11): 11036 (x ^ c1) v (y v c2) = y v c2.  [para(60(a,1),4257(a,1,1))].

given #722 (T,wt=11): 11217 c1' v ((x v c2) ^ (c1 v y)) = 1.  [para(4517(a,1),2(a,1)),flip(a)].

given #723 (T,wt=11): 11304 c1' v ((c2 v x) ^ (c2 v y)) = 1.  [para(112(a,1),4590(a,1,2,2))].

given #724 (T,wt=11): 11305 c1' v ((c2 v x) ^ (y v c2)) = 1.  [para(114(a,1),4590(a,1,2,2))].

given #725 (A,wt=12): 288 x v (y ^ x') != 1 | (y ^ x')' = x.  [para(98(a,1),38(b,1)),rewrite(2(3)),xx(b)].

given #726 (T,wt=11): 11324 c1' v ((x v c2) ^ (y v c1)) = 1.  [para(2(a,1),4684(a,1,2,1))].

given #727 (T,wt=11): 11403 c2' ^ ((x ^ c1) v (c2 ^ y)) = 0.  [para(4(a,1),5040(a,1,2,1))].

given #728 (T,wt=11): 11410 c2' ^ ((c1 ^ x) v (y ^ c1)) = 0.  [para(60(a,1),5040(a,1,2,2))].

given #729 (T,wt=11): 11433 x' ^ ((y ^ x) v (x ^ z)) = 0.  [para(5053(a,1),4(a,1)),flip(a)].

given #730 (A,wt=25): 289 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | (y ^ ((x ^ y) v z))' = x.  [para(23(a,1),38(b,1)),rewrite(2(4))].

given #731 (T,wt=11): 11437 x ^ ((y ^ x') v (x' ^ z)) = 0.  [para(208(a,1),5053(a,1,2)),rewrite(4(6))].

given #732 (T,wt=11): 11488 c2' ^ ((x ^ c2) v (c1 ^ y)) = 0.  [para(2(a,1),5118(a,1,2))].

given #733 (T,wt=11): 11489 c2' ^ ((x ^ c1) v (y ^ c2)) = 0.  [para(4(a,1),5118(a,1,2,1))].

given #734 (T,wt=11): 11558 (x v y)' ^ ((z ^ y) v x) = 0.  [para(5251(a,1),4(a,1)),flip(a)].

given #735 (A,wt=12): 290 x v (x v y)' != 1 | x v y = x.  [para(116(a,1),38(b,1)),rewrite(2(3),208(11)),xx(b)].

given #736 (F,wt=7): 16534 c1' v (c1' v c2')' != 1.  [ur(290,b,15,a)].

given #737 (F,wt=7): 16537 (c1' v (c1' v c2')')' != 0.  [ur(2070,b,16534,a),rewrite(2(9))].

given #738 (T,wt=11): 11610 (x v c2)' ^ ((y ^ c1) v x) = 0.  [para(5256(a,1),4(a,1)),flip(a)].

given #739 (T,wt=11): 11632 (x v c2)' ^ ((c1 ^ y) v x) = 0.  [para(5257(a,1),4(a,1)),flip(a)].

given #740 (T,wt=11): 12105 (c2 v x)' ^ (c1 v (c2 ^ y)) = 0.  [para(5736(a,1),4(a,1)),flip(a)].

given #741 (T,wt=11): 12126 (c2 v x)' ^ (c1 v (y ^ c2)) = 0.  [para(5741(a,1),4(a,1)),flip(a)].

given #742 (A,wt=12): 292 x v (y v x)' != 1 | y v x = x.  [para(132(a,1),38(b,1)),rewrite(2(3),208(11)),xx(b)].

given #743 (T,wt=11): 12149 (x v y)' ^ (y v (z ^ x)) = 0.  [para(5749(a,1),4(a,1)),flip(a)].

given #744 (T,wt=11): 12221 x' ^ ((y ^ x) v (z ^ x)) = 0.  [para(26(a,1),5750(a,1,1,1))].

given #745 (T,wt=11): 12225 c2' ^ ((x ^ c2) v (y ^ c1)) = 0.  [para(276(a,1),5750(a,1,1,1))].

given #746 (T,wt=11): 12290 x ^ ((y ^ x') v (z ^ x')) = 0.  [para(208(a,1),5755(a,1,2)),rewrite(4(6))].

given #747 (A,wt=12): 293 c1 v (c2' ^ x) != 1 | (c2' ^ x)' = c1.  [para(138(a,1),38(b,1)),rewrite(2(5)),xx(b)].

given #748 (T,wt=11): 12933 c1 ^ (x v (c2 ^ (y v c1))) = c1.  [para(2(a,1),6181(a,1,2))].

given #749 (T,wt=11): 13092 (c2 v x)' ^ (x v (y ^ c1)) = 0.  [para(6296(a,1),4(a,1)),flip(a)].

Low Water (keep, True_semantics): wt=25

given #750 (T,wt=11): 13130 (c2 v x)' ^ (x v (c1 ^ y)) = 0.  [para(6297(a,1),4(a,1)),flip(a)].

given #751 (T,wt=11): 13587 c2' ^ ((x ^ c1) v (y ^ c1)) = 0.  [para(276(a,1),6508(a,1,1,1))].

given #752 (A,wt=12): 294 c1 v (x ^ c2') != 1 | (x ^ c2')' = c1.  [para(140(a,1),38(b,1)),rewrite(2(5)),xx(b)].

given #753 (T,wt=11): 13588 c2' ^ ((x ^ c1) v (c1 ^ y)) = 0.  [para(304(a,1),6508(a,1,1,1))].

given #754 (T,wt=11): 13653 c1 ^ ((c2' ^ x) v (c2' ^ y)) = 0.  [para(6554(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #755 (T,wt=11): 13694 c1 ^ ((c2' ^ x) v (y ^ c2')) = 0.  [para(6572(a,1),59(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #756 (T,wt=11): 13834 (x ^ c1)' v ((c2 v y) ^ x) = 1.  [para(6970(a,1),2(a,1)),flip(a)].

given #757 (A,wt=16): 295 x v (y ^ (x ^ y)') != 1 | (y ^ (x ^ y)')' = x.  [para(34(a,1),38(b,1)),rewrite(2(4)),xx(b)].

given #758 (T,wt=11): 13863 (x ^ c1)' v ((y v c2) ^ x) = 1.  [para(6972(a,1),2(a,1)),flip(a)].

given #759 (T,wt=11): 14005 (c1 ^ x)' v (x ^ (c2 v y)) = 1.  [para(7367(a,1),2(a,1)),flip(a)].

given #760 (T,wt=11): 14057 (c1 ^ x)' v (x ^ (y v c2)) = 1.  [para(7368(a,1),2(a,1)),flip(a)].

given #761 (T,wt=11): 14310 c1' v ((x v c2) ^ (c2 v y)) = 1.  [para(114(a,1),7515(a,1,2,1))].

given #762 (A,wt=17): 296 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | (c2 ^ x)' = c1.  [para(59(a,1),38(b,1)),rewrite(2(4))].

given #763 (T,wt=11): 14326 c1' v ((x v c2) ^ (y v c2)) = 1.  [para(114(a,1),7516(a,1,2,1))].

given #764 (T,wt=11): 14450 c2 v ((c1' v x) ^ (c1' v y)) = 1.  [para(7649(a,1),1440(a,1,2,2,1)),rewrite(82(10),2(10),75(10),2(9))].

given #765 (T,wt=11): 14493 c2 v ((c1' v x) ^ (y v c1')) = 1.  [para(7698(a,1),1440(a,1,2,2,1)),rewrite(82(10),2(10),75(10),2(9))].

given #766 (T,wt=11): 14946 c2' ^ ((c1 ^ x) v (c1 ^ y)) = 0.  [para(304(a,1),8686(a,1,1,1))].

given #767 (A,wt=13): 297 c2 v x != 1 | c1 != 0 | (c2 v x)' = c1.  [para(191(a,1),38(b,1)),rewrite(2(4),112(4))].

given #768 (T,wt=11): 15067 (c1 ^ x)' v (c2 ^ (c1 v y)) = 1.  [para(8865(a,1),2(a,1)),flip(a)].

given #769 (T,wt=11): 15095 (c1 ^ x)' v (c2 ^ (y v c1)) = 1.  [para(8875(a,1),2(a,1)),flip(a)].

given #770 (T,wt=11): 15461 (x v c2)' ^ (c1 v (x ^ y)) = 0.  [para(9993(a,1),4(a,1)),flip(a)].

given #771 (T,wt=11): 15479 (x v c2)' ^ (c1 v (y ^ x)) = 0.  [para(9997(a,1),4(a,1)),flip(a)].

given #772 (A,wt=13): 298 x v c2 != 1 | c1 != 0 | (x v c2)' = c1.  [para(193(a,1),38(b,1)),rewrite(2(4),114(4))].

given #773 (T,wt=11): 16086 c2 v ((x v c1') ^ (c1' v y)) = 1.  [para(10617(a,1),1440(a,1,2,2,1)),rewrite(82(10),2(10),75(10),2(9))].

given #774 (T,wt=11): 16126 c2 v ((x v c1') ^ (y v c1')) = 1.  [para(10645(a,1),1440(a,1,2,2,1)),rewrite(82(10),2(10),75(10),2(9))].

given #775 (T,wt=11): 16490 c1 ^ ((x ^ c2') v (c2' ^ y)) = 0.  [hyper(283,a,1034,a,b,11437,a(flip)),rewrite(11437(9),4(10),75(12),208(11),11437(18))].

given #776 (T,wt=11): 16664 c1 ^ ((x ^ c2') v (y ^ c2')) = 0.  [hyper(283,a,1034,a,b,12290,a(flip)),rewrite(12290(9),4(10),75(12),208(11),12290(18))].

given #777 (A,wt=12): 299 c1 v (c2 v x)' != 1 | c2 v x = c1.  [para(197(a,1),38(b,1)),rewrite(2(5),208(14)),xx(b)].

given #778 (T,wt=12): 300 c1 v (x v c2)' != 1 | x v c2 = c1.  [para(198(a,1),38(b,1)),rewrite(2(5),208(14)),xx(b)].

given #779 (T,wt=12): 301 (x v y) ^ y' != 0 | x v y = y.  [para(223(a,1),38(a,1)),rewrite(208(10)),flip(c),xx(a)].

given #780 (T,wt=12): 302 (x ^ y) v y' != 1 | (x ^ y)' = y'.  [para(224(a,1),38(b,1)),xx(b)].

given #781 (T,wt=12): 311 c2 ^ (x ^ c1)' != 0 | (x ^ c1)' = c2'.  [para(279(a,1),10(a,1)),flip(c),xx(a)].

given #782 (A,wt=13): 303 c2 != 1 | x ^ c1 != 0 | (x ^ c1)' = c2.  [para(60(a,1),38(b,1)),rewrite(2(4),276(4))].

given #783 (T,wt=12): 313 c2 ^ (x ^ c1)' != 0 | x ^ c1 = c2.  [para(279(a,1),36(a,1)),rewrite(4(8),208(14)),xx(a)].

given #784 (T,wt=12): 322 c2 ^ (c1 ^ x)' != 0 | (c1 ^ x)' = c2'.  [para(309(a,1),10(a,1)),flip(c),xx(a)].

given #785 (T,wt=12): 325 c2 ^ (c1 ^ x)' != 0 | c1 ^ x = c2.  [para(309(a,1),36(a,1)),rewrite(4(8),208(14)),xx(a)].

given #786 (T,wt=12): 341 (x ^ y) v x' != 1 | (x ^ y)' = x'.  [para(98(a,1),39(b,1)),xx(b)].

given #787 (A,wt=16): 314 (x v c2) ^ (y ^ c1)' != 0 | (x v c2)' = (y ^ c1)'.  [para(279(a,1),37(a,1,2)),rewrite(94(2)),xx(a)].

given #788 (T,wt=12): 345 (x ^ c1) v c2' != 1 | (x ^ c1)' = c2'.  [para(137(a,1),39(b,1,2)),rewrite(97(9)),xx(b)].

given #789 (T,wt=12): 350 (c1 ^ x) v c2' != 1 | (c1 ^ x)' = c2'.  [para(140(a,1),39(b,1)),xx(b)].

given #790 (T,wt=12): 1180 x' ^ (x v y) != 0 | x v y = x.  [para(84(a,1),65(a,1)),rewrite(208(10)),flip(c),xx(a)].

given #791 (T,wt=12): 1187 c1' ^ (c2 v x) != 0 | c2 v x = c1.  [para(171(a,1),65(a,1)),rewrite(208(13)),flip(c),xx(a)].

given #792 (A,wt=13): 316 c2 != 1 | c1 ^ x != 0 | c2' = c1 ^ x.  [para(304(a,1),10(a,1)),rewrite(19(7),59(7))].

given #793 (T,wt=12): 1389 x' v (x ^ y) != 1 | x ^ y = x.  [para(87(a,1),80(b,1)),rewrite(208(10)),flip(c),xx(b)].

given #794 (T,wt=12): 1394 c2' v (c1 ^ x) != 1 | c1 ^ x = c2.  [para(138(a,1),80(b,1)),rewrite(208(13)),flip(c),xx(b)].

given #795 (T,wt=12): 1858 c1' ^ (x v c2) != 0 | x v c2 = c1.  [para(1827(a,1),10(a,1)),rewrite(208(13)),flip(c),xx(a)].

given #796 (T,wt=12): 1860 (x v c2) ^ c1' != 0 | x v c2 = c1.  [para(1827(a,1),38(a,1)),rewrite(208(13)),flip(c),xx(a)].

given #797 (A,wt=13): 319 c2 != 1 | c1 ^ x != 0 | (c1 ^ x)' = c2.  [para(304(a,1),36(a,1)),rewrite(4(7),19(7),59(7))].

given #798 (T,wt=12): 2667 x ^ (y v x') != 0 | x' v y = x'.  [para(2(a,1),121(a,1,2))].

given #799 (T,wt=12): 2785 x v (y ^ x') != 1 | x' ^ y = x'.  [para(4(a,1),122(a,1,2))].

given #800 (T,wt=12): 2871 x ^ (x' v y) != 0 | y v x' = x'.  [para(2(a,1),124(a,1,2))].

given #801 (T,wt=12): 2983 x v (x' ^ y) != 1 | y ^ x' = x'.  [para(4(a,1),125(a,1,2))].

given #802 (A,wt=17): 320 x v c2 != 1 | c1 ^ y != 0 | (x v c2)' = c1 ^ y.  [para(304(a,1),37(a,1,2)),rewrite(19(9),226(9))].

given #803 (T,wt=12): 3671 x v (y v x)' != 1 | (x v y)' = x'.  [para(2(a,1),135(a,1,2,1))].

given #804 (T,wt=12): 3715 x v (x v y)' != 1 | (y v x)' = x'.  [para(2(a,1),144(a,1,2,1))].

given #805 (T,wt=12): 3801 c1 v (x ^ c2') != 1 | c2' ^ x = c1'.  [para(4(a,1),147(a,1,2))].

given #806 (T,wt=12): 3866 c2 ^ c1' != 0 | c1 v (c2 ^ c1') = c1.  [back_rewrite(3169),rewrite(3834(14))].

given #807 (A,wt=16): 326 (x v c2) ^ (c1 ^ y)' != 0 | (x v c2)' = (c1 ^ y)'.  [para(309(a,1),37(a,1,2)),rewrite(94(2)),xx(a)].

given #808 (T,wt=12): 4389 c1 v (c2' ^ x) != 1 | x ^ c2' = c1'.  [para(4(a,1),156(a,1,2))].

given #809 (T,wt=12): 4426 x ^ (y ^ x)' != 0 | (x ^ y)' = x'.  [para(4(a,1),160(a,1,2,1))].

given #810 (T,wt=12): 4456 x ^ (x ^ y)' != 0 | (y ^ x)' = x'.  [para(4(a,1),165(a,1,2,1))].

given #811 (T,wt=12): 4740 c1 v c2' != 1 | c2 ^ (c1 v c2') = c2.  [para(1723(a,1),175(b,1)),rewrite(2(4),208(12),2(15),4(17),2454(18)),flip(c),xx(b)].

given #812 (A,wt=19): 327 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (y ^ x)' = z.  [para(4(a,1),39(a,1,1))].

given #813 (T,wt=12): 5082 c2' v (x ^ c1) != 1 | x ^ c1 = c2.  [para(5042(a,1),10(b,1)),rewrite(208(13)),flip(c),xx(b)].

given #814 (T,wt=12): 5083 (x ^ c1) v c2' != 1 | x ^ c1 = c2.  [para(5042(a,1),36(b,1)),rewrite(208(13)),flip(c),xx(b)].

given #815 (T,wt=12): 5229 c2 ^ (x v c1') != 0 | c2' = c1' v x.  [para(2(a,1),180(a,1,2))].

given #816 (T,wt=12): 5353 c2 ^ (c1' v x) != 0 | c2' = x v c1'.  [para(2(a,1),181(a,1,2))].

Low Water (keep, True_semantics): wt=24

given #817 (A,wt=19): 328 (x ^ y) v z != 1 | y ^ (z ^ x) != 0 | (x ^ y)' = z.  [para(4(a,1),39(b,1)),rewrite(5(6))].

given #818 (T,wt=12): 6642 x' ^ (y v x) != 0 | (y v x)' = x'.  [para(223(a,1),205(a,1)),xx(a)].

given #819 (T,wt=12): 6643 x' v (y ^ x) != 1 | (y ^ x)' = x'.  [para(224(a,1),205(b,1)),xx(b)].

given #820 (T,wt=12): 6645 c1' ^ (x v c2) != 0 | (x v c2)' = c1'.  [para(1827(a,1),205(a,1)),xx(a)].

given #821 (T,wt=12): 6675 c2' v (x ^ c1) != 1 | (x ^ c1)' = c2'.  [para(5042(a,1),205(b,1)),xx(b)].

given #822 (A,wt=17): 329 x v y != 1 | z ^ x != 0 | (z ^ x)' = x v y.  [para(6(a,1),39(b,1,2)),rewrite(17(3),104(3))].

given #823 (T,wt=12): 6779 x' v (x ^ y) != 1 | (x ^ y)' = x'.  [para(98(a,1),206(b,1)),xx(b)].

given #824 (T,wt=12): 6783 c2' v (c1 ^ x) != 1 | (c1 ^ x)' = c2'.  [para(140(a,1),206(b,1)),xx(b)].

given #825 (T,wt=12): 7413 (x ^ y) v x' != 1 | x ^ y = x.  [para(87(a,1),210(b,1)),rewrite(208(10)),flip(c),xx(b)].

given #826 (T,wt=12): 7415 (c1 ^ x) v c2' != 1 | c1 ^ x = c2.  [para(138(a,1),210(b,1)),rewrite(208(13)),flip(c),xx(b)].

given #827 (A,wt=25): 330 x v ((y ^ z) v u) != 1 | y ^ (z ^ (x v u)) != 0 | (y ^ z)' = x v u.  [para(17(a,1),39(a,1))].

given #828 (T,wt=12): 7830 x ^ (y v x') != 0 | (x' v y)' = x.  [para(2(a,1),213(a,1,2))].

given #829 (T,wt=12): 7832 x' ^ (x v y) != 0 | (x v y)' = x'.  [para(208(a,1),213(a,1,2,1)),rewrite(208(7))].

given #830 (T,wt=12): 7958 x ^ (x' v y) != 0 | (y v x')' = x.  [para(2(a,1),214(a,1,2))].

given #831 (T,wt=12): 8294 x ^ (y ^ x)' != 0 | x ^ y = x.  [para(4(a,1),216(a,1,2,1))].

given #832 (A,wt=17): 331 x ^ y != 1 | x ^ y != 0 | (x ^ y)' = x ^ y.  [para(29(a,1),39(a,1)),rewrite(67(5),66(5))].

given #833 (T,wt=12): 8374 x ^ (x ^ y)' != 0 | y ^ x = x.  [para(4(a,1),217(a,1,2,1))].

given #834 (T,wt=12): 8375 (x v y) ^ x' != 0 | x v y = x.  [para(6(a,1),217(a,1,2,1)),rewrite(6(7)),flip(b)].

given #835 (T,wt=12): 8378 (c2 v x) ^ c1' != 0 | c2 v x = c1.  [para(191(a,1),217(a,1,2,1)),rewrite(191(11)),flip(b)].

given #836 (T,wt=12): 8484 c1 v c2' != 1 | (c2 ^ (c1 v c2'))' = c2'.  [para(1723(a,1),219(b,1)),rewrite(2(4),2(14),4(16),2454(17)),xx(b)].

given #837 (A,wt=19): 334 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (x ^ y)' = z.  [para(19(a,1),39(b,1))].

given #838 (T,wt=12): 8653 c2 ^ (x v c1') != 0 | (c1' v x)' = c2.  [para(2(a,1),220(a,1,2))].

given #839 (T,wt=12): 8758 c2 ^ (c1' v x) != 0 | (x v c1')' = c2.  [para(2(a,1),221(a,1,2))].

given #840 (T,wt=12): 9110 c1 v (x v c2)' != 1 | (c2 v x)' = c1'.  [para(2(a,1),230(a,1,2,1))].

given #841 (T,wt=12): 9214 c1 v (c2 v x)' != 1 | (x v c2)' = c1'.  [para(2(a,1),235(a,1,2,1))].

given #842 (A,wt=27): 336 (x ^ y) v ((y v z) ^ u) != 1 | x ^ (y ^ u) != 0 | (x ^ y)' = (y v z) ^ u.  [para(22(a,1),39(b,1,2))].

given #843 (T,wt=12): 9630 (x v y) ^ x' != 0 | (y v x)' = x'.  [para(8(a,1),238(a,1,2)),rewrite(94(2)),xx(a)].

given #844 (T,wt=12): 9637 (x v y) ^ y' != 0 | (y v x)' = y'.  [para(96(a,1),238(a,1)),xx(a)].

given #845 (T,wt=12): 9642 (c2 v x) ^ c1' != 0 | (x v c2)' = c1'.  [para(166(a,1),238(a,1,2)),rewrite(94(2)),xx(a)].

given #846 (T,wt=12): 9647 (x v c2) ^ c1' != 0 | (c2 v x)' = c1'.  [para(173(a,1),238(a,1)),xx(a)].

given #847 (A,wt=20): 337 x ^ (y ^ ((x ^ y)' v z)) != 0 | (x ^ y)' v z = (x ^ y)'.  [para(84(a,1),39(a,1)),flip(c),xx(a)].

given #848 (T,wt=12): 10013 c1' ^ (c2 v x) != 0 | (c2 v x)' = c1'.  [para(173(a,1),239(a,1)),xx(a)].

given #849 (T,wt=12): 14337 x' ^ (x v y) != 0 | y v x = x.  [para(2(a,1),270(a,1,2))].

given #850 (T,wt=12): 14731 x' v (x ^ y) != 1 | y ^ x = x.  [para(4(a,1),273(a,1,2))].

given #851 (T,wt=12): 14897 (x ^ y) v x' != 1 | y ^ x = x.  [para(4(a,1),275(a,1,1))].

given #852 (A,wt=16): 338 (x ^ y) v (y' ^ z) != 1 | (x ^ y)' = y' ^ z.  [para(87(a,1),39(b,1,2)),rewrite(97(8)),xx(b)].

given #853 (T,wt=12): 16192 x v (y ^ x') != 1 | (x' ^ y)' = x.  [para(4(a,1),287(a,1,2))].

given #854 (T,wt=12): 16241 x v (x' ^ y) != 1 | (y ^ x')' = x.  [para(4(a,1),288(a,1,2))].

given #855 (T,wt=12): 16293 c2 ^ c1' != 0 | (c1 v (c2 ^ c1'))' = c1'.  [para(1523(a,1),289(a,1)),rewrite(4(7),4(14),2(16),3834(17)),xx(a)].

given #856 (T,wt=12): 16535 x v (y v x)' != 1 | x v y = x.  [para(2(a,1),290(a,1,2,1))].

given #857 (A,wt=20): 339 x ^ (y ^ (z v (x ^ y)')) != 0 | z v (x ^ y)' = (x ^ y)'.  [para(96(a,1),39(a,1)),flip(c),xx(a)].

given #858 (T,wt=12): 16566 x v (x v y)' != 1 | y v x = x.  [para(2(a,1),292(a,1,2,1))].

given #859 (T,wt=12): 16685 c1 v (x ^ c2') != 1 | (c2' ^ x)' = c1.  [para(4(a,1),293(a,1,2))].

given #860 (T,wt=12): 16792 c1 v (c2' ^ x) != 1 | (x ^ c2')' = c1.  [para(4(a,1),294(a,1,2))].

given #861 (T,wt=12): 17063 c1 v (x v c2)' != 1 | c2 v x = c1.  [para(2(a,1),299(a,1,2,1))].

given #862 (A,wt=16): 340 (x ^ y) v (z ^ y') != 1 | (x ^ y)' = z ^ y'.  [para(98(a,1),39(b,1,2)),rewrite(97(8)),xx(b)].

given #863 (T,wt=12): 17065 c1 v (c2 v x)' != 1 | x v c2 = c1.  [para(2(a,1),300(a,1,2,1))].

given #864 (T,wt=12): 17067 (x v y) ^ x' != 0 | y v x = x.  [para(2(a,1),301(a,1,1))].

given #865 (T,wt=12): 17069 (x ^ y) v x' != 1 | (y ^ x)' = x'.  [para(4(a,1),302(a,1,1))].

given #866 (T,wt=12): 17075 c2 ^ (c1 ^ x)' != 0 | (x ^ c1)' = c2'.  [para(4(a,1),311(a,1,2,1))].

given #867 (A,wt=31): 342 (x ^ y) v (z ^ ((y ^ z) v u)) != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z ^ ((y ^ z) v u).  [para(23(a,1),39(b,1,2))].

given #868 (T,wt=12): 17079 c2 ^ (c1 ^ x)' != 0 | x ^ c1 = c2.  [para(4(a,1),313(a,1,2,1))].

given #869 (T,wt=12): 17081 c2 ^ (x ^ c1)' != 0 | (c1 ^ x)' = c2'.  [para(4(a,1),322(a,1,2,1))].

given #870 (T,wt=12): 17083 c2 ^ (x ^ c1)' != 0 | c1 ^ x = c2.  [para(4(a,1),325(a,1,2,1))].

given #871 (T,wt=12): 17085 (x ^ y) v y' != 1 | (y ^ x)' = y'.  [para(4(a,1),341(a,1,1))].

given #872 (A,wt=21): 343 (x ^ y) v z != 1 | x ^ y != 0 | (x ^ y)' = (x ^ y) v z.  [para(23(a,1),39(b,1)),rewrite(70(4))].

given #873 (T,wt=12): 17090 (c1 ^ x) v c2' != 1 | (x ^ c1)' = c2'.  [para(4(a,1),345(a,1,1))].

given #874 (T,wt=12): 17092 (x ^ c1) v c2' != 1 | (c1 ^ x)' = c2'.  [para(4(a,1),350(a,1,1))].

given #875 (T,wt=12): 17094 x' ^ (y v x) != 0 | x v y = x.  [para(2(a,1),1180(a,1,2))].

given #876 (T,wt=12): 17100 c1' ^ (x v c2) != 0 | c2 v x = c1.  [para(2(a,1),1187(a,1,2))].

given #877 (A,wt=16): 344 (x ^ y) v (y v z)' != 1 | (y v z)' = (x ^ y)'.  [para(116(a,1),39(b,1,2)),rewrite(97(8)),flip(c),xx(b)].

given #878 (T,wt=12): 17106 x' v (y ^ x) != 1 | x ^ y = x.  [para(4(a,1),1389(a,1,2))].

given #879 (T,wt=12): 17109 c2' v (x ^ c1) != 1 | c1 ^ x = c2.  [para(4(a,1),1394(a,1,2))].

given #880 (T,wt=12): 17111 c1' ^ (c2 v x) != 0 | x v c2 = c1.  [para(2(a,1),1858(a,1,2))].

given #881 (T,wt=12): 17113 (c2 v x) ^ c1' != 0 | x v c2 = c1.  [para(2(a,1),1860(a,1,1))].

given #882 (A,wt=16): 346 (x ^ y) v (z v y)' != 1 | (z v y)' = (x ^ y)'.  [para(132(a,1),39(b,1,2)),rewrite(97(8)),flip(c),xx(b)].

given #883 (T,wt=12): 17477 c2' v (c1 ^ x) != 1 | x ^ c1 = c2.  [para(4(a,1),5082(a,1,2))].

given #884 (T,wt=12): 17479 (c1 ^ x) v c2' != 1 | x ^ c1 = c2.  [para(4(a,1),5083(a,1,1))].

given #885 (T,wt=12): 17577 x' ^ (x v y) != 0 | (y v x)' = x'.  [para(2(a,1),6642(a,1,2))].

given #886 (T,wt=12): 17580 x' v (x ^ y) != 1 | (y ^ x)' = x'.  [para(4(a,1),6643(a,1,2))].

given #887 (A,wt=16): 347 (x ^ c1) v (c2' ^ y) != 1 | (x ^ c1)' = c2' ^ y.  [para(138(a,1),39(b,1,2)),rewrite(97(10)),xx(b)].

given #888 (T,wt=12): 17583 c1' ^ (c2 v x) != 0 | (x v c2)' = c1'.  [para(2(a,1),6645(a,1,2))].

given #889 (T,wt=12): 17585 c2' v (c1 ^ x) != 1 | (x ^ c1)' = c2'.  [para(4(a,1),6675(a,1,2))].

given #890 (T,wt=12): 17667 x' v (y ^ x) != 1 | (x ^ y)' = x'.  [para(4(a,1),6779(a,1,2))].

given #891 (T,wt=12): 17670 c2' v (x ^ c1) != 1 | (c1 ^ x)' = c2'.  [para(4(a,1),6783(a,1,2))].

given #892 (A,wt=31): 348 (x ^ y) v z != 1 | x ^ (y ^ ((x ^ (y ^ u)) v z)) != 0 | (x ^ y)' = (x ^ (y ^ u)) v z.  [para(24(a,1),39(a,1)),rewrite(5(6),5(15))].

given #893 (T,wt=12): 17672 (x ^ y) v y' != 1 | y ^ x = y.  [para(4(a,1),7413(a,1,1))].

given #894 (T,wt=12): 17674 (x ^ c1) v c2' != 1 | c1 ^ x = c2.  [para(4(a,1),7415(a,1,1))].

given #895 (T,wt=12): 17681 x' ^ (y v x) != 0 | (x v y)' = x'.  [para(208(a,1),7830(a,1,2,2)),rewrite(208(7))].

given #896 (T,wt=12): 17693 (x v y) ^ y' != 0 | y v x = y.  [para(2(a,1),8375(a,1,1))].

given #897 (A,wt=16): 349 (x ^ c1) v (y ^ c2') != 1 | (x ^ c1)' = y ^ c2'.  [para(140(a,1),39(b,1,2)),rewrite(97(10)),xx(b)].

given #898 (T,wt=12): 17695 (x v c2) ^ c1' != 0 | c2 v x = c1.  [para(2(a,1),8378(a,1,1))].

given #899 (T,wt=12): 17756 c1' ^ (x v c2) != 0 | (c2 v x)' = c1'.  [para(4(a,1),9647(a,1))].

given #900 (T,wt=13): 364 x ^ (y ^ (z v (x v u))) = y ^ x.  [para(62(a,1),19(a,1,2)),flip(a)].

given #901 (T,wt=13): 369 1 != x | y ^ x != 0 | (x ^ y)' = x.  [para(67(a,1),39(b,1)),rewrite(2(2),7(2)),flip(a)].

given #902 (A,wt=20): 351 x ^ (y ^ (x ^ (y ^ z))') != 0 | (x ^ (y ^ z))' = (x ^ y)'.  [para(149(a,1),39(a,1)),rewrite(5(5),5(14)),flip(c),xx(a)].

given #903 (T,wt=13): 434 x v y != 1 | 0 != y | (y v x)' = y.  [para(71(a,1),37(a,1)),rewrite(4(5),6(5)),flip(b)].

given #904 (T,wt=13): 436 x v (y v (z ^ (x ^ u))) = y v x.  [para(78(a,1),17(a,1,2)),flip(a)].

given #905 (T,wt=13): 476 c2 != 1 | x ^ c1 != 0 | (c1 ^ x)' = c2.  [para(81(a,1),39(b,1)),rewrite(2(4),304(4))].

given #906 (T,wt=13): 477 x ^ ((y v (z v x)) ^ u) = x ^ u.  [para(88(a,1),5(a,1,1)),flip(a)].

given #907 (A,wt=20): 352 x ^ (y ^ (z ^ (x ^ y))') != 0 | (z ^ (x ^ y))' = (x ^ y)'.  [para(158(a,1),39(a,1)),flip(c),xx(a)].

given #908 (T,wt=13): 479 x ^ (y ^ (z v (u v x))) = y ^ x.  [para(88(a,1),19(a,1,2)),flip(a)].

given #909 (T,wt=13): 482 x v ((y ^ (z ^ x)) v u) = x v u.  [para(106(a,1),3(a,1,1)),flip(a)].

given #910 (T,wt=13): 484 x v (y v (z ^ (u ^ x))) = y v x.  [para(106(a,1),17(a,1,2)),flip(a)].

given #911 (T,wt=13): 487 (c2 ^ x) v (y ^ (c1 ^ x)) = c2 ^ x.  [para(59(a,1),106(a,1,2,2))].

given #912 (A,wt=35): 353 (x ^ y) v z != 1 | x ^ (y ^ (z v (((x ^ y) v z) ^ u))) != 0 | (x ^ y)' = z v (((x ^ y) v z) ^ u).  [para(25(a,1),39(a,1))].

given #913 (T,wt=13): 490 (x ^ c2) v (y ^ (x ^ c1)) = x ^ c2.  [para(81(a,1),106(a,1,2,2))].

given #914 (T,wt=13): 598 (x v c1) ^ (x v (c2 v y)) = x v c1.  [para(112(a,1),21(a,1,2,2))].

given #915 (T,wt=13): 606 x v c2 != 1 | c1 != 0 | (c2 v x)' = c1.  [para(113(a,1),37(a,1)),rewrite(4(8),191(8))].

given #916 (T,wt=13): 610 (x v c1) ^ (y v (x v c2)) = x v c1.  [para(113(a,1),88(a,1,2,2))].

given #917 (A,wt=24): 354 x ^ (y ^ (z v ((x ^ y) v z)')) != 0 | z v ((x ^ y) v z)' = (x ^ y)'.  [para(31(a,1),39(a,1)),flip(c),xx(a)].

given #918 (T,wt=13): 613 (x v c1) ^ (x v (y v c2)) = x v c1.  [para(114(a,1),21(a,1,2,2))].

given #919 (T,wt=13): 619 (x v y) ^ ((x v (y v z))' ^ u) = 0.  [para(3(a,1),123(a,1,2,1,1))].

given #920 (T,wt=13): 705 (x v y) ^ (z ^ (x v (y v u))') = 0.  [para(3(a,1),126(a,1,2,2,1))].

given #921 (T,wt=13): 713 x ^ (y ^ (z v ((x ^ y) v u))') = 0.  [para(136(a,1),5(a,1)),flip(a)].

given #922 (A,wt=20): 355 (x ^ y) v (z ^ (y ^ z)') != 1 | (x ^ y)' = z ^ (y ^ z)'.  [para(34(a,1),39(b,1,2)),rewrite(97(9)),xx(b)].

given #923 (T,wt=13): 718 x ^ (y ^ (z v (u v (x ^ y)))') = 0.  [para(141(a,1),5(a,1)),flip(a)].

given #924 (T,wt=13): 721 ((x ^ y) v z) ^ (u v (x v z))' = 0.  [para(24(a,1),141(a,1,2,1,2))].

given #925 (T,wt=13): 726 (x v y) ^ ((x v (z v y))' ^ u) = 0.  [para(17(a,1),142(a,1,2,1,1))].

given #926 (T,wt=13): 727 ((x ^ y) v z) ^ ((x v z)' ^ u) = 0.  [para(24(a,1),142(a,1,2,1,1))].

given #927 (A,wt=23): 356 (x ^ c1) v (c2 ^ y) != 1 | x ^ (c1 ^ y) != 0 | (x ^ c1)' = c2 ^ y.  [para(59(a,1),39(b,1,2))].

given #928 (T,wt=13): 755 (x v y) ^ (z ^ (x v (u v y))') = 0.  [para(17(a,1),146(a,1,2,2,1))].

given #929 (T,wt=13): 756 ((x ^ y) v z) ^ (u ^ (x v z)') = 0.  [para(24(a,1),146(a,1,2,2,1))].

given #930 (T,wt=13): 763 (x ^ y) v ((x ^ (y ^ z))' v u) = 1.  [para(5(a,1),153(a,1,2,1,1))].

given #931 (T,wt=13): 774 (x ^ y) v (z v (x ^ (y ^ u))') = 1.  [para(5(a,1),154(a,1,2,2,1))].

given #932 (A,wt=17): 357 c2 v x != 1 | y ^ c1 != 0 | (y ^ c1)' = c2 v x.  [para(191(a,1),39(b,1,2)),rewrite(17(5),278(5))].

given #933 (T,wt=13): 784 x v (y v (z ^ ((x v y) ^ u))') = 1.  [para(161(a,1),3(a,1)),flip(a)].

given #934 (T,wt=13): 896 (x ^ y) v ((x ^ (z ^ y))' v u) = 1.  [para(19(a,1),162(a,1,2,1,1))].

given #935 (T,wt=13): 897 ((x v y) ^ z) v ((x ^ z)' v u) = 1.  [para(22(a,1),162(a,1,2,1,1))].

given #936 (T,wt=13): 911 x v (y v (z ^ (u ^ (x v y)))') = 1.  [para(164(a,1),3(a,1)),flip(a)].

given #937 (A,wt=16): 359 (x ^ c1) v (c2 v y)' != 1 | (c2 v y)' = (x ^ c1)'.  [para(197(a,1),39(b,1,2)),rewrite(97(10)),flip(c),xx(b)].

given #938 (T,wt=13): 914 ((x v y) ^ z) v (u ^ (x ^ z))' = 1.  [para(22(a,1),164(a,1,2,1,2))].

given #939 (T,wt=13): 930 (x ^ y) v (z v (x ^ (u ^ y))') = 1.  [para(19(a,1),167(a,1,2,2,1))].

given #940 (T,wt=13): 931 ((x v y) ^ z) v (u v (x ^ z)') = 1.  [para(22(a,1),167(a,1,2,2,1))].

given #941 (T,wt=13): 1037 (x ^ (c2 ^ y)) v (c1 ^ (x ^ y))' = 1.  [para(19(a,1),199(a,1,1))].

given #942 (A,wt=16): 360 (x ^ c1) v (y v c2)' != 1 | (y v c2)' = (x ^ c1)'.  [para(198(a,1),39(b,1,2)),rewrite(97(10)),flip(c),xx(b)].

given #943 (T,wt=13): 1038 (c2 ^ (x ^ y)) v (x ^ (c1 ^ y))' = 1.  [para(19(a,1),199(a,1,2,1))].

given #944 (T,wt=13): 1040 (c2 ^ ((c1 v x) ^ y)) v (c1 ^ y)' = 1.  [para(22(a,1),199(a,1,2,1))].

given #945 (T,wt=13): 1067 c1 ^ ((x v (c2 v y)) ^ z) = c1 ^ z.  [para(202(a,1),5(a,1,1)),flip(a)].

given #946 (T,wt=13): 1068 c1 ^ (x ^ (y v (c2 v z))) = x ^ c1.  [para(202(a,1),19(a,1,2)),flip(a)].

given #947 (A,wt=16): 361 (x ^ y') v (z ^ y) != 1 | (x ^ y')' = z ^ y.  [para(224(a,1),39(b,1,2)),rewrite(97(8)),xx(b)].

given #948 (T,wt=13): 1074 x' ^ (x v (y ^ x')) = x' ^ (x v y).  [para(8(a,1),58(a,1,2,2,2)),rewrite(32(3)),flip(a)].

given #949 (T,wt=13): 1085 c1' ^ (c2 v (x ^ c1')) = c1' ^ (c2 v x).  [para(166(a,1),58(a,1,2,2,2)),rewrite(32(5)),flip(a)].

given #950 (T,wt=13): 1125 c1 ^ ((x v (y v c2)) ^ z) = c1 ^ z.  [para(225(a,1),5(a,1,1)),flip(a)].

given #951 (T,wt=13): 1126 c1 ^ (x ^ (y v (z v c2))) = x ^ c1.  [para(225(a,1),19(a,1,2)),flip(a)].

given #952 (A,wt=23): 362 (x ^ c2) v (y ^ c1) != 1 | x ^ (y ^ c1) != 0 | (x ^ c2)' = y ^ c1.  [para(60(a,1),39(b,1,2))].

given #953 (T,wt=13): 1150 (x v (y ^ z)) ^ (u v (x v y))' = 0.  [para(63(a,1),141(a,1,2,1,2))].

given #954 (T,wt=13): 1151 (x v (y ^ z)) ^ ((x v y)' ^ u) = 0.  [para(63(a,1),142(a,1,2,1,1))].

given #955 (T,wt=13): 1153 (x v (y ^ z)) ^ (u ^ (x v y)') = 0.  [para(63(a,1),146(a,1,2,2,1))].

given #956 (T,wt=13): 1218 c2 v ((x ^ (y ^ c1)) v z) = c2 v z.  [para(305(a,1),3(a,1,1)),flip(a)].

given #957 (A,wt=17): 363 c1 v (c2 ^ x) != 1 | x ^ c1 != 0 | (c2 ^ x)' = c1.  [para(60(a,1),39(b,1)),rewrite(2(4))].

given #958 (T,wt=13): 1219 c2 v (x v (y ^ (z ^ c1))) = x v c2.  [para(305(a,1),17(a,1,2)),flip(a)].

given #959 (T,wt=13): 1263 1 != x | y ^ x != 0 | x' = x ^ y.  [para(4(a,1),69(b,1))].

given #960 (T,wt=13): 1268 c1 != 1 | c1 ^ x != 0 | c1' = c1 ^ x.  [para(59(a,1),69(b,1)),rewrite(59(13)),flip(a)].

given #961 (T,wt=13): 1270 c1 != 1 | x ^ c1 != 0 | c1' = x ^ c1.  [para(81(a,1),69(b,1)),rewrite(81(13)),flip(a)].

given #962 (A,wt=23): 365 (x ^ y) v (y ^ z) != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = y ^ z.  [para(66(a,1),39(b,1,2))].

given #963 (T,wt=13): 1274 c2 v ((x ^ (c1 ^ y)) v z) = c2 v z.  [para(318(a,1),3(a,1,1)),flip(a)].

given #964 (T,wt=13): 1275 c2 v (x v (y ^ (c1 ^ z))) = x v c2.  [para(318(a,1),17(a,1,2)),flip(a)].

given #965 (T,wt=13): 1298 x v y != 1 | 0 != y | y' = y v x.  [para(2(a,1),72(a,1))].

given #966 (T,wt=13): 1333 (x ^ (y v z)) v ((x ^ y)' v u) = 1.  [para(77(a,1),162(a,1,2,1,1))].

given #967 (A,wt=21): 367 x v y != 1 | z ^ (x v y) != 0 | (x v y)' = z ^ (x v y).  [para(67(a,1),37(b,1)),rewrite(105(4))].

given #968 (T,wt=13): 1334 (x ^ (y v z)) v (u ^ (x ^ y))' = 1.  [para(77(a,1),164(a,1,2,1,2))].

given #969 (T,wt=13): 1335 (x ^ (y v z)) v (u v (x ^ y)') = 1.  [para(77(a,1),167(a,1,2,2,1))].

given #970 (T,wt=13): 1336 (c2 ^ (x ^ (c1 v y))) v (x ^ c1)' = 1.  [para(77(a,1),199(a,1,2,1))].

given #971 (T,wt=13): 1337 (x ^ (y ^ c2)) v (c1 ^ (x ^ y))' = 1.  [para(5(a,1),472(a,1,1)),rewrite(4(6))].

given #972 (A,wt=23): 368 (x ^ y) v (z ^ y) != 1 | x ^ (z ^ y) != 0 | (x ^ y)' = z ^ y.  [para(67(a,1),39(b,1,2))].

given #973 (T,wt=13): 1338 (c2 ^ (x ^ y)) v (x ^ (y ^ c1))' = 1.  [para(5(a,1),472(a,1,2,1)),rewrite(4(3))].

given #974 (T,wt=13): 1363 (x v c1) ^ (y v (c2 v x)) = x v c1.  [para(602(a,1),88(a,1,2,2))].

given #975 (T,wt=13): 1375 c2 v x != 1 | c2 != 0 | c2' = c2 v x.  [para(602(a,1),72(a,1)),rewrite(602(13)),flip(b)].

given #976 (T,wt=13): 1377 (x v (y v c1)) ^ (c2 v (x v y))' = 0.  [para(3(a,1),604(a,1,1)),rewrite(2(6))].

given #977 (A,wt=23): 370 x ^ (y v (z ^ (u v (y ^ (u v x))))) = x ^ (y v (z ^ (u v y))).  [para(2(a,1),42(a,2,2,2,2))].

given #978 (T,wt=13): 1378 (c1 v (x v y)) ^ (x v (y v c2))' = 0.  [para(3(a,1),604(a,1,2,1)),rewrite(2(3))].

given #979 (T,wt=13): 1499 ((x v y) ^ z) v ((y ^ z)' v u) = 1.  [para(89(a,1),162(a,1,2,1,1))].

given #980 (T,wt=13): 1500 ((x v y) ^ z) v (u ^ (y ^ z))' = 1.  [para(89(a,1),164(a,1,2,1,2))].

given #981 (T,wt=13): 1501 ((x v y) ^ z) v (u v (y ^ z)') = 1.  [para(89(a,1),167(a,1,2,2,1))].

Low Water (keep, True_semantics): wt=23

given #982 (A,wt=29): 371 x ^ (y v (z ^ (u v (v v (y ^ (u v (v v x))))))) = x ^ (y v (z ^ (y v (u v v)))).  [para(3(a,1),42(a,1,2,2,2,2,2)),rewrite(3(5))].

given #983 (T,wt=13): 1503 (c2 ^ ((x v c1) ^ y)) v (c1 ^ y)' = 1.  [para(89(a,1),199(a,1,2,1))].

given #984 (T,wt=13): 1548 x ^ (y ^ (z v (y ^ x))) = x ^ y.  [para(4(a,1),90(a,1,2,2,2))].

given #985 (T,wt=13): 1552 (x ^ (y v (z ^ x))) v (z ^ x)' = 1.  [para(90(a,1),158(a,1,2,1))].

given #986 (T,wt=13): 1553 c1 ^ (x ^ (y v (c2 ^ x))) = c1 ^ x.  [para(90(a,1),59(a,1,2)),rewrite(59(4)),flip(a)].

given #987 (A,wt=31): 372 x ^ (y v (z v (u ^ (v v ((y v z) ^ (v v x)))))) = x ^ (y v (z v (u ^ (y v (z v v))))).  [para(3(a,1),42(a,1,2)),rewrite(3(11),3(13))].

given #988 (T,wt=13): 1555 x ^ (y ^ (y ^ (z v (x ^ y)))') = 0.  [para(90(a,1),224(a,1,2)),rewrite(4(6),5(6))].

given #989 (T,wt=13): 1575 (c1 v (x v y)) ^ (x v (c2 v y))' = 0.  [para(17(a,1),1358(a,1,2,1)),rewrite(2(3))].

given #990 (T,wt=13): 1577 (c1 v ((c2 ^ x) v y)) ^ (c2 v y)' = 0.  [para(24(a,1),1358(a,1,2,1)),rewrite(2(5))].

given #991 (T,wt=13): 1583 (c1 v (x v (c2 ^ y))) ^ (x v c2)' = 0.  [para(63(a,1),1358(a,1,2,1)),rewrite(2(5))].

given #992 (A,wt=23): 374 x ^ (y v ((z v (y ^ (z v x))) ^ u)) = x ^ (y v (u ^ (y v z))).  [para(4(a,1),42(a,1,2,2))].

given #993 (T,wt=13): 1597 x v y != 1 | 0 != x | x' = y v x.  [para(2(a,1),91(a,1))].

given #994 (T,wt=13): 1612 (x v (c1 v y)) ^ (c2 v (x v y))' = 0.  [para(17(a,1),1376(a,1,1)),rewrite(2(6))].

given #995 (T,wt=13): 1638 (x v y) ^ (z v (y v x)) = x v y.  [para(2(a,1),92(a,1,2)),rewrite(3(3))].

given #996 (T,wt=13): 1716 (x ^ (y v z)) v ((x ^ z)' v u) = 1.  [para(93(a,1),162(a,1,2,1,1))].

given #997 (A,wt=27): 375 x ^ ((y v (z ^ (u v (y ^ (u v x))))) ^ v) = x ^ ((y v (z ^ (y v u))) ^ v).  [para(42(a,1),5(a,1,1)),rewrite(5(5)),flip(a)].

given #998 (T,wt=13): 1717 (x ^ (y v z)) v (u ^ (x ^ z))' = 1.  [para(93(a,1),164(a,1,2,1,2))].

Low Water (keep, True_semantics): wt=21

given #999 (T,wt=13): 1718 (x ^ (y v z)) v (u v (x ^ z)') = 1.  [para(93(a,1),167(a,1,2,2,1))].

given #1000 (T,wt=13): 1719 (c2 ^ (x ^ (y v c1))) v (x ^ c1)' = 1.  [para(93(a,1),199(a,1,2,1))].

given #1001 (T,wt=13): 1771 (x v (y v z)) ^ (y v x) = x v y.  [para(100(a,1),4(a,1)),flip(a)].

given #1002 (A,wt=29): 376 x ^ (y ^ (z v (u ^ (v v (z ^ (v v (x ^ y))))))) = x ^ (y ^ (z v (u ^ (z v v)))).  [para(42(a,1),5(a,1)),rewrite(5(5)),flip(a)].

given #1003 (T,wt=13): 1775 x v (y v (z ^ (y v x))) = x v y.  [para(100(a,1),78(a,1,2,2)),rewrite(3(4))].

given #1004 (T,wt=13): 1776 (c1 v x) ^ (x v (c2 v y)) = x v c1.  [para(112(a,1),100(a,1,2,2))].

given #1005 (T,wt=13): 1777 (c1 v x) ^ (x v (y v c2)) = x v c1.  [para(114(a,1),100(a,1,2,2))].

given #1006 (T,wt=13): 1819 (x v (y v z)) ^ (z v x) = z v x.  [para(101(a,1),4(a,1)),flip(a)].

given #1007 (A,wt=31): 377 x ^ ((y ^ z) v (u ^ ((y ^ z) v v))) = x ^ ((y ^ z) v (u ^ (v v (y ^ (z ^ (v v x)))))).  [para(5(a,1),42(a,1,2,2,2,2)),flip(a)].

given #1008 (T,wt=13): 1868 (x ^ (y ^ z))' v (u v (x ^ y)) = 1.  [para(5(a,1),1825(a,1,1,1))].

given #1009 (T,wt=13): 1870 x v (y v (((x ^ z) v y) ^ u)') = 1.  [para(24(a,1),1825(a,1,2)),rewrite(2(6),3(6))].

given #1010 (T,wt=13): 1881 x v (y v ((x v (y ^ z)) ^ u)') = 1.  [para(63(a,1),1825(a,1,2)),rewrite(2(6),3(6))].

given #1011 (T,wt=13): 1885 (x ^ (y ^ z))' v (u v (x ^ z)) = 1.  [para(19(a,1),1826(a,1,1,1))].

given #1012 (A,wt=27): 378 x ^ (y v (z ^ (u ^ (v v (y ^ (v v x)))))) = x ^ (y v (z ^ (u ^ (y v v)))).  [para(5(a,1),42(a,1,2,2)),rewrite(5(10))].

given #1013 (T,wt=13): 1886 (x ^ y)' v (z v ((x v u) ^ y)) = 1.  [para(22(a,1),1826(a,1,1,1))].

given #1014 (T,wt=13): 1888 x v (y v (z ^ ((x ^ u) v y))') = 1.  [para(24(a,1),1826(a,1,2)),rewrite(2(6),3(6))].

given #1015 (T,wt=13): 1899 x v (y v (z ^ (x v (y ^ u)))') = 1.  [para(63(a,1),1826(a,1,2)),rewrite(2(6),3(6))].

given #1016 (T,wt=13): 1901 (x ^ y)' v (z v (x ^ (y v u))) = 1.  [para(77(a,1),1826(a,1,1,1))].

given #1017 (A,wt=21): 379 x ^ (y ^ (z v (u ^ (z v x)))) = x ^ (y ^ (z v (u ^ x))).  [para(7(a,1),42(a,1,2,2,2,2,2)),rewrite(26(3),5(4),5(9)),flip(a)].

given #1018 (T,wt=13): 1903 (x ^ y)' v (z v ((u v x) ^ y)) = 1.  [para(89(a,1),1826(a,1,1,1))].

given #1019 (T,wt=13): 1905 (x ^ y)' v (z v (x ^ (u v y))) = 1.  [para(93(a,1),1826(a,1,1,1))].

given #1020 (T,wt=13): 2002 ((x ^ y) v z) ^ (u v (y v z))' = 0.  [para(104(a,1),141(a,1,2,1,2))].

given #1021 (T,wt=13): 2003 ((x ^ y) v z) ^ ((y v z)' ^ u) = 0.  [para(104(a,1),142(a,1,2,1,1))].

given #1022 (A,wt=39): 380 x v (y v (z ^ (u v (y ^ (u v x))))) != 1 | x ^ (y v (z ^ (y v u))) != 0 | x' = y v (z ^ (u v (y ^ (u v x)))).  [para(42(a,1),10(b,1))].

Low Water (keep, True_semantics): wt=20

given #1023 (T,wt=13): 2005 ((x ^ y) v z) ^ (u ^ (y v z)') = 0.  [para(104(a,1),146(a,1,2,2,1))].

given #1024 (T,wt=13): 2016 (c1 v ((x ^ c2) v y)) ^ (c2 v y)' = 0.  [para(104(a,1),1358(a,1,2,1)),rewrite(2(5))].

given #1025 (T,wt=13): 2022 x v (y v (((z ^ x) v y) ^ u)') = 1.  [para(104(a,1),1825(a,1,2)),rewrite(2(6),3(6))].

given #1026 (T,wt=13): 2023 x v (y v (z ^ ((u ^ x) v y))') = 1.  [para(104(a,1),1826(a,1,2)),rewrite(2(6),3(6))].

given #1027 (A,wt=29): 381 (x v y) ^ (z v (u ^ (v v (z ^ (x v (v v y)))))) = (x v y) ^ (z v (u ^ (z v v))).  [para(17(a,1),42(a,1,2,2,2,2,2))].

given #1028 (T,wt=13): 2039 (x v (y ^ (z v x))) ^ (z v x)' = 0.  [para(105(a,1),132(a,1,2,1))].

given #1029 (T,wt=13): 2043 x v (y v (y v (z ^ (x v y)))') = 1.  [para(105(a,1),223(a,1,2)),rewrite(2(6),3(6))].

given #1030 (T,wt=13): 2092 (x v (y ^ z)) ^ (u v (x v z))' = 0.  [para(109(a,1),141(a,1,2,1,2))].

given #1031 (T,wt=13): 2093 (x v (y ^ z)) ^ ((x v z)' ^ u) = 0.  [para(109(a,1),142(a,1,2,1,1))].

given #1032 (A,wt=29): 382 x ^ (y v (z ^ (u v (v v (y ^ (u v (v v x))))))) = x ^ (y v (z ^ (u v (y v v)))).  [para(17(a,1),42(a,2,2,2,2)),rewrite(3(3),3(5))].

given #1033 (T,wt=13): 2095 (x v (y ^ z)) ^ (u ^ (x v z)') = 0.  [para(109(a,1),146(a,1,2,2,1))].

Low Water (displace, True_semantics): id=11683, wt=56

Low Water (displace, True_semantics): id=11870, wt=55

Low Water (displace, True_semantics): id=12022, wt=53

given #1034 (T,wt=13): 2104 (c1 v (x v (y ^ c2))) ^ (x v c2)' = 0.  [para(109(a,1),1358(a,1,2,1)),rewrite(2(5))].

given #1035 (T,wt=13): 2110 x v (y v ((x v (z ^ y)) ^ u)') = 1.  [para(109(a,1),1825(a,1,2)),rewrite(2(6),3(6))].

Low Water (displace, True_semantics): id=12070, wt=51

Low Water (displace, True_semantics): id=12021, wt=49

Low Water (displace, True_semantics): id=12655, wt=48

Low Water (displace, True_semantics): id=12168, wt=47

Low Water (displace, True_semantics): id=12641, wt=45

Low Water (displace, True_semantics): id=12776, wt=44

given #1036 (T,wt=13): 2111 x v (y v (z ^ (x v (u ^ y)))') = 1.  [para(109(a,1),1826(a,1,2)),rewrite(2(6),3(6))].

Low Water (displace, True_semantics): id=12848, wt=43

Low Water (displace, True_semantics): id=12943, wt=41

Low Water (displace, True_semantics): id=13423, wt=40

given #1037 (A,wt=23): 383 (x v (y ^ (x v z))) ^ (x v (y ^ (z v x))) = x v (y ^ (x v z)).  [para(42(a,2),28(a,1)),rewrite(62(8))].

given #1038 (T,wt=13): 2114 1 != x | x ^ y != 0 | x' = y ^ x.  [para(4(a,1),107(b,1))].

given #1039 (T,wt=13): 2150 (x ^ y) v (z ^ (y ^ x)) = x ^ y.  [para(4(a,1),110(a,1,2)),rewrite(5(3))].

given #1040 (T,wt=13): 2200 x v (c2 v (y ^ (x v c1))) = x v c2.  [para(115(a,1),106(a,1,2,2)),rewrite(3(6))].

Low Water (displace, True_semantics): id=13364, wt=39

Low Water (displace, True_semantics): id=11770, wt=38

Low Water (displace, True_semantics): id=13263, wt=37

Low Water (displace, True_semantics): id=13712, wt=36

given #1041 (T,wt=13): 2216 (x v (y v z)) ^ (z v (x v y))' = 0.  [para(3(a,1),2213(a,1,1))].

given #1042 (A,wt=27): 386 x ^ (y ^ (z v (u ^ (v v (z ^ (v v x)))))) = y ^ (x ^ (z v (u ^ (z v v)))).  [para(42(a,1),19(a,1,2)),flip(a)].

given #1043 (T,wt=13): 2217 (x v (y v z)) ^ (y v (z v x))' = 0.  [para(3(a,1),2213(a,1,2,1))].

given #1044 (T,wt=13): 2219 (x v (y v z)) ^ (x v (z v y))' = 0.  [para(17(a,1),2213(a,1,1)),rewrite(3(4))].

given #1045 (T,wt=13): 2239 x' v y != 1 | x' ^ y != 0 | x = y.  [para(223(a,1),117(a,1,2,1)),rewrite(73(3),208(10),223(11),73(10))].

given #1046 (T,wt=9): 22197 x' != 1 | x' != 0 | x' = x.  [para(28(a,1),2239(b,1)),rewrite(29(3)),flip(c)].

given #1047 (A,wt=25): 388 x ^ (y v ((y v z) ^ (z v (u v (y ^ (z v (u v x))))))) = x ^ (y v z).  [para(21(a,1),42(a,2,2,2)),rewrite(3(4),3(6),70(11))].

given #1048 (T,wt=12): 22201 x' v (x' v y)' != 1 | (x' v y)' = x.  [para(116(a,1),2239(b,1)),flip(c),xx(b)].

Low Water (displace, True_semantics): id=13871, wt=35

given #1049 (T,wt=12): 22202 x' v (y v x')' != 1 | (y v x')' = x.  [para(132(a,1),2239(b,1)),flip(c),xx(b)].

given #1050 (T,wt=12): 22203 x' ^ (x' ^ y)' != 0 | (x' ^ y)' = x.  [para(149(a,1),2239(a,1)),flip(c),xx(a)].

given #1051 (T,wt=12): 22204 x' ^ (y ^ x')' != 0 | (y ^ x')' = x.  [para(158(a,1),2239(a,1)),flip(c),xx(a)].

given #1052 (A,wt=33): 389 x v ((y ^ (z v (x ^ (z v u)))) v (u ^ (x v (y ^ (x v z))))) = x v (y ^ (z v (x ^ (z v u)))).  [para(42(a,1),26(a,1,2)),rewrite(3(10))].

given #1053 (T,wt=12): 22227 x' v (y v x')' != 1 | (x' v y)' = x.  [para(2(a,1),22201(a,1,2,1))].

given #1054 (T,wt=12): 22229 x' v (x' v y)' != 1 | (y v x')' = x.  [para(2(a,1),22202(a,1,2,1))].

given #1055 (T,wt=12): 22230 x' ^ (y ^ x')' != 0 | (x' ^ y)' = x.  [para(4(a,1),22203(a,1,2,1))].

given #1056 (T,wt=12): 22232 x' ^ (x' ^ y)' != 0 | (y ^ x')' = x.  [para(4(a,1),22204(a,1,2,1))].

given #1057 (A,wt=25): 390 x v ((y ^ (x v z)) v (u ^ (x v (y ^ (z v x))))) = x v (y ^ (x v z)).  [para(42(a,2),26(a,1,2)),rewrite(370(9),3(8))].

given #1058 (T,wt=13): 2241 c2 != 1 | c2 ^ x != 0 | c2' = c2 ^ x.  [para(276(a,1),117(a,1,2,1)),rewrite(7(4),276(13))].

given #1059 (T,wt=13): 2272 x ^ (y ^ (((x v z) ^ y) v u)') = 0.  [para(134(a,1),22(a,1,2)),rewrite(97(2)),flip(a)].

given #1060 (T,wt=13): 2282 x ^ (y ^ (((z v x) ^ y) v u)') = 0.  [para(134(a,1),89(a,1,2)),rewrite(97(2)),flip(a)].

Low Water (displace, True_semantics): id=14170, wt=33

given #1061 (T,wt=13): 2287 x ^ (y ^ (z v ((x v u) ^ y))') = 0.  [para(143(a,1),22(a,1,2)),rewrite(97(2)),flip(a)].

Low Water (displace, True_semantics): id=14335, wt=32

given #1062 (A,wt=25): 392 x ^ (y v (z ^ (u v (y ^ (u v (x v v)))))) = x ^ (y v (z ^ (y v u))).  [para(42(a,1),22(a,1,2)),rewrite(22(6)),flip(a)].

given #1063 (T,wt=13): 2297 x ^ (y ^ (z v ((u v x) ^ y))') = 0.  [para(143(a,1),89(a,1,2)),rewrite(97(2)),flip(a)].

given #1064 (T,wt=13): 2303 (x v ((x v y) ^ z)) ^ (x v y)' = 0.  [para(25(a,1),145(a,1,2,1))].

given #1065 (T,wt=13): 2309 (x v (y ^ (z ^ u))) ^ (x v z)' = 0.  [para(78(a,1),145(a,1,2,1,2))].

given #1066 (T,wt=13): 2310 (x v (y ^ (z ^ u))) ^ (x v u)' = 0.  [para(106(a,1),145(a,1,2,1,2))].

Low Water (displace, True_semantics): id=14721, wt=31

given #1067 (A,wt=23): 393 x ^ (y v (z ^ (y' v (u v (y ^ (y' v (u v x))))))) = x ^ (y v z).  [para(84(a,1),42(a,2,2,2,2)),rewrite(3(5),3(7),32(12))].

given #1068 (T,wt=13): 2313 (x v (y ^ (z ^ c1))) ^ (x v c2)' = 0.  [para(305(a,1),145(a,1,2,1,2))].

given #1069 (T,wt=13): 2314 (x v (y ^ (c1 ^ z))) ^ (x v c2)' = 0.  [para(318(a,1),145(a,1,2,1,2))].

given #1070 (T,wt=13): 2315 (x v (y v c1)) ^ (x v (c2 v y))' = 0.  [para(602(a,1),145(a,1,2,1,2))].

given #1071 (T,wt=13): 2319 (x v (y ^ (x v z))) ^ (x v z)' = 0.  [para(105(a,1),145(a,1,2,1))].

given #1072 (A,wt=23): 394 x ^ (y v (z ^ (u v (y' v (y ^ (u v (y' v x))))))) = x ^ (y v z).  [para(96(a,1),42(a,2,2,2,2)),rewrite(3(5),3(7),32(12))].

given #1073 (T,wt=13): 2332 ((x ^ (y ^ z)) v u) ^ (y v u)' = 0.  [para(19(a,1),155(a,1,1,1))].

Low Water (displace, True_semantics): id=13675, wt=30

Low Water (displace, True_semantics): id=15128, wt=29

given #1074 (T,wt=13): 2344 ((x ^ y) v (z ^ (x ^ u))) ^ x' = 0.  [para(78(a,1),155(a,1,2,1))].

given #1075 (T,wt=13): 2345 ((x ^ y) v (z ^ (u ^ x))) ^ x' = 0.  [para(106(a,1),155(a,1,2,1))].

Low Water (displace, True_semantics): id=15400, wt=28

given #1076 (T,wt=13): 2349 ((c2 ^ x) v (y ^ (z ^ c1))) ^ c2' = 0.  [para(305(a,1),155(a,1,2,1))].

given #1077 (A,wt=35): 395 x ^ ((y v (z ^ (u v (y ^ (u v x))))) ^ ((x ^ (y v (z ^ (y v u)))) v v)) = x ^ (y v (z ^ (u v y))).  [para(42(a,1),23(a,1,2,2,1)),rewrite(370(18))].

given #1078 (T,wt=13): 2350 ((c2 ^ x) v (y ^ (c1 ^ z))) ^ c2' = 0.  [para(318(a,1),155(a,1,2,1))].

given #1079 (T,wt=13): 2351 ((c2 ^ x) v (y v c1)) ^ (c2 v y)' = 0.  [para(602(a,1),155(a,1,2,1))].

given #1080 (T,wt=13): 2353 (x v (y v z)) ^ (y v (x v z))' = 0.  [para(100(a,1),155(a,1,1,1)),rewrite(3(2),3(4))].

given #1081 (T,wt=13): 2354 ((x ^ y) v z) ^ (x v (z v u))' = 0.  [para(155(a,1),102(a,1,2)),rewrite(4(4),86(4)),flip(a)].

given #1082 (A,wt=31): 396 x ^ ((y v (z ^ (y v u))) ^ ((x ^ (y v (z ^ (u v y)))) v v)) = x ^ (y v (z ^ (y v u))).  [para(42(a,2),23(a,1,2,2,1)),rewrite(370(9))].

given #1083 (T,wt=13): 2363 ((x v (y v z)) ^ u) v (y ^ u)' = 1.  [para(118(a,1),158(a,1,2,1))].

given #1084 (T,wt=13): 2364 x ^ (y ^ ((z v (x v u)) ^ y)') = 0.  [para(34(a,1),118(a,1,2)),rewrite(97(2)),flip(a)].

given #1085 (T,wt=13): 2371 x ^ (y ^ (y ^ (z v (x v u)))') = 0.  [para(188(a,1),118(a,1,2)),rewrite(97(2)),flip(a)].

given #1086 (T,wt=13): 2373 x ^ (c1 ^ (c2 ^ (y v (x v z)))') = 0.  [para(473(a,1),118(a,1,2)),rewrite(97(2),4(6)),flip(a)].

given #1087 (A,wt=35): 397 x ^ ((y v (z ^ (u v (y ^ (u v x))))) ^ ((x ^ (y v (z ^ (u v y)))) v v)) = x ^ (y v (z ^ (y v u))).  [para(42(a,1),23(a,2)),rewrite(370(11))].

given #1088 (T,wt=13): 2414 (x ^ (y v z)) v (x ^ (z v y))' = 1.  [para(100(a,1),159(a,1,2,1,2))].

given #1089 (T,wt=13): 2418 (x ^ (y ^ z)) v (z ^ (x ^ y))' = 1.  [para(5(a,1),2405(a,1,1))].

given #1090 (T,wt=13): 2419 (x ^ (y ^ z)) v (y ^ (z ^ x))' = 1.  [para(5(a,1),2405(a,1,2,1))].

given #1091 (T,wt=13): 2421 (x ^ (y ^ z)) v (x ^ (z ^ y))' = 1.  [para(19(a,1),2405(a,1,1)),rewrite(5(4))].

given #1092 (A,wt=31): 398 ((x ^ y) v z) ^ (u v (v ^ (u v x))) = ((x ^ y) v z) ^ (u v (v ^ (x v (u ^ (x v z))))).  [para(24(a,1),42(a,1,2,2,2,2,2)),flip(a)].

given #1093 (T,wt=13): 2454 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x).  [para(13(a,1),119(a,1,1)),rewrite(4(5),4(10))].

given #1094 (T,wt=11): 22748 x ^ (c1 v (c2 ^ x)) = c2 ^ x.  [para(2454(a,1),58(a,1,2)),rewrite(93(5)),flip(a)].

given #1095 (T,wt=11): 22786 x v (c2 ^ (c1 v x)) = x v c1.  [para(2454(a,1),1775(a,1,2))].

given #1096 (T,wt=11): 22804 x ^ (c1 v (x ^ c2)) = c2 ^ x.  [para(4(a,1),22748(a,1,2,2))].

Low Water (displace, True_semantics): id=16048, wt=27

given #1097 (A,wt=31): 399 x ^ (y v (z ^ ((y ^ u) v (v v (y ^ ((y ^ u) v (v v x))))))) = x ^ (y v (z ^ (y v v))).  [para(24(a,1),42(a,2,2,2,2)),rewrite(3(5),3(7))].

given #1098 (T,wt=11): 22840 x v (c2 ^ (x v c1)) = x v c1.  [para(2(a,1),22786(a,1,2,2))].

given #1099 (T,wt=13): 2537 (x ^ ((x ^ y) v z)) v (x ^ y)' = 1.  [para(23(a,1),168(a,1,2,1))].

given #1100 (T,wt=13): 2538 (x ^ (c2 ^ y)) v (x ^ (c1 ^ y))' = 1.  [para(59(a,1),168(a,1,2,1,2))].

given #1101 (T,wt=13): 2543 (x ^ (y v (z v u))) v (x ^ z)' = 1.  [para(62(a,1),168(a,1,2,1,2))].

given #1102 (A,wt=23): 400 x v ((y ^ (z v (x ^ (z v u)))) v (u ^ (x v (y ^ (x v z))))') = 1.  [para(42(a,1),158(a,1,2,1)),rewrite(3(11))].

given #1103 (T,wt=13): 2545 (x ^ (y ^ c2)) v (x ^ (y ^ c1))' = 1.  [para(81(a,1),168(a,1,2,1,2))].

given #1104 (T,wt=13): 2546 (x ^ (y v (z v u))) v (x ^ u)' = 1.  [para(88(a,1),168(a,1,2,1,2))].

Low Water (displace, True_semantics): id=16681, wt=26

Low Water (displace, True_semantics): id=16735, wt=25

given #1105 (T,wt=13): 2557 (x ^ (y v (c2 v z))) v (x ^ c1)' = 1.  [para(202(a,1),168(a,1,2,1,2))].

given #1106 (T,wt=13): 2560 (x ^ (y v (z v c2))) v (x ^ c1)' = 1.  [para(225(a,1),168(a,1,2,1,2))].

given #1107 (A,wt=19): 401 x v ((y ^ (x v z)) v (u ^ (x v (y ^ (z v x))))') = 1.  [para(42(a,2),158(a,1,2,1)),rewrite(370(9),3(9))].

given #1108 (T,wt=13): 2565 (x ^ (y v (x ^ z))) v (x ^ z)' = 1.  [para(90(a,1),168(a,1,2,1))].

given #1109 (T,wt=13): 2571 (x ^ (y v c2)) v (x ^ (y v c1))' = 1.  [para(115(a,1),168(a,1,2,1,2))].

given #1110 (T,wt=13): 2591 ((x v y) ^ (z v (x v u))) v x' = 1.  [para(62(a,1),169(a,1,2,1))].

given #1111 (T,wt=13): 2593 ((c1 v x) ^ (y ^ c2)) v (y ^ c1)' = 1.  [para(81(a,1),169(a,1,2,1))].

given #1112 (A,wt=35): 402 (x v ((y v x) ^ z)) ^ (u v (v ^ (u v y))) = (x v ((y v x) ^ z)) ^ (u v (v ^ (y v (u ^ (y v x))))).  [para(25(a,1),42(a,1,2,2,2,2,2)),flip(a)].

given #1113 (T,wt=13): 2594 ((x v y) ^ (z v (u v x))) v x' = 1.  [para(88(a,1),169(a,1,2,1))].

given #1114 (T,wt=13): 2607 ((c1 v x) ^ (y v (c2 v z))) v c1' = 1.  [para(202(a,1),169(a,1,2,1))].

given #1115 (T,wt=13): 2610 ((c1 v x) ^ (y v (z v c2))) v c1' = 1.  [para(225(a,1),169(a,1,2,1))].

given #1116 (T,wt=13): 2617 (x ^ y)' v (((x v z) ^ y) v u) = 1.  [para(169(a,1),100(a,1,1)),rewrite(73(8),2574(11))].

Low Water (displace, True_semantics): id=17476, wt=24

given #1117 (A,wt=35): 403 x ^ (y v (z ^ (u v (((y v u) ^ v) v (y ^ (u v (((y v u) ^ v) v x))))))) = x ^ (y v (z ^ (y v u))).  [para(25(a,1),42(a,2,2,2,2)),rewrite(3(7),3(9))].

given #1118 (T,wt=13): 2629 x v (y v ((z ^ (x ^ u)) v y)') = 1.  [para(19(a,1),187(a,1,2,2,1,1))].

given #1119 (T,wt=13): 2666 x ^ ((x v y) ^ (z v (x v u)))' = 0.  [para(190(a,1),118(a,1)),flip(a)].

given #1120 (T,wt=13): 2680 c1 v (c2 ^ (x v c1)) = c2 ^ (x v c1).  [para(20(a,1),194(a,1,1))].

given #1121 (T,wt=13): 2705 (x v (c1 ^ y)) ^ (x v (c2 ^ y))' = 0.  [para(194(a,1),133(a,1,2,1,2))].

Low Water (keep, True_semantics): wt=19

given #1122 (A,wt=23): 404 x ^ (c2 v (y ^ (c1' v (z v (c2 ^ (c1' v (z v x))))))) = x ^ (c2 v y).  [para(171(a,1),42(a,2,2,2,2)),rewrite(3(9),3(11),32(17))].

given #1123 (T,wt=13): 2720 ((c2 v x) ^ y) v ((c1 ^ y)' v z) = 1.  [para(195(a,1),162(a,1,2,1,1))].

given #1124 (T,wt=13): 2721 ((c2 v x) ^ y) v (z ^ (c1 ^ y))' = 1.  [para(195(a,1),164(a,1,2,1,2))].

given #1125 (T,wt=13): 2722 ((c2 v x) ^ y) v (z v (c1 ^ y)') = 1.  [para(195(a,1),167(a,1,2,2,1))].

given #1126 (T,wt=13): 2728 (c1 ^ x)' v (y v ((c2 v z) ^ x)) = 1.  [para(195(a,1),1826(a,1,1,1))].

given #1127 (A,wt=23): 405 x ^ (c2 v (y ^ (z v (c1' v (c2 ^ (z v (c1' v x))))))) = x ^ (c2 v y).  [para(173(a,1),42(a,2,2,2,2)),rewrite(3(9),3(11),32(17))].

given #1128 (T,wt=13): 2734 c1 ^ (x ^ (((c2 v y) ^ x) v z)') = 0.  [para(134(a,1),195(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #1129 (T,wt=13): 2735 c1 ^ (x ^ (y v ((c2 v z) ^ x))') = 0.  [para(143(a,1),195(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #1130 (T,wt=13): 2745 (x ^ (c2 v y)) v ((x ^ c1)' v z) = 1.  [para(203(a,1),162(a,1,2,1,1))].

given #1131 (T,wt=13): 2746 (x ^ (c2 v y)) v (z ^ (x ^ c1))' = 1.  [para(203(a,1),164(a,1,2,1,2))].

given #1132 (A,wt=35): 406 (x ^ (y v (z ^ (y v u)))) v (x ^ ((y v (z ^ (u v (y ^ (u v x))))) ^ v)) = x ^ (y v (z ^ (u v y))).  [para(42(a,1),27(a,1,1)),rewrite(370(18))].

given #1133 (T,wt=13): 2747 (x ^ (c2 v y)) v (z v (x ^ c1)') = 1.  [para(203(a,1),167(a,1,2,2,1))].

given #1134 (T,wt=13): 2749 (x ^ c1)' v (y v (x ^ (c2 v z))) = 1.  [para(203(a,1),1826(a,1,1,1))].

given #1135 (T,wt=13): 2765 ((x v c2) ^ y) v ((c1 ^ y)' v z) = 1.  [para(226(a,1),162(a,1,2,1,1))].

given #1136 (T,wt=13): 2766 ((x v c2) ^ y) v (z ^ (c1 ^ y))' = 1.  [para(226(a,1),164(a,1,2,1,2))].

given #1137 (A,wt=31): 407 (x ^ (y v (z ^ (u v y)))) v (x ^ ((y v (z ^ (y v u))) ^ v)) = x ^ (y v (z ^ (y v u))).  [para(42(a,2),27(a,1,1)),rewrite(370(6))].

given #1138 (T,wt=13): 2767 ((x v c2) ^ y) v (z v (c1 ^ y)') = 1.  [para(226(a,1),167(a,1,2,2,1))].

given #1139 (T,wt=13): 2772 (c1 ^ x)' v (y v ((z v c2) ^ x)) = 1.  [para(226(a,1),1826(a,1,1,1))].

given #1140 (T,wt=13): 2778 c1 ^ (x ^ (((y v c2) ^ x) v z)') = 0.  [para(134(a,1),226(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #1141 (T,wt=13): 2779 c1 ^ (x ^ (y v ((z v c2) ^ x))') = 0.  [para(143(a,1),226(a,1,2)),rewrite(4(3),86(3)),flip(a)].

given #1142 (A,wt=35): 408 (x ^ (y v (z ^ (u v y)))) v (x ^ ((y v (z ^ (u v (y ^ (u v x))))) ^ v)) = x ^ (y v (z ^ (y v u))).  [para(42(a,1),27(a,2)),rewrite(370(6))].

given #1143 (T,wt=13): 2784 c1 ^ (x ^ ((y v (c2 v z)) ^ x)') = 0.  [para(190(a,1),226(a,1,2)),rewrite(4(3),86(3),3(5)),flip(a)].

given #1144 (T,wt=13): 2795 (x ^ (y v c2)) v ((x ^ c1)' v z) = 1.  [para(228(a,1),162(a,1,2,1,1))].

given #1145 (T,wt=13): 2796 (x ^ (y v c2)) v (z ^ (x ^ c1))' = 1.  [para(228(a,1),164(a,1,2,1,2))].

given #1146 (T,wt=13): 2797 (x ^ (y v c2)) v (z v (x ^ c1)') = 1.  [para(228(a,1),167(a,1,2,2,1))].

given #1147 (A,wt=31): 409 x ^ ((y ^ z) v (u ^ ((y ^ (z ^ v)) v (y ^ (z ^ ((y ^ (z ^ v)) v x)))))) = x ^ (y ^ z).  [para(27(a,1),42(a,2,2,2,2)),rewrite(5(8),26(16))].

given #1148 (T,wt=13): 2799 (x ^ c1)' v (y v (x ^ (z v c2))) = 1.  [para(228(a,1),1826(a,1,1,1))].

given #1149 (T,wt=13): 2820 ((x ^ c1) v y) ^ (z v (c2 v y))' = 0.  [para(278(a,1),141(a,1,2,1,2))].

given #1150 (T,wt=13): 2821 ((x ^ c1) v y) ^ ((c2 v y)' ^ z) = 0.  [para(278(a,1),142(a,1,2,1,1))].

given #1151 (T,wt=13): 2823 ((x ^ c1) v y) ^ (z ^ (c2 v y)') = 0.  [para(278(a,1),146(a,1,2,2,1))].

given #1152 (A,wt=27): 410 x ^ (y v (z ^ (u v ((y v u)' v (y ^ (u v ((y v u)' v x))))))) = x ^ (y v z).  [para(31(a,1),42(a,2,2,2,2)),rewrite(3(7),3(9),32(14))].

given #1153 (T,wt=13): 2834 c2 v (x v (((y ^ c1) v x) ^ z)') = 1.  [para(278(a,1),1825(a,1,2)),rewrite(2(8),3(8))].

given #1154 (T,wt=13): 2835 c2 v (x v (y ^ ((z ^ c1) v x))') = 1.  [para(278(a,1),1826(a,1,2)),rewrite(2(8),3(8))].

given #1155 (T,wt=13): 2840 c2 v (x v ((y ^ (c1 ^ z)) v x)') = 1.  [para(187(a,1),278(a,1,2)),rewrite(2(3),83(3),5(5)),flip(a)].

given #1156 (T,wt=13): 2851 x ^ (c1 ^ (y v (c2 ^ x))) = x ^ c1.  [para(281(a,1),88(a,1,2,2)),rewrite(5(6))].

given #1157 (A,wt=25): 411 x ^ ((y v (z ^ (u v (y ^ (u v x))))) ^ (x ^ (y v (z ^ (y v u))))') = 0.  [para(42(a,1),34(a,1,2,2,1))].

given #1158 (T,wt=13): 2868 (x v (y ^ c1)) ^ (x v (c2 ^ y))' = 0.  [para(281(a,1),145(a,1,2,1,2))].

given #1159 (T,wt=13): 2882 (x v (y ^ c1)) ^ (z v (x v c2))' = 0.  [para(306(a,1),141(a,1,2,1,2))].

given #1160 (T,wt=13): 2883 (x v (y ^ c1)) ^ ((x v c2)' ^ z) = 0.  [para(306(a,1),142(a,1,2,1,1))].

given #1161 (T,wt=13): 2884 (x v (y ^ c1)) ^ (z ^ (x v c2)') = 0.  [para(306(a,1),146(a,1,2,2,1))].

given #1162 (A,wt=21): 412 x ^ ((y v (z ^ (y v u))) ^ (x ^ (y v (z ^ (u v y))))') = 0.  [para(42(a,2),34(a,1,2,2,1)),rewrite(370(9))].

given #1163 (T,wt=13): 2889 x v c2 != 1 | c2 != 0 | c2' = x v c2.  [para(306(a,1),72(a,1)),rewrite(306(14)),flip(b)].

given #1164 (T,wt=13): 2895 x v (c2 v ((x v (y ^ c1)) ^ z)') = 1.  [para(306(a,1),1825(a,1,2)),rewrite(2(8),3(8))].

given #1165 (T,wt=13): 2896 x v (c2 v (y ^ (x v (z ^ c1)))') = 1.  [para(306(a,1),1826(a,1,2)),rewrite(2(8),3(8))].

given #1166 (T,wt=13): 2912 ((c1 ^ x) v y) ^ (z v (c2 v y))' = 0.  [para(315(a,1),141(a,1,2,1,2))].

given #1167 (A,wt=31): 414 x v ((y ^ (x v z)) v u) != 1 | u ^ (x v (y ^ (z v x))) != 0 | u' = x v (y ^ (x v z)).  [para(42(a,2),36(b,1)),rewrite(3(4),370(12))].

given #1168 (T,wt=13): 2913 ((c1 ^ x) v y) ^ ((c2 v y)' ^ z) = 0.  [para(315(a,1),142(a,1,2,1,1))].

given #1169 (T,wt=13): 2915 ((c1 ^ x) v y) ^ (z ^ (c2 v y)') = 0.  [para(315(a,1),146(a,1,2,2,1))].

given #1170 (T,wt=13): 2926 c2 v (x v (((c1 ^ y) v x) ^ z)') = 1.  [para(315(a,1),1825(a,1,2)),rewrite(2(8),3(8))].

given #1171 (T,wt=13): 2927 c2 v (x v (y ^ ((c1 ^ z) v x))') = 1.  [para(315(a,1),1826(a,1,2)),rewrite(2(8),3(8))].

given #1172 (A,wt=23): 415 x ^ (y' v (z ^ (u v (y v (y' ^ (u v (y v x))))))) = x ^ (y' v z).  [para(223(a,1),42(a,2,2,2,2)),rewrite(3(5),3(7),32(13))].

given #1173 (T,wt=13): 2942 (x v (c1 ^ y)) ^ (z v (x v c2))' = 0.  [para(317(a,1),141(a,1,2,1,2))].

given #1174 (T,wt=13): 2943 (x v (c1 ^ y)) ^ ((x v c2)' ^ z) = 0.  [para(317(a,1),142(a,1,2,1,1))].

given #1175 (T,wt=13): 2945 (x v (c1 ^ y)) ^ (z ^ (x v c2)') = 0.  [para(317(a,1),146(a,1,2,2,1))].

given #1176 (T,wt=13): 2955 x v (c2 v ((x v (c1 ^ y)) ^ z)') = 1.  [para(317(a,1),1825(a,1,2)),rewrite(2(8),3(8))].

given #1177 (A,wt=23): 416 x ^ ((y v (z ^ (y v u))) ^ (y v (z ^ (u v (y ^ (u v x)))))') = 0.  [para(42(a,1),224(a,1,2)),rewrite(4(11),5(11))].

given #1178 (T,wt=13): 2956 x v (c2 v (y ^ (x v (c1 ^ z)))') = 1.  [para(317(a,1),1826(a,1,2)),rewrite(2(8),3(8))].

given #1179 (T,wt=13): 2965 (x ^ (y ^ z)) v (y ^ x) = x ^ y.  [para(366(a,1),24(a,2)),rewrite(5(3),2960(6))].

given #1180 (T,wt=13): 2982 (x v (y ^ z)) ^ (x v (z ^ y))' = 0.  [para(366(a,1),145(a,1,2,1,2))].

given #1181 (T,wt=13): 2998 x ^ (c1 ^ (y v (x ^ c2))) = x ^ c1.  [para(471(a,1),62(a,1,2,2)),rewrite(5(6))].

given #1182 (A,wt=19): 417 (x v (y ^ (x v z)))' ^ (u ^ (x v (y ^ (z v x)))) = 0.  [para(42(a,2),224(a,1,2)),rewrite(370(10))].

given #1183 (T,wt=13): 3008 (x v (y ^ c1)) ^ (x v (y ^ c2))' = 0.  [para(471(a,1),133(a,1,2,1,2))].

given #1184 (T,wt=13): 3018 x v (c2 v (y ^ (c1 v x))) = x v c2.  [para(614(a,1),106(a,1,2,2)),rewrite(3(6))].

given #1185 (T,wt=13): 3026 (c1 v x) ^ (c2 v (x v y)) = c1 v x.  [para(614(a,1),102(a,1,2)),rewrite(21(6),2(7)),flip(a)].

given #1186 (T,wt=13): 3028 c1 v x != 1 | c1 != 0 | c1' = c1 v x.  [para(614(a,1),117(a,1,2)),rewrite(70(4),193(8),614(14))].

given #1187 (A,wt=39): 418 x v (y v (z ^ (u v (y ^ (u v x))))) != 1 | x ^ (y v (z ^ (y v u))) != 0 | (y v (z ^ (u v (y ^ (u v x)))))' = x.  [para(42(a,1),38(b,1)),rewrite(2(6))].

given #1188 (T,wt=13): 3031 (x ^ (y v c2)) v (x ^ (c1 v y))' = 1.  [para(614(a,1),168(a,1,2,1,2))].

given #1189 (T,wt=13): 3044 (x ^ ((x ^ y) v z)) v (y ^ x)' = 1.  [para(127(a,1),158(a,1,2,1))].

given #1190 (T,wt=13): 3045 c1 ^ (x ^ ((x ^ c2) v y)) = c1 ^ x.  [para(127(a,1),59(a,1,2)),rewrite(59(4)),flip(a)].

given #1191 (T,wt=13): 3047 x ^ (y ^ (y ^ ((y ^ x) v z))') = 0.  [para(127(a,1),224(a,1,2)),rewrite(4(6),5(6))].

given #1192 (A,wt=31): 419 x v ((y ^ (x v z)) v u) != 1 | u ^ (x v (y ^ (z v x))) != 0 | (x v (y ^ (x v z)))' = u.  [para(42(a,2),38(b,1)),rewrite(3(4),370(12))].

given #1193 (T,wt=13): 3069 (x v y)' ^ (((x ^ z) v y) ^ u) = 0.  [para(155(a,1),127(a,1,2,2,1)),rewrite(75(6),2326(11))].

given #1194 (T,wt=13): 3073 (x ^ ((y ^ x) v z)) v (x ^ y)' = 1.  [para(127(a,1),168(a,1,2,1))].

given #1195 (T,wt=13): 3088 (x v c1) ^ ((y v (c2 v x))' ^ z) = 0.  [para(602(a,1),717(a,1,2,1,1,2))].

given #1196 (T,wt=13): 3104 (x v c1) ^ (y ^ (z v (c2 v x))') = 0.  [para(602(a,1),720(a,1,2,2,1,2))].

given #1197 (A,wt=21): 421 c1 ^ (x ^ (y v (z ^ (y v c2)))) = c1 ^ (x ^ (y v (z ^ c2))).  [para(304(a,1),42(a,1,2,2,2,2,2)),rewrite(26(6),5(6),5(13)),flip(a)].

given #1198 (T,wt=13): 3206 (c2 ^ x) v ((y ^ (c1 ^ x))' v z) = 1.  [para(59(a,1),894(a,1,2,1,1,2))].

given #1199 (T,wt=13): 3209 (x ^ c2) v ((y ^ (x ^ c1))' v z) = 1.  [para(81(a,1),894(a,1,2,1,1,2))].

given #1200 (T,wt=13):