============================== Prover9 ===============================
Prover9 (32) version November-2006, November 2006.
Process 4111 was started by mccune on cleo.thornwood,
Wed Nov 22 11:31:27 2006
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 (F,wt=5): 28 x ^ x = x.  [para(7(a,1),6(a,1,2))].

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

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

given #16 (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 #17 (F,wt=5): 35 x v 0 = x.  [para(9(a,1),7(a,1,2))].

given #18 (F,wt=5): 69 1 ^ x = x.  [para(32(a,1),4(a,1)),flip(a)].

given #19 (T,wt=3): 77 1' = 0.  [hyper(10,a,35,a,b,69,a)].

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

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

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

given #23 (F,wt=5): 78 1 v x = 1.  [para(69(a,1),6(a,1))].

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

given #25 (T,wt=5): 88 x v 1 = 1.  [para(78(a,1),2(a,1)),flip(a)].

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

given #27 (F,wt=5): 91 x ^ 0 = 0.  [para(81(a,1),4(a,1)),flip(a)].

given #28 (F,wt=6): 90 0 != x | x' = 1.  [back_rewrite(70),rewrite(88(2)),xx(a)].

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

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

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

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

given #33 (F,wt=7): 79 x v (x' v y) = 1.  [back_rewrite(30),rewrite(78(5))].

given #34 (T,wt=7): 82 x ^ (x' ^ y) = 0.  [back_rewrite(33),rewrite(81(5))].

given #35 (T,wt=7): 89 x v (y v x') = 1.  [back_rewrite(73),rewrite(88(5))].

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

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

given #38 (F,wt=7): 92 x ^ (y ^ x') = 0.  [back_rewrite(85),rewrite(91(5))].

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

given #40 (T,wt=5): 132 c1 ^ c2' = 0.  [para(104(a,1),120(a,1,2,1))].

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

given #42 (F,wt=7): 127 x ^ (y v x)' = 0.  [para(2(a,1),120(a,1,2,1))].

given #43 (F,wt=7): 133 c1 ^ (c2' ^ x) = 0.  [para(132(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

given #44 (T,wt=7): 135 c1 ^ (x ^ c2') = 0.  [para(132(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

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

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

given #47 (F,wt=7): 150 x v (x ^ y)' = 1.  [para(8(a,1),24(a,1,2)),rewrite(88(2)),flip(a)].

given #48 (F,wt=7): 158 x v (y ^ x)' = 1.  [para(4(a,1),150(a,1,2,1))].

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

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

given #51 (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 #52 (F,wt=7): 173 c2 v (x v c1') = 1.  [para(166(a,1),17(a,1,2)),rewrite(88(2)),flip(a)].

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

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

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

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

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

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

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

given #60 (T,wt=7): 196 c1 ^ (c2 v x)' = 0.  [para(120(a,1),59(a,1,2)),rewrite(4(3),81(3)),flip(a)].

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

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

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

given #64 (T,wt=7): 231 x' v (y v x) = 1.  [para(216(a,1),89(a,1,2,2))].

given #65 (T,wt=7): 232 x' ^ (y ^ x) = 0.  [para(216(a,1),92(a,1,2,2))].

given #66 (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 #67 (F,wt=8): 226 c2 ^ c1' != 0 | c2 = c1.  [para(166(a,1),36(a,1)),rewrite(4(7),216(12)),flip(c),xx(a)].

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

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

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

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

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

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

given #74 (T,wt=8): 302 c1 v c2' != 1 | c2 = c1.  [para(132(a,1),38(b,1)),rewrite(2(4),216(12)),xx(b)].

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

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

given #77 (F,wt=9): 63 x ^ (y ^ x) = y ^ x.  [para(28(a,1),5(a,2,2)),rewrite(4(2))].

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

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

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

given #81 (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 #82 (F,wt=9): 71 x ^ (y v (x v z)) = x.  [para(17(a,1),6(a,1,2))].

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

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

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

given #86 (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 #87 (F,wt=9): 102 x v (y ^ (z ^ x)) = x.  [para(5(a,1),26(a,1,2))].

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

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

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

given #91 (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 #92 (F,wt=9): 114 c1 v (x v c2) = x v c2.  [para(104(a,1),17(a,1,2)),flip(a)].

given #93 (F,wt=9): 124 x ^ ((x v y)' ^ z) = 0.  [para(82(a,1),22(a,1,2)),rewrite(91(2)),flip(a)].

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

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

given #96 (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 #97 (F,wt=9): 141 x ^ (y v (z v x))' = 0.  [para(3(a,1),127(a,1,2,1))].

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

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

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

given #101 (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 #102 (F,wt=9): 155 x v (y v (x ^ z)') = 1.  [para(89(a,1),24(a,1,2)),rewrite(88(2)),flip(a)].

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

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

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

given #106 (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 #107 (F,wt=9): 167 x v (y v (z ^ x)') = 1.  [para(158(a,1),17(a,1,2)),rewrite(88(2)),flip(a)].

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

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

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

given #111 (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 #112 (F,wt=9): 200 c1 ^ (x ^ (c2 ^ x)') = 0.  [para(34(a,1),59(a,1,2)),rewrite(4(3),81(3)),flip(a)].

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

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

given #115 (T,wt=9): 208 c1 ^ ((c2 v x)' ^ y) = 0.  [para(196(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

given #116 (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 #117 (F,wt=9): 210 c1 ^ (x v (c2 v y))' = 0.  [para(17(a,1),196(a,1,2,1))].

given #118 (F,wt=9): 211 c1 ^ (x ^ (c2 v y)') = 0.  [para(196(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

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

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

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

given #122 (F,wt=6): 1149 c1 != 1 | c1' = 0.  [para(132(a,1),65(b,1)),rewrite(132(12)),flip(a),xx(b)].

given #123 (F,wt=6): 1151 x' != 1 | 0 = x.  [para(232(a,1),65(b,1)),rewrite(216(8),232(9)),flip(a),flip(c),xx(b)].

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

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

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

given #127 (F,wt=7): 1155 (c1 ^ (c1' v c2'))' != 1.  [ur(1151,b,116,a(flip))].

given #128 (F,wt=6): 1166 c2 != 0 | c2' = 1.  [para(166(a,1),68(a,1)),rewrite(166(12)),flip(b),xx(a)].

given #129 (T,wt=6): 1167 x' != 0 | 1 = x.  [para(231(a,1),68(a,1)),rewrite(216(8),231(9)),flip(b),flip(c),xx(a)].

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

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

given #132 (F,wt=9): 287 c2 v ((x ^ c1)' v y) = 1.  [para(279(a,1),3(a,1,1)),rewrite(78(2)),flip(a)].

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

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

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

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

given #137 (F,wt=9): 321 c2 v ((c1 ^ x)' v y) = 1.  [para(288(a,1),3(a,1,1)),rewrite(78(2)),flip(a)].

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

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

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

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

given #142 (F,wt=9): 441 x ^ (c1 ^ (x ^ c2)') = 0.  [para(87(a,1),232(a,1,2)),rewrite(4(6),5(6))].

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

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

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

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

given #147 (F,wt=9): 955 c1 ^ (x ^ (x ^ c2)') = 0.  [para(185(a,1),59(a,1,2)),rewrite(4(3),81(3)),flip(a)].

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

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

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

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

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

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

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

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

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

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

given #158 (F,wt=9): 1359 (x v c1) ^ (c2 v x)' = 0.  [para(495(a,1),127(a,1,2,1))].

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

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

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

given #162 (F,wt=6): 1611 c1' != 0 | c1 = 1.  [para(166(a,1),97(a,1)),rewrite(216(10),166(12)),flip(b),xx(a)].

given #163 (F,wt=9): 1385 x v (c2 v (c1 v x)') = 1.  [para(2(a,1),498(a,1,2,2,1))].

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

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

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

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

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

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

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

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

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

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

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

given #175 (T,wt=6): 1770 c2' != 1 | c2 = 0.  [para(1698(a,1),65(b,1)),rewrite(216(10),1698(15)),flip(a),xx(b)].

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

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

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

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

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

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

given #182 (F,wt=6): 1842 c2 != 1 | c2' = 0.  [para(104(a,1),251(a,1)),rewrite(104(6))].

given #183 (F,wt=10): 331 x ^ y != 0 | (x ^ y)' = 1.  [para(32(a,1),39(b,1,2)),rewrite(2(3),78(3)),xx(a)].

given #184 (T,wt=6): 1878 c1 != 0 | c1' = 1.  [para(13(a,1),331(a,1)),rewrite(13(6))].

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

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

given #187 (F,wt=10): 1610 (x ^ y)' != 0 | x ^ y = 1.  [para(150(a,1),97(a,1)),rewrite(216(10),150(11)),flip(b),xx(a)].

given #188 (F,wt=10): 1838 x v y != 0 | (y v x)' = 1.  [para(2(a,1),249(a,1))].

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

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

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

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

given #193 (F,wt=10): 1890 (x v y)' != 1 | x v y = 0.  [para(120(a,1),103(b,1)),rewrite(216(10),120(11)),flip(a),xx(b)].

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

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

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

given #197 (F,wt=6): 1966 c2' != 0 | c2 = 1.  [para(104(a,1),1911(a,1,1)),rewrite(104(7))].

given #198 (F,wt=10): 1958 (x v y)' != 1 | y v x = 0.  [para(2(a,1),1890(a,1,1))].

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

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

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

given #202 (F,wt=10): 1964 (x v y)' != 0 | y v x = 1.  [para(2(a,1),1911(a,1,1))].

given #203 (F,wt=10): 2007 (x ^ y)' != 1 | y ^ x = 0.  [para(4(a,1),1960(a,1,1))].

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

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

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

given #207 (F,wt=7): 2066 c1' v (x v c2) = 1.  [para(166(a,1),109(a,1,1)),rewrite(69(7),166(9))].

given #208 (F,wt=9): 2055 (x v y) ^ (y v x)' = 0.  [para(67(a,1),128(a,1,2,1))].

given #209 (T,wt=9): 2064 (x ^ y)' v (z v x) = 1.  [para(150(a,1),109(a,1,1)),rewrite(69(6),150(7))].

given #210 (T,wt=9): 2065 (x ^ y)' v (z v y) = 1.  [para(158(a,1),109(a,1,1)),rewrite(69(6),158(7))].

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

given #212 (F,wt=9): 2070 (x ^ c1)' v (y v c2) = 1.  [para(279(a,1),109(a,1,1)),rewrite(69(8),279(11))].

given #213 (F,wt=9): 2072 (c1 ^ x)' v (y v c2) = 1.  [para(288(a,1),109(a,1,1)),rewrite(69(8),288(11))].

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

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

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

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

given #218 (F,wt=11): 156 ((x ^ y) v z) ^ (x v z)' = 0.  [para(24(a,1),127(a,1,2,1))].

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

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

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

given #222 (F,wt=9): 2336 (x ^ y) v (y ^ x)' = 1.  [para(63(a,1),159(a,1,2,1))].

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

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

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

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

given #227 (F,wt=10): 2483 c2 != 1 | c2' ^ (x ^ c1) = c2'.  [para(283(a,1),118(a,1))].

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

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

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

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

given #232 (F,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 (F,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): 205 c1 ^ ((x v c2) ^ y) = c1 ^ y.  [para(193(a,1),5(a,1,1)),flip(a)].

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

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

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

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

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

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

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

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

given #243 (F,wt=11): 365 (x ^ y) v (y ^ x) = x ^ y.  [para(63(a,1),27(a,1,2))].

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

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

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

given #247 (F,wt=11): 613 (c1 v x) ^ (x v c2) = c1 v x.  [para(114(a,1),21(a,1,2))].

given #248 (F,wt=11): 620 x ^ ((y v (x v z))' ^ u) = 0.  [para(17(a,1),124(a,1,2,1,1))].

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

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

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

given #252 (F,wt=11): 719 x ^ (y ^ (z v (u v x))') = 0.  [para(141(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

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

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

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

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

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

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

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

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

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

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

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

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

given #265 (T,wt=11): 944 x v (y v (y v (x ^ z))') = 1.  [para(182(a,1),24(a,1,2)),rewrite(88(2)),flip(a)].

given #266 (A,wt=25): 137 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 #267 (F,wt=11): 954 x ^ (y ^ (y ^ (x v z))') = 0.  [para(185(a,1),22(a,1,2)),rewrite(91(2)),flip(a)].

given #268 (F,wt=11): 972 (c2 ^ (x v (c1 v y))) v c1' = 1.  [para(71(a,1),199(a,1,2,1))].

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

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

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

given #272 (F,wt=11): 1133 c1 ^ (x ^ (y v (c2 v z))') = 0.  [para(210(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

given #273 (F,wt=11): 1140 c1 ^ ((x v (y v c2))' ^ z) = 0.  [para(233(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

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

given #275 (T,wt=11): 1180 (x v (y ^ z)) ^ (x v y)' = 0.  [para(72(a,1),127(a,1,2,1))].

given #276 (A,wt=19): 139 (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 #277 (F,wt=11): 1182 x v (y v (x v (y ^ z))') = 1.  [para(72(a,1),231(a,1,2)),rewrite(2(5),3(5))].

given #278 (F,wt=11): 1204 c2 v ((x ^ (y ^ c1))' v z) = 1.  [para(5(a,1),287(a,1,2,1,1))].

given #279 (T,wt=11): 1217 c2 v (x v (y ^ (z ^ c1))') = 1.  [para(289(a,1),17(a,1,2)),rewrite(88(2)),flip(a)].

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

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

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

given #283 (F,wt=11): 1339 (x ^ (y v z)) v (x ^ y)' = 1.  [para(83(a,1),158(a,1,2,1))].

given #284 (T,wt=11): 1340 x ^ (y ^ (x ^ (y v z))') = 0.  [para(83(a,1),232(a,1,2)),rewrite(4(5),5(5))].

given #285 (T,wt=11): 1351 x ^ (c1 ^ (c2 ^ (x v y))') = 0.  [para(441(a,1),22(a,1,2)),rewrite(91(2),4(5)),flip(a)].

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

given #287 (F,wt=11): 1358 (x v c1) ^ (c2 v x) = x v c1.  [para(495(a,1),20(a,1,2))].

given #288 (F,wt=11): 1369 (x v c1) ^ (y v (c2 v x))' = 0.  [para(495(a,1),141(a,1,2,1,2))].

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

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

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

given #292 (F,wt=10): 3921 c1 != 1 | c2' ^ (x ^ c1) = c1'.  [para(102(a,1),147(a,1))].

given #293 (F,wt=11): 1380 (x v c1) ^ ((x v c2)' ^ y) = 0.  [para(497(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

given #294 (T,wt=11): 1382 (x v c1) ^ (y ^ (x v c2)') = 0.  [para(497(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

given #295 (T,wt=11): 1387 x v (c2 v (c1 v (x ^ y))') = 1.  [para(498(a,1),24(a,1,2)),rewrite(88(2),2(5)),flip(a)].

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

given #297 (F,wt=11): 1460 (x ^ c2) v ((c1 ^ x)' v y) = 1.  [para(961(a,1),3(a,1,1)),rewrite(78(2)),flip(a)].

given #298 (F,wt=11): 1462 (x ^ c2) v (y v (c1 ^ x)') = 1.  [para(961(a,1),17(a,1,2)),rewrite(88(2)),flip(a)].

given #299 (T,wt=11): 1472 (c2 ^ x) v ((x ^ c1)' v y) = 1.  [para(962(a,1),3(a,1,1)),rewrite(78(2)),flip(a)].

given #300 (T,wt=11): 1474 (c2 ^ x) v (y v (x ^ c1)') = 1.  [para(962(a,1),17(a,1,2)),rewrite(88(2)),flip(a)].

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

given #302 (F,wt=11): 1485 (c2 ^ (c1 v x)) v (c1' v y) = 1.  [para(963(a,1),3(a,1,1)),rewrite(78(2)),flip(a)].

given #303 (F,wt=11): 1487 (c2 ^ (c1 v x)) v (y v c1') = 1.  [para(963(a,1),17(a,1,2)),rewrite(88(2)),flip(a)].

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

given #305 (T,wt=11): 1505 x ^ (y ^ ((z v x) ^ y)') = 0.  [para(34(a,1),95(a,1,2)),rewrite(91(2)),flip(a)].

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

given #307 (F,wt=11): 1517 x ^ (y ^ (y ^ (z v x))') = 0.  [para(185(a,1),95(a,1,2)),rewrite(91(2)),flip(a)].

given #308 (F,wt=11): 1521 x ^ (c1 ^ (c2 ^ (y v x))') = 0.  [para(441(a,1),95(a,1,2)),rewrite(91(2),4(5)),flip(a)].

given #309 (T,wt=11): 1525 (c2 ^ (x v c1)) v (c1' v y) = 1.  [para(967(a,1),3(a,1,1)),rewrite(78(2)),flip(a)].

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

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

given #312 (F,wt=11): 1542 c1 ^ ((c2 ^ (c1 v x))' ^ y) = 0.  [para(1060(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

given #313 (F,wt=11): 1544 c1 ^ (c2 ^ (x v (c1 v y)))' = 0.  [para(17(a,1),1060(a,1,2,1,2))].

given #314 (T,wt=11): 1545 c1 ^ (x ^ (c2 ^ (c1 v y))') = 0.  [para(1060(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

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

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

given #317 (F,wt=11): 1583 (c1 v (x ^ (y ^ c2))) ^ c2' = 0.  [para(102(a,1),1359(a,1,2,1)),rewrite(2(5))].

given #318 (F,wt=11): 1598 (c1 v x) ^ ((x v c2)' ^ y) = 0.  [para(1377(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

given #319 (T,wt=11): 1601 (c1 v x) ^ (y ^ (x v c2)') = 0.  [para(1377(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

given #320 (T,wt=11): 1632 c1' v ((c2 ^ (c1 v x)) v y) = 1.  [para(1484(a,1),3(a,1,1)),rewrite(78(2)),flip(a)].

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

given #322 (F,wt=11): 1633 c1' v (x v (c2 ^ (c1 v y))) = 1.  [para(1484(a,1),17(a,1,2)),rewrite(88(2)),flip(a)].

given #323 (F,wt=11): 1634 c1' v (c2 ^ (x v (c1 v y))) = 1.  [para(17(a,1),1484(a,1,2,2))].

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

given #325 (T,wt=11): 1646 c1 ^ ((c2 ^ (x v c1))' ^ y) = 0.  [para(1519(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

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

given #327 (F,wt=11): 1648 c1 ^ (x ^ (c2 ^ (y v c1))') = 0.  [para(1519(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

given #328 (F,wt=11): 1665 (c1 v x) ^ (c2 v x) = c1 v x.  [para(112(a,1),98(a,1,2))].

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

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

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

given #332 (F,wt=11): 1682 c1' v (x v (c2 ^ (y v c1))) = 1.  [para(1524(a,1),17(a,1,2)),rewrite(88(2)),flip(a)].

given #333 (F,wt=11): 1692 (c1 v x) ^ ((c2 v x)' ^ y) = 0.  [para(1573(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

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

given #335 (T,wt=11): 1699 (c1 v (c2 ^ x)) ^ (c2' ^ y) = 0.  [para(1574(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

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

given #337 (F,wt=11): 1701 (c1 v (c2 ^ x)) ^ (y ^ c2') = 0.  [para(1574(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

given #338 (F,wt=11): 1707 (c1 v (x ^ c2)) ^ (c2' ^ y) = 0.  [para(1577(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

given #339 (T,wt=11): 1709 (c1 v (x ^ c2)) ^ (y ^ c2') = 0.  [para(1577(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

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

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

given #342 (F,wt=11): 1718 x ^ (y ^ (x ^ (z v y))') = 0.  [para(99(a,1),232(a,1,2)),rewrite(4(5),5(5))].

given #343 (F,wt=11): 1742 c2 v ((c1 v (c2 ^ x))' v y) = 1.  [para(1587(a,1),3(a,1,1)),rewrite(78(2)),flip(a)].

given #344 (T,wt=11): 1745 c2 v (x v (c1 v (c2 ^ y))') = 1.  [para(1587(a,1),17(a,1,2)),rewrite(88(2)),flip(a)].

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

given #346 (A,wt=25): 176 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 #347 (F,wt=11): 1757 c2' ^ ((c1 v (c2 ^ x)) ^ y) = 0.  [para(1698(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

given #348 (F,wt=11): 1758 c2' ^ (x ^ (c1 v (c2 ^ y))) = 0.  [para(1698(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

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

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

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

given #352 (F,wt=11): 1777 ((x ^ y) v z) ^ (y v z)' = 0.  [para(100(a,1),127(a,1,2,1))].

given #353 (F,wt=11): 1779 x v (y v ((z ^ x) v y)') = 1.  [para(31(a,1),100(a,1,2)),rewrite(88(2)),flip(a)].

given #354 (T,wt=11): 1798 x v (y v (y v (z ^ x))') = 1.  [para(182(a,1),100(a,1,2)),rewrite(88(2)),flip(a)].

given #355 (T,wt=11): 1802 x v (c2 v (c1 v (y ^ x))') = 1.  [para(498(a,1),100(a,1,2)),rewrite(88(2),2(5)),flip(a)].

given #356 (A,wt=19): 178 (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 #357 (F,wt=11): 1811 c2' ^ ((c1 v (x ^ c2)) ^ y) = 0.  [para(1706(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

given #358 (F,wt=11): 1812 c2' ^ (c1 v (x ^ (y ^ c2))) = 0.  [para(5(a,1),1706(a,1,2,2))].

given #359 (T,wt=11): 1813 c2' ^ (x ^ (c1 v (y ^ c2))) = 0.  [para(1706(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

given #360 (T,wt=11): 1824 c2 v ((c1 v (x ^ c2))' v y) = 1.  [para(1743(a,1),3(a,1,1)),rewrite(78(2)),flip(a)].

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

given #362 (F,wt=11): 1825 c2 v (c1 v (x ^ (y ^ c2)))' = 1.  [para(5(a,1),1743(a,1,2,1,2))].

given #363 (F,wt=11): 1827 c2 v (x v (c1 v (y ^ c2))') = 1.  [para(1743(a,1),17(a,1,2)),rewrite(88(2)),flip(a)].

given #364 (T,wt=11): 1924 (x v (y ^ z)) ^ (x v z)' = 0.  [para(105(a,1),127(a,1,2,1))].

given #365 (T,wt=11): 1927 x v (y v (x v (z ^ y))') = 1.  [para(105(a,1),231(a,1,2)),rewrite(2(5),3(5))].

given #366 (A,wt=15): 180 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 #367 (F,wt=11): 2019 x v (y v (z ^ (y v x))') = 1.  [para(108(a,1),161(a,1,2,1,2)),rewrite(3(5))].

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

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

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

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

given #372 (F,wt=11): 2056 (x v c1) ^ (x v (c2 v y))' = 0.  [para(112(a,1),128(a,1,2,1,2))].

given #373 (F,wt=11): 2057 (x v c1) ^ (x v (y v c2))' = 0.  [para(114(a,1),128(a,1,2,1,2))].

given #374 (T,wt=11): 2078 (x ^ (y ^ z))' v (u v y) = 1.  [para(161(a,1),109(a,1,1)),rewrite(69(7),161(9))].

given #375 (T,wt=11): 2079 (x ^ (y ^ z))' v (u v z) = 1.  [para(164(a,1),109(a,1,1)),rewrite(69(7),164(9))].

given #376 (A,wt=16): 183 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 #377 (F,wt=11): 2081 (c1 ^ x)' v (y v (c2 ^ x)) = 1.  [para(199(a,1),109(a,1,1)),rewrite(69(9),199(13))].

given #378 (F,wt=11): 2085 (x ^ (y ^ c1))' v (z v c2) = 1.  [para(289(a,1),109(a,1,1)),rewrite(69(9),289(13))].

given #379 (T,wt=11): 2087 (x ^ (c1 ^ y))' v (z v c2) = 1.  [para(324(a,1),109(a,1,1)),rewrite(69(9),324(13))].

given #380 (T,wt=11): 2088 (x ^ c1)' v (y v (x ^ c2)) = 1.  [para(440(a,1),109(a,1,1)),rewrite(69(9),440(13))].

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

given #382 (F,wt=11): 2092 (c1 ^ x)' v (y v (x ^ c2)) = 1.  [para(961(a,1),109(a,1,1)),rewrite(69(9),961(13))].

given #383 (F,wt=11): 2093 (x ^ c1)' v (y v (c2 ^ x)) = 1.  [para(962(a,1),109(a,1,1)),rewrite(69(9),962(13))].

given #384 (T,wt=11): 2094 (c1 v (c2 ^ x))' v (y v c2) = 1.  [para(1587(a,1),109(a,1,1)),rewrite(69(10),1587(15))].

given #385 (T,wt=11): 2096 (c1 v (x ^ c2))' v (y v c2) = 1.  [para(1743(a,1),109(a,1,1)),rewrite(69(10),1743(15))].

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

given #387 (F,wt=11): 2114 (x v y) ^ ((y v x)' ^ z) = 0.  [para(2055(a,1),5(a,1,1)),rewrite(81(2)),flip(a)].

given #388 (F,wt=11): 2116 (x v y) ^ (z ^ (y v x)') = 0.  [para(2055(a,1),19(a,1,2)),rewrite(91(2)),flip(a)].

given #389 (T,wt=11): 2134 c2 v (x v ((x v c1) ^ y)') = 1.  [para(495(a,1),2064(a,1,2)),rewrite(2(7),3(7))].

given #390 (T,wt=11): 2156 c2 v (x v (y ^ (x v c1))') = 1.  [para(495(a,1),2065(a,1,2)),rewrite(2(7),3(7))].

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

given #392 (F,wt=9): 5920 (x v y)' ^ (z ^ x) = 0.  [para(120(a,1),189(a,1,1)),rewrite(75(6),120(7))].

given #393 (F,wt=9): 5922 (x v y)' ^ (z ^ y) = 0.  [para(127(a,1),189(a,1,1)),rewrite(75(6),127(7))].

given #394 (T,wt=9): 5926 (c2 v x)' ^ (y ^ c1) = 0.  [para(196(a,1),189(a,1,1)),rewrite(75(8),196(11))].

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

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

given #397 (F,wt=11): 2181 (c1 v x) ^ (c2 v (x v y))' = 0.  [para(1377(a,1),110(a,1,2)),rewrite(4(4),81(4),2(6)),flip(a)].

given #398 (F,wt=11): 2208 x ^ (y ^ ((y ^ x) v z)') = 0.  [para(4(a,1),129(a,1,2,2,1,1))].

given #399 (T,wt=11): 2211 c1 ^ (x ^ ((c2 ^ x) v y)') = 0.  [para(129(a,1),59(a,1,2)),rewrite(4(3),81(3)),flip(a)].

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

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

given #402 (F,wt=11): 2226 c1 ^ (x ^ (y v (c2 ^ x))') = 0.  [para(143(a,1),59(a,1,2)),rewrite(4(3),81(3)),flip(a)].

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

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

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

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

given #407 (F,wt=11): 2279 (x v (y ^ z)) ^ (y v x)' = 0.  [para(2(a,1),156(a,1,1))].

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

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

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

given #411 (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 #412 (F,wt=11): 2289 ((x ^ y) v (z ^ x)) ^ x' = 0.  [para(26(a,1),156(a,1,2,1))].

given #413 (F,wt=11): 2294 ((x ^ c1) v y) ^ (c2 v y)' = 0.  [para(60(a,1),156(a,1,1,1))].

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

given #415 (T,wt=11): 2297 ((c2 ^ x) v (c1 ^ y)) ^ c2' = 0.  [para(282(a,1),156(a,1,2,1))].

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

given #417 (F,wt=11): 2317 x v (y v ((y v x) ^ z)') = 1.  [para(2(a,1),157(a,1,2,2,1,1))].

given #418 (F,wt=11): 2330 c2 v (x v ((c1 v x) ^ y)') = 1.  [para(157(a,1),1385(a,1,2,2,1)),rewrite(77(8),2(8),75(8),2(7))].

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

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

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

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

given #423 (F,wt=11): 2355 (x ^ y) v ((y ^ x)' v z) = 1.  [para(2336(a,1),3(a,1,1)),rewrite(78(2)),flip(a)].

given #424 (T,wt=11): 2358 (x ^ y) v (z v (y ^ x)') = 1.  [para(2336(a,1),17(a,1,2)),rewrite(88(2)),flip(a)].

given #425 (T,wt=11): 2372 (x ^ y)' v (z v (y ^ x)) = 1.  [para(2336(a,1),109(a,1,1)),rewrite(69(7),2336(9))].

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

given #427 (F,wt=11): 2386 c2 v (x v (y ^ (c1 v x))') = 1.  [para(163(a,1),1385(a,1,2,2,1)),rewrite(77(8),2(8),75(8),2(7))].

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

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

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

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

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

given #433 (F,wt=11): 2428 (x ^ (y v z)) v (y ^ x)' = 1.  [para(4(a,1),169(a,1,1))].

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

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

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

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

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

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

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

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

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

given #443 (F,wt=11): 2488 x v (y v ((y ^ z) v x)') = 1.  [para(184(a,1),17(a,1)),flip(a)].

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

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

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

given #447 (F,wt=11): 2504 c2 v (x v ((c1 ^ y) v x)') = 1.  [para(184(a,1),1385(a,1,2,2,1)),rewrite(77(8),2(8),75(8),2(7))].

given #448 (F,wt=11): 2505 x v ((x ^ y) v (z ^ x))' = 1.  [para(184(a,1),100(a,1)),flip(a)].

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

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

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

given #452 (F,wt=11): 2511 c1 ^ (x ^ ((c2 v y) ^ x)') = 0.  [para(187(a,1),59(a,1,2)),rewrite(4(3),81(3)),flip(a)].

given #453 (F,wt=11): 2520 c1 ^ (x ^ ((y v c2) ^ x)') = 0.  [para(114(a,1),187(a,1,2,2,1,1))].

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

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

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

given #457 (F,wt=11): 2528 (c1 ^ x) v (x ^ c2) = c2 ^ x.  [para(4(a,1),194(a,1,2))].

given #458 (F,wt=11): 2578 c1 ^ (x ^ (x ^ (c2 v y))') = 0.  [para(185(a,1),195(a,1,2)),rewrite(4(3),81(3)),flip(a)].

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

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

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

given #462 (F,wt=11): 2621 c1 ^ (x ^ (x ^ (y v c2))') = 0.  [para(185(a,1),205(a,1,2)),rewrite(4(3),81(3)),flip(a)].

given #463 (F,wt=11): 2634 c1 ^ ((c1 v x) ^ (y v c2))' = 0.  [para(205(a,1),187(a,1))].

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

given #465 (T,wt=11): 2719 c2 v (x v (x v (y ^ c1))') = 1.  [para(182(a,1),278(a,1,2)),rewrite(2(3),78(3)),flip(a)].

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

given #467 (F,wt=11): 2732 c2 v ((c2 ^ x) v (y ^ c1))' = 1.  [para(278(a,1),184(a,1))].

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

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

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

given #471 (A,wt=21): 223 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 #472 (F,wt=11): 2765 x v (c2 v (x v (y ^ c1))') = 1.  [para(284(a,1),231(a,1,2)),rewrite(2(7),3(7))].

given #473 (F,wt=11): 2793 ((c1 ^ x) v y) ^ (c2 v y)' = 0.  [para(315(a,1),127(a,1,2,1))].

given #474 (T,wt=11): 2810 c2 v (x v (x v (c1 ^ y))') = 1.  [para(182(a,1),315(a,1,2)),rewrite(2(3),78(3)),flip(a)].

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

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

given #477 (F,wt=11): 2852 x v (c2 v (x v (c1 ^ y))') = 1.  [para(317(a,1),231(a,1,2)),rewrite(2(7),3(7))].

given #478 (F,wt=11): 2919 x ^ (c1 ^ (y v (x ^ c2))') = 0.  [para(439(a,1),131(a,1,2,1,2)),rewrite(5(7))].

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

given #480 (T,wt=11): 2947 (x v y) ^ (z ^ x) = z ^ x.  [para(63(a,1),123(a,1,1)),rewrite(26(5)),flip(a)].

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

given #482 (F,wt=11): 3013 (x v c2) ^ (c1 v x) = c1 v x.  [para(613(a,1),4(a,1)),flip(a)].

given #483 (F,wt=11): 3023 x v (c2 v (y ^ (c1 v x))') = 1.  [para(613(a,1),164(a,1,2,1,2)),rewrite(3(7))].

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

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

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

given #487 (F,wt=11): 3205 (c2 ^ (c1 v x)) v (y ^ c1)' = 1.  [para(6(a,1),810(a,1,2,1,2))].

given #488 (F,wt=11): 3207 (c2 ^ x) v (c1 ^ (y ^ x))' = 1.  [para(19(a,1),810(a,1,2,1))].

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

given #490 (T,wt=11): 3231 (c2 ^ (x v y)) v (c1 ^ x)' = 1.  [para(83(a,1),810(a,1,2,1))].

given #491 (A,wt=25): 228 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 #492 (F,wt=11): 3236 (c2 ^ (x v y)) v (c1 ^ y)' = 1.  [para(99(a,1),810(a,1,2,1))].

given #493 (F,wt=11): 3283 (x ^ c2) v (x ^ (c1 ^ y))' = 1.  [para(4(a,1),813(a,1,2,1)),rewrite(5(5))].

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

given #495 (T,wt=11): 3295 (c2 ^ (x v y)) v (y ^ c1)' = 1.  [para(95(a,1),813(a,1,2,1)),rewrite(4(3))].

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

given #497 (F,wt=11): 3355 x v ((y ^ x) v (x ^ z))' = 1.  [para(944(a,1),100(a,1)),flip(a)].

given #498 (F,wt=11): 3357 c2 v ((x ^ c1) v (c2 ^ y))' = 1.  [para(944(a,1),278(a,1)),flip(a)].

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

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

given #500 (T,wt=11): 3434 x ^ ((y v x) ^ (x v z))' = 0.  [para(954(a,1),95(a,1)),flip(a)].

given #501 (A,wt=16): 230 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 #502 (F,wt=11): 3435 c1 ^ ((c2 v x) ^ (c1 v y))' = 0.  [para(954(a,1),195(a,1)),flip(a)].

given #503 (F,wt=11): 3437 c1 ^ ((x v c2) ^ (c1 v y))' = 0.  [para(954(a,1),205(a,1)),flip(a)].

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

given #505 (T,wt=11): 3645 c2 v (x v (c1 v (x ^ y))') = 1.  [para(1182(a,1),1385(a,1,2,2,1)),rewrite(77(8),2(8),75(8),2(7))].

given #506 (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 #507 (F,wt=11): 3691 c1 ^ ((c2 ^ (c1 v x)) v y) = c1.  [para(140(a,1),59(a,1)),rewrite(13(3),4(6)),flip(a)].

given #508 (F,wt=11): 3753 (x ^ y)' v (x ^ (y v z)) = 1.  [para(1339(a,1),2(a,1)),flip(a)].

given #509 (T,wt=11): 3793 c1 ^ (x ^ (c2 ^ (x v y))') = 0.  [para(1340(a,1),59(a,1,2)),rewrite(4(3),81(3)),flip(a)].

given #510 (T,wt=11): 3832 (c2 v x) ^ (x v c1) = x v c1.  [para(1358(a,1),4(a,1)),flip(a)].

given #511 (A,wt=12): 237 x' ^ (y v x) != 0 | y v x = x.  [para(231(a,1),10(a,1)),rewrite(216(10)),flip(c),xx(a)].

given #512 (F,wt=11): 3869 (c1 v x) ^ (y v (c2 v x))' = 0.  [para(2(a,1),1369(a,1,1))].

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

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

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

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

given #517 (F,wt=11): 3874 (x v c1) ^ (c2 v (y v x))' = 0.  [para(17(a,1),1369(a,1,2,1))].

given #518 (F,wt=11): 3875 (c1 v (x ^ c2)) ^ (y v c2)' = 0.  [para(26(a,1),1369(a,1,2,1,2)),rewrite(2(4))].

given #519 (T,wt=11): 3883 (c1 v (x ^ y)) ^ (c2 v x)' = 0.  [para(72(a,1),1369(a,1,2,1)),rewrite(2(3))].

given #520 (T,wt=11): 3889 (c1 v (x ^ y)) ^ (c2 v y)' = 0.  [para(105(a,1),1369(a,1,2,1)),rewrite(2(3))].

given #521 (A,wt=12): 239 (x v y) ^ y' != 0 | (x v y)' = y'.  [para(231(a,1),36(a,1)),xx(a)].

given #522 (F,wt=11): 4067 (x ^ y)' v ((z v x) ^ y) = 1.  [para(1503(a,1),2(a,1)),flip(a)].

given #523 (F,wt=11): 4069 (x ^ (y v z)) v (z ^ x)' = 1.  [para(4(a,1),1503(a,1,1))].

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

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

given #526 (A,wt=12): 240 x' v (y ^ x) != 1 | y ^ x = x.  [para(232(a,1),10(b,1)),rewrite(216(10)),flip(c),xx(b)].

given #527 (F,wt=11): 4077 ((x v y) ^ (z v y)) v y' = 1.  [para(20(a,1),1503(a,1,2,1))].

given #528 (F,wt=11): 4083 ((x v c1) ^ (c2 v y)) v c1' = 1.  [para(191(a,1),1503(a,1,2,1))].

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

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

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

given #532 (F,wt=11): 4164 x ^ ((y v x) ^ (z v x))' = 0.  [para(1505(a,1),95(a,1)),flip(a)].

given #533 (F,wt=11): 4169 c1 ^ ((x v c1) ^ (c2 v y))' = 0.  [para(1505(a,1),195(a,1)),flip(a)].

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

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

given #536 (A,wt=12): 242 (x ^ y) v y' != 1 | x ^ y = y.  [para(232(a,1),36(b,1)),rewrite(216(10)),flip(c),xx(b)].

given #537 (F,wt=11): 4245 c1 ^ ((x v c2) ^ (y v c1))' = 0.  [para(1517(a,1),205(a,1)),flip(a)].

given #538 (F,wt=11): 4257 c1 ^ (x ^ (c2 ^ (y v x))') = 0.  [para(1521(a,1),19(a,1)),flip(a)].

given #539 (T,wt=11): 4386 (x ^ y) v (z v x) = z v x.  [para(67(a,1),153(a,1,1)),rewrite(20(5)),flip(a)].

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

given #541 (A,wt=19): 243 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 #542 (F,wt=11): 4478 c1' v ((c2 v x) ^ (c1 v y)) = 1.  [para(123(a,1),1632(a,1,2))].

given #543 (F,wt=11): 4581 c1' v ((c2 v x) ^ (y v c1)) = 1.  [para(123(a,1),1680(a,1,2))].

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

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

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

given #547 (F,wt=11): 4685 (x ^ y)' v (x ^ (z v y)) = 1.  [para(1716(a,1),2(a,1)),flip(a)].

given #548 (F,wt=11): 4939 c2' ^ ((c1 ^ x) v (c2 ^ y)) = 0.  [para(153(a,1),1757(a,1,2))].

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

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

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

Low Water (keep): wt=71, part=0.99, limit=67

given #552 (F,wt=11): 5018 (x v y)' ^ ((z ^ x) v y) = 0.  [para(1777(a,1),4(a,1)),flip(a)].

Low Water (keep): wt=68, part=0.98, limit=63

given #553 (F,wt=11): 5020 ((x ^ y) v (y ^ z)) ^ y' = 0.  [para(7(a,1),1777(a,1,2,1))].

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

given #555 (T,wt=11): 5031 (c1 v x) ^ (c2 v (y v x))' = 0.  [para(191(a,1),1777(a,1,1,1)),rewrite(3(5))].

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

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

given #558 (F,wt=11): 5035 ((x ^ c2) v (c1 ^ y)) ^ c2' = 0.  [para(282(a,1),1777(a,1,2,1))].

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

Low Water (keep): wt=63, part=0.97, limit=61

given #560 (T,wt=11): 5114 x v ((y ^ x) v (z ^ x))' = 1.  [para(1779(a,1),100(a,1)),flip(a)].

Low Water (keep): wt=59, part=0.97, limit=59

given #561 (A,wt=17): 247 x v y != 1 | x v y != 0 | (x v y)' = x v y.  [para(28(a,1),37(b,1)),rewrite(67(2),66(2))].

given #562 (F,wt=11): 5122 c2 v ((x ^ c2) v (y ^ c1))' = 1.  [para(1779(a,1),278(a,1)),flip(a)].

given #563 (F,wt=11): 5123 c2 v ((x ^ c2) v (c1 ^ y))' = 1.  [para(1779(a,1),315(a,1)),flip(a)].

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

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

given #566 (A,wt=13): 248 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 #567 (F,wt=11): 5174 c2 v (x v (c1 v (y ^ x))') = 1.  [para(1802(a,1),17(a,1)),flip(a)].

given #568 (F,wt=11): 5264 c2' ^ ((c1 ^ x) v (y ^ c2)) = 0.  [para(153(a,1),1811(a,1,2))].

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

given #570 (T,wt=11): 5302 ((c1 ^ x) v (c2 ^ y)) ^ c2' = 0.  [para(282(a,1),179(a,1,1,2,1)),rewrite(282(9))].

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

given #572 (F,wt=11): 5350 (x v y)' ^ (x v (z ^ y)) = 0.  [para(1924(a,1),4(a,1)),flip(a)].

given #573 (F,wt=11): 5535 x v (c2 v ((x v c1) ^ y)') = 1.  [para(4(a,1),2044(a,1,2,2,1))].

Low Water (keep): wt=53, part=0.95, limit=53

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

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

given #576 (A,wt=25): 252 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 #577 (F,wt=11): 5579 ((x ^ c1) v y) ^ (y v c2)' = 0.  [para(276(a,1),2052(a,1,2,1,2))].

given #578 (F,wt=11): 5581 ((c1 ^ x) v y) ^ (y v c2)' = 0.  [para(282(a,1),2052(a,1,2,1,2))].

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

given #580 (T,wt=11): 5896 c2 v ((c1 v (x ^ c2)) ^ y)' = 1.  [para(2134(a,1),100(a,1)),rewrite(2(6)),flip(a)].

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

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

given #583 (F,wt=11): 5911 c2 v (x ^ (c1 v (y ^ c2)))' = 1.  [para(2156(a,1),100(a,1)),rewrite(2(6)),flip(a)].

given #584 (T,wt=11): 5940 (x v (y v z))' ^ (u ^ y) = 0.  [para(131(a,1),189(a,1,1)),rewrite(75(7),131(9))].

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

given #586 (A,wt=16): 255 (x v y) ^ (y' v z) != 0 | (x v y)' = y' v z.  [para(79(a,1),37(a,1,2)),rewrite(88(2)),xx(a)].

given #587 (F,wt=11): 5952 (x v (c2 v y))' ^ (z ^ c1) = 0.  [para(210(a,1),189(a,1,1)),rewrite(75(9),210(13))].

given #588 (F,wt=11): 5953 (x v (y v c2))' ^ (z ^ c1) = 0.  [para(233(a,1),189(a,1,1)),rewrite(75(9),233(13))].

given #589 (T,wt=11): 5957 (x v c2)' ^ (y ^ (x v c1)) = 0.  [para(497(a,1),189(a,1,1)),rewrite(75(9),497(13))].

given #590 (T,wt=11): 5959 (c2 ^ (c1 v x))' ^ (y ^ c1) = 0.  [para(1060(a,1),189(a,1,1)),rewrite(75(10),1060(15))].

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

Low Water (keep): wt=52, part=0.93, limit=49

given #592 (F,wt=11): 5961 (c2 v x)' ^ (y ^ (x v c1)) = 0.  [para(1359(a,1),189(a,1,1)),rewrite(75(9),1359(13))].

given #593 (F,wt=11): 5962 (x v c2)' ^ (y ^ (c1 v x)) = 0.  [para(1377(a,1),189(a,1,1)),rewrite(75(9),1377(13))].

given #594 (T,wt=11): 5964 (c2 ^ (x v c1))' ^ (y ^ c1) = 0.  [para(1519(a,1),189(a,1,1)),rewrite(75(10),1519(15))].

given #595 (T,wt=11): 5967 (c2 v x)' ^ (y ^ (c1 v x)) = 0.  [para(1573(a,1),189(a,1,1)),rewrite(75(9),1573(13))].

given #596 (A,wt=16): 257 (x v y) ^ (z v y') != 0 | (x v y)' = z v y'.  [para(89(a,1),37(a,1,2)),rewrite(88(2)),xx(a)].

given #597 (F,wt=11): 5974 (x v y)' ^ (z ^ (y v x)) = 0.  [para(2055(a,1),189(a,1,1)),rewrite(75(7),2055(9))].

given #598 (F,wt=11): 6009 (x ^ c2) v (c1 ^ (y ^ x))' = 1.  [para(189(a,1),2081(a,1,2)),rewrite(2(7))].

Low Water (keep): wt=49, part=0.93, limit=49

given #599 (T,wt=11): 6014 x ^ (c1 ^ ((x ^ c2) v y)') = 0.  [para(87(a,1),5920(a,1,2)),rewrite(4(7),5(7))].

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

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

given #602 (F,wt=11): 6132 (c1 v (c2 ^ x)) ^ (c2 v y)' = 0.  [para(24(a,1),2181(a,1,2,1))].

given #603 (F,wt=11): 6137 (c1 v (x ^ c2)) ^ (c2 v y)' = 0.  [para(100(a,1),2181(a,1,2,1))].

given #604 (T,wt=11): 6150 c1 ^ (x ^ ((x ^ c2) v y)') = 0.  [para(2208(a,1),59(a,1,2)),rewrite(4(3),81(3)),flip(a)].

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

given #606 (A,wt=31): 259 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): wt=47, part=0.92, limit=47

given #607 (F,wt=11): 6168 c1 ^ ((c2 ^ (c1 v x)) v y)' = 0.  [para(2211(a,1),22(a,1)),flip(a)].

given #608 (F,wt=11): 6179 c1 ^ ((c2 ^ (x v c1)) v y)' = 0.  [para(2211(a,1),95(a,1)),flip(a)].

given #609 (T,wt=11): 6189 c1 ^ (x ^ (y v (x ^ c2))') = 0.  [para(2223(a,1),59(a,1,2)),rewrite(4(3),81(3)),flip(a)].

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

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

given #612 (F,wt=11): 6238 c1 ^ (x v (c2 ^ (y v c1)))' = 0.  [para(2226(a,1),95(a,1)),flip(a)].

given #613 (F,wt=11): 6249 (x v (y ^ c1)) ^ (c2 v x)' = 0.  [para(278(a,1),2255(a,1,2,1))].

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

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

Low Water (keep): wt=45, part=0.92, limit=45

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

given #617 (F,wt=11): 6266 (x v c2)' ^ (x v (c1 ^ y)) = 0.  [para(2263(a,1),4(a,1)),flip(a)].

given #618 (F,wt=11): 6275 c1 ^ ((c2 ^ (x v c1)) v y) = c1.  [para(20(a,1),197(a,2)),rewrite(95(10))].

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

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

Low Water (keep): wt=44, part=0.91, limit=43

given #621 (A,wt=35): 262 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))].

given #622 (F,wt=11): 6390 x' ^ ((x ^ y) v (x ^ z)) = 0.  [para(7(a,1),2282(a,1,1,1))].

given #623 (F,wt=11): 6394 x' ^ ((x ^ y) v (z ^ x)) = 0.  [para(26(a,1),2282(a,1,1,1))].

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

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

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

given #627 (F,wt=11): 6401 c2' ^ ((c2 ^ x) v (c1 ^ y)) = 0.  [para(282(a,1),2282(a,1,1,1))].

Low Water (keep): wt=41, part=0.90, limit=41

given #628 (F,wt=11): 6445 x ^ ((x' ^ y) v (x' ^ z)) = 0.  [para(216(a,1),2284(a,1,2)),rewrite(4(6))].

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

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

Low Water (keep): wt=40, part=0.90, limit=40

given #631 (A,wt=27): 264 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))].

Low Water (keep): wt=39, part=0.90, limit=39

given #632 (F,wt=11): 6506 ((x ^ c1) v (y ^ c1)) ^ c2' = 0.  [para(276(a,1),2294(a,1,2,1))].

given #633 (F,wt=11): 6508 ((x ^ c1) v (c1 ^ y)) ^ c2' = 0.  [para(282(a,1),2294(a,1,2,1))].

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

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

given #636 (A,wt=16): 265 (x v y) ^ (y ^ z)' != 0 | (x v y)' = (y ^ z)'.  [para(150(a,1),37(a,1,2)),rewrite(88(2)),xx(a)].

given #637 (F,wt=11): 6632 ((c2 v x) ^ y) v (y ^ c1)' = 1.  [para(191(a,1),2332(a,1,2,1,2))].

given #638 (F,wt=11): 6633 ((x v c2) ^ y) v (y ^ c1)' = 1.  [para(193(a,1),2332(a,1,2,1,2))].

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

Low Water (keep): wt=36, part=0.88, limit=36

given #640 (T,wt=11): 6920 (x ^ (y v c2)) v (c1 ^ x)' = 1.  [para(205(a,1),2387(a,1,2,1))].

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

given #642 (F,wt=11): 6927 (x ^ c1)' v (x ^ (c2 v y)) = 1.  [para(2393(a,1),2(a,1)),flip(a)].

given #643 (F,wt=11): 6945 (x ^ c1)' v (x ^ (y v c2)) = 1.  [para(2394(a,1),2(a,1)),flip(a)].

given #644 (T,wt=11): 7029 (x ^ y)' v ((y v z) ^ x) = 1.  [para(4(a,1),2427(a,1,1,1))].

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

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

given #647 (F,wt=11): 7032 x' v ((x v y) ^ (x v z)) = 1.  [para(6(a,1),2427(a,1,1,1))].

given #648 (F,wt=11): 7036 x' v ((x v y) ^ (z v x)) = 1.  [para(20(a,1),2427(a,1,1,1))].

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

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

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

given #652 (F,wt=11): 7048 (c1 ^ x)' v ((c2 v y) ^ x) = 1.  [para(112(a,1),2427(a,1,2,1))].

given #653 (F,wt=11): 7053 (c1 ^ x)' v ((y v c2) ^ x) = 1.  [para(114(a,1),2427(a,1,2,1))].

given #654 (T,wt=11): 7185 x v ((x' v y) ^ (x' v z)) = 1.  [para(216(a,1),2431(a,1,2)),rewrite(2(6))].

given #655 (T,wt=11): 7377 x v ((x' v y) ^ (z v x')) = 1.  [para(216(a,1),2436(a,1,2)),rewrite(2(6))].

given #656 (A,wt=31): 269 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))].

Low Water (keep): wt=35, part=0.86, limit=33

Low Water (keep): wt=33, part=0.86, limit=33

given #657 (F,wt=11): 7382 ((c2 v x) ^ (y v c1)) v c1' = 1.  [para(112(a,1),2436(a,1,1,1))].

given #658 (F,wt=11): 7385 ((x v c2) ^ (y v c1)) v c1' = 1.  [para(114(a,1),2436(a,1,1,1))].

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

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

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

given #662 (F,wt=11): 7455 ((c2 v x) ^ (y v c2)) v c1' = 1.  [para(112(a,1),2441(a,1,1,1))].

given #663 (F,wt=11): 7457 ((x v c2) ^ (y v c2)) v c1' = 1.  [para(114(a,1),2441(a,1,1,1))].

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

Low Water (keep): wt=32, part=0.84, limit=32

given #665 (T,wt=11): 7592 c2 v ((c1 ^ x) v (c1 ^ y))' = 1.  [hyper(215,a,2490,a(flip),b,1573,a),rewrite(2490(8),69(11),216(10),2490(16))].

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

given #667 (F,wt=11): 7623 c2 v ((x ^ c1) v (y ^ c1))' = 1.  [para(2494(a,1),278(a,1)),flip(a)].

given #668 (F,wt=11): 7624 c2 v ((x ^ c1) v (c1 ^ y))' = 1.  [para(2494(a,1),315(a,1)),flip(a)].

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

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

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

given #672 (F,wt=11): 7881 x ^ (c1 ^ ((c2 v y) ^ x)') = 0.  [para(112(a,1),2509(a,1,2,2,1,1))].

given #673 (F,wt=11): 7884 x ^ (c1 ^ ((y v c2) ^ x)') = 0.  [para(114(a,1),2509(a,1,2,2,1,1))].

given #674 (T,wt=11): 7906 c1 ^ ((c2 v x) ^ (c2 v y))' = 0.  [para(2510(a,1),59(a,1,2)),rewrite(4(3),81(3)),flip(a)].

given #675 (T,wt=11): 8031 c1 ^ ((c2 v x) ^ (y v c2))' = 0.  [para(2511(a,1),205(a,1)),flip(a)].

given #676 (A,wt=20): 273 (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(88(2)),xx(a)].

given #677 (F,wt=11): 8046 c1 ^ ((x v c2) ^ (c2 v y))' = 0.  [para(2520(a,1),195(a,1)),flip(a)].

given #678 (F,wt=11): 8047 c1 ^ ((x v c2) ^ (y v c2))' = 0.  [para(2520(a,1),205(a,1)),flip(a)].

given #679 (T,wt=11): 8142 (x ^ c2) v (c1 ^ x) = c2 ^ x.  [para(2528(a,1),2(a,1)),flip(a)].

Low Water (keep): wt=31, part=0.83, limit=31

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

given #681 (A,wt=24): 274 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 #682 (F,wt=11): 8480 ((c1 ^ x) v (y ^ c2)) ^ c2' = 0.  [para(26(a,1),2793(a,1,2,1))].

given #683 (F,wt=11): 8483 ((c1 ^ x) v (y ^ c1)) ^ c2' = 0.  [para(276(a,1),2793(a,1,2,1))].

given #684 (T,wt=11): 8485 ((c1 ^ x) v (c1 ^ y)) ^ c2' = 0.  [para(282(a,1),2793(a,1,2,1))].

given #685 (T,wt=11): 8583 (x v c2) ^ (y ^ c1) = y ^ c1.  [para(2(a,1),2946(a,1,1))].

given #686 (A,wt=16): 275 (x v y') ^ (z v y) != 0 | (x v y')' = z v y.  [para(231(a,1),37(a,1,2)),rewrite(88(2)),xx(a)].

given #687 (F,wt=11): 8619 (x v y) ^ (z ^ y) = z ^ y.  [para(2(a,1),2947(a,1,1))].

given #688 (F,wt=11): 8737 (x ^ c2) v (c1 ^ (x ^ y))' = 1.  [para(4(a,1),3203(a,1,2,1)),rewrite(5(5))].

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

given #690 (T,wt=11): 8763 (c2 ^ (x v c1)) v (c1 ^ y)' = 1.  [para(95(a,1),3204(a,1,2,1))].

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

given #692 (F,wt=11): 8785 (x ^ c1)' v (c2 ^ (c1 v y)) = 1.  [para(3205(a,1),2(a,1)),flip(a)].

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

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

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

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

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

Low Water (keep): wt=29, part=0.81, limit=29

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

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

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

given #701 (A,wt=13): 285 c2 != 1 | x ^ c1 != 0 | (x ^ c1)' = c2.  [para(276(a,1),36(a,1)),rewrite(4(7),60(7))].

given #702 (F,wt=11): 9550 (c1 v (x ^ y)) ^ (y v c2)' = 0.  [para(100(a,1),3870(a,1,2,1)),rewrite(2(3))].

given #703 (F,wt=11): 9574 (x v c2)' ^ (c1 v (c2 ^ y)) = 0.  [para(3872(a,1),4(a,1)),flip(a)].

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

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

given #706 (A,wt=12): 290 c2 ^ (x ^ c1)' != 0 | (x ^ c1)' = c2'.  [para(279(a,1),10(a,1)),flip(c),xx(a)].

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

given #708 (F,wt=11): 9768 (x ^ y)' v ((z v y) ^ x) = 1.  [para(4(a,1),4067(a,1,1,1))].

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

given #710 (T,wt=11): 9770 x' v ((y v x) ^ (x v z)) = 1.  [para(6(a,1),4067(a,1,1,1))].

given #711 (A,wt=12): 292 c2 ^ (x ^ c1)' != 0 | x ^ c1 = c2.  [para(279(a,1),36(a,1)),rewrite(4(8),216(14)),xx(a)].

given #712 (F,wt=11): 9774 x' v ((y v x) ^ (z v x)) = 1.  [para(20(a,1),4067(a,1,1,1))].

given #713 (F,wt=11): 9779 c1' v ((x v c1) ^ (c2 v y)) = 1.  [para(191(a,1),4067(a,1,1,1))].

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

Low Water (keep): wt=28, part=0.80, limit=28

given #715 (T,wt=11): 9956 x v ((y v x') ^ (x' v z)) = 1.  [para(216(a,1),4072(a,1,2)),rewrite(2(6))].

given #716 (A,wt=16): 293 (x v c2) ^ (y ^ c1)' != 0 | (x v c2)' = (y ^ c1)'.  [para(279(a,1),37(a,1,2)),rewrite(88(2)),xx(a)].

given #717 (F,wt=11): 10008 x v ((y v x') ^ (z v x')) = 1.  [para(216(a,1),4077(a,1,2)),rewrite(2(6))].

given #718 (F,wt=11): 10279 (x ^ y) v (z v y) = z v y.  [para(4(a,1),4386(a,1,1))].

given #719 (T,wt=11): 10285 (x ^ c1) v (y v c2) = y v c2.  [para(60(a,1),4386(a,1,1))].

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

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

given #722 (F,wt=11): 10580 c1' v ((c2 v x) ^ (c2 v y)) = 1.  [para(112(a,1),4478(a,1,2,2))].

given #723 (F,wt=11): 10582 c1' v ((c2 v x) ^ (y v c2)) = 1.  [para(114(a,1),4478(a,1,2,2))].

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

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

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

given #727 (F,wt=11): 11059 c2' ^ ((c1 ^ x) v (y ^ c1)) = 0.  [para(60(a,1),4939(a,1,2,2))].

given #728 (F,wt=11): 11081 (x v y)' ^ (y v (z ^ x)) = 0.  [para(5016(a,1),4(a,1)),flip(a)].

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

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

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

given #732 (F,wt=11): 11411 x' ^ ((y ^ x) v (z ^ x)) = 0.  [para(26(a,1),5018(a,1,1,1))].

Low Water (keep): wt=27, part=0.77, limit=27

given #733 (F,wt=11): 11415 c2' ^ ((x ^ c2) v (y ^ c1)) = 0.  [para(276(a,1),5018(a,1,1,1))].

given #734 (T,wt=11): 11416 c2' ^ ((x ^ c2) v (c1 ^ y)) = 0.  [para(282(a,1),5018(a,1,1,1))].

given #735 (T,wt=11): 11469 x ^ ((y ^ x') v (x' ^ z)) = 0.  [para(216(a,1),5020(a,1,2)),rewrite(4(6))].

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

given #737 (F,wt=11): 11495 x ^ ((y ^ x') v (z ^ x')) = 0.  [para(216(a,1),5024(a,1,2)),rewrite(4(6))].

given #738 (F,wt=11): 11858 c2' ^ ((x ^ c1) v (y ^ c2)) = 0.  [para(4(a,1),5264(a,1,2,1))].

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

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

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

given #742 (F,wt=11): 12647 (c2 v x)' ^ (c1 v (c2 ^ y)) = 0.  [para(6132(a,1),4(a,1)),flip(a)].

given #743 (F,wt=11): 12668 (c2 v x)' ^ (c1 v (y ^ c2)) = 0.  [para(6137(a,1),4(a,1)),flip(a)].

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

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

given #746 (A,wt=21): 299 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 #747 (F,wt=11): 12912 c1 ^ (x v (c2 ^ (y v c1))) = c1.  [para(2(a,1),6275(a,1,2))].

given #748 (F,wt=11): 13170 c2' ^ ((x ^ c1) v (y ^ c1)) = 0.  [para(276(a,1),6399(a,1,1,1))].

given #749 (T,wt=11): 13171 c2' ^ ((x ^ c1) v (c1 ^ y)) = 0.  [para(282(a,1),6399(a,1,1,1))].

given #750 (T,wt=11): 13241 c1 ^ ((c2' ^ x) v (c2' ^ y)) = 0.  [para(6445(a,1),59(a,1,2)),rewrite(4(3),81(3)),flip(a)].

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

given #752 (F,wt=11): 13277 c1 ^ ((c2' ^ x) v (y ^ c2')) = 0.  [para(6465(a,1),59(a,1,2)),rewrite(4(3),81(3)),flip(a)].

given #753 (F,wt=11): 13636 (x ^ c1)' v ((c2 v y) ^ x) = 1.  [para(6632(a,1),2(a,1)),flip(a)].

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

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

given #756 (A,wt=12): 301 x v (x v y)' != 1 | x v y = x.  [para(120(a,1),38(b,1)),rewrite(2(3),216(11)),xx(b)].

given #757 (F,wt=7): 16570 c1' v (c1' v c2')' != 1.  [ur(301,b,15,a)].

given #758 (F,wt=7): 16573 (c1' v (c1' v c2')')' != 0.  [ur(1964,b,16570,a),rewrite(2(9))].

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

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

given #761 (A,wt=25): 303 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 #762 (F,wt=11): 13979 c1' v ((x v c2) ^ (y v c2)) = 1.  [para(114(a,1),7042(a,1,2,1))].

given #763 (F,wt=11): 14085 c2 v ((c1' v x) ^ (c1' v y)) = 1.  [hyper(215,a,7185,a(flip),b,1573,a),rewrite(7185(9),69(12),216(11),7185(18))].

given #764 (T,wt=11): 14121 c2 v ((c1' v x) ^ (y v c1')) = 1.  [hyper(215,a,7377,a(flip),b,1573,a),rewrite(7377(9),69(12),216(11),7377(18))].

given #765 (T,wt=11): 14726 c2' ^ ((c1 ^ x) v (c1 ^ y)) = 0.  [para(282(a,1),8476(a,1,1,1))].

Low Water (keep): wt=25, part=0.73, limit=25

given #766 (A,wt=12): 304 x v (y v x)' != 1 | y v x = x.  [para(127(a,1),38(b,1)),rewrite(2(3),216(11)),xx(b)].

given #767 (F,wt=11): 14954 (c1 ^ x)' v (c2 ^ (c1 v y)) = 1.  [para(8753(a,1),2(a,1)),flip(a)].

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

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

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

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

given #772 (F,wt=11): 15468 c2 v ((x v c1') ^ (c1' v y)) = 1.  [para(9956(a,1),1385(a,1,2,2,1)),rewrite(77(10),2(10),75(10),2(9))].

given #773 (F,wt=11): 15511 c2 v ((x v c1') ^ (y v c1')) = 1.  [para(10008(a,1),1385(a,1,2,2,1)),rewrite(77(10),2(10),75(10),2(9))].

given #774 (T,wt=11): 16105 c1 ^ ((x ^ c2') v (c2' ^ y)) = 0.  [hyper(295,a,962,a,b,11469,a(flip)),rewrite(11469(9),4(10),75(12),216(11),11469(18))].

given #775 (T,wt=11): 16317 c1 ^ ((x ^ c2') v (y ^ c2')) = 0.  [hyper(295,a,962,a,b,11495,a(flip)),rewrite(11495(9),4(10),75(12),216(11),11495(18))].

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

given #777 (F,wt=12): 311 c1 v (c2 v x)' != 1 | c2 v x = c1.  [para(196(a,1),38(b,1)),rewrite(2(5),216(14)),xx(b)].

given #778 (F,wt=12): 312 c1 v (x v c2)' != 1 | x v c2 = c1.  [para(198(a,1),38(b,1)),rewrite(2(5),216(14)),xx(b)].

given #779 (T,wt=12): 313 (x v y) ^ y' != 0 | x v y = y.  [para(231(a,1),38(a,1)),rewrite(216(10)),flip(c),xx(a)].

given #780 (T,wt=12): 314 (x ^ y) v y' != 1 | (x ^ y)' = y'.  [para(232(a,1),38(b,1)),xx(b)].

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

given #782 (F,wt=12): 322 c2 ^ (c1 ^ x)' != 0 | (c1 ^ x)' = c2'.  [para(288(a,1),10(a,1)),flip(c),xx(a)].

given #783 (F,wt=12): 325 c2 ^ (c1 ^ x)' != 0 | c1 ^ x = c2.  [para(288(a,1),36(a,1)),rewrite(4(8),216(14)),xx(a)].

given #784 (T,wt=12): 341 (x ^ y) v x' != 1 | (x ^ y)' = x'.  [para(92(a,1),39(b,1)),xx(b)].

given #785 (T,wt=12): 343 (x ^ c1) v c2' != 1 | (x ^ c1)' = c2'.  [para(132(a,1),39(b,1,2)),rewrite(91(9)),xx(b)].

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

given #787 (F,wt=12): 349 (c1 ^ x) v c2' != 1 | (c1 ^ x)' = c2'.  [para(135(a,1),39(b,1)),xx(b)].

given #788 (F,wt=12): 1248 x' ^ (x v y) != 0 | x v y = x.  [para(79(a,1),74(a,1)),rewrite(216(10)),flip(c),xx(a)].

given #789 (T,wt=12): 1253 c1' ^ (c2 v x) != 0 | c2 v x = c1.  [para(171(a,1),74(a,1)),rewrite(216(13)),flip(c),xx(a)].

given #790 (T,wt=12): 1404 x' v (x ^ y) != 1 | x ^ y = x.  [para(82(a,1),86(b,1)),rewrite(216(10)),flip(c),xx(b)].

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

given #792 (F,wt=12): 1410 c2' v (c1 ^ x) != 1 | c1 ^ x = c2.  [para(133(a,1),86(b,1)),rewrite(216(13)),flip(c),xx(b)].

given #793 (F,wt=12): 2102 c1' ^ (x v c2) != 0 | x v c2 = c1.  [para(2066(a,1),10(a,1)),rewrite(216(13)),flip(c),xx(a)].

given #794 (T,wt=12): 2104 (x v c2) ^ c1' != 0 | x v c2 = c1.  [para(2066(a,1),38(a,1)),rewrite(216(13)),flip(c),xx(a)].

given #795 (T,wt=12): 2346 x ^ (y v x') != 0 | x' v y = x'.  [para(2(a,1),117(a,1,2))].

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

given #797 (F,wt=12): 2479 x v (y ^ x') != 1 | x' ^ y = x'.  [para(4(a,1),118(a,1,2))].

given #798 (F,wt=12): 2565 x ^ (x' v y) != 0 | y v x' = x'.  [para(2(a,1),119(a,1,2))].

given #799 (T,wt=12): 3063 x v (x' ^ y) != 1 | y ^ x' = x'.  [para(4(a,1),125(a,1,2))].

given #800 (T,wt=12): 3130 x v (y v x)' != 1 | (x v y)' = x'.  [para(2(a,1),130(a,1,2,1))].

given #801 (A,wt=13): 316 c2 != 1 | c1 ^ x != 0 | c2' = c1 ^ x.  [para(282(a,1),10(a,1)),rewrite(19(7),59(7))].

given #802 (F,wt=12): 3816 x v (x v y)' != 1 | (y v x)' = x'.  [para(2(a,1),144(a,1,2,1))].

given #803 (F,wt=12): 3865 c2 ^ c1' != 0 | c1 v (c2 ^ c1') = c1.  [back_rewrite(3402),rewrite(3833(14))].

given #804 (T,wt=12): 3919 c1 v (x ^ c2') != 1 | c2' ^ x = c1'.  [para(4(a,1),147(a,1,2))].

given #805 (T,wt=12): 3950 c1 v (c2' ^ x) != 1 | x ^ c2' = c1'.  [para(4(a,1),148(a,1,2))].

given #806 (A,wt=13): 319 c2 != 1 | c1 ^ x != 0 | (c1 ^ x)' = c2.  [para(282(a,1),36(a,1)),rewrite(4(7),19(7),59(7))].

given #807 (F,wt=12): 4480 x ^ (y ^ x)' != 0 | (x ^ y)' = x'.  [para(4(a,1),160(a,1,2,1))].

given #808 (F,wt=12): 4518 x ^ (x ^ y)' != 0 | (y ^ x)' = x'.  [para(4(a,1),165(a,1,2,1))].

given #809 (T,wt=12): 4665 c2 ^ (x v c1') != 0 | c2' = c1' v x.  [para(2(a,1),174(a,1,2))].

given #810 (T,wt=12): 4898 c1 v c2' != 1 | c2 ^ (c1 v c2') = c2.  [para(1706(a,1),176(b,1)),rewrite(2(4),216(12),2(15),4(17),2529(18)),flip(c),xx(b)].

given #811 (A,wt=17): 320 x v c2 != 1 | c1 ^ y != 0 | (x v c2)' = c1 ^ y.  [para(282(a,1),37(a,1,2)),rewrite(19(9),205(9))].

given #812 (F,wt=12): 4945 c2' v (x ^ c1) != 1 | x ^ c1 = c2.  [para(4940(a,1),10(b,1)),rewrite(216(13)),flip(c),xx(b)].

given #813 (F,wt=12): 4946 (x ^ c1) v c2' != 1 | x ^ c1 = c2.  [para(4940(a,1),36(b,1)),rewrite(216(13)),flip(c),xx(b)].

given #814 (T,wt=12): 5607 c2 ^ (c1' v x) != 0 | c2' = x v c1'.  [para(2(a,1),181(a,1,2))].

given #815 (T,wt=12): 6681 c1 v (x v c2)' != 1 | (c2 v x)' = c1'.  [para(2(a,1),209(a,1,2,1))].

given #816 (A,wt=16): 326 (x v c2) ^ (c1 ^ y)' != 0 | (x v c2)' = (c1 ^ y)'.  [para(288(a,1),37(a,1,2)),rewrite(88(2)),xx(a)].

given #817 (F,wt=12): 6963 x' ^ (y v x) != 0 | (y v x)' = x'.  [para(231(a,1),213(a,1)),xx(a)].

given #818 (F,wt=12): 6964 x' v (y ^ x) != 1 | (y ^ x)' = x'.  [para(232(a,1),213(b,1)),xx(b)].

given #819 (T,wt=12): 6966 c1' ^ (x v c2) != 0 | (x v c2)' = c1'.  [para(2066(a,1),213(a,1)),xx(a)].

given #820 (T,wt=12): 6995 c2' v (x ^ c1) != 1 | (x ^ c1)' = c2'.  [para(4940(a,1),213(b,1)),xx(b)].

given #821 (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 #822 (F,wt=12): 7208 x' v (x ^ y) != 1 | (x ^ y)' = x'.  [para(92(a,1),214(b,1)),xx(b)].

Low Water (keep): wt=24, part=0.71, limit=24

given #823 (F,wt=12): 7212 c2' v (c1 ^ x) != 1 | (c1 ^ x)' = c2'.  [para(135(a,1),214(b,1)),xx(b)].

given #824 (T,wt=12): 7927 (x ^ y) v x' != 1 | x ^ y = x.  [para(82(a,1),218(b,1)),rewrite(216(10)),flip(c),xx(b)].

given #825 (T,wt=12): 7929 (c1 ^ x) v c2' != 1 | c1 ^ x = c2.  [para(133(a,1),218(b,1)),rewrite(216(13)),flip(c),xx(b)].

given #826 (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 #827 (F,wt=12): 8213 x ^ (y v x') != 0 | (x' v y)' = x.  [para(2(a,1),221(a,1,2))].

given #828 (F,wt=12): 8215 x' ^ (x v y) != 0 | (x v y)' = x'.  [para(216(a,1),221(a,1,2,1)),rewrite(216(7))].

given #829 (T,wt=12): 8277 x ^ (x' v y) != 0 | (y v x')' = x.  [para(2(a,1),222(a,1,2))].

given #830 (T,wt=12): 8546 x ^ (y ^ x)' != 0 | x ^ y = x.  [para(4(a,1),224(a,1,2,1))].

given #831 (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),100(3))].

given #832 (F,wt=12): 8674 x ^ (x ^ y)' != 0 | y ^ x = x.  [para(4(a,1),225(a,1,2,1))].

given #833 (F,wt=12): 8675 (x v y) ^ x' != 0 | x v y = x.  [para(6(a,1),225(a,1,2,1)),rewrite(6(7)),flip(b)].

given #834 (T,wt=12): 8678 (c2 v x) ^ c1' != 0 | c2 v x = c1.  [para(191(a,1),225(a,1,2,1)),rewrite(191(11)),flip(b)].

given #835 (T,wt=12): 8772 c2 ^ (x v c1') != 0 | (c1' v x)' = c2.  [para(2(a,1),227(a,1,2))].

given #836 (A,wt=17): 330 x ^ y != 1 | x ^ y != 0 | (x ^ y)' = x ^ y.  [para(29(a,1),39(a,1)),rewrite(63(5),62(5))].

given #837 (F,wt=12): 8950 c1 v c2' != 1 | (c2 ^ (c1 v c2'))' = c2'.  [para(1706(a,1),228(b,1)),rewrite(2(4),2(14),4(16),2529(17)),xx(b)].

given #838 (F,wt=12): 9189 c2 ^ (c1' v x) != 0 | (x v c1')' = c2.  [para(2(a,1),229(a,1,2))].

given #839 (T,wt=12): 9395 c1 v (c2 v x)' != 1 | (x v c2)' = c1'.  [para(2(a,1),235(a,1,2,1))].

given #840 (T,wt=12): 9518 x' ^ (x v y) != 0 | y v x = x.  [para(2(a,1),237(a,1,2))].

given #841 (A,wt=25): 332 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 #842 (F,wt=12): 9757 (x v y) ^ x' != 0 | (y v x)' = x'.  [para(2(a,1),239(a,1,1))].

given #843 (F,wt=12): 9974 x' v (x ^ y) != 1 | y ^ x = x.  [para(4(a,1),240(a,1,2))].

given #844 (T,wt=12): 10255 (x ^ y) v x' != 1 | y ^ x = x.  [para(4(a,1),242(a,1,1))].

given #845 (T,wt=12): 10665 (x v y) ^ y' != 0 | (y v x)' = y'.  [para(89(a,1),244(a,1)),xx(a)].

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

given #847 (F,wt=12): 10671 (c2 v x) ^ c1' != 0 | (x v c2)' = c1'.  [para(166(a,1),244(a,1,2)),rewrite(88(2)),xx(a)].

given #848 (F,wt=12): 10676 (x v c2) ^ c1' != 0 | (c2 v x)' = c1'.  [para(173(a,1),244(a,1)),xx(a)].

given #849 (T,wt=12): 11208 c1' ^ (c2 v x) != 0 | (c2 v x)' = c1'.  [para(173(a,1),245(a,1)),xx(a)].

given #850 (T,wt=12): 15281 c2 ^ (c1 ^ x)' != 0 | (x ^ c1)' = c2'.  [para(4(a,1),290(a,1,2,1))].

given #851 (A,wt=20): 336 x ^ (y ^ ((x ^ y)' v z)) != 0 | (x ^ y)' v z = (x ^ y)'.  [para(79(a,1),39(a,1)),flip(c),xx(a)].

given #852 (F,wt=12): 15386 c2 ^ (c1 ^ x)' != 0 | x ^ c1 = c2.  [para(4(a,1),292(a,1,2,1))].

given #853 (F,wt=12): 16353 x v (y ^ x') != 1 | (x' ^ y)' = x.  [para(4(a,1),298(a,1,2))].

given #854 (T,wt=12): 16512 x v (x' ^ y) != 1 | (y ^ x')' = x.  [para(4(a,1),300(a,1,2))].

given #855 (T,wt=12): 16571 x v (y v x)' != 1 | x v y = x.  [para(2(a,1),301(a,1,2,1))].

given #856 (A,wt=16): 337 (x ^ y) v (y' ^ z) != 1 | (x ^ y)' = y' ^ z.  [para(82(a,1),39(b,1,2)),rewrite(91(8)),xx(b)].

given #857 (F,wt=12): 16626 c2 ^ c1' != 0 | (c1 v (c2 ^ c1'))' = c1'.  [para(1524(a,1),303(a,1)),rewrite(4(7),4(14),2(16),3833(17)),xx(a)].

given #858 (F,wt=12): 16874 x v (x v y)' != 1 | y v x = x.  [para(2(a,1),304(a,1,2,1))].

given #859 (T,wt=12): 16918 c1 v (x ^ c2') != 1 | (c2' ^ x)' = c1.  [para(4(a,1),305(a,1,2))].

given #860 (T,wt=12): 16981 c1 v (c2' ^ x) != 1 | (x ^ c2')' = c1.  [para(4(a,1),306(a,1,2))].

given #861 (A,wt=20): 338 x ^ (y ^ (z v (x ^ y)')) != 0 | z v (x ^ y)' = (x ^ y)'.  [para(89(a,1),39(a,1)),flip(c),xx(a)].

given #862 (F,wt=12): 16982 c1 v (x v c2)' != 1 | c2 v x = c1.  [para(2(a,1),311(a,1,2,1))].

given #863 (F,wt=12): 16984 c1 v (c2 v x)' != 1 | x v c2 = c1.  [para(2(a,1),312(a,1,2,1))].

given #864 (T,wt=12): 16986 (x v y) ^ x' != 0 | y v x = x.  [para(2(a,1),313(a,1,1))].

given #865 (T,wt=12): 16988 (x ^ y) v x' != 1 | (y ^ x)' = x'.  [para(4(a,1),314(a,1,1))].

given #866 (A,wt=27): 339 (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 #867 (F,wt=12): 17003 c2 ^ (x ^ c1)' != 0 | (c1 ^ x)' = c2'.  [para(4(a,1),322(a,1,2,1))].

given #868 (F,wt=12): 17005 c2 ^ (x ^ c1)' != 0 | c1 ^ x = c2.  [para(4(a,1),325(a,1,2,1))].

given #869 (T,wt=12): 17007 (x ^ y) v y' != 1 | (y ^ x)' = y'.  [para(4(a,1),341(a,1,1))].

given #870 (T,wt=12): 17009 (c1 ^ x) v c2' != 1 | (x ^ c1)' = c2'.  [para(4(a,1),343(a,1,1))].

given #871 (A,wt=16): 340 (x ^ y) v (z ^ y') != 1 | (x ^ y)' = z ^ y'.  [para(92(a,1),39(b,1,2)),rewrite(91(8)),xx(b)].

given #872 (F,wt=12): 17015 (x ^ c1) v c2' != 1 | (c1 ^ x)' = c2'.  [para(4(a,1),349(a,1,1))].

given #873 (F,wt=12): 17017 x' ^ (y v x) != 0 | x v y = x.  [para(2(a,1),1248(a,1,2))].

given #874 (T,wt=12): 17023 c1' ^ (x v c2) != 0 | c2 v x = c1.  [para(2(a,1),1253(a,1,2))].

given #875 (T,wt=12): 17028 x' v (y ^ x) != 1 | x ^ y = x.  [para(4(a,1),1404(a,1,2))].

given #876 (A,wt=16): 342 (x ^ y) v (y v z)' != 1 | (y v z)' = (x ^ y)'.  [para(120(a,1),39(b,1,2)),rewrite(91(8)),flip(c),xx(b)].

given #877 (F,wt=12): 17032 c2' v (x ^ c1) != 1 | c1 ^ x = c2.  [para(4(a,1),1410(a,1,2))].

given #878 (F,wt=12): 17034 c1' ^ (c2 v x) != 0 | x v c2 = c1.  [para(2(a,1),2102(a,1,2))].

given #879 (T,wt=12): 17036 (c2 v x) ^ c1' != 0 | x v c2 = c1.  [para(2(a,1),2104(a,1,1))].

given #880 (T,wt=12): 17061 c2' v (c1 ^ x) != 1 | x ^ c1 = c2.  [para(4(a,1),4945(a,1,2))].

given #881 (A,wt=31): 344 (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 #882 (F,wt=12): 17063 (c1 ^ x) v c2' != 1 | x ^ c1 = c2.  [para(4(a,1),4946(a,1,1))].

given #883 (F,wt=12): 17070 x' ^ (x v y) != 0 | (y v x)' = x'.  [para(2(a,1),6963(a,1,2))].

given #884 (T,wt=12): 17073 x' v (x ^ y) != 1 | (y ^ x)' = x'.  [para(4(a,1),6964(a,1,2))].

given #885 (T,wt=12): 17076 c1' ^ (c2 v x) != 0 | (x v c2)' = c1'.  [para(2(a,1),6966(a,1,2))].

given #886 (A,wt=21): 345 (x ^ y) v z != 1 | x ^ y != 0 | (x ^ y)' = (x ^ y) v z.  [para(23(a,1),39(b,1)),rewrite(66(4))].

given #887 (F,wt=12): 17078 c2' v (c1 ^ x) != 1 | (x ^ c1)' = c2'.  [para(4(a,1),6995(a,1,2))].

given #888 (F,wt=12): 17419 x' v (y ^ x) != 1 | (x ^ y)' = x'.  [para(4(a,1),7208(a,1,2))].

given #889 (T,wt=12): 17422 c2' v (x ^ c1) != 1 | (c1 ^ x)' = c2'.  [para(4(a,1),7212(a,1,2))].

given #890 (T,wt=12): 17424 (x ^ y) v y' != 1 | y ^ x = y.  [para(4(a,1),7927(a,1,1))].

given #891 (A,wt=16): 346 (x ^ y) v (z v y)' != 1 | (z v y)' = (x ^ y)'.  [para(127(a,1),39(b,1,2)),rewrite(91(8)),flip(c),xx(b)].

given #892 (F,wt=12): 17426 (x ^ c1) v c2' != 1 | c1 ^ x = c2.  [para(4(a,1),7929(a,1,1))].

given #893 (F,wt=12): 17523 x' ^ (y v x) != 0 | (x v y)' = x'.  [para(216(a,1),8213(a,1,2,2)),rewrite(216(7))].

given #894 (T,wt=12): 17614 (x v y) ^ y' != 0 | y v x = y.  [para(2(a,1),8675(a,1,1))].

given #895 (T,wt=12): 17616 (x v c2) ^ c1' != 0 | c2 v x = c1.  [para(2(a,1),8678(a,1,1))].

given #896 (A,wt=16): 347 (x ^ c1) v (c2' ^ y) != 1 | (x ^ c1)' = c2' ^ y.  [para(133(a,1),39(b,1,2)),rewrite(91(10)),xx(b)].

given #897 (F,wt=12): 17686 c1' ^ (x v c2) != 0 | (c2 v x)' = c1'.  [para(4(a,1),10676(a,1))].

given #898 (F,wt=13): 368 1 != x | y ^ x != 0 | (x ^ y)' = x.  [para(63(a,1),39(b,1)),rewrite(2(2),7(2)),flip(a)].

given #899 (T,wt=13): 372 x v y != 1 | 0 != y | (y v x)' = y.  [para(67(a,1),37(a,1)),rewrite(4(5),6(5)),flip(b)].

given #900 (T,wt=13): 436 x ^ (y ^ (z v (x v u))) = y ^ x.  [para(71(a,1),19(a,1,2)),flip(a)].

given #901 (A,wt=16): 348 (x ^ c1) v (y ^ c2') != 1 | (x ^ c1)' = y ^ c2'.  [para(135(a,1),39(b,1,2)),rewrite(91(10)),xx(b)].

given #902 (F,wt=13): 437 x v (y v (z ^ (x ^ u))) = y v x.  [para(84(a,1),17(a,1,2)),flip(a)].

given #903 (F,wt=13): 444 c2 != 1 | x ^ c1 != 0 | (c1 ^ x)' = c2.  [para(87(a,1),39(b,1)),rewrite(2(4),282(4))].

given #904 (T,wt=13): 445 x ^ ((y v (z v x)) ^ u) = x ^ u.  [para(94(a,1),5(a,1,1)),flip(a)].

given #905 (T,wt=13): 447 x ^ (y ^ (z v (u v x))) = y ^ x.  [para(94(a,1),19(a,1,2)),flip(a)].

given #906 (A,wt=31): 350 (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 #907 (F,wt=13): 483 x v ((y ^ (z ^ x)) v u) = x v u.  [para(102(a,1),3(a,1,1)),flip(a)].

given #908 (F,wt=13): 485 x v (y v (z ^ (u ^ x))) = y v x.  [para(102(a,1),17(a,1,2)),flip(a)].

given #909 (T,wt=13): 488 (c2 ^ x) v (y ^ (c1 ^ x)) = c2 ^ x.  [para(59(a,1),102(a,1,2,2))].

given #910 (T,wt=13): 489 (x ^ c2) v (y ^ (x ^ c1)) = x ^ c2.  [para(87(a,1),102(a,1,2,2))].

given #911 (A,wt=20): 351 x ^ (y ^ (x ^ (y ^ z))') != 0 | (x ^ (y ^ z))' = (x ^ y)'.  [para(150(a,1),39(a,1)),rewrite(5(5),5(14)),flip(c),xx(a)].

given #912 (F,wt=13): 492 (x v c1) ^ (x v (c2 v y)) = x v c1.  [para(112(a,1),21(a,1,2,2))].

given #913 (F,wt=13): 500 x v c2 != 1 | c1 != 0 | (c2 v x)' = c1.  [para(113(a,1),37(a,1)),rewrite(4(8),191(8))].

given #914 (T,wt=13): 502 (x v c1) ^ (y v (x v c2)) = x v c1.  [para(113(a,1),94(a,1,2,2))].

given #915 (T,wt=13): 612 (x v c1) ^ (x v (y v c2)) = x v c1.  [para(114(a,1),21(a,1,2,2))].

given #916 (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 #917 (F,wt=13): 618 (x v y) ^ ((x v (y v z))' ^ u) = 0.  [para(3(a,1),124(a,1,2,1,1))].

given #918 (F,wt=13): 625 (x v y) ^ (z ^ (x v (y v u))') = 0.  [para(3(a,1),126(a,1,2,2,1))].

given #919 (T,wt=13): 633 x ^ (y ^ (z v ((x ^ y) v u))') = 0.  [para(131(a,1),5(a,1)),flip(a)].

given #920 (T,wt=13): 717 x ^ (y ^ (z v (u v (x ^ y)))') = 0.  [para(141(a,1),5(a,1)),flip(a)].

given #921 (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 #922 (F,wt=13): 720 ((x ^ y) v z) ^ (u v (x v z))' = 0.  [para(24(a,1),141(a,1,2,1,2))].

given #923 (F,wt=13): 725 (x v y) ^ ((x v (z v y))' ^ u) = 0.  [para(17(a,1),142(a,1,2,1,1))].

given #924 (T,wt=13): 726 ((x ^ y) v z) ^ ((x v z)' ^ u) = 0.  [para(24(a,1),142(a,1,2,1,1))].

given #925 (T,wt=13): 733 (x v y) ^ (z ^ (x v (u v y))') = 0.  [para(17(a,1),146(a,1,2,2,1))].

given #926 (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 #927 (F,wt=13): 734 ((x ^ y) v z) ^ (u ^ (x v z)') = 0.  [para(24(a,1),146(a,1,2,2,1))].

given #928 (F,wt=13): 741 (x ^ y) v ((x ^ (y ^ z))' v u) = 1.  [para(5(a,1),154(a,1,2,1,1))].

given #929 (T,wt=13): 773 (x ^ y) v (z v (x ^ (y ^ u))') = 1.  [para(5(a,1),155(a,1,2,2,1))].

given #930 (T,wt=13): 783 x v (y v (z ^ ((x v y) ^ u))') = 1.  [para(161(a,1),3(a,1)),flip(a)].

given #931 (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(91(9)),xx(b)].

given #932 (F,wt=13): 792 (x ^ y) v ((x ^ (z ^ y))' v u) = 1.  [para(19(a,1),162(a,1,2,1,1))].

given #933 (F,wt=13): 793 ((x v y) ^ z) v ((x ^ z)' v u) = 1.  [para(22(a,1),162(a,1,2,1,1))].

given #934 (T,wt=13): 805 x v (y v (z ^ (u ^ (x v y)))') = 1.  [para(164(a,1),3(a,1)),flip(a)].

given #935 (T,wt=13): 808 ((x v y) ^ z) v (u ^ (x ^ z))' = 1.  [para(22(a,1),164(a,1,2,1,2))].

given #936 (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 #937 (F,wt=13): 929 (x ^ y) v (z v (x ^ (u ^ y))') = 1.  [para(19(a,1),167(a,1,2,2,1))].

given #938 (F,wt=13): 930 ((x v y) ^ z) v (u v (x ^ z)') = 1.  [para(22(a,1),167(a,1,2,2,1))].

given #939 (T,wt=13): 965 (x ^ (c2 ^ y)) v (c1 ^ (x ^ y))' = 1.  [para(19(a,1),199(a,1,1))].

given #940 (T,wt=13): 966 (c2 ^ (x ^ y)) v (x ^ (c1 ^ y))' = 1.  [para(19(a,1),199(a,1,2,1))].

given #941 (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 #942 (F,wt=13): 968 (c2 ^ ((c1 v x) ^ y)) v (c1 ^ y)' = 1.  [para(22(a,1),199(a,1,2,1))].

given #943 (F,wt=13): 1068 c1 ^ ((x v (c2 v y)) ^ z) = c1 ^ z.  [para(202(a,1),5(a,1,1)),flip(a)].

given #944 (T,wt=13): 1069 c1 ^ (x ^ (y v (c2 v z))) = x ^ c1.  [para(202(a,1),19(a,1,2)),flip(a)].

given #945 (T,wt=13): 1070 c1 ^ ((x v (y v c2)) ^ z) = c1 ^ z.  [para(204(a,1),5(a,1,1)),flip(a)].

given #946 (A,wt=16): 359 (x ^ c1) v (c2 v y)' != 1 | (c2 v y)' = (x ^ c1)'.  [para(196(a,1),39(b,1,2)),rewrite(91(10)),flip(c),xx(b)].

given #947 (F,wt=13): 1071 c1 ^ (x ^ (y v (z v c2))) = x ^ c1.  [para(204(a,1),19(a,1,2)),flip(a)].

given #948 (F,wt=13): 1081 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): 1092 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): 1145 1 != x | y ^ x != 0 | x' = x ^ y.  [para(4(a,1),65(b,1))].

given #951 (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(91(10)),flip(c),xx(b)].

given #952 (F,wt=13): 1150 c1 != 1 | c1 ^ x != 0 | c1' = c1 ^ x.  [para(59(a,1),65(b,1)),rewrite(59(13)),flip(a)].

given #953 (F,wt=13): 1152 c1 != 1 | x ^ c1 != 0 | c1' = x ^ c1.  [para(87(a,1),65(b,1)),rewrite(87(13)),flip(a)].

given #954 (T,wt=13): 1163 x v y != 1 | 0 != y | y' = y v x.  [para(2(a,1),68(a,1))].

given #955 (T,wt=13): 1169 c2 v ((x ^ (y ^ c1)) v z) = c2 v z.  [para(283(a,1),3(a,1,1)),flip(a)].

given #956 (A,wt=16): 361 (x ^ y') v (z ^ y) != 1 | (x ^ y')' = z ^ y.  [para(232(a,1),39(b,1,2)),rewrite(91(8)),xx(b)].

given #957 (F,wt=13): 1170 c2 v (x v (y ^ (z ^ c1))) = x v c2.  [para(283(a,1),17(a,1,2)),flip(a)].

given #958 (F,wt=13): 1193 (x v (y ^ z)) ^ (u v (x v y))' = 0.  [para(72(a,1),141(a,1,2,1,2))].

given #959 (T,wt=13): 1194 (x v (y ^ z)) ^ ((x v y)' ^ u) = 0.  [para(72(a,1),142(a,1,2,1,1))].

given #960 (T,wt=13): 1195 (x v (y ^ z)) ^ (u ^ (x v y)') = 0.  [para(72(a,1),146(a,1,2,2,1))].

given #961 (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 #962 (F,wt=13): 1236 c2 v ((x ^ (c1 ^ y)) v z) = c2 v z.  [para(318(a,1),3(a,1,1)),flip(a)].

given #963 (F,wt=13): 1237 c2 v (x v (y ^ (c1 ^ z))) = x v c2.  [para(318(a,1),17(a,1,2)),flip(a)].

given #964 (T,wt=13): 1326 (x ^ (y ^ c2)) v (c1 ^ (x ^ y))' = 1.  [para(5(a,1),440(a,1,1)),rewrite(4(6))].

given #965 (T,wt=13): 1327 (c2 ^ (x ^ y)) v (x ^ (y ^ c1))' = 1.  [para(5(a,1),440(a,1,2,1)),rewrite(4(3))].

given #966 (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 #967 (F,wt=13): 1346 (x ^ (y v z)) v ((x ^ y)' v u) = 1.  [para(83(a,1),162(a,1,2,1,1))].

given #968 (F,wt=13): 1347 (x ^ (y v z)) v (u ^ (x ^ y))' = 1.  [para(83(a,1),164(a,1,2,1,2))].

given #969 (T,wt=13): 1348 (x ^ (y v z)) v (u v (x ^ y)') = 1.  [para(83(a,1),167(a,1,2,2,1))].

given #970 (T,wt=13): 1349 (c2 ^ (x ^ (c1 v y))) v (x ^ c1)' = 1.  [para(83(a,1),199(a,1,2,1))].

given #971 (A,wt=23): 364 (x ^ y) v (y ^ z) != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = y ^ z.  [para(62(a,1),39(b,1,2))].

given #972 (F,wt=13): 1363 (x v c1) ^ (y v (c2 v x)) = x v c1.  [para(495(a,1),94(a,1,2,2))].

given #973 (F,wt=13): 1375 c2 v x != 1 | c2 != 0 | c2' = c2 v x.  [para(495(a,1),68(a,1)),rewrite(495(13)),flip(b)].

given #974 (T,wt=13): 1378 (x v (y v c1)) ^ (c2 v (x v y))' = 0.  [para(3(a,1),497(a,1,1)),rewrite(2(6))].

given #975 (T,wt=13): 1379 (c1 v (x v y)) ^ (x v (y v c2))' = 0.  [para(3(a,1),497(a,1,2,1)),rewrite(2(3))].

given #976 (A,wt=21): 366 x v y != 1 | z ^ (x v y) != 0 | (x v y)' = z ^ (x v y).  [para(63(a,1),37(b,1)),rewrite(101(4))].

given #977 (F,wt=13): 1513 ((x v y) ^ z) v ((y ^ z)' v u) = 1.  [para(95(a,1),162(a,1,2,1,1))].

given #978 (F,wt=13): 1514 ((x v y) ^ z) v (u ^ (y ^ z))' = 1.  [para(95(a,1),164(a,1,2,1,2))].

given #979 (T,wt=13): 1516 ((x v y) ^ z) v (u v (y ^ z)') = 1.  [para(95(a,1),167(a,1,2,2,1))].

given #980 (T,wt=13): 1518 (c2 ^ ((x v c1) ^ y)) v (c1 ^ y)' = 1.  [para(95(a,1),199(a,1,2,1))].

Low Water (keep): wt=23, part=0.58, limit=23

given #981 (A,wt=23): 367 (x ^ y) v (z ^ y) != 1 | x ^ (z ^ y) != 0 | (x ^ y)' = z ^ y.  [para(63(a,1),39(b,1,2))].

given #982 (F,wt=13): 1549 x ^ (y ^ (z v (y ^ x))) = x ^ y.  [para(4(a,1),96(a,1,2,2,2))].

given #983 (F,wt=13): 1553 (x ^ (y v (z ^ x))) v (z ^ x)' = 1.  [para(96(a,1),158(a,1,2,1))].

given #984 (T,wt=13): 1554 c1 ^ (x ^ (y v (c2 ^ x))) = c1 ^ x.  [para(96(a,1),59(a,1,2)),rewrite(59(4)),flip(a)].

given #985 (T,wt=13): 1555 x ^ (y ^ (y ^ (z v (x ^ y)))') = 0.  [para(96(a,1),232(a,1,2)),rewrite(4(6),5(6))].

given #986 (A,wt=23): 369 x v (y v z) != 1 | (x v y) ^ (y v z) != 0 | (x v y)' = y v z.  [para(66(a,1),37(a,1,2))].

given #987 (F,wt=13): 1576 (c1 v (x v y)) ^ (x v (c2 v y))' = 0.  [para(17(a,1),1359(a,1,2,1)),rewrite(2(3))].

given #988 (F,wt=13): 1578 (c1 v ((c2 ^ x) v y)) ^ (c2 v y)' = 0.  [para(24(a,1),1359(a,1,2,1)),rewrite(2(5))].

given #989 (T,wt=13): 1584 (c1 v (x v (c2 ^ y))) ^ (x v c2)' = 0.  [para(72(a,1),1359(a,1,2,1)),rewrite(2(5))].

given #990 (T,wt=13): 1600 (x v (c1 v y)) ^ (c2 v (x v y))' = 0.  [para(17(a,1),1377(a,1,1)),rewrite(2(6))].

given #991 (A,wt=23): 371 x v (y v z) != 1 | (x v z) ^ (y v z) != 0 | (x v z)' = y v z.  [para(67(a,1),37(a,1,2))].

given #992 (F,wt=13): 1607 x v y != 1 | 0 != x | x' = y v x.  [para(2(a,1),97(a,1))].

given #993 (F,wt=13): 1652 (x v y) ^ (z v (y v x)) = x v y.  [para(2(a,1),98(a,1,2)),rewrite(3(3))].

given #994 (T,wt=13): 1725 (x ^ (y v z)) v ((x ^ z)' v u) = 1.  [para(99(a,1),162(a,1,2,1,1))].

given #995 (T,wt=13): 1726 (x ^ (y v z)) v (u ^ (x ^ z))' = 1.  [para(99(a,1),164(a,1,2,1,2))].

given #996 (A,wt=21): 373 x v (y ^ z) != 1 | y ^ z != 0 | (y ^ z)' = x v (y ^ z).  [para(67(a,1),39(a,1)),rewrite(96(8))].

Low Water (keep): wt=21, part=0.56, limit=21

given #997 (F,wt=13): 1727 (x ^ (y v z)) v (u v (x ^ z)') = 1.  [para(99(a,1),167(a,1,2,2,1))].

given #998 (F,wt=13): 1728 (c2 ^ (x ^ (y v c1))) v (x ^ c1)' = 1.  [para(99(a,1),199(a,1,2,1))].

given #999 (T,wt=13): 1792 ((x ^ y) v z) ^ (u v (y v z))' = 0.  [para(100(a,1),141(a,1,2,1,2))].

given #1000 (T,wt=13): 1793 ((x ^ y) v z) ^ ((y v z)' ^ u) = 0.  [para(100(a,1),142(a,1,2,1,1))].

given #1001 (A,wt=23): 374 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 #1002 (F,wt=13): 1794 ((x ^ y) v z) ^ (u ^ (y v z)') = 0.  [para(100(a,1),146(a,1,2,2,1))].

given #1003 (F,wt=13): 1806 (c1 v ((x ^ c2) v y)) ^ (c2 v y)' = 0.  [para(100(a,1),1359(a,1,2,1)),rewrite(2(5))].

given #1004 (T,wt=13): 1843 x v (y v (z ^ (y v x))) = x v y.  [para(2(a,1),101(a,1,2,2,2))].

given #1005 (T,wt=13): 1846 (x v (y ^ (z v x))) ^ (z v x)' = 0.  [para(101(a,1),127(a,1,2,1))].

given #1006 (A,wt=29): 375 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 #1007 (F,wt=13): 1849 x v (y v (y v (z ^ (x v y)))') = 1.  [para(101(a,1),231(a,1,2)),rewrite(2(6),3(6))].

given #1008 (F,wt=13): 1886 1 != x | x ^ y != 0 | x' = y ^ x.  [para(4(a,1),103(b,1))].

given #1009 (T,wt=13): 1938 (x v (y ^ z)) ^ (u v (x v z))' = 0.  [para(105(a,1),141(a,1,2,1,2))].

given #1010 (T,wt=13): 1939 (x v (y ^ z)) ^ ((x v z)' ^ u) = 0.  [para(105(a,1),142(a,1,2,1,1))].

given #1011 (A,wt=31): 376 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 #1012 (F,wt=13): 1940 (x v (y ^ z)) ^ (u ^ (x v z)') = 0.  [para(105(a,1),146(a,1,2,2,1))].

given #1013 (F,wt=13): 1950 (c1 v (x v (y ^ c2))) ^ (x v c2)' = 0.  [para(105(a,1),1359(a,1,2,1)),rewrite(2(5))].

given #1014 (T,wt=13): 1967 (x ^ y) v (z ^ (y ^ x)) = x ^ y.  [para(4(a,1),106(a,1,2)),rewrite(5(3))].

Low Water (keep): wt=20, part=0.53, limit=20

given #1015 (T,wt=13): 2012 (x v (y v z)) ^ (y v x) = x v y.  [para(108(a,1),4(a,1)),flip(a)].

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

given #1017 (F,wt=13): 2016 (c1 v x) ^ (x v (c2 v y)) = x v c1.  [para(112(a,1),108(a,1,2,2))].

given #1018 (F,wt=13): 2017 (c1 v x) ^ (x v (y v c2)) = x v c1.  [para(114(a,1),108(a,1,2,2))].

given #1019 (T,wt=13): 2041 x v (c2 v (y ^ (x v c1))) = x v c2.  [para(115(a,1),102(a,1,2,2)),rewrite(3(6))].

given #1020 (T,wt=13): 2058 (x v (y v z)) ^ (z v x) = z v x.  [para(109(a,1),4(a,1)),flip(a)].

given #1021 (A,wt=23): 378 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 #1022 (F,wt=13): 2112 (x v (y v z)) ^ (z v (x v y))' = 0.  [para(3(a,1),2055(a,1,1))].

given #1023 (F,wt=13): 2113 (x v (y v z)) ^ (y v (z v x))' = 0.  [para(3(a,1),2055(a,1,2,1))].

given #1024 (T,wt=13): 2115 (x v (y v z)) ^ (x v (z v y))' = 0.  [para(17(a,1),2055(a,1,1)),rewrite(3(4))].

given #1025 (T,wt=13): 2119 (x ^ (y ^ z))' v (u v (x ^ y)) = 1.  [para(5(a,1),2064(a,1,1,1))].

given #1026 (A,wt=27): 379 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 #1027 (F,wt=13): 2121 x v (y v (((x ^ z) v y) ^ u)') = 1.  [para(24(a,1),2064(a,1,2)),rewrite(2(6),3(6))].

given #1028 (F,wt=13): 2132 x v (y v ((x v (y ^ z)) ^ u)') = 1.  [para(72(a,1),2064(a,1,2)),rewrite(2(6),3(6))].

given #1029 (T,wt=13): 2135 x v (y v (((z ^ x) v y) ^ u)') = 1.  [para(100(a,1),2064(a,1,2)),rewrite(2(6),3(6))].

given #1030 (T,wt=13): 2137 x v (y v ((x v (z ^ y)) ^ u)') = 1.  [para(105(a,1),2064(a,1,2)),rewrite(2(6),3(6))].

given #1031 (A,wt=29): 380 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 #1032 (F,wt=13): 2139 (x ^ (y ^ z))' v (u v (x ^ z)) = 1.  [para(19(a,1),2065(a,1,1,1))].

given #1033 (F,wt=13): 2140 (x ^ y)' v (z v ((x v u) ^ y)) = 1.  [para(22(a,1),2065(a,1,1,1))].

given #1034 (T,wt=13): 2142 x v (y v (z ^ ((x ^ u) v y))') = 1.  [para(24(a,1),2065(a,1,2)),rewrite(2(6),3(6))].

given #1035 (T,wt=13): 2153 x v (y v (z ^ (x v (y ^ u)))') = 1.  [para(72(a,1),2065(a,1,2)),rewrite(2(6),3(6))].

given #1036 (A,wt=31): 381 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 #1037 (F,wt=13): 2155 (x ^ y)' v (z v (x ^ (y v u))) = 1.  [para(83(a,1),2065(a,1,1,1))].

given #1038 (F,wt=13): 2157 (x ^ y)' v (z v ((u v x) ^ y)) = 1.  [para(95(a,1),2065(a,1,1,1))].

given #1039 (T,wt=13): 2159 (x ^ y)' v (z v (x ^ (u v y))) = 1.  [para(99(a,1),2065(a,1,1,1))].

Low Water (displace): id=11651, wt=59

Low Water (displace): id=11843, wt=53

Low Water (displace): id=12208, wt=51

Low Water (displace): id=12370, wt=49

given #1040 (T,wt=13): 2160 x v (y v (z ^ ((u ^ x) v y))') = 1.  [para(100(a,1),2065(a,1,2)),rewrite(2(6),3(6))].

Low Water (displace): id=12216, wt=47

Low Water (displace): id=12721, wt=45

Low Water (displace): id=12988, wt=43

Low Water (displace): id=13099, wt=41

Low Water (displace): id=12734, wt=40

Low Water (displace): id=13217, wt=39

given #1041 (A,wt=27): 382 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 #1042 (F,wt=13): 2162 x v (y v (z ^ (x v (u ^ y)))') = 1.  [para(105(a,1),2065(a,1,2)),rewrite(2(6),3(6))].

Low Water (displace): id=12511, wt=38

Low Water (displace): id=13433, wt=37

Low Water (displace): id=13674, wt=36

given #1043 (F,wt=13): 2210 x ^ (y ^ (((x v z) ^ y) v u)') = 0.  [para(129(a,1),22(a,1,2)),rewrite(91(2)),flip(a)].

given #1044 (T,wt=13): 2220 x ^ (y ^ (((z v x) ^ y) v u)') = 0.  [para(129(a,1),95(a,1,2)),rewrite(91(2)),flip(a)].

Low Water (displace): id=13744, wt=35

given #1045 (T,wt=13): 2225 x ^ (y ^ (z v ((x v u) ^ y))') = 0.  [para(143(a,1),22(a,1,2)),rewrite(91(2)),flip(a)].

given #1046 (A,wt=21): 383 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 #1047 (F,wt=13): 2235 x ^ (y ^ (z v ((u v x) ^ y))') = 0.  [para(143(a,1),95(a,1,2)),rewrite(91(2)),flip(a)].

Low Water (displace): id=14045, wt=33

given #1048 (F,wt=13): 2259 (x v ((x v y) ^ z)) ^ (x v y)' = 0.  [para(25(a,1),145(a,1,2,1))].

given #1049 (T,wt=13): 2265 (x v (y ^ (z ^ u))) ^ (x v z)' = 0.  [para(84(a,1),145(a,1,2,1,2))].

Low Water (displace): id=14301, wt=32

given #1050 (T,wt=13): 2266 (x v (y ^ (z ^ u))) ^ (x v u)' = 0.  [para(102(a,1),145(a,1,2,1,2))].

given #1051 (A,wt=39): 384 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))].

given #1052 (F,wt=13): 2268 (x v (y ^ (z ^ c1))) ^ (x v c2)' = 0.  [para(283(a,1),145(a,1,2,1,2))].

given #1053 (F,wt=13): 2270 (x v (y ^ (c1 ^ z))) ^ (x v c2)' = 0.  [para(318(a,1),145(a,1,2,1,2))].

given #1054 (T,wt=13): 2271 (x v (y v c1)) ^ (x v (c2 v y))' = 0.  [para(495(a,1),145(a,1,2,1,2))].

given #1055 (T,wt=13): 2275 (x v (y ^ (x v z))) ^ (x v z)' = 0.  [para(101(a,1),145(a,1,2,1))].

given #1056 (A,wt=23): 385 (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(71(8))].

given #1057 (F,wt=13): 2288 ((x ^ (y ^ z)) v u) ^ (y v u)' = 0.  [para(19(a,1),156(a,1,1,1))].

given #1058 (F,wt=13): 2300 ((x ^ y) v (z ^ (x ^ u))) ^ x' = 0.  [para(84(a,1),156(a,1,2,1))].

Low Water (displace): id=14578, wt=31

given #1059 (T,wt=13): 2301 ((x ^ y) v (z ^ (u ^ x))) ^ x' = 0.  [para(102(a,1),156(a,1,2,1))].

given #1060 (T,wt=13): 2304 ((c2 ^ x) v (y ^ (z ^ c1))) ^ c2' = 0.  [para(283(a,1),156(a,1,2,1))].

given #1061 (A,wt=29): 387 (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 #1062 (F,wt=13): 2306 ((c2 ^ x) v (y ^ (c1 ^ z))) ^ c2' = 0.  [para(318(a,1),156(a,1,2,1))].

given #1063 (F,wt=13): 2307 ((c2 ^ x) v (y v c1)) ^ (c2 v y)' = 0.  [para(495(a,1),156(a,1,2,1))].

given #1064 (T,wt=13): 2313 (x v (y v z)) ^ (y v (x v z))' = 0.  [para(108(a,1),156(a,1,1,1)),rewrite(3(2),3(4))].

given #1065 (T,wt=13): 2314 ((x ^ y) v z) ^ (x v (z v u))' = 0.  [para(156(a,1),110(a,1,2)),rewrite(4(4),81(4)),flip(a)].

given #1066 (A,wt=29): 388 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 #1067 (F,wt=13): 2345 (x ^ (y v z)) v (x ^ (z v y))' = 1.  [para(108(a,1),159(a,1,2,1,2))].

given #1068 (F,wt=13): 2356 (x ^ (y ^ z)) v (z ^ (x ^ y))' = 1.  [para(5(a,1),2336(a,1,1))].

given #1069 (T,wt=13): 2357 (x ^ (y ^ z)) v (y ^ (z ^ x))' = 1.  [para(5(a,1),2336(a,1,2,1))].

Low Water (displace): id=13994, wt=30

Low Water (displace): id=15071, wt=29

given #1070 (T,wt=13): 2359 (x ^ (y ^ z)) v (x ^ (z ^ y))' = 1.  [para(19(a,1),2336(a,1,1)),rewrite(5(4))].

given #1071 (A,wt=27): 389 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 #1072 (F,wt=13): 2391 (x ^ ((x ^ y) v z)) v (x ^ y)' = 1.  [para(23(a,1),168(a,1,2,1))].

given #1073 (F,wt=13): 2392 (x ^ (c2 ^ y)) v (x ^ (c1 ^ y))' = 1.  [para(59(a,1),168(a,1,2,1,2))].

given #1074 (T,wt=13): 2397 (x ^ (y v (z v u))) v (x ^ z)' = 1.  [para(71(a,1),168(a,1,2,1,2))].

Low Water (displace): id=15431, wt=28

given #1075 (T,wt=13): 2398 (x ^ (y ^ c2)) v (x ^ (y ^ c1))' = 1.  [para(87(a,1),168(a,1,2,1,2))].

given #1076 (A,wt=33): 391 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 #1077 (F,wt=13): 2399 (x ^ (y v (z v u))) v (x ^ u)' = 1.  [para(94(a,1),168(a,1,2,1,2))].

given #1078 (F,wt=13): 2411 (x ^ (y v (c2 v z))) v (x ^ c1)' = 1.  [para(202(a,1),168(a,1,2,1,2))].

given #1079 (T,wt=13): 2412 (x ^ (y v (z v c2))) v (x ^ c1)' = 1.  [para(204(a,1),168(a,1,2,1,2))].

given #1080 (T,wt=13): 2419 (x ^ (y v (x ^ z))) v (x ^ z)' = 1.  [para(96(a,1),168(a,1,2,1))].

given #1081 (A,wt=25): 392 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(374(9),3(8))].

given #1082 (F,wt=13): 2422 (x ^ (y v c2)) v (x ^ (y v c1))' = 1.  [para(115(a,1),168(a,1,2,1,2))].

given #1083 (F,wt=13): 2433 ((x v (y v z)) ^ u) v (y ^ u)' = 1.  [para(17(a,1),169(a,1,1,1))].

given #1084 (T,wt=13): 2447 ((x v y) ^ (z v (x v u))) v x' = 1.  [para(71(a,1),169(a,1,2,1))].

given #1085 (T,wt=13): 2448 ((c1 v x) ^ (y ^ c2)) v (y ^ c1)' = 1.  [para(87(a,1),169(a,1,2,1))].

given #1086 (A,wt=25): 393 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),66(11))].

given #1087 (F,wt=13): 2449 ((x v y) ^ (z v (u v x))) v x' = 1.  [para(94(a,1),169(a,1,2,1))].

given #1088 (F,wt=13): 2463 ((c1 v x) ^ (y v (c2 v z))) v c1' = 1.  [para(202(a,1),169(a,1,2,1))].

given #1089 (T,wt=13): 2464 ((c1 v x) ^ (y v (z v c2))) v c1' = 1.  [para(204(a,1),169(a,1,2,1))].

given #1090 (T,wt=13): 2473 (x ^ y)' v (((x v z) ^ y) v u) = 1.  [para(169(a,1),108(a,1,1)),rewrite(69(8),2427(11))].

given #1091 (A,wt=21): 394 c2 ^ (x v (y ^ (c1 v (x ^ c2)))) = c2 ^ (x v (y ^ (x v c1))).  [para(104(a,1),42(a,1,2,2,2,2,2))].

given #1092 (F,wt=13): 2489 x v (y v ((z ^ (x ^ u)) v y)') = 1.  [para(19(a,1),184(a,1,2,2,1,1))].

given #1093 (F,wt=13): 2508 x ^ (y ^ ((z v (x v u)) ^ y)') = 0.  [para(17(a,1),187(a,1,2,2,1,1))].

given #1094 (T,wt=13): 2529 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x).  [para(6(a,1),194(a,1,1))].

given #1095 (T,wt=11): 22802 x ^ (c1 v (c2 ^ x)) = c2 ^ x.  [para(2529(a,1),58(a,1,2)),rewrite(99(5)),flip(a)].

given #1096 (A,wt=23): 395 x ^ (y v (z ^ (y' v (u v (y ^ (y' v (u v x))))))) = x ^ (y v z).  [para(79(a,1),42(a,2,2,2,2)),rewrite(3(5),3(7),32(12))].

Low Water (displace): id=15885, wt=27

given #1097 (F,wt=11): 22843 x v (c2 ^ (c1 v x)) = x v c1.  [para(2529(a,1),1843(a,1,2))].

given #1098 (F,wt=11): 22858 x ^ (c1 v (x ^ c2)) = c2 ^ x.  [para(4(a,1),22802(a,1,2,2))].

Low Water (displace): id=16600, wt=26

Low Water (displace): id=16622, wt=25

given #1099 (T,wt=11): 22906 x v (c2 ^ (x v c1)) = x v c1.  [para(2(a,1),22843(a,1,2,2))].

given #1100 (T,wt=13): 2534 c1 v (c2 ^ (x v c1)) = c2 ^ (x v c1).  [para(20(a,1),194(a,1,1))].

given #1101 (A,wt=23): 396 x ^ (y v (z ^ (u v (y' v (y ^ (u v (y' v x))))))) = x ^ (y v z).  [para(89(a,1),42(a,2,2,2,2)),rewrite(3(5),3(7),32(12))].

given #1102 (F,wt=13): 2558 (x v (c1 ^ y)) ^ (x v (c2 ^ y))' = 0.  [para(194(a,1),128(a,1,2,1,2))].

given #1103 (F,wt=13): 2574 ((c2 v x) ^ y) v ((c1 ^ y)' v z) = 1.  [para(195(a,1),162(a,1,2,1,1))].

Low Water (displace): id=17418, wt=24

given #1104 (T,wt=13): 2575 ((c2 v x) ^ y) v (z ^ (c1 ^ y))' = 1.  [para(195(a,1),164(a,1,2,1,2))].

given #1105 (T,wt=13): 2577 ((c2 v x) ^ y) v (z v (c1 ^ y)') = 1.  [para(195(a,1),167(a,1,2,2,1))].

Low Water (keep): wt=19, part=0.50, limit=19

given #1106 (A,wt=25): 397 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 #1107 (F,wt=13): 2587 (c1 ^ x)' v (y v ((c2 v z) ^ x)) = 1.  [para(195(a,1),2065(a,1,1,1))].

given #1108 (F,wt=13): 2588 c1 ^ (x ^ (((c2 v y) ^ x) v z)') = 0.  [para(129(a,1),195(a,1,2)),rewrite(4(3),81(3)),flip(a)].

given #1109 (T,wt=13): 2589 c1 ^ (x ^ (y v ((c2 v z) ^ x))') = 0.  [para(143(a,1),195(a,1,2)),rewrite(4(3),81(3)),flip(a)].

given #1110 (T,wt=13): 2598 (x ^ (c2 v y)) v ((x ^ c1)' v z) = 1.  [para(203(a,1),162(a,1,2,1,1))].

given #1111 (A,wt=35): 398 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(374(18))].

given #1112 (F,wt=13): 2599 (x ^ (c2 v y)) v (z ^ (x ^ c1))' = 1.  [para(203(a,1),164(a,1,2,1,2))].

given #1113 (F,wt=13): 2600 (x ^ (c2 v y)) v (z v (x ^ c1)') = 1.  [para(203(a,1),167(a,1,2,2,1))].

given #1114 (T,wt=13): 2606 (x ^ c1)' v (y v (x ^ (c2 v z))) = 1.  [para(203(a,1),2065(a,1,1,1))].

given #1115 (T,wt=13): 2617 ((x v c2) ^ y) v ((c1 ^ y)' v z) = 1.  [para(205(a,1),162(a,1,2,1,1))].

given #1116 (A,wt=31): 399 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(374(9))].

given #1117 (F,wt=13): 2618 ((x v c2) ^ y) v (z ^ (c1 ^ y))' = 1.  [para(205(a,1),164(a,1,2,1,2))].

given #1118 (F,wt=13): 2620 ((x v c2) ^ y) v (z v (c1 ^ y)') = 1.  [para(205(a,1),167(a,1,2,2,1))].

given #1119 (T,wt=13): 2629 (c1 ^ x)' v (y v ((z v c2) ^ x)) = 1.  [para(205(a,1),2065(a,1,1,1))].

given #1120 (T,wt=13): 2630 c1 ^ (x ^ (((y v c2) ^ x) v z)') = 0.  [para(129(a,1),205(a,1,2)),rewrite(4(3),81(3)),flip(a)].

given #1121 (A,wt=35): 400 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(374(11))].

given #1122 (F,wt=13): 2631 c1 ^ (x ^ (y v ((z v c2) ^ x))') = 0.  [para(143(a,1),205(a,1,2)),rewrite(4(3),81(3)),flip(a)].

given #1123 (F,wt=13): 2635 c1 ^ (x ^ ((y v (c2 v z)) ^ x)') = 0.  [para(187(a,1),205(a,1,2)),rewrite(4(3),81(3),3(5)),flip(a)].

given #1124 (T,wt=13): 2641 (x ^ (y v c2)) v ((x ^ c1)' v z) = 1.  [para(207(a,1),162(a,1,2,1,1))].

given #1125 (T,wt=13): 2642 (x ^ (y v c2)) v (z ^ (x ^ c1))' = 1.  [para(207(a,1),164(a,1,2,1,2))].

given #1126 (A,wt=31): 401 ((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 #1127 (F,wt=13): 2643 (x ^ (y v c2)) v (z v (x ^ c1)') = 1.  [para(207(a,1),167(a,1,2,2,1))].

given #1128 (F,wt=13): 2649 (x ^ c1)' v (y v (x ^ (z v c2))) = 1.  [para(207(a,1),2065(a,1,1,1))].

given #1129 (T,wt=13): 2668 x' v y != 1 | x' ^ y != 0 | x = y.  [para(231(a,1),121(a,1,2,1)),rewrite(69(3),216(10),231(11),69(10))].

given #1130 (T,wt=9): 23450 x' != 1 | x' != 0 | x' = x.  [para(28(a,1),2668(b,1)),rewrite(29(3)),flip(c)].

given #1131 (A,wt=31): 402 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 #1132 (F,wt=12): 23453 x' v (x' v y)' != 1 | (x' v y)' = x.  [para(120(a,1),2668(b,1)),flip(c),xx(b)].

given #1133 (F,wt=12): 23454 x' v (y v x')' != 1 | (y v x')' = x.  [para(127(a,1),2668(b,1)),flip(c),xx(b)].

given #1134 (T,wt=12): 23455 x' ^ (x' ^ y)' != 0 | (x' ^ y)' = x.  [para(150(a,1),2668(a,1)),flip(c),xx(a)].

given #1135 (T,wt=12): 23456 x' ^ (y ^ x')' != 0 | (y ^ x')' = x.  [para(158(a,1),2668(a,1)),flip(c),xx(a)].

given #1136 (A,wt=23): 403 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 #1137 (F,wt=12): 23477 x' v (y v x')' != 1 | (x' v y)' = x.  [para(2(a,1),23453(a,1,2,1))].

given #1138 (F,wt=12): 23479 x' v (x' v y)' != 1 | (y v x')' = x.  [para(2(a,1),23454(a,1,2,1))].

given #1139 (T,wt=12): 23480 x' ^ (y ^ x')' != 0 | (x' ^ y)' = x.  [para(4(a,1),23455(a,1,2,1))].

given #1140 (T,wt=12): 23482 x' ^ (x' ^ y)' != 0 | (y ^ x')' = x.  [para(4(a,1),23456(a,1,2,1))].

given #1141 (A,wt=19): 404 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(374(9),3(9))].

given #1142 (F,wt=13): 2670 c2 != 1 | c2 ^ x != 0 | c2' = c2 ^ x.  [para(276(a,1),121(a,1,2,1)),rewrite(7(4),276(13))].

given #1143 (F,wt=13): 2713 ((x ^ c1) v y) ^ (z v (c2 v y))' = 0.  [para(278(a,1),141(a,1,2,1,2))].

given #1144 (T,wt=13): 2714 ((x ^ c1) v y) ^ ((c2 v y)' ^ z) = 0.  [para(278(a,1),142(a,1,2,1,1))].

given #1145 (T,wt=13): 2715 ((x ^ c1) v y) ^ (z ^ (c2 v y)') = 0.  [para(278(a,1),146(a,1,2,2,1))].

given #1146 (A,wt=23): 405 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 #1147 (F,wt=13): 2728 c2 v (x v (((y ^ c1) v x) ^ z)') = 1.  [para(278(a,1),2064(a,1,2)),rewrite(2(8),3(8))].

given #1148 (F,wt=13): 2729 c2 v (x v (y ^ ((z ^ c1) v x))') = 1.  [para(278(a,1),2065(a,1,2)),rewrite(2(8),3(8))].

given #1149 (T,wt=13): 2733 c2 v (x v ((y ^ (c1 ^ z)) v x)') = 1.  [para(184(a,1),278(a,1,2)),rewrite(2(3),78(3),5(5)),flip(a)].

given #1150 (T,wt=13): 2743 x ^ (c1 ^ (y v (c2 ^ x))) = x ^ c1.  [para(281(a,1),94(a,1,2,2)),rewrite(5(6))].

given #1151 (A,wt=35): 406 (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 #1152 (F,wt=13): 2761 (x v (y ^ c1)) ^ (x v (c2 ^ y))' = 0.  [para(281(a,1),145(a,1,2,1,2))].

given #1153 (F,wt=13): 2774 (x v (y ^ c1)) ^ (z v (x v c2))' = 0.  [para(284(a,1),141(a,1,2,1,2))].

given #1154 (T,wt=13): 2775 (x v (y ^ c1)) ^ ((x v c2)' ^ z) = 0.  [para(284(a,1),142(a,1,2,1,1))].

given #1155 (T,wt=13): 2776 (x v (y ^ c1)) ^ (z ^ (x v c2)') = 0.  [para(284(a,1),146(a,1,2,2,1))].

given #1156 (A,wt=35): 407 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 #1157 (F,wt=13): 2780 x v c2 != 1 | c2 != 0 | c2' = x v c2.  [para(284(a,1),68(a,1)),rewrite(284(14)),flip(b)].

given #1158 (F,wt=13): 2787 x v (c2 v ((x v (y ^ c1)) ^ z)') = 1.  [para(284(a,1),2064(a,1,2)),rewrite(2(8),3(8))].

given #1159 (T,wt=13): 2788 x v (c2 v (y ^ (x v (z ^ c1)))') = 1.  [para(284(a,1),2065(a,1,2)),rewrite(2(8),3(8))].

given #1160 (T,wt=13): 2804 ((c1 ^ x) v y) ^ (z v (c2 v y))' = 0.  [para(315(a,1),141(a,1,2,1,2))].

given #1161 (A,wt=23): 408 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 #1162 (F,wt=13): 2805 ((c1 ^ x) v y) ^ ((c2 v y)' ^ z) = 0.  [para(315(a,1),142(a,1,2,1,1))].

given #1163 (F,wt=13): 2806 ((c1 ^ x) v y) ^ (z ^ (c2 v y)') = 0.  [para(315(a,1),146(a,1,2,2,1))].

given #1164 (T,wt=13): 2819 c2 v (x v (((c1 ^ y) v x) ^ z)') = 1.  [para(315(a,1),2064(a,1,2)),rewrite(2(8),3(8))].

given #1165 (T,wt=13): 2820 c2 v (x v (y ^ ((c1 ^ z) v x))') = 1.  [para(315(a,1),2065(a,1,2)),rewrite(2(8),3(8))].

given #1166 (A,wt=27): 409 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 #1167 (F,wt=13): 2833 x ^ (y ^ (y ^ (z v (x v u)))') = 0.  [para(185(a,1),122(a,1,2)),rewrite(91(2)),flip(a)].

given #1168 (F,wt=13): 2835 x ^ (c1 ^ (c2 ^ (y v (x v z)))') = 0.  [para(441(a,1),122(a,1,2)),rewrite(91(2),4(6)),flip(a)].

given #1169 (T,wt=13): 2848 x ^ ((x v y) ^ (z v (x v u)))' = 0.  [para(122(a,1),187(a,1))].

given #1170 (T,wt=13): 2861 (x v (c1 ^ y)) ^ (z v (x v c2))' = 0.  [para(317(a,1),141(a,1,2,1,2))].

given #1171 (A,wt=25): 410 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 #1172 (F,wt=13): 2862 (x v (c1 ^ y)) ^ ((x v c2)' ^ z) = 0.  [para(317(a,1),142(a,1,2,1,1))].

given #1173 (F,wt=13): 2863 (x v (c1 ^ y)) ^ (z ^ (x v c2)') = 0.  [para(317(a,1),146(a,1,2,2,1))].

given #1174 (T,wt=13): 2874 x v (c2 v ((x v (c1 ^ y)) ^ z)') = 1.  [para(317(a,1),2064(a,1,2)),rewrite(2(8),3(8))].

given #1175 (T,wt=13): 2875 x v (c2 v (y ^ (x v (c1 ^ z)))') = 1.  [para(317(a,1),2065(a,1,2)),rewrite(2(8),3(8))].

given #1176 (A,wt=21): 411 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(374(9))].

given #1177 (F,wt=13): 2884 (x ^ (y ^ z)) v (y ^ x) = x ^ y.  [para(365(a,1),24(a,2)),rewrite(5(3),2879(6))].

given #1178 (F,wt=13): 2901 (x v (y ^ z)) ^ (x v (z ^ y))' = 0.  [para(365(a,1),145(a,1,2,1,2))].

given #1179 (T,wt=13): 2916 x ^ (c1 ^ (y v (x ^ c2))) = x ^ c1.  [para(439(a,1),71(a,1,2,2)),rewrite(5(6))].

given #1180 (T,wt=13): 2924 (x v (y ^ c1)) ^ (x v (y ^ c2))' = 0.  [para(439(a,1),128(a,1,2,1,2))].

given #1181 (A,wt=35): 412 (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(374(18))].

given #1182 (F,wt=13): 3020 x v (c2 v (y ^ (c1 v x))) = x v c2.  [para(613(a,1),102(a,1,2,2)),rewrite(3(6))].

given #1183 (F,wt=13): 3030 (c1 v x) ^ (c2 v (x v y)) = c1 v x.  [para(613(a,1),110(a,1,2)),rewrite(21(6),2(7)),flip(a)].

given #1184 (T,wt=13): 3031 (x ^ (y v c2)) v (x ^ (c1 v y))' = 1.  [para(613(a,1),168(a,1,2,1,2))].

given #1185 (T,wt=13): 3033 c1 v x != 1 | c1 != 0 | c1' = c1 v x.  [para(613(a,1),121(a,1,2)),rewrite(66(4),193(8),613(14))].

given #1186 (A,wt=31): 413 (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(374(6))].

given #1187 (F,wt=13): 3053 (x v c1) ^ ((y v (c2 v x))' ^ z) = 0.  [para(495(a,1),716(a,1,2,1,1,2))].

given #1188 (F,wt=13): 3070 (x v c1) ^ (y ^ (z v (c2 v x))') = 0.  [para(495(a,1),719(a,1,2,2,1,2))].

given #1189 (T,wt=13): 3105 (c2 ^ x) v ((y ^ (c1 ^ x))' v z) = 1.  [para(59(a,1),790(a,1,2,1,1,2))].

given #1190 (T,wt=13): 3108 (x ^ c2) v ((y ^ (x ^ c1))' v z) = 1.  [para(87(a,1),790(a,1,2,1,1,2))].

given #1191 (A,wt=35): 414 (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(374(6))].

given #1192 (F,wt=13): 3139 (c2 ^ (x v (c1 v y))) v (c1' v z) = 1.  [para(71(a,1),795(a,1,2,1,1))].

given #1193 (F,wt=13): 3140 (c2 ^ (x v (y v c1))) v (c1' v z) = 1.  [para(94(a,1),795(a,1,2,1,1))].

given #1194 (T,wt=13): 3180 (c2 ^ x) v (y v (z ^ (c1 ^ x))') = 1.  [para(59(a,1),807(a,1,2,2,1,2))].

given #1195 (T,wt=13): 3184 (x ^ c2) v (y v (z ^ (x ^ c1))') = 1.  [para(87(a,1),807(a,1,2,2,1,2))].

given #1196 (A,wt=31): 415 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 #1197 (F,wt=13): 3211 (c2 ^ ((x ^ c1) v y)) v (x ^ c1)' = 1.  [para(23(a,1),810(a,1,2,1))].

given #1198 (F,wt=13): 3214 (c2 ^ (x v (c1 v y))) v (z ^ c1)' = 1.  [para(71(a,1),810(a,1,2,1,2))].

given #1199 (T,wt=13): 3215 (c2 ^ (x v (y v c1))) v (z ^ c1)' = 1.  [para(94(a,1),810(a,1,2,1,2))].

given #1200 (T,wt=13): 3234 (c2 ^ (x v (y ^ c1))) v (y ^ c1)' = 1.  [para(96(a,1),810(a,1,2,1))].

given #1201 (A,wt=23): 416 c1 ^ (x v (y ^ (z v (x ^ (z v c2))))) = c1 ^ (x v (y ^ (x v z))).  [para(42(a,1),59(a,1,2)),rewrite(59(7)),flip(a)].

given #1202 (F,wt=13): 3237 (x ^ (c1 ^ y))' v (z v (c2 ^ y)) = 1.  [para(810(a,1),109(a,1,1)),rewrite(69(10),810(15))].

given #1203 (F,wt=13): 3244 (x ^ ((x ^ y) v z)) v (y ^ x)' = 1.  [para(136(a,1),158(a,1,2,1))].

given #1204 (T,wt=13): 3245 c1 ^ (x ^ ((x ^ c2) v y)) = c1 ^ x.  [para(136(a,1),59(a,1,2)),rewrite(59(4)),flip(a)].

given #1205 (T,wt=13): 3246 x ^ (y ^ (y ^ ((y ^ x) v z))') = 0.  [para(136(a,1),232(a,1,2)),rewrite(4(6),5(6))].

given #1206 (A,wt=31): 417 x v ((y ^ (x v z)) v u) != 1 | u ^ (x v (y ^ (z v x))) != 0 | u' = x v (y ^ (x v z)).