============================== Prover9 ===============================
Prover9 (32) version April-2007, April 2007.
Process 27129 was started by mccune on cleo,
Fri Apr 13 09:21:43 2007
The command was "/home/mccune/bin/prover9 -f lt.in uc.in H65d.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 H65d.in

assign(max_seconds,600).

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

formulas(goals).
x ^ (y v z) = (x ^ y) v (x ^ z) # answer(distributivity).
end_of_list.

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

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

% Formulas that are not ordinary clauses:
1 x ^ (y v z) = (x ^ y) v (x ^ z) # answer(distributivity) # 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 ^ u)) = x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) # label(H65).  [assumption].
(c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity).  [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, c3, ^, v, ' ]).
After inverse_order: Function symbol precedence:  lex([ 0, 1, c1, c2, c3, ^, 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 (x ^ ((x ^ y) v (z ^ u)))) = x ^ (y v (z ^ u)).  [copy(11),flip(a)].
13 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity).  [deny(1)].
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].
12 x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) = x ^ (y v (z ^ u)).  [copy(11),flip(a)].
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: 14 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: 16 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=6): 8 x v x' = 1.  [assumption].

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

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

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

given #11 (I,wt=13): 13 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity).  [deny(1)].

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

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

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

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

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

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

given #18 (T,wt=5): 67 1 ^ x = x.  [para(30(a,1),4(a,1)),flip(a)].

given #19 (T,wt=4): 76 1' = 0.  [hyper(10,a,33,a,b,67,a)].

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

given #21 (T,wt=4): 79 0' = 1.  [hyper(10,a,69,a,b,30,a)].

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

given #23 (T,wt=5): 77 1 v x = 1.  [para(67(a,1),6(a,1))].

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

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

given #26 (T,wt=5): 91 x ^ 0 = 0.  [para(80(a,1),4(a,1)),flip(a)].

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

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

given #29 (T,wt=7): 89 0 != x | x' = 1.  [back_rewrite(68),rewrite(88(2)),xx(a)].

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

given #31 (T,wt=8): 78 x v (x' v y) = 1.  [back_rewrite(28),rewrite(77(5))].

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

given #33 (T,wt=8): 81 x ^ (x' ^ y) = 0.  [back_rewrite(31),rewrite(80(5))].

given #34 (T,wt=8): 90 x v (y v x') = 1.  [back_rewrite(54),rewrite(88(5))].

given #35 (T,wt=8): 92 x ^ (y ^ x') = 0.  [back_rewrite(74),rewrite(91(5))].

given #36 (T,wt=8): 114 x ^ (x v y)' = 0.  [para(9(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

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

given #38 (T,wt=8): 130 x ^ (y v x)' = 0.  [para(2(a,1),114(a,1,2,1))].

given #39 (T,wt=9): 52 x ^ (y v (x v z)) = x.  [para(15(a,1),6(a,1,2))].

given #40 (T,wt=9): 57 x ^ (x ^ y) = x ^ y.  [para(26(a,1),5(a,1,1)),flip(a)].

given #41 (T,wt=9): 59 x ^ (y ^ x) = y ^ x.  [para(26(a,1),5(a,2,2)),rewrite(4(2))].

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

given #43 (T,wt=8): 162 x v (x ^ y)' = 1.  [para(8(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #44 (T,wt=8): 171 x v (y ^ x)' = 1.  [para(4(a,1),162(a,1,2,1))].

given #45 (T,wt=9): 63 x v (x v y) = x v y.  [para(27(a,1),3(a,1,1)),flip(a)].

given #46 (T,wt=9): 65 x v (y v x) = y v x.  [para(27(a,1),3(a,2,2)),rewrite(2(2))].

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

given #48 (T,wt=9): 73 x v (y ^ (x ^ z)) = x.  [para(17(a,1),7(a,1,2))].

given #49 (T,wt=9): 82 x ^ (y v (z v x)) = x.  [para(3(a,1),18(a,1,2))].

given #50 (T,wt=9): 104 x v (y ^ (z ^ x)) = x.  [para(5(a,1),24(a,1,2))].

given #51 (T,wt=10): 29 x v (y v (x v y)') = 1.  [para(8(a,1),3(a,1)),flip(a)].

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

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

given #54 (T,wt=10): 60 1 != x | 0 != x | x' = x.  [para(26(a,1),10(b,1)),rewrite(27(1)),flip(a),flip(b)].

given #55 (T,wt=10): 112 x v (y v (x' v z)) = 1.  [para(78(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #56 (T,wt=10): 121 x ^ (y ^ (x' ^ z)) = 0.  [para(81(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

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

given #58 (T,wt=5): 250 x'' = x.  [para(8(a,1),34(a,1)),rewrite(4(5),9(5)),xx(a),xx(b)].

given #59 (T,wt=8): 267 x' v (y v x) = 1.  [para(250(a,1),90(a,1,2,2))].

given #60 (T,wt=8): 268 x' ^ (y ^ x) = 0.  [para(250(a,1),92(a,1,2,2))].

given #61 (T,wt=10): 122 x ^ ((x v y)' ^ z) = 0.  [para(81(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

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

given #63 (T,wt=10): 124 x v (y v (z v x')) = 1.  [para(3(a,1),90(a,1,2))].

given #64 (T,wt=10): 127 x ^ (y ^ (z ^ x')) = 0.  [para(5(a,1),92(a,1,2))].

given #65 (T,wt=10): 129 x ^ (y ^ (x v z)') = 0.  [para(92(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #66 (T,wt=10): 134 x ^ (y v (x v z))' = 0.  [para(15(a,1),114(a,1,2,1))].

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

given #68 (T,wt=10): 143 x ^ (y v (z v x))' = 0.  [para(3(a,1),130(a,1,2,1))].

given #69 (T,wt=10): 144 x ^ ((y v x)' ^ z) = 0.  [para(130(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #70 (T,wt=10): 148 x ^ (y ^ (z v x)') = 0.  [para(130(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #71 (T,wt=10): 167 x v ((x ^ y)' v z) = 1.  [para(78(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

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

given #73 (T,wt=10): 168 x v (y v (x ^ z)') = 1.  [para(90(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #74 (T,wt=10): 174 x v (y ^ (x ^ z))' = 1.  [para(17(a,1),162(a,1,2,1))].

given #75 (T,wt=10): 175 x v ((y ^ x)' v z) = 1.  [para(171(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #76 (T,wt=10): 177 x v (y ^ (z ^ x))' = 1.  [para(5(a,1),171(a,1,2,1))].

given #77 (A,wt=21): 40 x ^ (y v (x ^ ((z ^ u) v (x ^ y)))) = x ^ (y v (z ^ u)).  [para(2(a,1),12(a,1,2,2,2))].

given #78 (T,wt=10): 179 x v (y v (z ^ x)') = 1.  [para(171(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #79 (T,wt=10): 217 x v (y v (y v x)') = 1.  [para(2(a,1),29(a,1,2,2,1))].

given #80 (T,wt=10): 232 x ^ (y ^ (y ^ x)') = 0.  [para(4(a,1),32(a,1,2,2,1))].

given #81 (T,wt=10): 269 x' v (y v (x v z)) = 1.  [para(250(a,1),112(a,1,2,2,1))].

given #82 (A,wt=27): 41 x ^ (y v (z v (x ^ ((x ^ (y v z)) v (u ^ v))))) = x ^ (y v (z v (u ^ v))).  [para(3(a,1),12(a,1,2)),rewrite(3(11))].

given #83 (T,wt=10): 270 x' ^ (y ^ (x ^ z)) = 0.  [para(250(a,1),121(a,1,2,2,1))].

given #84 (T,wt=10): 271 x' v (y v (z v x)) = 1.  [para(3(a,1),267(a,1,2))].

given #85 (T,wt=10): 276 x' ^ (y ^ (z ^ x)) = 0.  [para(5(a,1),268(a,1,2))].

given #86 (T,wt=10): 601 (x ^ y)' v (z v x) = 1.  [para(7(a,1),271(a,1,2,2))].

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

given #88 (T,wt=10): 604 (x ^ y)' v (z v y) = 1.  [para(24(a,1),271(a,1,2,2))].

given #89 (T,wt=10): 615 (x v y)' ^ (z ^ x) = 0.  [para(6(a,1),276(a,1,2,2))].

given #90 (T,wt=10): 618 (x v y)' ^ (z ^ y) = 0.  [para(18(a,1),276(a,1,2,2))].

given #91 (T,wt=11): 53 x v (y v (x ^ z)) = y v x.  [para(7(a,1),15(a,1,2)),flip(a)].

given #92 (A,wt=25): 43 x ^ ((y v (x ^ ((x ^ y) v (z ^ u)))) ^ v) = x ^ ((y v (z ^ u)) ^ v).  [para(12(a,1),5(a,1,1)),rewrite(5(4)),flip(a)].

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

given #94 (T,wt=11): 83 x ^ ((y v x) ^ z) = x ^ z.  [para(18(a,1),5(a,1,1)),flip(a)].

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

given #96 (T,wt=11): 102 x v ((y ^ x) v z) = x v z.  [para(24(a,1),3(a,1,1)),flip(a)].

given #97 (A,wt=29): 44 x ^ (y ^ (z v (x ^ (y ^ ((x ^ (y ^ z)) v (u ^ v)))))) = x ^ (y ^ (z v (u ^ v))).  [para(12(a,1),5(a,1)),rewrite(5(4),5(7),5(10)),flip(a)].

given #98 (T,wt=11): 106 x v (y v (z ^ x)) = y v x.  [para(24(a,1),15(a,1,2)),flip(a)].

given #99 (T,wt=11): 150 x ^ (y v (z v (x v u))) = x.  [para(3(a,1),52(a,1,2))].

given #100 (T,wt=11): 159 (x v y) ^ (z ^ x) = z ^ x.  [para(59(a,1),20(a,2)),rewrite(158(4))].

given #101 (T,wt=11): 185 (x v y) ^ (y v x) = x v y.  [para(65(a,1),19(a,1,2))].

given #102 (A,wt=17): 45 x ^ (y v (x ^ ((x ^ y) v z))) = x ^ (y v z).  [para(6(a,1),12(a,1,2,2,2,2)),rewrite(6(7))].

given #103 (T,wt=10): 1036 (x v y) ^ (y v x)' = 0.  [para(185(a,1),268(a,1,2)),rewrite(4(4))].

given #104 (T,wt=11): 186 (x ^ y) v (z v x) = z v x.  [para(65(a,1),22(a,2)),rewrite(184(4))].

given #105 (T,wt=11): 197 x v (y ^ (z ^ (x ^ u))) = x.  [para(5(a,1),73(a,1,2))].

given #106 (T,wt=11): 200 x ^ (y v (z v (u v x))) = x.  [para(3(a,1),82(a,1,2,2))].

given #107 (A,wt=20): 55 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z.  [para(15(a,1),10(a,1))].

given #108 (T,wt=11): 210 x v (y ^ (z ^ (u ^ x))) = x.  [para(5(a,1),104(a,1,2,2))].

given #109 (T,wt=11): 230 (x ^ y) v (y ^ x) = x ^ y.  [para(59(a,1),25(a,1,2))].

given #110 (T,wt=10): 1225 (x ^ y) v (y ^ x)' = 1.  [para(230(a,1),267(a,1,2)),rewrite(2(4))].

given #111 (T,wt=11): 294 x v y != 0 | (x v y)' = 1.  [para(30(a,1),35(b,1)),rewrite(88(2),88(2)),xx(a)].

given #112 (A,wt=14): 62 1 != x | x ^ y != 0 | x' = x ^ y.  [back_rewrite(39),rewrite(57(4))].

given #113 (T,wt=7): 1248 x' != 1 | 0 = x.  [para(268(a,1),62(b,1)),rewrite(250(8),268(9)),flip(a),flip(c),xx(b)].

given #114 (T,wt=11): 295 x v y != 1 | (x v y)' = 0.  [para(33(a,1),35(a,1,2)),rewrite(4(6),80(6)),xx(b)].

given #115 (T,wt=11): 409 x ^ y != 0 | (x ^ y)' = 1.  [para(30(a,1),37(b,1,2)),rewrite(2(3),77(3)),xx(a)].

given #116 (T,wt=11): 410 x ^ y != 1 | (x ^ y)' = 0.  [para(33(a,1),37(a,1)),rewrite(91(5),91(5)),xx(b)].

given #117 (A,wt=14): 66 x v y != 1 | 0 != x | x' = x v y.  [back_rewrite(38),rewrite(63(2))].

given #118 (T,wt=7): 1258 x' != 0 | 1 = x.  [para(267(a,1),66(a,1)),rewrite(250(8),267(9)),flip(b),flip(c),xx(a)].

given #119 (T,wt=11): 827 (x v y) ^ (z ^ y) = z ^ y.  [para(59(a,1),83(a,2)),rewrite(158(4))].

given #120 (T,wt=11): 879 (x ^ y) v (z v y) = z v y.  [para(65(a,1),102(a,2)),rewrite(184(4))].

given #121 (T,wt=11): 1244 x v y != 0 | (y v x)' = 1.  [para(2(a,1),294(a,1))].

given #122 (A,wt=20): 75 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x' = y ^ z.  [para(17(a,1),10(b,1))].

given #123 (T,wt=11): 1249 (x v y)' != 1 | x v y = 0.  [para(615(a,1),62(b,1)),rewrite(250(10),615(12)),flip(a),xx(b)].

given #124 (T,wt=11): 1250 x v y != 1 | (y v x)' = 0.  [para(2(a,1),295(a,1))].

given #125 (T,wt=11): 1252 x ^ y != 0 | (y ^ x)' = 1.  [para(4(a,1),409(a,1))].

given #126 (T,wt=11): 1254 x ^ y != 1 | (y ^ x)' = 0.  [para(4(a,1),410(a,1))].

given #127 (A,wt=13): 84 x ^ (y ^ (z v (x ^ y))) = x ^ y.  [para(18(a,1),5(a,1)),flip(a)].

given #128 (T,wt=11): 1259 (x ^ y)' != 0 | x ^ y = 1.  [para(601(a,1),66(a,1)),rewrite(250(10),601(12)),flip(b),xx(a)].

given #129 (T,wt=11): 1346 (x v y)' != 1 | y v x = 0.  [para(2(a,1),1249(a,1,1))].

given #130 (T,wt=11): 1348 (x ^ y)' != 1 | x ^ y = 0.  [para(25(a,1),1249(a,1,1)),rewrite(25(8))].

given #131 (T,wt=11): 1381 (x ^ y)' != 0 | y ^ x = 1.  [para(4(a,1),1259(a,1,1))].

given #132 (A,wt=14): 85 x v y != 1 | 0 != y | y' = x v y.  [para(18(a,1),10(b,1)),rewrite(65(2)),flip(b)].

given #133 (T,wt=11): 1383 (x v y)' != 0 | x v y = 1.  [para(19(a,1),1259(a,1,1)),rewrite(19(8))].

given #134 (T,wt=11): 1386 (x ^ y)' != 1 | y ^ x = 0.  [para(230(a,1),1346(a,1,1)),rewrite(230(7))].

given #135 (T,wt=11): 1390 (x v y)' != 0 | y v x = 1.  [para(185(a,1),1381(a,1,1)),rewrite(185(7))].

given #136 (T,wt=12): 110 x v (y v ((x v y)' v z)) = 1.  [para(78(a,1),3(a,1)),flip(a)].

given #137 (A,wt=13): 86 (x v y) ^ (x v (z v y)) = x v y.  [para(15(a,1),18(a,1,2))].

given #138 (T,wt=12): 119 x ^ (y ^ ((x ^ y)' ^ z)) = 0.  [para(81(a,1),5(a,1)),flip(a)].

given #139 (T,wt=12): 123 x v (y v (z v (x v y)')) = 1.  [para(90(a,1),3(a,1)),flip(a)].

given #140 (T,wt=12): 126 x ^ (y ^ (z ^ (x ^ y)')) = 0.  [para(92(a,1),5(a,1)),flip(a)].

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

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

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

given #144 (T,wt=12): 145 x ^ (y ^ (z v (x ^ y))') = 0.  [para(130(a,1),5(a,1)),flip(a)].

given #145 (T,wt=12): 147 (x v y) ^ (x v (z v y))' = 0.  [para(15(a,1),130(a,1,2,1))].

given #146 (T,wt=12): 169 ((x ^ y) v z) ^ (x v z)' = 0.  [para(22(a,1),130(a,1,2,1))].

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

given #148 (T,wt=12): 170 x v (y v ((x v y) ^ z)') = 1.  [para(162(a,1),3(a,1)),flip(a)].

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

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

given #151 (T,wt=12): 180 (x ^ y) v (x ^ (z ^ y))' = 1.  [para(17(a,1),171(a,1,2,1))].

given #152 (A,wt=19): 96 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z).  [para(3(a,1),19(a,1,1)),rewrite(3(5),3(8))].

given #153 (T,wt=12): 181 ((x v y) ^ z) v (x ^ z)' = 1.  [para(20(a,1),171(a,1,2,1))].

given #154 (T,wt=12): 220 x v (y v (z v (x v z)')) = 1.  [para(29(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #155 (T,wt=12): 222 x v (y v ((x ^ z) v y)') = 1.  [para(29(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #156 (T,wt=12): 235 x ^ (y ^ (z ^ (x ^ z)')) = 0.  [para(32(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

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

given #158 (T,wt=12): 237 x ^ (y ^ ((x v z) ^ y)') = 0.  [para(32(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #159 (T,wt=12): 239 x v (y v (z v (x' v u))) = 1.  [para(3(a,1),112(a,1,2))].

given #160 (T,wt=12): 241 x v (y v ((x ^ z)' v u)) = 1.  [para(112(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #161 (T,wt=12): 243 x ^ (y ^ (z ^ (x' ^ u))) = 0.  [para(5(a,1),121(a,1,2))].

given #162 (A,wt=19): 99 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z).  [para(15(a,1),19(a,1,1)),rewrite(3(4))].

given #163 (T,wt=12): 245 x ^ (y ^ ((x v z)' ^ u)) = 0.  [para(121(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #164 (T,wt=12): 273 x v ((x v y)' v (z v y)) = 1.  [para(15(a,1),267(a,1,2)),rewrite(15(5))].

given #165 (T,wt=12): 278 x ^ ((x ^ y)' ^ (z ^ y)) = 0.  [para(17(a,1),268(a,1,2)),rewrite(17(5))].

given #166 (T,wt=12): 284 x ^ ((y v (x v z))' ^ u) = 0.  [para(15(a,1),122(a,1,2,1,1))].

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

given #168 (T,wt=12): 330 x v (y v (z v (u v x'))) = 1.  [para(3(a,1),124(a,1,2,2))].

given #169 (T,wt=12): 332 x v (y v (z v (x ^ u)')) = 1.  [para(124(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #170 (T,wt=12): 337 x ^ (y ^ (z ^ (u ^ x'))) = 0.  [para(5(a,1),127(a,1,2,2))].

given #171 (T,wt=12): 339 x ^ (y ^ (z ^ (x v u)')) = 0.  [para(127(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

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

given #173 (T,wt=12): 344 x ^ (y ^ (z v (x v u))') = 0.  [para(15(a,1),129(a,1,2,2,1))].

given #174 (T,wt=12): 347 x ^ (y v (z v (x v u)))' = 0.  [para(3(a,1),134(a,1,2,1))].

given #175 (T,wt=12): 371 x ^ (y v (z v (u v x)))' = 0.  [para(3(a,1),143(a,1,2,1,2))].

given #176 (T,wt=12): 372 x ^ ((y v (z v x))' ^ u) = 0.  [para(143(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #177 (A,wt=13): 103 x v (y v (z ^ (x v y))) = x v y.  [para(24(a,1),3(a,1)),flip(a)].

given #178 (T,wt=12): 376 x ^ (y ^ (z v (u v x))') = 0.  [para(143(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #179 (T,wt=12): 385 x ^ (y ^ ((z v x)' ^ u)) = 0.  [para(144(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #180 (T,wt=12): 390 x ^ (y ^ (z ^ (u v x)')) = 0.  [para(5(a,1),148(a,1,2))].

given #181 (T,wt=12): 400 x v ((y ^ (x ^ z))' v u) = 1.  [para(17(a,1),167(a,1,2,1,1))].

given #182 (A,wt=14): 105 1 != x | y ^ x != 0 | x' = y ^ x.  [para(24(a,1),10(a,1)),rewrite(59(4)),flip(a)].

given #183 (T,wt=12): 460 x v (y v (z ^ (x ^ u))') = 1.  [para(17(a,1),168(a,1,2,2,1))].

given #184 (T,wt=12): 467 x v (y ^ (z ^ (x ^ u)))' = 1.  [para(5(a,1),174(a,1,2,1))].

given #185 (T,wt=12): 473 x v ((y ^ (z ^ x))' v u) = 1.  [para(5(a,1),175(a,1,2,1,1))].

given #186 (T,wt=12): 475 x v (y v ((z ^ x)' v u)) = 1.  [para(175(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #187 (A,wt=13): 107 (x ^ y) v (x ^ (z ^ y)) = x ^ y.  [para(17(a,1),24(a,1,2))].

given #188 (T,wt=12): 483 x v (y ^ (z ^ (u ^ x)))' = 1.  [para(5(a,1),177(a,1,2,1,2))].

given #189 (T,wt=12): 485 x v (y v (z ^ (u ^ x))') = 1.  [para(177(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #190 (T,wt=12): 534 x v (y v (z v (u ^ x)')) = 1.  [para(3(a,1),179(a,1,2))].

given #191 (T,wt=12): 543 x v (y v ((y v x)' v z)) = 1.  [para(217(a,1),3(a,1,1)),rewrite(77(2),3(5)),flip(a)].

given #192 (A,wt=22): 109 x v (y v z) != 1 | x v y != 0 | (x v y)' = x v (y v z).  [back_rewrite(98),rewrite(108(4))].

given #193 (T,wt=12): 547 x v (y v (z v (z v x)')) = 1.  [para(217(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #194 (T,wt=12): 549 x v (y v (y v (x ^ z))') = 1.  [para(217(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #195 (T,wt=12): 553 x ^ (y ^ ((y ^ x)' ^ z)) = 0.  [para(232(a,1),5(a,1,1)),rewrite(80(2),5(5)),flip(a)].

given #196 (T,wt=12): 557 x ^ (y ^ (z ^ (z ^ x)')) = 0.  [para(232(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #197 (A,wt=15): 111 x ^ (x' v y) != 0 | x' v y = x'.  [para(78(a,1),10(a,1)),flip(c),xx(a)].

given #198 (T,wt=12): 559 x ^ (y ^ (y ^ (x v z))') = 0.  [para(232(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #199 (T,wt=12): 564 x' v (y v (z v (x v u))) = 1.  [para(3(a,1),269(a,1,2))].

given #200 (T,wt=12): 594 x' ^ (y ^ (z ^ (x ^ u))) = 0.  [para(5(a,1),270(a,1,2))].

given #201 (T,wt=12): 600 x' v (y v (z v (u v x))) = 1.  [para(3(a,1),271(a,1,2,2))].

given #202 (A,wt=17): 113 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u).  [para(20(a,1),5(a,1)),rewrite(5(2)),flip(a)].

given #203 (T,wt=12): 607 (x ^ (y ^ z))' v (u v y) = 1.  [para(73(a,1),271(a,1,2,2))].

given #204 (T,wt=12): 608 (x ^ (y ^ z))' v (u v z) = 1.  [para(104(a,1),271(a,1,2,2))].

given #205 (T,wt=12): 614 x' ^ (y ^ (z ^ (u ^ x))) = 0.  [para(5(a,1),276(a,1,2,2))].

given #206 (T,wt=12): 622 (x v (y v z))' ^ (u ^ y) = 0.  [para(52(a,1),276(a,1,2,2))].

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

given #208 (T,wt=12): 623 (x v (y v z))' ^ (u ^ z) = 0.  [para(82(a,1),276(a,1,2,2))].

given #209 (T,wt=12): 628 (x ^ y)' v (z v (x v u)) = 1.  [para(601(a,1),3(a,1,1)),rewrite(77(2),3(5)),flip(a)].

given #210 (T,wt=12): 629 (x ^ y)' v (z v (u v x)) = 1.  [para(3(a,1),601(a,1,2))].

given #211 (T,wt=12): 681 (x ^ y)' v (z v (y v u)) = 1.  [para(604(a,1),3(a,1,1)),rewrite(77(2),3(5)),flip(a)].

given #212 (A,wt=13): 116 x ^ ((y v (x v z)) ^ u) = x ^ u.  [para(15(a,1),20(a,1,2,1))].

given #213 (T,wt=12): 682 (x ^ y)' v (z v (u v y)) = 1.  [para(3(a,1),604(a,1,2))].

given #214 (T,wt=12): 692 (x v y)' ^ (z ^ (x ^ u)) = 0.  [para(615(a,1),5(a,1,1)),rewrite(80(2),5(5)),flip(a)].

given #215 (T,wt=12): 693 (x v y)' ^ (z ^ (u ^ x)) = 0.  [para(5(a,1),615(a,1,2))].

given #216 (T,wt=12): 700 (x v y)' ^ (z ^ (y ^ u)) = 0.  [para(618(a,1),5(a,1,1)),rewrite(80(2),5(5)),flip(a)].

given #217 (A,wt=15): 117 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u).  [para(20(a,1),17(a,1,2)),flip(a)].

given #218 (T,wt=12): 701 (x v y)' ^ (z ^ (u ^ y)) = 0.  [para(5(a,1),618(a,1,2))].

given #219 (T,wt=12): 715 (x v (y ^ z)) ^ (x v y)' = 0.  [para(53(a,1),130(a,1,2,1))].

given #220 (T,wt=12): 718 x v (y v (x v (y ^ z))') = 1.  [para(53(a,1),267(a,1,2)),rewrite(2(5),3(5))].

given #221 (T,wt=12): 806 (x ^ (y v z)) v (x ^ y)' = 1.  [para(72(a,1),171(a,1,2,1))].

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

given #223 (T,wt=12): 808 x ^ (y ^ (x ^ (y v z))') = 0.  [para(72(a,1),268(a,1,2)),rewrite(4(5),5(5))].

given #224 (T,wt=12): 829 ((x v y) ^ z) v (y ^ z)' = 1.  [para(83(a,1),171(a,1,2,1))].

given #225 (T,wt=12): 833 x ^ (y ^ ((z v x) ^ y)') = 0.  [para(32(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #226 (T,wt=12): 840 x ^ (y ^ (y ^ (z v x))') = 0.  [para(232(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #227 (A,wt=15): 120 x v (x' ^ y) != 1 | x' ^ y = x'.  [para(81(a,1),10(b,1)),flip(c),xx(b)].

given #228 (T,wt=12): 854 (x ^ (y v z)) v (x ^ z)' = 1.  [para(87(a,1),171(a,1,2,1))].

given #229 (T,wt=12): 858 x ^ (y ^ (x ^ (z v y))') = 0.  [para(87(a,1),268(a,1,2)),rewrite(4(5),5(5))].

given #230 (T,wt=12): 878 ((x ^ y) v z) ^ (y v z)' = 0.  [para(102(a,1),130(a,1,2,1))].

given #231 (T,wt=12): 883 x v (y v ((z ^ x) v y)') = 1.  [para(29(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #232 (A,wt=15): 125 x ^ (y v x') != 0 | y v x' = x'.  [para(90(a,1),10(a,1)),flip(c),xx(a)].

given #233 (T,wt=12): 890 x v (y v (y v (z ^ x))') = 1.  [para(217(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #234 (T,wt=12): 983 (x v (y ^ z)) ^ (x v z)' = 0.  [para(106(a,1),130(a,1,2,1))].

given #235 (T,wt=12): 986 x v (y v (x v (z ^ y))') = 1.  [para(106(a,1),267(a,1,2)),rewrite(2(5),3(5))].

given #236 (T,wt=12): 1039 x v (y v (z ^ (y v x))') = 1.  [para(185(a,1),177(a,1,2,1,2)),rewrite(3(5))].

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

given #238 (T,wt=12): 1040 x v (y v (z v (y v x)')) = 1.  [para(185(a,1),179(a,1,2,2,1)),rewrite(3(5))].

given #239 (T,wt=12): 1041 (x v y)' ^ (z ^ (y v x)) = 0.  [para(185(a,1),276(a,1,2,2))].

given #240 (T,wt=12): 1042 (x v y)' v (z v (y v x)) = 1.  [para(185(a,1),604(a,1,1,1))].

given #241 (T,wt=12): 1043 (x v y) ^ (y v (x v z))' = 0.  [para(185(a,1),615(a,1,2)),rewrite(3(2),4(5))].

given #242 (A,wt=15): 133 x v (x v y)' != 1 | (x v y)' = x'.  [para(114(a,1),10(b,1)),flip(c),xx(b)].

given #243 (T,wt=12): 1044 (x v y) ^ (z v (y v x))' = 0.  [para(185(a,1),618(a,1,2)),rewrite(4(5))].

given #244 (T,wt=12): 1100 (x v y) ^ ((y v x)' ^ z) = 0.  [para(1036(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #245 (T,wt=12): 1102 (x v y) ^ (z ^ (y v x)') = 0.  [para(1036(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #246 (T,wt=12): 1228 x ^ (y ^ (z v (y ^ x))') = 0.  [para(230(a,1),143(a,1,2,1,2)),rewrite(5(5))].

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

given #248 (T,wt=12): 1229 x ^ (y ^ (z ^ (y ^ x)')) = 0.  [para(230(a,1),148(a,1,2,2,1)),rewrite(5(5))].

given #249 (T,wt=12): 1230 (x ^ y)' v (z v (y ^ x)) = 1.  [para(230(a,1),271(a,1,2,2))].

given #250 (T,wt=12): 1231 (x ^ y) v (y ^ (x ^ z))' = 1.  [para(230(a,1),601(a,1,2)),rewrite(5(2),2(5))].

given #251 (T,wt=12): 1232 (x ^ y) v (z ^ (y ^ x))' = 1.  [para(230(a,1),604(a,1,2)),rewrite(2(5))].

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

given #253 (T,wt=12): 1233 (x ^ y)' ^ (z ^ (y ^ x)) = 0.  [para(230(a,1),618(a,1,1,1))].

given #254 (T,wt=12): 1237 (x ^ y) v ((y ^ x)' v z) = 1.  [para(1225(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #255 (T,wt=12): 1240 (x ^ y) v (z v (y ^ x)') = 1.  [para(1225(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #256 (T,wt=12): 1473 (x v y) ^ (y v (z v x))' = 0.  [para(2(a,1),131(a,1,2,1)),rewrite(3(3))].

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

given #258 (T,wt=12): 1480 ((x ^ y) v z) ^ (z v x)' = 0.  [para(186(a,1),131(a,1,2,1))].

given #259 (T,wt=12): 1482 ((x ^ y) v z) ^ (z v y)' = 0.  [para(879(a,1),131(a,1,2,1))].

given #260 (T,wt=12): 1497 x ^ (y ^ ((y ^ x) v z)') = 0.  [para(4(a,1),132(a,1,2,2,1,1))].

given #261 (T,wt=12): 1539 (x v (y ^ z)) ^ (y v x)' = 0.  [para(2(a,1),169(a,1,1))].

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

given #263 (T,wt=12): 1541 (x v y)' ^ ((x ^ z) v y) = 0.  [para(169(a,1),4(a,1)),flip(a)].

given #264 (T,wt=12): 1543 ((x ^ y) v (x ^ z)) ^ x' = 0.  [para(7(a,1),169(a,1,2,1))].

given #265 (T,wt=12): 1548 ((x ^ y) v (z ^ x)) ^ x' = 0.  [para(24(a,1),169(a,1,2,1))].

given #266 (T,wt=12): 1580 x v ((y v x)' v (z v y)) = 1.  [para(29(a,1),95(a,1,1)),rewrite(3(6),67(7),29(9))].

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

given #268 (T,wt=12): 1605 x v (y v ((y v x) ^ z)') = 1.  [para(2(a,1),170(a,1,2,2,1,1))].

given #269 (T,wt=12): 1616 (x ^ y) v (y ^ (z ^ x))' = 1.  [para(4(a,1),172(a,1,2,1)),rewrite(5(3))].

given #270 (T,wt=12): 1623 ((x v y) ^ z) v (z ^ x)' = 1.  [para(159(a,1),172(a,1,2,1))].

given #271 (T,wt=12): 1625 ((x v y) ^ z) v (z ^ y)' = 1.  [para(827(a,1),172(a,1,2,1))].

given #272 (A,wt=19): 140 x ^ (y ^ (z ^ ((y ^ (x ^ z)) v u))) = x ^ (y ^ z).  [para(17(a,1),21(a,1,2,2,1)),rewrite(5(5))].

given #273 (T,wt=12): 1686 (x ^ y)' v ((x v z) ^ y) = 1.  [para(181(a,1),2(a,1)),flip(a)].

given #274 (T,wt=12): 1688 (x ^ (y v z)) v (y ^ x)' = 1.  [para(4(a,1),181(a,1,1))].

given #275 (T,wt=12): 1690 ((x v y) ^ (x v z)) v x' = 1.  [para(6(a,1),181(a,1,2,1))].

given #276 (T,wt=12): 1695 ((x v y) ^ (z v x)) v x' = 1.  [para(18(a,1),181(a,1,2,1))].

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

given #278 (T,wt=12): 1736 x v (y v ((y ^ z) v x)') = 1.  [para(222(a,1),15(a,1)),flip(a)].

given #279 (T,wt=12): 1739 x v ((x ^ y) v (x ^ z))' = 1.  [para(222(a,1),22(a,1)),flip(a)].

given #280 (T,wt=12): 1744 x v ((x ^ y) v (z ^ x))' = 1.  [para(222(a,1),102(a,1)),flip(a)].

given #281 (T,wt=12): 1818 x ^ (y ^ ((y v z) ^ x)') = 0.  [para(237(a,1),17(a,1)),flip(a)].

given #282 (A,wt=15): 142 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y.  [para(21(a,1),20(a,1,2)),rewrite(20(3)),flip(a)].

given #283 (T,wt=12): 1820 x ^ ((x v y) ^ (x v z))' = 0.  [para(237(a,1),20(a,1)),flip(a)].

given #284 (T,wt=12): 1825 x ^ ((x v y) ^ (z v x))' = 0.  [para(237(a,1),83(a,1)),flip(a)].

given #285 (T,wt=12): 1954 x ^ ((y ^ x)' ^ (z ^ y)) = 0.  [para(4(a,1),278(a,1,2,1,1))].

given #286 (T,wt=12): 2431 x v (y v ((z ^ y) v x)') = 1.  [para(879(a,1),543(a,1,2)),rewrite(2(4))].

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

given #288 (T,wt=12): 2466 x v ((y ^ x) v (x ^ z))' = 1.  [para(549(a,1),102(a,1)),flip(a)].

given #289 (T,wt=12): 2487 x ^ (y ^ ((z v y) ^ x)') = 0.  [para(827(a,1),553(a,1,2)),rewrite(4(4))].

given #290 (T,wt=12): 2528 x ^ ((y v x) ^ (x v z))' = 0.  [para(559(a,1),83(a,1)),flip(a)].

given #291 (T,wt=12): 3101 (x v y)' ^ (x v (y ^ z)) = 0.  [para(715(a,1),4(a,1)),flip(a)].

given #292 (A,wt=15): 149 (x v y) ^ (z v (x v (y v u))) = x v y.  [para(3(a,1),52(a,1,2,2))].

given #293 (T,wt=12): 3138 (x ^ y)' v (x ^ (y v z)) = 1.  [para(806(a,1),2(a,1)),flip(a)].

given #294 (T,wt=12): 3245 (x ^ y)' v ((z v x) ^ y) = 1.  [para(829(a,1),2(a,1)),flip(a)].

given #295 (T,wt=12): 3247 (x ^ (y v z)) v (z ^ x)' = 1.  [para(4(a,1),829(a,1,1))].

given #296 (T,wt=12): 3249 ((x v y) ^ (y v z)) v y' = 1.  [para(6(a,1),829(a,1,2,1))].

given #297 (A,wt=13): 152 x ^ (y ^ (z v (x v u))) = y ^ x.  [para(52(a,1),17(a,1,2)),flip(a)].

given #298 (T,wt=12): 3254 ((x v y) ^ (z v y)) v y' = 1.  [para(18(a,1),829(a,1,2,1))].

given #299 (T,wt=12): 3304 x ^ ((y v x) ^ (z v x))' = 0.  [para(833(a,1),83(a,1)),flip(a)].

given #300 (T,wt=12): 3352 (x ^ y)' v (x ^ (z v y)) = 1.  [para(854(a,1),2(a,1)),flip(a)].

given #301 (T,wt=12): 3412 (x v (y ^ z)) ^ (z v x)' = 0.  [para(2(a,1),878(a,1,1))].

given #302 (A,wt=13): 153 x v (y v (x v z)) = y v (x v z).  [para(52(a,1),24(a,1,2)),rewrite(2(3))].

given #303 (T,wt=12): 3413 (x v y)' ^ ((z ^ x) v y) = 0.  [para(878(a,1),4(a,1)),flip(a)].

given #304 (T,wt=12): 3415 ((x ^ y) v (y ^ z)) ^ y' = 0.  [para(7(a,1),878(a,1,2,1))].

given #305 (T,wt=12): 3420 ((x ^ y) v (z ^ y)) ^ y' = 0.  [para(24(a,1),878(a,1,2,1))].

given #306 (T,wt=12): 3472 x v ((y ^ x) v (z ^ x))' = 1.  [para(883(a,1),102(a,1)),flip(a)].

given #307 (A,wt=18): 154 x v (y v z) != 1 | 0 != y | y' = x v (y v z).  [back_rewrite(151),rewrite(153(3))].

given #308 (T,wt=12): 3521 (x v y)' ^ (x v (z ^ y)) = 0.  [para(983(a,1),4(a,1)),flip(a)].

given #309 (T,wt=12): 4023 (x v y)' ^ ((y ^ z) v x) = 0.  [para(1480(a,1),4(a,1)),flip(a)].

given #310 (T,wt=12): 4049 (x v y)' ^ ((z ^ y) v x) = 0.  [para(1482(a,1),4(a,1)),flip(a)].

given #311 (T,wt=12): 4112 (x v y)' ^ (y v (x ^ z)) = 0.  [para(1539(a,1),4(a,1)),flip(a)].

given #312 (A,wt=13): 156 x ^ (y ^ (x ^ z)) = y ^ (x ^ z).  [para(57(a,1),5(a,2,2)),rewrite(17(3),5(2))].

given #313 (T,wt=12): 4211 x' ^ ((x ^ y) v (x ^ z)) = 0.  [para(7(a,1),1541(a,1,1,1))].

given #314 (T,wt=12): 4215 x' ^ ((x ^ y) v (z ^ x)) = 0.  [para(24(a,1),1541(a,1,1,1))].

given #315 (T,wt=12): 4502 (x ^ y)' v ((y v z) ^ x) = 1.  [para(1623(a,1),2(a,1)),flip(a)].

given #316 (T,wt=12): 4525 (x ^ y)' v ((z v y) ^ x) = 1.  [para(1625(a,1),2(a,1)),flip(a)].

given #317 (A,wt=13): 158 x ^ (y ^ (z ^ x)) = y ^ (z ^ x).  [para(5(a,1),59(a,1,2)),rewrite(5(5))].

given #318 (T,wt=12): 4660 (x ^ y)' v (y ^ (x v z)) = 1.  [para(4(a,1),1686(a,1,2))].

given #319 (T,wt=12): 4662 x' v ((x v y) ^ (x v z)) = 1.  [para(6(a,1),1686(a,1,1,1))].

given #320 (T,wt=12): 4666 x' v ((x v y) ^ (z v x)) = 1.  [para(18(a,1),1686(a,1,1,1))].

given #321 (T,wt=12): 5386 (x ^ y)' v (y ^ (z v x)) = 1.  [para(4(a,1),3245(a,1,2))].

given #322 (A,wt=17): 160 x v (y v (((x v y) ^ z) v u)) = x v (y v u).  [para(22(a,1),3(a,1)),rewrite(3(2)),flip(a)].

given #323 (T,wt=12): 5388 x' v ((y v x) ^ (x v z)) = 1.  [para(6(a,1),3245(a,1,1,1))].

given #324 (T,wt=12): 5392 x' v ((y v x) ^ (z v x)) = 1.  [para(18(a,1),3245(a,1,1,1))].

given #325 (T,wt=12): 5673 (x v y)' ^ (y v (z ^ x)) = 0.  [para(3412(a,1),4(a,1)),flip(a)].

given #326 (T,wt=12): 5733 x' ^ ((y ^ x) v (x ^ z)) = 0.  [para(7(a,1),3413(a,1,1,1))].

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

given #328 (T,wt=12): 5737 x' ^ ((y ^ x) v (z ^ x)) = 0.  [para(24(a,1),3413(a,1,1,1))].

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

given #330 (T,wt=13): 184 x v (y v (z v x)) = y v (z v x).  [para(3(a,1),65(a,1,2)),rewrite(3(5))].

given #331 (T,wt=13): 187 x v (y v ((y v x) ^ z)) = x v y.  [para(2(a,1),23(a,1,2,2,1))].

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

given #333 (T,wt=13): 199 x v (y v (z ^ (x ^ u))) = y v x.  [para(73(a,1),15(a,1,2)),flip(a)].

given #334 (T,wt=13): 201 x ^ ((y v (z v x)) ^ u) = x ^ u.  [para(82(a,1),5(a,1,1)),flip(a)].

given #335 (T,wt=13): 205 x ^ (y ^ (z v (u v x))) = y ^ x.  [para(82(a,1),17(a,1,2)),flip(a)].

given #336 (T,wt=13): 208 x v ((y ^ (z ^ x)) v u) = x v u.  [para(104(a,1),3(a,1,1)),flip(a)].

given #337 (A,wt=15): 164 x v (y v ((x ^ z) v u)) = y v (x v u).  [para(22(a,1),15(a,1,2)),flip(a)].

given #338 (T,wt=13): 212 x v (y v (z ^ (u ^ x))) = y v x.  [para(104(a,1),15(a,1,2)),flip(a)].

given #339 (T,wt=13): 223 (x ^ y) v (y ^ (x ^ z)) = y ^ x.  [para(4(a,1),25(a,1,1))].

given #340 (T,wt=13): 224 (x ^ y) v (y ^ (z ^ x)) = x ^ y.  [para(4(a,1),25(a,1,2)),rewrite(5(3))].

given #341 (T,wt=13): 257 x ^ (x ^ y)' != 0 | x ^ y = x.  [para(162(a,1),34(a,1)),rewrite(4(6),250(11)),xx(a)].

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

given #343 (T,wt=13): 258 x ^ (y ^ x)' != 0 | y ^ x = x.  [para(171(a,1),34(a,1)),rewrite(4(6),250(11)),xx(a)].

given #344 (T,wt=13): 272 x' ^ (y v x) != 0 | y v x = x.  [para(267(a,1),10(a,1)),rewrite(250(10)),flip(c),xx(a)].

given #345 (T,wt=13): 277 x' v (y ^ x) != 1 | y ^ x = x.  [para(268(a,1),10(b,1)),rewrite(250(10)),flip(c),xx(b)].

given #346 (T,wt=13): 280 (x ^ y) v y' != 1 | x ^ y = y.  [para(268(a,1),34(b,1)),rewrite(250(10)),flip(c),xx(b)].

given #347 (A,wt=15): 173 x ^ (x ^ y)' != 0 | (x ^ y)' = x'.  [para(162(a,1),10(a,1)),flip(c),xx(a)].

given #348 (T,wt=13): 358 x v (x v y)' != 1 | x v y = x.  [para(114(a,1),36(b,1)),rewrite(2(3),250(11)),xx(b)].

given #349 (T,wt=13): 360 x v (y v x)' != 1 | y v x = x.  [para(130(a,1),36(b,1)),rewrite(2(3),250(11)),xx(b)].

given #350 (T,wt=13): 365 (x v y) ^ y' != 0 | x v y = y.  [para(267(a,1),36(a,1)),rewrite(250(10)),flip(c),xx(a)].

given #351 (T,wt=13): 1003 x ^ (y v (z v (u v (x v v)))) = x.  [para(3(a,1),150(a,1,2,2))].

given #352 (A,wt=15): 178 x ^ (y ^ x)' != 0 | (y ^ x)' = x'.  [para(171(a,1),10(a,1)),flip(c),xx(a)].

given #353 (T,wt=13): 1017 (x v (y v z)) ^ (u ^ y) = u ^ y.  [para(15(a,1),159(a,1,1))].

given #354 (T,wt=13): 1034 x v (y v (z ^ (y v x))) = x v y.  [para(185(a,1),104(a,1,2,2)),rewrite(3(4))].

given #355 (T,wt=13): 1045 (x v (y v z)) ^ (y v x) = y v x.  [para(185(a,1),159(a,1,2)),rewrite(3(2),185(7))].

given #356 (T,wt=13): 1109 (x ^ (y ^ z)) v (u v y) = u v y.  [para(17(a,1),186(a,1,1))].

given #357 (A,wt=14): 182 (x ^ ((y ^ x) v z)) v (y ^ x)' = 1.  [para(21(a,1),171(a,1,2,1))].

given #358 (T,wt=13): 1127 x v (y ^ (z ^ (u ^ (x ^ v)))) = x.  [para(5(a,1),197(a,1,2,2))].

given #359 (T,wt=13): 1137 x ^ (y v (z v (u v (v v x)))) = x.  [para(3(a,1),200(a,1,2,2,2))].

given #360 (T,wt=13): 1164 x' ^ (x v y) != 0 | x v y = x.  [para(78(a,1),55(a,1)),rewrite(250(10)),flip(c),xx(a)].

given #361 (T,wt=13): 1193 x v (y ^ (z ^ (u ^ (v ^ x)))) = x.  [para(5(a,1),210(a,1,2,2,2))].

given #362 (A,wt=19): 188 x v (y v (z v ((x v (y v z)) ^ u))) = x v (y v z).  [para(23(a,1),3(a,1)),rewrite(3(2),3(4)),flip(a)].

given #363 (T,wt=13): 1222 (x ^ (y ^ z)) v (y ^ x) = x ^ y.  [para(230(a,1),22(a,2)),rewrite(5(3),1217(6))].

given #364 (T,wt=13): 1223 x ^ (y ^ (z v (y ^ x))) = x ^ y.  [para(230(a,1),82(a,1,2,2)),rewrite(5(4))].

given #365 (T,wt=13): 1260 (x v (y v z)) ^ (u ^ z) = u ^ z.  [para(3(a,1),827(a,1,1))].

given #366 (T,wt=13): 1278 (x v (y v z)) ^ (z v y) = z v y.  [para(185(a,1),827(a,1,2)),rewrite(185(7))].

given #367 (A,wt=26): 189 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | x' = y v ((x v y) ^ z).  [para(23(a,1),10(a,1))].

given #368 (T,wt=13): 1285 (x ^ (y ^ z)) v (u v z) = u v z.  [para(5(a,1),879(a,1,1))].

given #369 (T,wt=13): 1305 (x ^ (y ^ z)) v (z ^ y) = z ^ y.  [para(230(a,1),879(a,1,2)),rewrite(230(7))].

given #370 (T,wt=13): 1315 x' v (x ^ y) != 1 | x ^ y = x.  [para(81(a,1),75(b,1)),rewrite(250(10)),flip(c),xx(b)].

given #371 (T,wt=13): 1414 (x v y) ^ (z v (y v x)) = x v y.  [para(2(a,1),86(a,1,2)),rewrite(3(3))].

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

given #373 (T,wt=13): 1569 (x v (y v z)) ^ (z v x) = z v x.  [para(95(a,1),4(a,1)),flip(a)].

given #374 (T,wt=13): 2321 (x ^ y) v (z ^ (y ^ x)) = x ^ y.  [para(4(a,1),107(a,1,2)),rewrite(5(3))].

given #375 (T,wt=13): 4244 x ^ ((x' ^ y) v (x' ^ z)) = 0.  [para(250(a,1),1543(a,1,2)),rewrite(4(6))].

given #376 (T,wt=13): 4267 x ^ ((x' ^ y) v (z ^ x')) = 0.  [para(250(a,1),1548(a,1,2)),rewrite(4(6))].

given #377 (A,wt=19): 191 x v (y v (z v ((y v (x v z)) ^ u))) = x v (y v z).  [para(15(a,1),23(a,1,2,2,1)),rewrite(3(5))].

given #378 (T,wt=13): 4755 x v ((x' v y) ^ (x' v z)) = 1.  [para(250(a,1),1690(a,1,2)),rewrite(2(6))].

given #379 (T,wt=13): 4780 x v ((x' v y) ^ (z v x')) = 1.  [para(250(a,1),1695(a,1,2)),rewrite(2(6))].

given #380 (T,wt=13): 4971 x ^ (((x v y) ^ (x v z)) v u) = x.  [para(142(a,1),20(a,1)),rewrite(6(2)),flip(a)].

given #381 (T,wt=13): 4986 x ^ (((x v y) ^ (z v x)) v u) = x.  [para(142(a,1),83(a,1)),rewrite(18(2)),flip(a)].

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

given #383 (T,wt=13): 5492 x v ((y v x') ^ (x' v z)) = 1.  [para(250(a,1),3249(a,1,2)),rewrite(2(6))].

given #384 (T,wt=13): 5581 x v ((y v x') ^ (z v x')) = 1.  [para(250(a,1),3254(a,1,2)),rewrite(2(6))].

given #385 (T,wt=13): 5767 x ^ ((y ^ x') v (x' ^ z)) = 0.  [para(250(a,1),3415(a,1,2)),rewrite(4(6))].

given #386 (T,wt=13): 5787 x ^ ((y ^ x') v (z ^ x')) = 0.  [para(250(a,1),3420(a,1,2)),rewrite(4(6))].

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

given #388 (T,wt=13): 7416 (x ^ (y ^ z)) v (z ^ x) = z ^ x.  [para(224(a,1),2(a,1)),flip(a)].

given #389 (T,wt=13): 7511 x ^ (y ^ x)' != 0 | x ^ y = x.  [para(4(a,1),257(a,1,2,1))].

given #390 (T,wt=13): 7600 x ^ (x ^ y)' != 0 | y ^ x = x.  [para(4(a,1),258(a,1,2,1))].

given #391 (T,wt=13): 7602 (x v y) ^ x' != 0 | x v y = x.  [para(6(a,1),258(a,1,2,1)),rewrite(6(7)),flip(b)].

given #392 (A,wt=14): 194 (x v ((y v x) ^ z)) ^ (y v x)' = 0.  [para(23(a,1),130(a,1,2,1))].

given #393 (T,wt=13): 7627 x' ^ (x v y) != 0 | y v x = x.  [para(2(a,1),272(a,1,2))].

given #394 (T,wt=13): 7642 x' v (x ^ y) != 1 | y ^ x = x.  [para(4(a,1),277(a,1,2))].

given #395 (T,wt=13): 7668 (x ^ y) v x' != 1 | y ^ x = x.  [para(4(a,1),280(a,1,1))].

given #396 (T,wt=13): 7672 x v (y v x)' != 1 | x v y = x.  [para(2(a,1),358(a,1,2,1))].

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

given #398 (T,wt=13): 7675 x v (x v y)' != 1 | y v x = x.  [para(2(a,1),360(a,1,2,1))].

given #399 (T,wt=13): 7677 (x ^ y) v x' != 1 | x ^ y = x.  [para(7(a,1),360(a,1,2,1)),rewrite(7(7)),flip(b)].

given #400 (T,wt=13): 7692 (x v y) ^ x' != 0 | y v x = x.  [para(2(a,1),365(a,1,1))].

given #401 (T,wt=13): 8224 x' ^ (y v x) != 0 | x v y = x.  [para(2(a,1),1164(a,1,2))].

given #402 (A,wt=15): 196 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y.  [para(5(a,1),73(a,1,2,2))].

given #403 (T,wt=13): 8979 x' v (y ^ x) != 1 | x ^ y = x.  [para(4(a,1),1315(a,1,2))].

given #404 (T,wt=13): 9421 x ^ (((y v x) ^ (x v z)) v u) = x.  [para(2(a,1),4971(a,1,2,1,1))].

given #405 (T,wt=13): 9422 x ^ (y v ((x v z) ^ (x v u))) = x.  [para(2(a,1),4971(a,1,2))].

given #406 (T,wt=13): 9518 x ^ (((y v x) ^ (z v x)) v u) = x.  [para(2(a,1),4986(a,1,2,1,1))].

given #407 (A,wt=18): 198 1 != x | y ^ (x ^ z) != 0 | x' = y ^ (x ^ z).  [para(73(a,1),10(a,1)),rewrite(156(5)),flip(a)].

given #408 (T,wt=13): 9519 x ^ (y v ((x v z) ^ (u v x))) = x.  [para(2(a,1),4986(a,1,2))].

given #409 (T,wt=13): 9963 (x v y) ^ y' != 0 | y v x = y.  [para(2(a,1),7602(a,1,1))].

given #410 (T,wt=13): 10001 x v (((x ^ y) v (x ^ z)) ^ u) = x.  [para(195(a,1),22(a,1)),rewrite(7(2)),flip(a)].

given #411 (T,wt=13): 10017 x v (((x ^ y) v (z ^ x)) ^ u) = x.  [para(195(a,1),102(a,1)),rewrite(24(2)),flip(a)].

given #412 (A,wt=15): 202 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y.  [para(82(a,1),5(a,1)),flip(a)].

given #413 (T,wt=13): 10132 (x ^ y) v y' != 1 | y ^ x = y.  [para(4(a,1),7677(a,1,1))].

given #414 (T,wt=13): 10213 x ^ (y v ((z v x) ^ (x v u))) = x.  [para(2(a,1),9421(a,1,2))].

given #415 (T,wt=13): 10407 x ^ (y v ((z v x) ^ (u v x))) = x.  [para(2(a,1),9518(a,1,2))].

Low Water (keep, True_semantics): wt=45

given #416 (T,wt=13): 10660 x v (((y ^ x) v (x ^ z)) ^ u) = x.  [para(4(a,1),10001(a,1,2,1,1))].

Low Water (keep, True_semantics): wt=42

given #417 (A,wt=18): 203 x v (y v z) != 1 | 0 != z | z' = x v (y v z).  [para(82(a,1),10(b,1)),rewrite(184(3)),flip(b)].

Low Water (keep, True_semantics): wt=38

given #418 (T,wt=13): 10661 x v (y ^ ((x ^ z) v (x ^ u))) = x.  [para(4(a,1),10001(a,1,2))].

given #419 (T,wt=13): 10763 x v (((y ^ x) v (z ^ x)) ^ u) = x.  [para(4(a,1),10017(a,1,2,1,1))].

Low Water (keep, True_semantics): wt=37

given #420 (T,wt=13): 10764 x v (y ^ ((x ^ z) v (u ^ x))) = x.  [para(4(a,1),10017(a,1,2))].

Low Water (keep, True_semantics): wt=36

Low Water (keep, True_semantics): wt=35

given #421 (T,wt=13): 11191 x v (y ^ ((z ^ x) v (x ^ u))) = x.  [para(4(a,1),10660(a,1,2))].

given #422 (A,wt=15): 204 (x v y) ^ (z v (x v (u v y))) = x v y.  [para(15(a,1),82(a,1,2,2))].

given #423 (T,wt=13): 11424 x v (y ^ ((z ^ x) v (u ^ x))) = x.  [para(4(a,1),10763(a,1,2))].

Low Water (keep, True_semantics): wt=34

given #424 (T,wt=14): 218 x v (y v (z v (x v (y v z))')) = 1.  [para(29(a,1),3(a,1)),rewrite(3(3)),flip(a)].

given #425 (T,wt=14): 221 x v (y v (z v (y v (x v z))')) = 1.  [para(15(a,1),29(a,1,2,2,1)),rewrite(3(5))].

given #426 (T,wt=14): 233 x ^ (y ^ (z ^ (x ^ (y ^ z))')) = 0.  [para(32(a,1),5(a,1)),rewrite(5(3)),flip(a)].

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

given #428 (T,wt=14): 236 x ^ (y ^ (z ^ (y ^ (x ^ z))')) = 0.  [para(17(a,1),32(a,1,2,2,1)),rewrite(5(5))].

given #429 (T,wt=14): 238 x v (y v (z v ((x v y)' v u))) = 1.  [para(112(a,1),3(a,1)),flip(a)].

given #430 (T,wt=14): 242 x ^ (y ^ (z ^ ((x ^ y)' ^ u))) = 0.  [para(121(a,1),5(a,1)),flip(a)].

given #431 (T,wt=14): 247 x v y != 1 | x ^ y != 0 | y' = x.  [para(4(a,1),34(b,1))].

given #432 (A,wt=21): 207 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z).  [para(23(a,1),82(a,1,2,2))].

Low Water (keep, True_semantics): wt=33

given #433 (T,wt=14): 249 1 != x | x ^ y != 0 | (x ^ y)' = x.  [para(7(a,1),34(a,1)),rewrite(4(4),57(4)),flip(a)].

given #434 (T,wt=14): 253 1 != x | y ^ x != 0 | (y ^ x)' = x.  [para(24(a,1),34(a,1)),rewrite(4(4),59(4)),flip(a)].

given #435 (T,wt=14): 259 x v y != 1 | 0 != x | (x v y)' = x.  [para(63(a,1),34(a,1)),rewrite(4(5),6(5)),flip(b)].

given #436 (T,wt=14): 260 x v y != 1 | 0 != y | (x v y)' = y.  [para(65(a,1),34(a,1)),rewrite(4(5),18(5)),flip(b)].

given #437 (A,wt=15): 209 x v (y v (z ^ (u ^ (x v y)))) = x v y.  [para(104(a,1),3(a,1)),flip(a)].

given #438 (T,wt=14): 274 x v (y v (y v ((x v y) ^ z))') = 1.  [para(23(a,1),267(a,1,2)),rewrite(2(6),3(6))].

Low Water (keep, True_semantics): wt=31

given #439 (T,wt=14): 279 x ^ (y ^ (y ^ ((x ^ y) v z))') = 0.  [para(21(a,1),268(a,1,2)),rewrite(4(6),5(6))].

given #440 (T,wt=14): 281 (x v y) ^ ((x v (y v z))' ^ u) = 0.  [para(3(a,1),122(a,1,2,1,1))].

given #441 (T,wt=14): 282 x ^ (y ^ (((x ^ y) v z)' ^ u)) = 0.  [para(122(a,1),5(a,1)),flip(a)].

given #442 (A,wt=18): 211 1 != x | y ^ (z ^ x) != 0 | x' = y ^ (z ^ x).  [para(104(a,1),10(a,1)),rewrite(158(5)),flip(a)].

given #443 (T,wt=14): 316 x v y != 1 | 0 != y | (y v x)' = y.  [para(65(a,1),35(a,1)),rewrite(4(5),6(5)),flip(b)].

given #444 (T,wt=14): 329 x v (y v (z v (u v (x v y)'))) = 1.  [para(124(a,1),3(a,1)),flip(a)].

given #445 (T,wt=14): 336 x ^ (y ^ (z ^ (u ^ (x ^ y)'))) = 0.  [para(127(a,1),5(a,1)),flip(a)].

given #446 (T,wt=14): 341 (x v y) ^ (z ^ (x v (y v u))') = 0.  [para(3(a,1),129(a,1,2,2,1))].

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

given #448 (T,wt=14): 342 x ^ (y ^ (z ^ ((x ^ y) v u)')) = 0.  [para(129(a,1),5(a,1)),flip(a)].

given #449 (T,wt=14): 346 (x v y) ^ (z v (x v (y v u)))' = 0.  [para(3(a,1),134(a,1,2,1,2))].

given #450 (T,wt=14): 348 x ^ (y ^ (z v ((x ^ y) v u))') = 0.  [para(134(a,1),5(a,1)),flip(a)].

given #451 (T,wt=14): 373 x ^ (y ^ (z v (u v (x ^ y)))') = 0.  [para(143(a,1),5(a,1)),flip(a)].

given #452 (A,wt=17): 214 x v (y v (z v (u ^ (x v y)))) = x v (y v z).  [para(19(a,1),104(a,1,2,2)),rewrite(3(5),3(4))].

given #453 (T,wt=14): 375 (x v y) ^ (z v (x v (u v y)))' = 0.  [para(15(a,1),143(a,1,2,1,2))].

given #454 (T,wt=14): 377 ((x ^ y) v z) ^ (u v (x v z))' = 0.  [para(22(a,1),143(a,1,2,1,2))].

given #455 (T,wt=14): 379 x ^ (y ^ (z ^ (u v (x ^ y))')) = 0.  [para(25(a,1),143(a,1,2,1,2)),rewrite(5(6),5(5))].

given #456 (T,wt=14): 382 x ^ (y ^ ((z v (x ^ y))' ^ u)) = 0.  [para(144(a,1),5(a,1)),flip(a)].

given #457 (A,wt=17): 215 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z.  [para(20(a,1),104(a,1,2,2))].

Low Water (keep, True_semantics): wt=30

given #458 (T,wt=14): 384 (x v y) ^ ((x v (z v y))' ^ u) = 0.  [para(15(a,1),144(a,1,2,1,1))].

given #459 (T,wt=14): 386 ((x ^ y) v z) ^ ((x v z)' ^ u) = 0.  [para(22(a,1),144(a,1,2,1,1))].

given #460 (T,wt=14): 392 (x v y) ^ (z ^ (x v (u v y))') = 0.  [para(15(a,1),148(a,1,2,2,1))].

given #461 (T,wt=14): 393 ((x ^ y) v z) ^ (u ^ (x v z)') = 0.  [para(22(a,1),148(a,1,2,2,1))].

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

Low Water (keep, True_semantics): wt=29

given #463 (T,wt=14): 397 x v (y v (((x v y) ^ z)' v u)) = 1.  [para(167(a,1),3(a,1)),flip(a)].

given #464 (T,wt=14): 398 (x ^ y) v ((x ^ (y ^ z))' v u) = 1.  [para(5(a,1),167(a,1,2,1,1))].

given #465 (T,wt=14): 430 1 != x | y ^ x != 0 | (x ^ y)' = x.  [para(59(a,1),37(b,1)),rewrite(2(2),7(2)),flip(a)].

given #466 (T,wt=14): 457 x v (y v (z v ((x v y) ^ u)')) = 1.  [para(168(a,1),3(a,1)),flip(a)].

given #467 (A,wt=19): 219 x ^ (y v (x v y)') != 0 | y v (x v y)' = x'.  [para(29(a,1),10(a,1)),flip(c),xx(a)].

given #468 (T,wt=14): 458 (x ^ y) v (z v (x ^ (y ^ u))') = 1.  [para(5(a,1),168(a,1,2,2,1))].

given #469 (T,wt=14): 465 x v (y v (z ^ ((x v y) ^ u))') = 1.  [para(174(a,1),3(a,1)),flip(a)].

given #470 (T,wt=14): 466 (x ^ y) v (z ^ (x ^ (y ^ u)))' = 1.  [para(5(a,1),174(a,1,2,1,2))].

given #471 (T,wt=14): 472 x v (y v ((z ^ (x v y))' v u)) = 1.  [para(175(a,1),3(a,1)),flip(a)].

given #472 (A,wt=19): 225 (x ^ (y ^ z)) v (x ^ (y ^ (z ^ u))) = x ^ (y ^ z).  [para(5(a,1),25(a,1,1)),rewrite(5(5),5(8))].

given #473 (T,wt=14): 476 (x ^ y) v ((x ^ (z ^ y))' v u) = 1.  [para(17(a,1),175(a,1,2,1,1))].

given #474 (T,wt=14): 477 ((x v y) ^ z) v ((x ^ z)' v u) = 1.  [para(20(a,1),175(a,1,2,1,1))].

Low Water (keep, True_semantics): wt=28

given #475 (T,wt=14): 482 x v (y v (z ^ (u ^ (x v y)))') = 1.  [para(177(a,1),3(a,1)),flip(a)].

given #476 (T,wt=14): 486 (x ^ y) v (z ^ (x ^ (u ^ y)))' = 1.  [para(17(a,1),177(a,1,2,1,2))].

given #477 (A,wt=22): 226 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = x ^ (y ^ z).  [para(25(a,1),10(a,1)),rewrite(17(7),17(6),5(5),156(6),57(6))].

given #478 (T,wt=14): 487 x v (y v (z v (u ^ (x v y))')) = 1.  [para(19(a,1),177(a,1,2,1,2)),rewrite(3(6),3(5))].

Low Water (keep, True_semantics): wt=27

given #479 (T,wt=14): 488 ((x v y) ^ z) v (u ^ (x ^ z))' = 1.  [para(20(a,1),177(a,1,2,1,2))].

given #480 (T,wt=14): 536 (x ^ y) v (z v (x ^ (u ^ y))') = 1.  [para(17(a,1),179(a,1,2,2,1))].

given #481 (T,wt=14): 537 ((x v y) ^ z) v (u v (x ^ z)') = 1.  [para(20(a,1),179(a,1,2,2,1))].

given #482 (A,wt=17): 227 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y).  [para(25(a,1),15(a,1,2)),flip(a)].

given #483 (T,wt=14): 544 x v (y v (z v (z v (x v y))')) = 1.  [para(217(a,1),3(a,1)),flip(a)].

given #484 (T,wt=14): 545 x v (y v (z v (y v (z v x))')) = 1.  [para(3(a,1),217(a,1,2,2,1)),rewrite(3(5))].

given #485 (T,wt=14): 548 x v (y v (z v (x v (z v y))')) = 1.  [para(15(a,1),217(a,1,2,2,1)),rewrite(3(6))].

given #486 (T,wt=14): 554 x ^ (y ^ (z ^ (z ^ (x ^ y))')) = 0.  [para(232(a,1),5(a,1)),flip(a)].

given #487 (A,wt=19): 228 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z).  [para(17(a,1),25(a,1,1)),rewrite(5(4))].

given #488 (T,wt=14): 555 x ^ (y ^ (z ^ (y ^ (z ^ x))')) = 0.  [para(5(a,1),232(a,1,2,2,1)),rewrite(5(5))].

given #489 (T,wt=14): 558 x ^ (y ^ (z ^ (x ^ (z ^ y))')) = 0.  [para(17(a,1),232(a,1,2,2,1)),rewrite(5(6))].

given #490 (T,wt=14): 563 (x v y)' v (z v (x v (y v u))) = 1.  [para(3(a,1),269(a,1,2,2))].

given #491 (T,wt=14): 593 (x ^ y)' ^ (z ^ (x ^ (y ^ u))) = 0.  [para(5(a,1),270(a,1,2,2))].

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

given #493 (T,wt=14): 603 (x v y)' v (z v (x v (u v y))) = 1.  [para(15(a,1),271(a,1,2,2))].

given #494 (T,wt=14): 605 ((x ^ y) v z)' v (u v (x v z)) = 1.  [para(22(a,1),271(a,1,2,2))].

given #495 (T,wt=14): 609 (x ^ (y ^ z))' v (u v (x ^ y)) = 1.  [para(25(a,1),271(a,1,2,2))].

given #496 (T,wt=14): 617 (x ^ y)' ^ (z ^ (x ^ (u ^ y))) = 0.  [para(17(a,1),276(a,1,2,2))].

given #497 (A,wt=17): 231 x ^ (y ^ (z ^ (u v (x ^ y)))) = x ^ (y ^ z).  [para(25(a,1),82(a,1,2,2)),rewrite(5(5),5(4))].

given #498 (T,wt=14): 619 (x v (y v z))' ^ (u ^ (x v y)) = 0.  [para(19(a,1),276(a,1,2,2))].

given #499 (T,wt=14): 620 ((x v y) ^ z)' ^ (u ^ (x ^ z)) = 0.  [para(20(a,1),276(a,1,2,2))].

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

given #500 (T,wt=14): 631 x v (((x v y) ^ z)' v (u v y)) = 1.  [para(15(a,1),601(a,1,2)),rewrite(15(6))].

given #501 (T,wt=14): 632 x v (y v (((x ^ z) v y) ^ u)') = 1.  [para(22(a,1),601(a,1,2)),rewrite(2(6),3(6))].

given #502 (A,wt=19): 234 x v (y ^ (x ^ y)') != 1 | y ^ (x ^ y)' = x'.  [para(32(a,1),10(b,1)),flip(c),xx(b)].

given #503 (T,wt=14): 684 x v ((y ^ (x v z))' v (u v z)) = 1.  [para(15(a,1),604(a,1,2)),rewrite(15(6))].

Low Water (keep, True_semantics): wt=26

given #504 (T,wt=14): 685 (x ^ (y ^ z))' v (u v (x ^ z)) = 1.  [para(17(a,1),604(a,1,1,1))].

given #505 (T,wt=14): 686 (x ^ y)' v (z v ((x v u) ^ y)) = 1.  [para(20(a,1),604(a,1,1,1))].

given #506 (T,wt=14): 688 x v (y v (z ^ ((x ^ u) v y))') = 1.  [para(22(a,1),604(a,1,2)),rewrite(2(6),3(6))].

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

given #508 (T,wt=14): 695 x ^ (((x ^ y) v z)' ^ (u ^ y)) = 0.  [para(17(a,1),615(a,1,2)),rewrite(17(6))].

given #509 (T,wt=14): 696 x ^ (y ^ (((x v z) ^ y) v u)') = 0.  [para(20(a,1),615(a,1,2)),rewrite(4(6),5(6))].

given #510 (T,wt=14): 703 (x v (y v z))' ^ (u ^ (x v z)) = 0.  [para(15(a,1),618(a,1,1,1))].

given #511 (T,wt=14): 704 x ^ ((y v (x ^ z))' ^ (u ^ z)) = 0.  [para(17(a,1),618(a,1,2)),rewrite(17(6))].

given #512 (A,wt=19): 244 x v (y ^ (x' ^ z)) != 1 | y ^ (x' ^ z) = x'.  [para(121(a,1),10(b,1)),flip(c),xx(b)].

given #513 (T,wt=14): 705 x ^ (y ^ (z v ((x v u) ^ y))') = 0.  [para(20(a,1),618(a,1,2)),rewrite(4(6),5(6))].

given #514 (T,wt=14): 707 (x v y)' ^ (z ^ ((x ^ u) v y)) = 0.  [para(22(a,1),618(a,1,1,1))].

given #515 (T,wt=14): 721 (x v (y ^ z)) ^ (u v (x v y))' = 0.  [para(53(a,1),143(a,1,2,1,2))].

given #516 (T,wt=14): 722 (x v (y ^ z)) ^ ((x v y)' ^ u) = 0.  [para(53(a,1),144(a,1,2,1,1))].

Low Water (keep, True_semantics): wt=25

given #517 (A,wt=20): 246 x v (y v z) != 1 | z ^ (x v y) != 0 | z' = x v y.  [para(3(a,1),34(a,1))].

given #518 (T,wt=14): 723 (x v (y ^ z)) ^ (u ^ (x v y)') = 0.  [para(53(a,1),148(a,1,2,2,1))].

given #519 (T,wt=14): 725 (x v (y ^ z))' v (u v (x v y)) = 1.  [para(53(a,1),271(a,1,2,2))].

given #520 (T,wt=14): 726 x v (y v ((x v (y ^ z)) ^ u)') = 1.  [para(53(a,1),601(a,1,2)),rewrite(2(6),3(6))].

given #521 (T,wt=14): 727 x v (y v (z ^ (x v (y ^ u)))') = 1.  [para(53(a,1),604(a,1,2)),rewrite(2(6),3(6))].

given #522 (A,wt=20): 248 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | (y ^ z)' = x.  [para(5(a,1),34(b,1))].

given #523 (T,wt=14): 728 (x v y)' ^ (z ^ (x v (y ^ u))) = 0.  [para(53(a,1),618(a,1,1,1))].

given #524 (T,wt=14): 813 (x ^ (y v z)) v ((x ^ y)' v u) = 1.  [para(72(a,1),175(a,1,2,1,1))].

given #525 (T,wt=14): 814 (x ^ (y v z)) v (u ^ (x ^ y))' = 1.  [para(72(a,1),177(a,1,2,1,2))].

given #526 (T,wt=14): 815 (x ^ (y v z)) v (u v (x ^ y)') = 1.  [para(72(a,1),179(a,1,2,2,1))].

given #527 (A,wt=20): 251 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z)' = y.  [para(15(a,1),34(a,1))].

given #528 (T,wt=14): 816 (x ^ (y v z))' ^ (u ^ (x ^ y)) = 0.  [para(72(a,1),276(a,1,2,2))].

given #529 (T,wt=14): 817 (x ^ y)' v (z v (x ^ (y v u))) = 1.  [para(72(a,1),604(a,1,1,1))].

given #530 (T,wt=14): 818 x ^ (y ^ ((x ^ (y v z)) v u)') = 0.  [para(72(a,1),615(a,1,2)),rewrite(4(6),5(6))].

given #531 (T,wt=14): 819 x ^ (y ^ (z v (x ^ (y v u)))') = 0.  [para(72(a,1),618(a,1,2)),rewrite(4(6),5(6))].

given #532 (A,wt=20): 252 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z' = x ^ y.  [para(17(a,1),34(b,1))].

given #533 (T,wt=14): 837 ((x v y) ^ z) v ((y ^ z)' v u) = 1.  [para(83(a,1),175(a,1,2,1,1))].

given #534 (T,wt=14): 838 ((x v y) ^ z) v (u ^ (y ^ z))' = 1.  [para(83(a,1),177(a,1,2,1,2))].

given #535 (T,wt=14): 839 ((x v y) ^ z) v (u v (y ^ z)') = 1.  [para(83(a,1),179(a,1,2,2,1))].

given #536 (T,wt=14): 841 ((x v y) ^ z)' ^ (u ^ (y ^ z)) = 0.  [para(83(a,1),276(a,1,2,2))].

given #537 (A,wt=15): 254 x ^ (x' v y) != 0 | (x' v y)' = x.  [para(78(a,1),34(a,1)),rewrite(4(6)),xx(a)].

given #538 (T,wt=14): 842 (x ^ y)' v (z v ((u v x) ^ y)) = 1.  [para(83(a,1),604(a,1,1,1))].

Low Water (keep, True_semantics): wt=24

given #539 (T,wt=14): 843 x ^ (y ^ (((z v x) ^ y) v u)') = 0.  [para(83(a,1),615(a,1,2)),rewrite(4(6),5(6))].

given #540 (T,wt=14): 844 x ^ (y ^ (z v ((u v x) ^ y))') = 0.  [para(83(a,1),618(a,1,2)),rewrite(4(6),5(6))].

given #541 (T,wt=14): 863 (x ^ (y v z)) v ((x ^ z)' v u) = 1.  [para(87(a,1),175(a,1,2,1,1))].

given #542 (A,wt=15): 255 x ^ (y v x') != 0 | (y v x')' = x.  [para(90(a,1),34(a,1)),rewrite(4(6)),xx(a)].

given #543 (T,wt=14): 864 (x ^ (y v z)) v (u ^ (x ^ z))' = 1.  [para(87(a,1),177(a,1,2,1,2))].

given #544 (T,wt=14): 865 (x ^ (y v z)) v (u v (x ^ z)') = 1.  [para(87(a,1),179(a,1,2,2,1))].

given #545 (T,wt=14): 866 (x ^ (y v z))' ^ (u ^ (x ^ z)) = 0.  [para(87(a,1),276(a,1,2,2))].

given #546 (T,wt=14): 867 (x ^ y)' v (z v (x ^ (u v y))) = 1.  [para(87(a,1),604(a,1,1,1))].

given #547 (A,wt=22): 256 x v y != 1 | x ^ ((x ^ z) v y) != 0 | ((x ^ z) v y)' = x.  [para(22(a,1),34(a,1)),rewrite(4(6))].

Low Water (keep, True_semantics): wt=23

given #548 (T,wt=14): 868 x ^ (y ^ ((x ^ (z v y)) v u)') = 0.  [para(87(a,1),615(a,1,2)),rewrite(4(6),5(6))].

given #549 (T,wt=14): 869 x ^ (y ^ (z v (x ^ (u v y)))') = 0.  [para(87(a,1),618(a,1,2)),rewrite(4(6),5(6))].

given #550 (T,wt=14): 886 ((x ^ y) v z) ^ (u v (y v z))' = 0.  [para(102(a,1),143(a,1,2,1,2))].

given #551 (T,wt=14): 887 ((x ^ y) v z) ^ ((y v z)' ^ u) = 0.  [para(102(a,1),144(a,1,2,1,1))].

given #552 (A,wt=26): 261 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | (y v ((x v y) ^ z))' = x.  [para(23(a,1),34(a,1)),rewrite(4(7))].

given #553 (T,wt=14): 888 ((x ^ y) v z) ^ (u ^ (y v z)') = 0.  [para(102(a,1),148(a,1,2,2,1))].

given #554 (T,wt=14): 891 ((x ^ y) v z)' v (u v (y v z)) = 1.  [para(102(a,1),271(a,1,2,2))].

given #555 (T,wt=14): 892 x v (y v (((z ^ x) v y) ^ u)') = 1.  [para(102(a,1),601(a,1,2)),rewrite(2(6),3(6))].

given #556 (T,wt=14): 893 x v (y v (z ^ ((u ^ x) v y))') = 1.  [para(102(a,1),604(a,1,2)),rewrite(2(6),3(6))].

given #557 (A,wt=18): 262 1 != x | y ^ (x ^ z) != 0 | (y ^ (x ^ z))' = x.  [para(73(a,1),34(a,1)),rewrite(4(5),156(5)),flip(a)].

given #558 (T,wt=14): 894 (x v y)' ^ (z ^ ((u ^ x) v y)) = 0.  [para(102(a,1),618(a,1,1,1))].

given #559 (T,wt=14): 989 (x v (y ^ z)) ^ (u v (x v z))' = 0.  [para(106(a,1),143(a,1,2,1,2))].

given #560 (T,wt=14): 990 (x v (y ^ z)) ^ ((x v z)' ^ u) = 0.  [para(106(a,1),144(a,1,2,1,1))].

given #561 (T,wt=14): 991 (x v (y ^ z)) ^ (u ^ (x v z)') = 0.  [para(106(a,1),148(a,1,2,2,1))].

Low Water (keep, True_semantics): wt=22

given #562 (A,wt=18): 263 1 != x | y ^ (z ^ x) != 0 | (y ^ (z ^ x))' = x.  [para(104(a,1),34(a,1)),rewrite(4(5),158(5)),flip(a)].

given #563 (T,wt=14): 993 (x v (y ^ z))' v (u v (x v z)) = 1.  [para(106(a,1),271(a,1,2,2))].

given #564 (T,wt=14): 994 x v (y v ((x v (z ^ y)) ^ u)') = 1.  [para(106(a,1),601(a,1,2)),rewrite(2(6),3(6))].

given #565 (T,wt=14): 995 x v (y v (z ^ (x v (u ^ y)))') = 1.  [para(106(a,1),604(a,1,2)),rewrite(2(6),3(6))].

given #566 (T,wt=14): 996 (x v y)' ^ (z ^ (x v (u ^ y))) = 0.  [para(106(a,1),618(a,1,1,1))].

given #567 (A,wt=19): 264 x ^ (y v (x v y)') != 0 | (y v (x v y)')' = x.  [para(29(a,1),34(a,1)),rewrite(4(7)),xx(a)].

given #568 (T,wt=14): 1011 (x v (y v (z v u)))' ^ (v ^ z) = 0.  [para(150(a,1),276(a,1,2,2))].

given #569 (T,wt=14): 1012 x' v (y v (z v (u v (x v v)))) = 1.  [para(150(a,1),604(a,1,1,1))].

given #570 (T,wt=14): 1013 x ^ (y v (z v (u v (x v v))))' = 0.  [para(150(a,1),618(a,1,2)),rewrite(4(6))].

given #571 (T,wt=14): 1098 (x v (y v z)) ^ (z v (x v y))' = 0.  [para(3(a,1),1036(a,1,1))].

given #572 (A,wt=22): 265 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ (y ^ z))' = x ^ y.  [para(25(a,1),34(a,1)),rewrite(4(7),17(7),17(6),5(5),156(6),57(6))].

given #573 (T,wt=14): 1099 (x v (y v z)) ^ (y v (z v x))' = 0.  [para(3(a,1),1036(a,1,2,1))].

given #574 (T,wt=14): 1101 (x v (y v z)) ^ (x v (z v y))' = 0.  [para(15(a,1),1036(a,1,1)),rewrite(3(4))].

given #575 (T,wt=14): 1133 (x ^ (y ^ (z ^ u)))' v (v v z) = 1.  [para(197(a,1),271(a,1,2,2))].

given #576 (T,wt=14): 1134 x v (y ^ (z ^ (u ^ (x ^ v))))' = 1.  [para(197(a,1),604(a,1,2)),rewrite(2(6))].

given #577 (A,wt=19): 266 x ^ (y v (x' v z)) != 0 | (y v (x' v z))' = x.  [para(112(a,1),34(a,1)),rewrite(4(7)),xx(a)].

given #578 (T,wt=14): 1135 x' ^ (y ^ (z ^ (u ^ (x ^ v)))) = 0.  [para(197(a,1),618(a,1,1,1))].

given #579 (T,wt=14): 1150 (x v (y v (z v u)))' ^ (v ^ u) = 0.  [para(200(a,1),276(a,1,2,2))].

given #580 (T,wt=14): 1151 x' v (y v (z v (u v (v v x)))) = 1.  [para(200(a,1),604(a,1,1,1))].

given #581 (T,wt=14): 1152 x ^ (y v (z v (u v (v v x))))' = 0.  [para(200(a,1),618(a,1,2)),rewrite(4(6))].

given #582 (A,wt=15): 275 (x v y) ^ y' != 0 | (x v y)' = y'.  [para(267(a,1),34(a,1)),xx(a)].

given #583 (T,wt=14): 1204 (x ^ (y ^ (z ^ u)))' v (v v u) = 1.  [para(210(a,1),271(a,1,2,2))].

given #584 (T,wt=14): 1205 x v (y ^ (z ^ (u ^ (v ^ x))))' = 1.  [para(210(a,1),604(a,1,2)),rewrite(2(6))].

given #585 (T,wt=14): 1206 x' ^ (y ^ (z ^ (u ^ (v ^ x)))) = 0.  [para(210(a,1),618(a,1,1,1))].

given #586 (T,wt=14): 1238 (x ^ (y ^ z)) v (z ^ (x ^ y))' = 1.  [para(5(a,1),1225(a,1,1))].

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

given #588 (T,wt=14): 1239 (x ^ (y ^ z)) v (y ^ (z ^ x))' = 1.  [para(5(a,1),1225(a,1,2,1))].

given #589 (T,wt=14): 1241 (x ^ (y ^ z)) v (x ^ (z ^ y))' = 1.  [para(17(a,1),1225(a,1,1)),rewrite(5(4))].

given #590 (T,wt=14): 1246 1 != x | y ^ x != 0 | x' = x ^ y.  [para(4(a,1),62(b,1))].

given #591 (T,wt=14): 1256 x v y != 1 | 0 != y | y' = y v x.  [para(2(a,1),66(a,1))].

given #592 (A,wt=20): 285 x v (y v z) != 1 | (z v x) ^ y != 0 | (z v x)' = y.  [para(2(a,1),35(a,1)),rewrite(3(2))].

given #593 (T,wt=14): 1359 (x ^ (y v (z ^ x))) v (z ^ x)' = 1.  [para(84(a,1),171(a,1,2,1))].

given #594 (T,wt=14): 1361 x ^ (y ^ (y ^ (z v (x ^ y)))') = 0.  [para(84(a,1),268(a,1,2)),rewrite(4(6),5(6))].

given #595 (T,wt=14): 1391 x v y != 1 | 0 != x | x' = y v x.  [para(2(a,1),85(a,1))].

given #596 (T,wt=14): 1405 x v (y v (z v ((x v z)' v u))) = 1.  [para(110(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #597 (A,wt=20): 286 x v (y v z) != 1 | (y v x) ^ z != 0 | (x v y)' = z.  [para(2(a,1),35(b,1,1))].

given #598 (T,wt=14): 1407 x v (y v (((x ^ z) v y)' v u)) = 1.  [para(110(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #599 (T,wt=14): 1411 x v (y v (((z ^ x) v y)' v u)) = 1.  [para(110(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #600 (T,wt=14): 1428 x v (y v (z v (u ^ (x v z))')) = 1.  [para(86(a,1),177(a,1,2,1,2)),rewrite(3(6),3(5))].

given #601 (T,wt=14): 1429 x v (y v (z v (u v (x v z)'))) = 1.  [para(86(a,1),179(a,1,2,2,1)),rewrite(3(6),3(5))].

given #602 (A,wt=26): 287 x v (y v (z v u)) != 1 | (x v (y v z)) ^ u != 0 | (x v (y v z))' = u.  [para(3(a,1),35(a,1,2))].

given #603 (T,wt=14): 1430 (x v y) ^ (x v (z v (y v u)))' = 0.  [para(86(a,1),615(a,1,2)),rewrite(3(3),3(2),4(6))].

given #604 (T,wt=14): 1441 x ^ (y ^ (z ^ ((x ^ z)' ^ u))) = 0.  [para(119(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #605 (T,wt=14): 1443 x ^ (y ^ (((x v z) ^ y)' ^ u)) = 0.  [para(119(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #606 (T,wt=14): 1447 x ^ (y ^ (((z v x) ^ y)' ^ u)) = 0.  [para(119(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #607 (A,wt=20): 288 x v (y v z) != 1 | z ^ (x v y) != 0 | (x v y)' = z.  [para(4(a,1),35(b,1))].

given #608 (T,wt=14): 1454 x v (y v (z v ((x ^ u) v y)')) = 1.  [para(123(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #609 (T,wt=14): 1458 x v (y v (z v ((u ^ x) v y)')) = 1.  [para(123(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #610 (T,wt=14): 1463 x ^ (y ^ (z ^ (u ^ (x ^ z)'))) = 0.  [para(126(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #611 (T,wt=14): 1465 x ^ (y ^ (z ^ ((x v u) ^ y)')) = 0.  [para(126(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #612 (A,wt=18): 289 x v y != 1 | y ^ z != 0 | (x v y)' = y ^ z.  [para(7(a,1),35(a,1,2)),rewrite(17(6),83(6))].

given #613 (T,wt=14): 1469 x ^ (y ^ (z ^ ((u v x) ^ y)')) = 0.  [para(126(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #614 (T,wt=14): 1479 (x v (y ^ z)) ^ (x v (u v y))' = 0.  [para(186(a,1),131(a,1,2,1,2))].

given #615 (T,wt=14): 1481 (x v (y ^ z)) ^ (x v (u v z))' = 0.  [para(879(a,1),131(a,1,2,1,2))].

given #616 (T,wt=14): 1500 x ^ (y ^ (z ^ ((x ^ z) v u)')) = 0.  [para(132(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

Low Water (keep, True_semantics): wt=21

given #617 (A,wt=26): 290 x v (y v (z v u)) != 1 | (x v z) ^ (y v u) != 0 | (x v z)' = y v u.  [para(15(a,1),35(a,1,2))].

given #618 (T,wt=14): 1510 x ^ (y ^ (z ^ (u v (x ^ z))')) = 0.  [para(145(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #619 (T,wt=14): 1519 (x v y) ^ (x v (z v (u v y)))' = 0.  [para(3(a,1),147(a,1,2,1,2))].

given #620 (T,wt=14): 1524 (x v ((x v y) ^ z)) ^ (x v y)' = 0.  [para(23(a,1),147(a,1,2,1))].

given #621 (T,wt=14): 1525 (x v (y ^ (z ^ u))) ^ (x v z)' = 0.  [para(73(a,1),147(a,1,2,1,2))].

given #622 (A,wt=20): 291 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x)' = z.  [para(15(a,1),35(a,1))].

given #623 (T,wt=14): 1526 (x v (y ^ (z ^ u))) ^ (x v u)' = 0.  [para(104(a,1),147(a,1,2,1,2))].

given #624 (T,wt=14): 1536 (x v (y ^ z)) ^ (x v (z ^ y))' = 0.  [para(230(a,1),147(a,1,2,1,2))].

given #625 (T,wt=14): 1547 ((x ^ (y ^ z)) v u) ^ (y v u)' = 0.  [para(17(a,1),169(a,1,1,1))].

given #626 (T,wt=14): 1551 ((x ^ y) v (z ^ (x ^ u))) ^ x' = 0.  [para(73(a,1),169(a,1,2,1))].

given #627 (A,wt=26): 292 x v (y v (z v u)) != 1 | (y v (x v z)) ^ u != 0 | (x v (y v z))' = u.  [para(15(a,1),35(b,1,1)),rewrite(3(2))].

given #628 (T,wt=14): 1552 ((x ^ y) v (z ^ (u ^ x))) ^ x' = 0.  [para(104(a,1),169(a,1,2,1))].

given #629 (T,wt=14): 1560 ((x ^ y) v z) ^ (y v (u v z))' = 0.  [para(159(a,1),169(a,1,1,1)),rewrite(3(4))].

given #630 (T,wt=14): 1565 (x v (y v z)) ^ (y v (x v z))' = 0.  [para(94(a,1),169(a,1,1,1)),rewrite(3(2),3(4))].

given #631 (T,wt=14): 1584 x v (y v (z v ((z v x)' v u))) = 1.  [para(95(a,1),175(a,1,2,1,1)),rewrite(3(6),3(5))].

given #632 (A,wt=18): 293 x v y != 1 | x v y != 0 | (x v y)' = x v y.  [para(26(a,1),35(b,1)),rewrite(65(2),63(2))].

given #633 (T,wt=14): 1585 x v (y v (z v (u ^ (z v x))')) = 1.  [para(95(a,1),177(a,1,2,1,2)),rewrite(3(6),3(5))].

given #634 (T,wt=14): 1586 x v (y v (z v (u v (z v x)'))) = 1.  [para(95(a,1),179(a,1,2,2,1)),rewrite(3(6),3(5))].

given #635 (T,wt=14): 1587 (x v (y v z))' ^ (u ^ (z v x)) = 0.  [para(95(a,1),276(a,1,2,2))].

given #636 (T,wt=14): 1588 (x v y)' v (z v (y v (u v x))) = 1.  [para(95(a,1),604(a,1,1,1))].

given #637 (A,wt=26): 296 x v (y v (z ^ u)) != 1 | z ^ ((x v y) ^ u) != 0 | (x v y)' = z ^ u.  [para(17(a,1),35(b,1))].

given #638 (T,wt=14): 1589 (x v y) ^ (y v (z v (x v u)))' = 0.  [para(95(a,1),615(a,1,2)),rewrite(3(3),3(2),4(6))].

given #639 (T,wt=14): 1590 (x v y) ^ (z v (y v (u v x)))' = 0.  [para(95(a,1),618(a,1,2)),rewrite(4(6))].

given #640 (T,wt=14): 1602 x v ((y v x)' v (z v (u v y))) = 1.  [para(110(a,1),95(a,1,1)),rewrite(3(7),3(6),67(8),110(11))].

given #641 (T,wt=14): 1603 x v (y v ((z v x)' v (u v z))) = 1.  [para(123(a,1),95(a,1,1)),rewrite(3(7),3(6),67(8),123(11))].

Low Water (keep, True_semantics): wt=20

given #642 (A,wt=22): 297 x v (y v z) != 1 | y v z != 0 | (y v z)' = x v (y v z).  [para(18(a,1),35(b,1)),rewrite(184(3),153(3))].

given #643 (T,wt=14): 1608 x v (y v (z v ((x v z) ^ u)')) = 1.  [para(170(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #644 (T,wt=14): 1615 x v (((y v x) ^ z)' v (u v y)) = 1.  [para(170(a,1),95(a,1,1)),rewrite(3(7),67(8),170(11))].

given #645 (T,wt=14): 1619 (x ^ y) v (x ^ (z ^ (y ^ u)))' = 1.  [para(17(a,1),172(a,1,2,1,2))].

given #646 (T,wt=14): 1622 (x ^ (y v z)) v (x ^ (u ^ y))' = 1.  [para(159(a,1),172(a,1,2,1,2))].

given #647 (A,wt=19): 299 (x v y) ^ (y' v z) != 0 | (x v y)' = y' v z.  [para(78(a,1),35(a,1,2)),rewrite(88(2)),xx(a)].

given #648 (T,wt=14): 1624 (x ^ (y v z)) v (x ^ (u ^ z))' = 1.  [para(827(a,1),172(a,1,2,1,2))].

given #649 (T,wt=14): 1626 (x ^ (y v z)) v (x ^ (z v y))' = 1.  [para(94(a,1),172(a,1,2,1,2))].

given #650 (T,wt=14): 1635 x v ((y ^ (z v x))' v (u v z)) = 1.  [para(176(a,1),95(a,1,1)),rewrite(3(7),67(8),176(11))].

given #651 (T,wt=14): 1637 (x ^ y) v (x ^ (z ^ (u ^ y)))' = 1.  [para(5(a,1),180(a,1,2,1,2))].

given #652 (A,wt=32): 300 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(20(a,1),35(b,1)),rewrite(3(2),3(15))].

given #653 (T,wt=14): 1643 (x ^ ((x ^ y) v z)) v (x ^ y)' = 1.  [para(21(a,1),180(a,1,2,1))].

given #654 (T,wt=14): 1644 (x ^ (y v (z v u))) v (x ^ z)' = 1.  [para(52(a,1),180(a,1,2,1,2))].

given #655 (T,wt=14): 1645 (x ^ (y v (z v u))) v (x ^ u)' = 1.  [para(82(a,1),180(a,1,2,1,2))].

given #656 (T,wt=14): 1656 (x ^ (y v (x ^ z))) v (x ^ z)' = 1.  [para(84(a,1),180(a,1,2,1))].

given #657 (A,wt=23): 301 x v (y v ((x v y)' ^ z)) != 1 | (x v y)' ^ z = (x v y)'.  [para(81(a,1),35(b,1)),flip(c),xx(b)].

given #658 (T,wt=14): 1692 ((x v (y v z)) ^ u) v (y ^ u)' = 1.  [para(15(a,1),181(a,1,1,1))].

given #659 (T,wt=14): 1699 ((x v y) ^ (z v (x v u))) v x' = 1.  [para(52(a,1),181(a,1,2,1))].

given #660 (T,wt=14): 1700 ((x v y) ^ (z v (u v x))) v x' = 1.  [para(82(a,1),181(a,1,2,1))].

given #661 (T,wt=14): 1709 ((x v y) ^ z) v (y ^ (u ^ z))' = 1.  [para(186(a,1),181(a,1,1,1)),rewrite(5(4))].

given #662 (A,wt=19): 302 (x v y) ^ (z v y') != 0 | (x v y)' = z v y'.  [para(90(a,1),35(a,1,2)),rewrite(88(2)),xx(a)].

given #663 (T,wt=14): 1714 (x ^ y)' v (((x v z) ^ y) v u) = 1.  [para(181(a,1),94(a,1,1)),rewrite(67(8),1686(11))].

given #664 (T,wt=14): 1722 x v (y v (z v (u v (x v u)'))) = 1.  [para(3(a,1),220(a,1,2))].

given #665 (T,wt=14): 1724 x v (y v (z v ((x ^ u) v z)')) = 1.  [para(220(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #666 (T,wt=14): 1729 x v (y v (z v ((u ^ x) v z)')) = 1.  [para(220(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #667 (A,wt=15): 303 (x v y) ^ x' != 0 | (x v y)' = x'.  [para(90(a,1),35(a,1)),xx(a)].

given #668 (T,wt=14): 1738 x v (y v ((z ^ (x ^ u)) v y)') = 1.  [para(17(a,1),222(a,1,2,2,1,1))].

given #669 (T,wt=14): 1748 x v (((y ^ z) v x)' v (u v y)) = 1.  [para(222(a,1),95(a,1,1)),rewrite(3(7),67(8),222(11))].

given #670 (T,wt=14): 1754 x ^ (y ^ (z ^ (u ^ (x ^ u)'))) = 0.  [para(5(a,1),235(a,1,2))].

given #671 (T,wt=14): 1756 x ^ (y ^ (z ^ ((x v u) ^ z)')) = 0.  [para(235(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #672 (A,wt=23): 304 x v (y v (z ^ (x v y)')) != 1 | z ^ (x v y)' = (x v y)'.  [para(92(a,1),35(b,1)),flip(c),xx(b)].

given #673 (T,wt=14): 1762 x ^ (y ^ (z ^ ((u v x) ^ z)')) = 0.  [para(235(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #674 (T,wt=14): 1809 ((x ^ y) v z) ^ (x v (z v u))' = 0.  [para(169(a,1),97(a,1,2)),rewrite(4(4),80(4)),flip(a)].

given #675 (T,wt=14): 1817 x ^ (y ^ ((z v (x v u)) ^ y)') = 0.  [para(15(a,1),237(a,1,2,2,1,1))].

given #676 (T,wt=14): 1835 x v (y v (z v (u v (x' v v)))) = 1.  [para(3(a,1),239(a,1,2,2))].

given #677 (A,wt=23): 305 x v (y v (x v (y v z))') != 1 | (x v (y v z))' = (x v y)'.  [para(114(a,1),35(b,1)),rewrite(3(2),3(14)),flip(c),xx(b)].

given #678 (T,wt=14): 1836 x v (y v (z v ((x ^ u)' v v))) = 1.  [para(239(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #679 (T,wt=14): 1841 x v (y v (z v ((u ^ x)' v v))) = 1.  [para(239(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #680 (T,wt=14): 1846 x v (y v ((z ^ (x ^ u))' v v)) = 1.  [para(17(a,1),241(a,1,2,2,1,1))].

given #681 (T,wt=14): 1852 x v (y v (z v ((y v x)' v u))) = 1.  [para(94(a,1),241(a,1,2,2,1,1)),rewrite(3(6))].

given #682 (A,wt=36): 306 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(21(a,1),35(b,1))].

given #683 (T,wt=14): 1856 x ^ (y ^ (z ^ (u ^ (x' ^ v)))) = 0.  [para(5(a,1),243(a,1,2,2))].

given #684 (T,wt=14): 1857 x ^ (y ^ (z ^ ((x v u)' ^ v))) = 0.  [para(243(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #685 (T,wt=14): 1862 x ^ (y ^ (z ^ ((u v x)' ^ v))) = 0.  [para(243(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #686 (T,wt=14): 1880 x v (y v ((z ^ (u ^ x))' v v)) = 1.  [para(177(a,1),99(a,1,1,2)),rewrite(88(2),67(8),485(11))].

given #687 (A,wt=23): 307 x v (y v (z v (x v y))') != 1 | (z v (x v y))' = (x v y)'.  [para(130(a,1),35(b,1)),flip(c),xx(b)].

given #688 (T,wt=14): 1883 (x ^ y)' v (z v (u v (x v v))) = 1.  [para(601(a,1),99(a,1,1,2)),rewrite(88(2),3(5),67(8),629(11))].

given #689 (T,wt=14): 1884 (x ^ y)' v (z v (u v (y v v))) = 1.  [para(604(a,1),99(a,1,1,2)),rewrite(88(2),3(5),67(8),682(11))].

given #690 (T,wt=14): 1890 (x ^ y) v (z v ((y ^ x)' v u)) = 1.  [para(1225(a,1),99(a,1,1,2)),rewrite(88(2),67(8),1240(11))].

given #691 (T,wt=14): 1898 x v (y v (((y v x) ^ z)' v u)) = 1.  [para(170(a,1),99(a,1,1)),rewrite(67(8),1605(11))].

given #692 (A,wt=22): 309 x v y != 1 | (x v y) ^ z != 0 | (x v y)' = (x v y) ^ z.  [para(57(a,1),35(b,1)),rewrite(23(4))].

given #693 (T,wt=14): 1901 x v (y v ((z ^ (y v x))' v u)) = 1.  [para(176(a,1),99(a,1,1)),rewrite(67(8),1039(11))].

given #694 (T,wt=14): 1908 x v (y v (((y ^ z) v x)' v u)) = 1.  [para(222(a,1),99(a,1,1)),rewrite(67(8),1736(11))].

given #695 (T,wt=14): 1912 x ^ (y ^ ((z v (x v u))' ^ v)) = 0.  [para(15(a,1),245(a,1,2,2,1,1))].

given #696 (T,wt=14): 1922 x v ((x v y)' v (z v (y v u))) = 1.  [para(273(a,1),3(a,1,1)),rewrite(77(2),3(6),3(5)),flip(a)].

given #697 (A,wt=22): 310 x v y != 1 | z ^ (x v y) != 0 | (x v y)' = z ^ (x v y).  [para(59(a,1),35(b,1)),rewrite(103(4))].

given #698 (T,wt=14): 1924 x v ((x v y)' v (z v (u v y))) = 1.  [para(3(a,1),273(a,1,2,2))].

given #699 (T,wt=14): 1926 x v (y v ((x v z)' v (u v z))) = 1.  [para(273(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #700 (T,wt=14): 1928 x v (((x ^ y) v z)' v (u v z)) = 1.  [para(273(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #701 (T,wt=14): 1931 x v (y v (x v (z ^ (y ^ u)))') = 1.  [para(73(a,1),273(a,1,2,2)),rewrite(2(5))].

given #702 (A,wt=28): 311 x v (y v z) != 1 | (x v y) ^ ((y ^ u) v z) != 0 | (x v y)' = (y ^ u) v z.  [para(22(a,1),35(a,1,2))].

given #703 (T,wt=14): 1932 x v (y v (x v (z ^ (u ^ y)))') = 1.  [para(104(a,1),273(a,1,2,2)),rewrite(2(5))].

given #704 (T,wt=14): 1940 x v (((y ^ x) v z)' v (u v z)) = 1.  [para(273(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #705 (T,wt=14): 1948 x v ((y ^ z) v (x v (z ^ y))') = 1.  [para(230(a,1),273(a,1,2,2)),rewrite(2(5))].

given #706 (T,wt=14): 1949 x v (y v (y v (z ^ (x v y)))') = 1.  [para(273(a,1),879(a,1)),rewrite(2(4),2(7),3(7)),flip(a)].

given #707 (A,wt=19): 312 (x v y) ^ (y ^ z)' != 0 | (x v y)' = (y ^ z)'.  [para(162(a,1),35(a,1,2)),rewrite(88(2)),xx(a)].

given #708 (T,wt=14): 1955 x ^ ((x ^ y)' ^ (z ^ (y ^ u))) = 0.  [para(278(a,1),5(a,1,1)),rewrite(80(2),5(6),5(5)),flip(a)].

given #709 (T,wt=14): 1957 x ^ ((x ^ y)' ^ (z ^ (u ^ y))) = 0.  [para(5(a,1),278(a,1,2,2))].

given #710 (T,wt=14): 1959 x ^ (y ^ ((x ^ z)' ^ (u ^ z))) = 0.  [para(278(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #711 (T,wt=14): 1961 x ^ (((x v y) ^ z)' ^ (u ^ z)) = 0.  [para(278(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #712 (A,wt=19): 313 (x v y) ^ (z ^ y)' != 0 | (x v y)' = (z ^ y)'.  [para(171(a,1),35(a,1,2)),rewrite(88(2)),xx(a)].

given #713 (T,wt=14): 1964 x ^ (y ^ (x ^ (z v (y v u)))') = 0.  [para(52(a,1),278(a,1,2,2)),rewrite(4(5))].

given #714 (T,wt=14): 1965 x ^ (y ^ (x ^ (z v (u v y)))') = 0.  [para(82(a,1),278(a,1,2,2)),rewrite(4(5))].

given #715 (T,wt=14): 1972 x ^ (((y v x) ^ z)' ^ (u ^ z)) = 0.  [para(278(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #716 (T,wt=14): 1977 x ^ ((y v z) ^ (x ^ (z v y))') = 0.  [para(185(a,1),278(a,1,2,2)),rewrite(4(5))].

given #717 (A,wt=24): 314 x v (y v z) != 1 | (x v y) ^ (y v z) != 0 | (x v y)' = y v z.  [para(63(a,1),35(a,1,2))].

given #718 (T,wt=14): 1991 x ^ ((y v (z v (x v u)))' ^ v) = 0.  [para(3(a,1),284(a,1,2,1,1))].

given #719 (T,wt=14): 1998 x ^ (y ^ ((z v (u v x))' ^ v)) = 0.  [para(186(a,1),284(a,1,2,1,1,2)),rewrite(5(6))].

given #720 (T,wt=14): 2030 x v (y v (z v (u v (v v x')))) = 1.  [para(3(a,1),330(a,1,2,2,2))].

given #721 (T,wt=14): 2031 x v (y v (z v (u v (x ^ v)'))) = 1.  [para(330(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #722 (A,wt=24): 315 x v (y v z) != 1 | (x v z) ^ (y v z) != 0 | (x v z)' = y v z.  [para(65(a,1),35(a,1,2))].

given #723 (T,wt=14): 2036 x v (y v (z v (u v (v ^ x)'))) = 1.  [para(330(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #724 (T,wt=14): 2042 x v (y v (z v (u ^ (x ^ v))')) = 1.  [para(17(a,1),332(a,1,2,2,2,1))].

given #725 (T,wt=14): 2048 x v (y v (z v (u v (y v x)'))) = 1.  [para(94(a,1),332(a,1,2,2,2,1)),rewrite(3(6))].

given #726 (T,wt=14): 2054 x ^ (y ^ (z ^ (u ^ (v ^ x')))) = 0.  [para(5(a,1),337(a,1,2,2,2))].

given #727 (A,wt=32): 317 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(23(a,1),35(a,1,2))].

given #728 (T,wt=14): 2055 x ^ (y ^ (z ^ (u ^ (x v v)'))) = 0.  [para(337(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #729 (T,wt=14): 2060 x ^ (y ^ (z ^ (u ^ (v v x)'))) = 0.  [para(337(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #730 (T,wt=14): 2065 x ^ (y ^ (z ^ (u v (x v v))')) = 0.  [para(15(a,1),339(a,1,2,2,2,1))].

given #731 (T,wt=14): 2103 x ^ (y ^ (z v (u v (x v v)))') = 0.  [para(3(a,1),344(a,1,2,2,1))].

given #732 (A,wt=23): 321 (x v y) ^ (z v (y v z)') != 0 | (x v y)' = z v (y v z)'.  [para(29(a,1),35(a,1,2)),rewrite(88(2)),xx(a)].

given #733 (T,wt=14): 2110 x ^ (y ^ (z ^ (u v (v v x))')) = 0.  [para(186(a,1),344(a,1,2,2,1,2)),rewrite(5(6))].

given #734 (T,wt=14): 2118 x ^ (y ^ (z v (u v (v v x)))') = 0.  [para(186(a,1),347(a,1,2,1,2,2)),rewrite(5(6))].

given #735 (T,wt=14): 2121 x ^ ((y v (z v (u v x)))' ^ v) = 0.  [para(371(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #736 (T,wt=14): 2135 x ^ (y ^ (z v (u v (y ^ x)))') = 0.  [para(230(a,1),371(a,1,2,1,2,2)),rewrite(5(6))].

given #737 (A,wt=27): 323 x v (y v (z ^ ((x v y) ^ z)')) != 1 | z ^ ((x v y) ^ z)' = (x v y)'.  [para(32(a,1),35(b,1)),flip(c),xx(b)].

given #738 (T,wt=14): 2151 x ^ (y ^ ((z v (y ^ x))' ^ u)) = 0.  [para(230(a,1),372(a,1,2,1,1,2)),rewrite(5(6))].

given #739 (T,wt=14): 2158 (x v (y ^ (z v x))) ^ (z v x)' = 0.  [para(103(a,1),130(a,1,2,1))].

given #740 (T,wt=14): 2182 (x v (y ^ (x v z))) ^ (x v z)' = 0.  [para(103(a,1),147(a,1,2,1))].

given #741 (T,wt=14): 2200 x ^ (y ^ (z ^ (u v (y ^ x))')) = 0.  [para(230(a,1),376(a,1,2,2,1,2)),rewrite(5(6))].

given #742 (A,wt=23): 324 (x v y) ^ (z v (y' v u)) != 0 | (x v y)' = z v (y' v u).  [para(112(a,1),35(a,1,2)),rewrite(88(2)),xx(a)].

given #743 (T,wt=14): 2215 x ^ (y ^ (z ^ ((y ^ x)' ^ u))) = 0.  [para(230(a,1),385(a,1,2,2,1,1)),rewrite(5(6))].

given #744 (T,wt=14): 2230 x ^ (y ^ (z ^ (u ^ (y ^ x)'))) = 0.  [para(230(a,1),390(a,1,2,2,2,1)),rewrite(5(6))].

given #745 (T,wt=14): 2237 x v ((y ^ (z ^ (x ^ u)))' v v) = 1.  [para(5(a,1),400(a,1,2,1,1))].

given #746 (T,wt=14): 2244 (x ^ (y ^ z))' v (u v (v v y)) = 1.  [para(400(a,1),95(a,1,1)),rewrite(3(7),67(8),400(11))].

given #747 (A,wt=19): 325 (x v y) ^ (x' v z) != 0 | (x v y)' = x' v z.  [para(112(a,1),35(a,1)),xx(a)].

given #748 (T,wt=14): 2246 1 != x | x ^ y != 0 | x' = y ^ x.  [para(4(a,1),105(b,1))].

given #749 (T,wt=14): 2260 x v (y v (z ^ (u ^ (x ^ v)))') = 1.  [para(5(a,1),460(a,1,2,2,1))].

given #750 (T,wt=14): 2265 x v (y v (z v (u ^ (v ^ x))')) = 1.  [para(159(a,1),460(a,1,2,2,1,2)),rewrite(3(6))].

given #751 (T,wt=14): 2267 x v (y v (z v (u ^ (y v x))')) = 1.  [para(94(a,1),460(a,1,2,2,1,2)),rewrite(3(6))].

given #752 (A,wt=27): 326 x v (y v (z ^ ((x v y)' ^ u))) != 1 | z ^ ((x v y)' ^ u) = (x v y)'.  [para(121(a,1),35(b,1)),flip(c),xx(b)].

given #753 (T,wt=14): 2277 x v (y v (z ^ (u ^ (v ^ x)))') = 1.  [para(159(a,1),467(a,1,2,1,2,2)),rewrite(3(6))].

given #754 (T,wt=14): 2279 x v (y v (z ^ (u ^ (y v x)))') = 1.  [para(94(a,1),467(a,1,2,1,2,2)),rewrite(3(6))].

given #755 (T,wt=14): 2283 x v ((y ^ (z ^ (u ^ x)))' v v) = 1.  [para(5(a,1),473(a,1,2,1,1,2))].

given #756 (T,wt=14): 2299 (x ^ (y ^ z))' v (u v (v v z)) = 1.  [para(473(a,1),95(a,1,1)),rewrite(3(7),67(8),473(11))].

given #757 (A,wt=19): 327 (x v y') ^ (z v y) != 0 | (x v y')' = z v y.  [para(267(a,1),35(a,1,2)),rewrite(88(2)),xx(a)].

given #758 (T,wt=14): 2424 x v (y v ((y v (x ^ z))' v u)) = 1.  [para(543(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #759 (T,wt=14): 2429 x v (y v ((y v (z ^ x))' v u)) = 1.  [para(543(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #760 (T,wt=14): 2446 x v (y v (z v (u v (u v x)'))) = 1.  [para(3(a,1),547(a,1,2))].

given #761 (T,wt=14): 2448 x v (y v (z v (z v (x ^ u))')) = 1.  [para(547(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #762 (A,wt=27): 328 x v (y v ((x v (y v z))' ^ u)) != 1 | (x v (y v z))' ^ u = (x v y)'.  [para(122(a,1),35(b,1)),rewrite(3(2),3(15)),flip(c),xx(b)].

given #763 (T,wt=14): 2453 x v (y v (z v (z v (u ^ x))')) = 1.  [para(547(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #764 (T,wt=14): 2461 x v (y v (y v (z ^ (x ^ u)))') = 1.  [para(17(a,1),549(a,1,2,2,1,2))].

given #765 (T,wt=14): 2469 x v (y v (z v (z v (y v x))')) = 1.  [para(94(a,1),549(a,1,2,2,1,2)),rewrite(3(6))].

given #766 (T,wt=14): 2470 x v ((x v (y ^ z))' v (u v y)) = 1.  [para(549(a,1),95(a,1,1)),rewrite(3(7),67(8),549(11))].

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

given #768 (T,wt=14): 2472 x v (y v ((x v (y ^ z))' v u)) = 1.  [para(549(a,1),99(a,1,1)),rewrite(67(8),718(11))].

given #769 (T,wt=14): 2478 x ^ (y ^ (z ^ ((z ^ x)' ^ u))) = 0.  [para(553(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #770 (T,wt=14): 2480 x ^ (y ^ ((y ^ (x v z))' ^ u)) = 0.  [para(553(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #771 (T,wt=14): 2485 x ^ (y ^ ((y ^ (z v x))' ^ u)) = 0.  [para(553(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #772 (A,wt=19): 333 x ^ (y v (z v x')) != 0 | (y v (z v x'))' = x.  [para(124(a,1),34(a,1)),rewrite(4(7)),xx(a)].

given #773 (T,wt=10): 21636 x v y != 0 | y v x = 0.  [para(94(a,1),333(a,1)),rewrite(217(7),76(5)),flip(b)].

given #774 (T,wt=10): 21639 x ^ y != 0 | y ^ x = 0.  [para(230(a,1),21636(a,1)),rewrite(230(6))].

given #775 (T,wt=14): 2489 (x v y)' ^ (((x ^ z) v y) ^ u) = 0.  [para(169(a,1),553(a,1,2,2,1,1)),rewrite(79(6),67(6))].

given #776 (T,wt=14): 2496 x ^ (y ^ (z ^ (u ^ (u ^ x)'))) = 0.  [para(5(a,1),557(a,1,2))].

given #777 (A,wt=23): 334 (x v y) ^ (z v (u v y')) != 0 | (x v y)' = z v (u v y').  [para(124(a,1),35(a,1,2)),rewrite(88(2)),xx(a)].

given #778 (T,wt=14): 2498 x ^ (y ^ (z ^ (z ^ (x v u))')) = 0.  [para(557(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #779 (T,wt=14): 2503 x ^ (y ^ (z ^ (z ^ (u v x))')) = 0.  [para(557(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #780 (T,wt=14): 2507 x ^ ((y ^ x)' ^ (z ^ (u ^ y))) = 0.  [para(119(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6),5(5))].

given #781 (T,wt=14): 2508 x ^ (y ^ ((z ^ x)' ^ (u ^ z))) = 0.  [para(126(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6),5(5))].

given #782 (A,wt=19): 335 (x v y) ^ (z v x') != 0 | (x v y)' = z v x'.  [para(124(a,1),35(a,1)),xx(a)].

given #783 (T,wt=14): 2509 x ^ (((y ^ x) v z)' ^ (u ^ y)) = 0.  [para(132(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6))].

given #784 (T,wt=14): 2510 x ^ ((y v (z ^ x))' ^ (u ^ z)) = 0.  [para(145(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6))].

given #785 (T,wt=14): 2513 x ^ (((y v z) ^ x)' ^ (u ^ y)) = 0.  [para(237(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6))].

given #786 (T,wt=14): 2514 (x ^ y)' ^ (z ^ (y ^ (u ^ x))) = 0.  [para(278(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6),5(5))].

given #787 (A,wt=19): 338 x v (y ^ (z ^ x')) != 1 | y ^ (z ^ x') = x'.  [para(127(a,1),10(b,1)),flip(c),xx(b)].

given #788 (T,wt=14): 2515 (x v (y v z))' ^ (u ^ (v ^ y)) = 0.  [para(284(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6))].

given #789 (T,wt=14): 2516 (x v (y v z))' ^ (u ^ (v ^ z)) = 0.  [para(372(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6))].

given #790 (T,wt=14): 2523 x ^ (y ^ (y ^ (z v (x v u)))') = 0.  [para(15(a,1),559(a,1,2,2,1,2))].

given #791 (T,wt=14): 2532 x ^ ((x ^ (y v z))' ^ (u ^ y)) = 0.  [para(559(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6))].

given #792 (A,wt=27): 340 x v (y v (z ^ (u ^ (x v y)'))) != 1 | z ^ (u ^ (x v y)') = (x v y)'.  [para(127(a,1),35(b,1)),flip(c),xx(b)].

given #793 (T,wt=14): 2538 (x ^ y)' v (z v (u v (v v x))) = 1.  [para(186(a,1),564(a,1,2,2,2))].

given #794 (T,wt=14): 2540 (x ^ y)' v (z v (u v (v v y))) = 1.  [para(879(a,1),564(a,1,2,2,2))].

given #795 (T,wt=14): 2546 (x v y)' ^ (z ^ (u ^ (v ^ x))) = 0.  [para(159(a,1),594(a,1,2,2,2))].

given #796 (T,wt=14): 2548 (x v y)' ^ (z ^ (u ^ (v ^ y))) = 0.  [para(827(a,1),594(a,1,2,2,2))].

given #797 (A,wt=19): 343 x v (y ^ (x v z)') != 1 | y ^ (x v z)' = x'.  [para(129(a,1),10(b,1)),flip(c),xx(b)].

given #798 (T,wt=14): 2550 (x v y)' ^ (z ^ (u ^ (y v x))) = 0.  [para(94(a,1),594(a,1,2,2,2))].

given #799 (T,wt=14): 2567 (x ^ y)' v (z v (u v (y ^ x))) = 1.  [para(230(a,1),600(a,1,2,2,2))].

given #800 (T,wt=14): 2625 x ^ (y ^ (x ^ ((x ^ y) v z))') = 0.  [para(113(a,1),235(a,1))].

given #801 (T,wt=14): 2658 (x ^ (y ^ z))' v (u v (y v v)) = 1.  [para(607(a,1),3(a,1,1)),rewrite(77(2),3(6)),flip(a)].

given #802 (A,wt=27): 345 x v (y v (z ^ (x v (y v u))')) != 1 | z ^ (x v (y v u))' = (x v y)'.  [para(129(a,1),35(b,1)),rewrite(3(2),3(15)),flip(c),xx(b)].

given #803 (T,wt=14): 2669 (x ^ (y ^ z))' v (u v (z v v)) = 1.  [para(159(a,1),607(a,1,1,1,2))].

given #804 (T,wt=14): 2672 (x ^ y) v (z ^ (y ^ (x ^ u)))' = 1.  [para(230(a,1),607(a,1,2)),rewrite(5(2),2(6))].

given #805 (T,wt=14): 2673 (x ^ (y v z))' v (u v (z v y)) = 1.  [para(94(a,1),607(a,1,1,1,2))].

given #806 (T,wt=14): 2700 (x ^ y) v (z ^ (u ^ (y ^ x)))' = 1.  [para(230(a,1),608(a,1,2)),rewrite(2(6))].

given #807 (A,wt=19): 349 x v (y v (x v z))' != 1 | (y v (x v z))' = x'.  [para(134(a,1),10(b,1)),flip(c),xx(b)].

given #808 (T,wt=14): 2739 (x v (y v z))' ^ (u ^ (y ^ v)) = 0.  [para(622(a,1),5(a,1,1)),rewrite(80(2),5(6)),flip(a)].

given #809 (T,wt=14): 2749 (x v y) ^ (z v (y v (x v u)))' = 0.  [para(185(a,1),622(a,1,2)),rewrite(3(2),4(6))].

given #810 (T,wt=14): 2752 (x v (y v z))' ^ (u ^ (z ^ v)) = 0.  [para(186(a,1),622(a,1,1,1,2))].

given #811 (T,wt=14): 2801 (x v y)' ^ (z ^ (u ^ (y ^ v))) = 0.  [para(73(a,1),623(a,1,1,1,2))].

given #812 (A,wt=27): 350 x v (y v (z v (x v (y v u)))') != 1 | (z v (x v (y v u)))' = (x v y)'.  [para(134(a,1),35(b,1)),rewrite(3(2),3(15)),flip(c),xx(b)].

given #813 (T,wt=14): 2811 (x v y) ^ (z v (u v (y v x)))' = 0.  [para(185(a,1),623(a,1,2)),rewrite(4(6))].

given #814 (T,wt=14): 2817 (x v (y ^ z))' ^ (u ^ (z ^ y)) = 0.  [para(230(a,1),623(a,1,1,1,2))].

given #815 (T,wt=14): 2836 (x v y)' v (z v (y v (x v u))) = 1.  [para(94(a,1),628(a,1,1,1)),rewrite(3(4))].

given #816 (T,wt=14): 2850 (x ^ (y ^ z))' v (u v (y ^ x)) = 1.  [para(230(a,1),629(a,1,2,2)),rewrite(5(2))].

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

given #818 (T,wt=14): 2851 (x v y)' v (z v (u v (y v x))) = 1.  [para(94(a,1),629(a,1,1,1))].

given #819 (T,wt=14): 2907 x ^ ((x v y) ^ (z v (x v u)))' = 0.  [para(116(a,1),237(a,1))].

given #820 (T,wt=14): 2926 x ^ (y ^ ((z v (y v u)) ^ x)') = 0.  [para(116(a,1),557(a,1,2))].

given #821 (T,wt=14): 2928 x ^ ((y v (x v z)) ^ (x v u))' = 0.  [para(116(a,1),559(a,1))].

given #822 (A,wt=20): 352 x v (y v z) != 1 | (x v z) ^ y != 0 | y' = x v z.  [para(15(a,1),36(a,1))].

given #823 (T,wt=14): 2954 (x ^ (y ^ z))' v (u v (z ^ y)) = 1.  [para(230(a,1),682(a,1,2,2))].

given #824 (T,wt=14): 2966 (x v y)' ^ (z ^ (u ^ (x ^ v))) = 0.  [para(5(a,1),692(a,1,2))].

given #825 (T,wt=14): 2974 (x v (y v z))' ^ (u ^ (y v x)) = 0.  [para(94(a,1),692(a,1,2,2)),rewrite(3(2))].

given #826 (T,wt=14): 3011 (x ^ y)' ^ (z ^ (y ^ (x ^ u))) = 0.  [para(230(a,1),700(a,1,1,1)),rewrite(5(4))].

given #827 (A,wt=20): 353 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | (x ^ y)' = z.  [para(17(a,1),36(b,1))].

given #828 (T,wt=14): 3013 (x v (y v z))' ^ (u ^ (z v y)) = 0.  [para(94(a,1),700(a,1,2,2))].

given #829 (T,wt=14): 3039 x ^ (y ^ ((x ^ (y v z))' ^ u)) = 0.  [para(119(a,1),117(a,1,2)),rewrite(91(2)),flip(a)].

given #830 (T,wt=14): 3040 x ^ (y ^ (z ^ (x ^ (y v u))')) = 0.  [para(126(a,1),117(a,1,2)),rewrite(91(2)),flip(a)].

given #831 (T,wt=14): 3044 x ^ (y ^ ((x v z) ^ (y v u))') = 0.  [para(237(a,1),117(a,1,2)),rewrite(91(2)),flip(a)].

given #832 (A,wt=22): 354 x v (y v z) != 1 | x v y != 0 | (x v (y v z))' = x v y.  [para(19(a,1),36(b,1)),rewrite(2(4),15(4),15(3),3(2),153(3),63(3))].

given #833 (T,wt=14): 3055 x ^ (y ^ (((y v z) ^ x)' ^ u)) = 0.  [para(553(a,1),117(a,1,2)),rewrite(91(2)),flip(a)].

given #834 (T,wt=14): 3057 x ^ (y ^ ((y v z) ^ (x v u))') = 0.  [para(559(a,1),117(a,1,2)),rewrite(91(2)),flip(a)].

given #835 (T,wt=14): 3087 (x ^ y)' ^ (z ^ (u ^ (y ^ x))) = 0.  [para(230(a,1),701(a,1,1,1))].

given #836 (T,wt=14): 3112 (x v (y ^ z)) ^ (x v (z v u))' = 0.  [para(159(a,1),715(a,1,1,2))].

given #837 (A,wt=22): 355 x v ((x v y) ^ z) != 1 | x ^ z != 0 | ((x v y) ^ z)' = x.  [para(20(a,1),36(b,1)),rewrite(2(3))].

given #838 (T,wt=14): 3119 (x v y)' ^ ((x v (y ^ z)) ^ u) = 0.  [para(715(a,1),553(a,1,2,2,1,1)),rewrite(79(6),67(6))].

given #839 (T,wt=14): 3123 x v (y v (z v (x v (z ^ u))')) = 1.  [para(718(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #840 (T,wt=14): 3124 x v (y v ((x ^ z) v (y ^ u))') = 1.  [para(718(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #841 (T,wt=14): 3129 x v (y v ((z ^ x) v (y ^ u))') = 1.  [para(718(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #842 (A,wt=15): 356 x v (x' ^ y) != 1 | (x' ^ y)' = x.  [para(81(a,1),36(b,1)),rewrite(2(3)),xx(b)].

given #843 (T,wt=14): 3130 x v (y v (z v (x v (u ^ y))')) = 1.  [para(159(a,1),718(a,1,2,2,1,2)),rewrite(3(5))].

given #844 (T,wt=14): 3132 x v (y v (z v (x v (u ^ z))')) = 1.  [para(827(a,1),718(a,1,2,2,1,2)),rewrite(3(5))].

given #845 (T,wt=14): 3133 x v ((y v (x ^ z))' v (u v y)) = 1.  [para(718(a,1),95(a,1,1)),rewrite(3(7),67(8),718(11))].

Low Water (displace, True_semantics): id=11550, wt=35

given #846 (T,wt=14): 3151 (x ^ (y v z)) v (x ^ (z ^ u))' = 1.  [para(186(a,1),806(a,1,1,2))].

Low Water (displace, True_semantics): id=11681, wt=34

given #847 (A,wt=15): 357 x v (y ^ x') != 1 | (y ^ x')' = x.  [para(92(a,1),36(b,1)),rewrite(2(3)),xx(b)].

given #848 (T,wt=14): 3155 (x ^ y)' v ((x ^ (y v z)) v u) = 1.  [para(806(a,1),94(a,1,1)),rewrite(67(8),3138(11))].

Low Water (displace, True_semantics): id=12086, wt=33

given #849 (T,wt=14): 3230 x ^ (y ^ (z ^ (x ^ (z v u))')) = 0.  [para(808(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #850 (T,wt=14): 3235 x ^ (y ^ ((z v x) ^ (y v u))') = 0.  [para(808(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

Low Water (displace, True_semantics): id=12413, wt=31

given #851 (T,wt=14): 3237 x ^ (y ^ (z ^ (x ^ (u v y))')) = 0.  [para(186(a,1),808(a,1,2,2,1,2)),rewrite(5(5))].

given #852 (A,wt=26): 359 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | (y ^ ((x ^ y) v z))' = x.  [para(21(a,1),36(b,1)),rewrite(2(4))].

given #853 (T,wt=14): 3238 x ^ (y ^ (z ^ (x ^ (u v z))')) = 0.  [para(879(a,1),808(a,1,2,2,1,2)),rewrite(5(5))].

given #854 (T,wt=14): 3241 x ^ ((y ^ (x v z))' ^ (u ^ y)) = 0.  [para(808(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6))].

given #855 (T,wt=14): 3246 ((x v (y v z)) ^ u) v (z ^ u)' = 1.  [para(3(a,1),829(a,1,1,1))].

given #856 (T,wt=14): 3258 ((x v y) ^ (z v (y v u))) v y' = 1.  [para(52(a,1),829(a,1,2,1))].

given #857 (A,wt=18): 361 x v (y v z) != 1 | 0 != y | (x v (y v z))' = y.  [para(52(a,1),36(b,1)),rewrite(2(3),153(3)),flip(b)].

given #858 (T,wt=14): 3261 ((x v y) ^ (z v (u v y))) v y' = 1.  [para(82(a,1),829(a,1,2,1))].

given #859 (T,wt=14): 3275 (x ^ (y ^ z)) v (y ^ (x ^ z))' = 1.  [para(230(a,1),829(a,1,1,1)),rewrite(5(2),5(4))].

given #860 (T,wt=14): 3278 (x ^ y)' v (((z v x) ^ y) v u) = 1.  [para(829(a,1),94(a,1,1)),rewrite(67(8),3245(11))].

Low Water (displace, True_semantics): id=12879, wt=30

given #861 (T,wt=14): 3291 x ^ (y ^ ((z v (u v x)) ^ y)') = 0.  [para(3(a,1),833(a,1,2,2,1,1))].

given #862 (A,wt=18): 362 x v (y v z) != 1 | 0 != z | (x v (y v z))' = z.  [para(82(a,1),36(b,1)),rewrite(2(3),184(3)),flip(b)].

given #863 (T,wt=14): 3314 x ^ (((y v z) ^ x)' ^ (u ^ z)) = 0.  [para(833(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6))].

Low Water (displace, True_semantics): id=13147, wt=29

given #864 (T,wt=14): 3318 x ^ ((y v x) ^ (z v (x v u)))' = 0.  [para(833(a,1),116(a,1)),flip(a)].

given #865 (T,wt=14): 3320 x ^ (y ^ (y ^ (z v (u v x)))') = 0.  [para(3(a,1),840(a,1,2,2,1,2))].

given #866 (T,wt=14): 3336 x ^ (y ^ (z ^ (z ^ (y ^ x))')) = 0.  [para(230(a,1),840(a,1,2,2,1,2)),rewrite(5(6))].

given #867 (A,wt=19): 363 x v (y ^ (x ^ y)') != 1 | (y ^ (x ^ y)')' = x.  [para(32(a,1),36(b,1)),rewrite(2(4)),xx(b)].

given #868 (T,wt=14): 3343 x ^ ((x ^ (y v z))' ^ (u ^ z)) = 0.  [para(840(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6))].

given #869 (T,wt=14): 3347 x ^ ((y v (x v z)) ^ (u v x))' = 0.  [para(840(a,1),116(a,1)),flip(a)].

given #870 (T,wt=14): 3348 x ^ (y ^ ((y v z) ^ (u v x))') = 0.  [para(840(a,1),117(a,1,2)),rewrite(91(2)),flip(a)].

Low Water (displace, True_semantics): id=13458, wt=28

Low Water (displace, True_semantics): id=13778, wt=27

given #871 (T,wt=14): 3375 (x ^ y)' v ((x ^ (z v y)) v u) = 1.  [para(854(a,1),94(a,1,1)),rewrite(67(8),3352(11))].

given #872 (A,wt=19): 364 x v (y ^ (x' ^ z)) != 1 | (y ^ (x' ^ z))' = x.  [para(121(a,1),36(b,1)),rewrite(2(4)),xx(b)].

given #873 (T,wt=14): 3387 x ^ (y ^ ((x ^ (z v y))' ^ u)) = 0.  [para(858(a,1),5(a,1,1)),rewrite(80(2),5(6)),flip(a)].

given #874 (T,wt=14): 3389 x ^ (y ^ ((x v z) ^ (u v y))') = 0.  [para(858(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #875 (T,wt=14): 3397 x ^ (y ^ ((z v x) ^ (u v y))') = 0.  [para(858(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #876 (T,wt=14): 3407 x ^ ((y ^ (z v x))' ^ (u ^ y)) = 0.  [para(858(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6),5(6))].

given #877 (A,wt=15): 366 (x ^ y) v y' != 1 | (x ^ y)' = y'.  [para(268(a,1),36(b,1)),xx(b)].

given #878 (T,wt=14): 3414 ((x ^ (y ^ z)) v u) ^ (z v u)' = 0.  [para(5(a,1),878(a,1,1,1))].

given #879 (T,wt=14): 3425 ((x ^ y) v (z ^ (y ^ u))) ^ y' = 0.  [para(73(a,1),878(a,1,2,1))].

given #880 (T,wt=14): 3426 ((x ^ y) v (z ^ (u ^ y))) ^ y' = 0.  [para(104(a,1),878(a,1,2,1))].

given #881 (T,wt=14): 3444 ((x ^ y) v z) ^ (y v (z v u))' = 0.  [para(878(a,1),97(a,1,2)),rewrite(4(4),80(4)),flip(a)].

given #882 (A,wt=19): 367 x v ((x v y)' ^ z) != 1 | ((x v y)' ^ z)' = x.  [para(122(a,1),36(b,1)),rewrite(2(4)),xx(b)].

given #883 (T,wt=14): 3450 (x v y)' ^ (((z ^ x) v y) ^ u) = 0.  [para(878(a,1),553(a,1,2,2,1,1)),rewrite(79(6),67(6))].

given #884 (T,wt=14): 3458 x v (y v ((z ^ (u ^ x)) v y)') = 1.  [para(5(a,1),883(a,1,2,2,1,1))].

given #885 (T,wt=14): 3478 x v (((y ^ z) v x)' v (u v z)) = 1.  [para(883(a,1),95(a,1,1)),rewrite(3(7),67(8),883(11))].

Low Water (displace, True_semantics): id=14941, wt=26

given #886 (T,wt=14): 3482 x v (y v (((z ^ y) v x)' v u)) = 1.  [para(883(a,1),99(a,1,1)),rewrite(67(8),2431(11))].

given #887 (A,wt=19): 368 x v (y ^ (z ^ x')) != 1 | (y ^ (z ^ x'))' = x.  [para(127(a,1),36(b,1)),rewrite(2(4)),xx(b)].

given #888 (T,wt=10): 23180 x ^ y != 1 | y ^ x = 1.  [para(223(a,1),368(a,1)),rewrite(232(7),79(5)),flip(b)].

given #889 (T,wt=10): 23183 x v y != 1 | y v x = 1.  [para(185(a,1),23180(a,1)),rewrite(185(6))].

given #890 (T,wt=14): 3492 x v (y v (y v (z ^ (u ^ x)))') = 1.  [para(5(a,1),890(a,1,2,2,1,2))].

given #891 (T,wt=14): 3509 x v ((x v (y ^ z))' v (u v z)) = 1.  [para(890(a,1),95(a,1,1)),rewrite(3(7),67(8),890(11))].

given #892 (A,wt=19): 369 x v (y ^ (x v z)') != 1 | (y ^ (x v z)')' = x.  [para(129(a,1),36(b,1)),rewrite(2(4)),xx(b)].

given #893 (T,wt=14): 3514 x v (y v ((x v (z ^ y))' v u)) = 1.  [para(890(a,1),99(a,1,1)),rewrite(67(8),986(11))].

given #894 (T,wt=14): 3550 (x v y)' ^ ((x v (z ^ y)) ^ u) = 0.  [para(983(a,1),553(a,1,2,2,1,1)),rewrite(79(6),67(6))].

given #895 (T,wt=14): 3559 x v (y v ((x ^ z) v (u ^ y))') = 1.  [para(986(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

Low Water (keep, True_semantics): wt=19

given #896 (T,wt=14): 3567 x v (y v ((z ^ x) v (u ^ y))') = 1.  [para(986(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #897 (A,wt=17): 370 x v (y v (x v z))' != 1 | y v (x v z) = x.  [para(134(a,1),36(b,1)),rewrite(2(4),250(13)),xx(b)].

given #898 (T,wt=14): 3573 x v ((y v (z ^ x))' v (u v y)) = 1.  [para(986(a,1),95(a,1,1)),rewrite(3(7),67(8),986(11))].

given #899 (T,wt=14): 3587 x v (y v (z ^ (y v (x ^ u)))') = 1.  [para(1039(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #900 (T,wt=14): 3592 x v (y v (z ^ (y v (u ^ x)))') = 1.  [para(1039(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #901 (T,wt=14): 3600 x v (y v (z v (y v (x ^ u))')) = 1.  [para(1040(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #902 (A,wt=19): 374 x v (y v (z v x))' != 1 | (y v (z v x))' = x'.  [para(143(a,1),10(b,1)),flip(c),xx(b)].

given #903 (T,wt=14): 3605 x v (y v (z v (y v (u ^ x))')) = 1.  [para(1040(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

Low Water (displace, True_semantics): id=15573, wt=25

given #904 (T,wt=14): 3610 (x v y)' ^ (z ^ ((y v x) ^ u)) = 0.  [para(1041(a,1),5(a,1,1)),rewrite(80(2),5(6)),flip(a)].

given #905 (T,wt=14): 3634 (x v y) ^ ((y v (x v z))' ^ u) = 0.  [para(1043(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #906 (T,wt=14): 3637 (x v y) ^ (z ^ (y v (x v u))') = 0.  [para(1043(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #907 (A,wt=16): 378 (x v ((y v x) ^ z)) ^ (u v (y v x))' = 0.  [para(23(a,1),143(a,1,2,1,2))].

given #908 (T,wt=14): 3641 ((x ^ y) v z) ^ (z v (u v x))' = 0.  [para(186(a,1),1043(a,1,2,1,2))].

given #909 (T,wt=14): 3642 ((x ^ y) v z) ^ (z v (u v y))' = 0.  [para(879(a,1),1043(a,1,2,1,2))].

given #910 (T,wt=14): 3651 (x v y) ^ ((z v (y v x))' ^ u) = 0.  [para(1044(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #911 (T,wt=14): 3654 (x v y) ^ (z ^ (u v (y v x))') = 0.  [para(1044(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #912 (A,wt=27): 380 x v (y v (z v (u v (x v y)))') != 1 | (z v (u v (x v y)))' = (x v y)'.  [para(143(a,1),35(b,1)),flip(c),xx(b)].

given #913 (T,wt=14): 3664 (x v y) ^ (z ^ ((y v x)' ^ u)) = 0.  [para(1100(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #914 (T,wt=14): 3669 (x v y) ^ ((y v (z v x))' ^ u) = 0.  [para(1100(a,1),97(a,1,2)),rewrite(4(3),80(3),3(4)),flip(a)].

given #915 (T,wt=14): 3673 (x v y) ^ (z ^ (u ^ (y v x)')) = 0.  [para(5(a,1),1102(a,1,2))].

given #916 (T,wt=14): 3680 (x v y) ^ (z ^ (y v (u v x))') = 0.  [para(1102(a,1),97(a,1,2)),rewrite(4(3),80(3),3(4)),flip(a)].

given #917 (A,wt=17): 381 x v (y v (z v x))' != 1 | y v (z v x) = x.  [para(143(a,1),36(b,1)),rewrite(2(4),250(13)),xx(b)].

given #918 (T,wt=14): 3686 x ^ (y ^ (z ^ (u v (z ^ x))')) = 0.  [para(1228(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #919 (T,wt=14): 3688 x ^ (y ^ (z v (y ^ (x v u)))') = 0.  [para(1228(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #920 (T,wt=14): 3693 x ^ (y ^ (z v (y ^ (u v x)))') = 0.  [para(1228(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #921 (T,wt=14): 3700 x ^ (y ^ (z v ((y v u) ^ x))') = 0.  [para(1228(a,1),117(a,1,2)),rewrite(91(2)),flip(a)].

given #922 (A,wt=19): 383 x v ((y v x)' ^ z) != 1 | (y v x)' ^ z = x'.  [para(144(a,1),10(b,1)),flip(c),xx(b)].

given #923 (T,wt=14): 3709 (x ^ ((x ^ y) v z)) v (y ^ x)' = 1.  [para(135(a,1),171(a,1,2,1))].

given #924 (T,wt=14): 3711 x ^ (y ^ (y ^ ((y ^ x) v z))') = 0.  [para(135(a,1),268(a,1,2)),rewrite(4(6),5(6))].

given #925 (T,wt=14): 3735 (x ^ ((y ^ x) v z)) v (x ^ y)' = 1.  [para(135(a,1),180(a,1,2,1))].

given #926 (T,wt=14): 3745 (x ^ y) v (z v (u ^ (y ^ x))') = 1.  [para(135(a,1),483(a,1,2,1,2)),rewrite(3(6))].

given #927 (A,wt=16): 387 (x v ((y v x) ^ z)) ^ ((y v x)' ^ u) = 0.  [para(23(a,1),144(a,1,2,1,1))].

Low Water (displace, True_semantics): id=16527, wt=24

given #928 (T,wt=14): 3747 (x ^ y) v (z v (u v (y ^ x)')) = 1.  [para(135(a,1),485(a,1,2,2,1)),rewrite(3(6))].

given #929 (T,wt=14): 3751 (x ^ y)' v (z v ((y ^ x) v u)) = 1.  [para(135(a,1),608(a,1,1,1))].

given #930 (T,wt=14): 3753 ((x ^ y) v z)' ^ (u ^ (y ^ x)) = 0.  [para(135(a,1),614(a,1,2,2))].

given #931 (T,wt=14): 3763 x ^ (y ^ (z v ((y ^ x) v u))') = 0.  [para(135(a,1),701(a,1,2)),rewrite(4(6),5(6))].

given #932 (A,wt=27): 388 x v (y v ((z v (x v y))' ^ u)) != 1 | (z v (x v y))' ^ u = (x v y)'.  [para(144(a,1),35(b,1)),flip(c),xx(b)].

given #933 (T,wt=14): 3778 x ^ (y ^ (z ^ (u ^ (z ^ x)'))) = 0.  [para(1229(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #934 (T,wt=14): 3780 x ^ (y ^ (z ^ (y ^ (x v u))')) = 0.  [para(1229(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #935 (T,wt=14): 3785 x ^ (y ^ (z ^ (y ^ (u v x))')) = 0.  [para(1229(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #936 (T,wt=14): 3792 x ^ (y ^ (z ^ ((y v u) ^ x)')) = 0.  [para(1229(a,1),117(a,1,2)),rewrite(91(2)),flip(a)].

given #937 (A,wt=19): 389 x v ((y v x)' ^ z) != 1 | ((y v x)' ^ z)' = x.  [para(144(a,1),36(b,1)),rewrite(2(4)),xx(b)].

given #938 (T,wt=14): 3804 (x ^ y) v ((y ^ (x ^ z))' v u) = 1.  [para(1231(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #939 (T,wt=14): 3808 (x ^ y) v (z v (y ^ (x ^ u))') = 1.  [para(1231(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #940 (T,wt=14): 3810 (x ^ y) v (y ^ (z ^ (x ^ u)))' = 1.  [para(17(a,1),1231(a,1,2,1,2))].

given #941 (T,wt=14): 3813 ((x v y) ^ z) v (z ^ (u ^ x))' = 1.  [para(159(a,1),1231(a,1,2,1,2))].

given #942 (A,wt=19): 391 x v (y ^ (z v x)') != 1 | y ^ (z v x)' = x'.  [para(148(a,1),10(b,1)),flip(c),xx(b)].

given #943 (T,wt=14): 3815 ((x v y) ^ z) v (z ^ (u ^ y))' = 1.  [para(827(a,1),1231(a,1,2,1,2))].

given #944 (T,wt=14): 3817 ((x v y) ^ z) v (z ^ (y v x))' = 1.  [para(94(a,1),1231(a,1,2,1,2))].

given #945 (T,wt=14): 3822 (x ^ y) v ((z ^ (y ^ x))' v u) = 1.  [para(1232(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #946 (T,wt=14): 3833 (x ^ (y v (z v u))) v (z ^ x)' = 1.  [para(116(a,1),1232(a,1,2,1))].

given #947 (A,wt=16): 394 (x v ((y v x) ^ z)) ^ (u ^ (y v x)') = 0.  [para(23(a,1),148(a,1,2,2,1))].

given #948 (T,wt=14): 3942 (x v y) ^ (y v (z v (u v x)))' = 0.  [para(3(a,1),1473(a,1,2,1,2))].

Low Water (displace, True_semantics): id=16154, wt=23

given #949 (T,wt=14): 3947 ((x ^ (y ^ z)) v u) ^ (u v y)' = 0.  [para(73(a,1),1473(a,1,2,1,2))].

Low Water (keep, True_semantics): wt=18

given #950 (T,wt=14): 3948 ((x ^ (y ^ z)) v u) ^ (u v z)' = 0.  [para(104(a,1),1473(a,1,2,1,2))].

given #951 (T,wt=14): 3958 ((x ^ y) v z) ^ (z v (y ^ x))' = 0.  [para(230(a,1),1473(a,1,2,1,2))].

given #952 (A,wt=27): 395 x v (y v (z ^ (u v (x v y))')) != 1 | z ^ (u v (x v y))' = (x v y)'.  [para(148(a,1),35(b,1)),flip(c),xx(b)].

given #953 (T,wt=14): 4024 ((x ^ y) v z) ^ ((z v x)' ^ u) = 0.  [para(1480(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #954 (T,wt=14): 4028 ((x ^ y) v z) ^ (u ^ (z v x)') = 0.  [para(1480(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #955 (T,wt=14): 4032 ((x ^ y) v z) ^ (z v (y v u))' = 0.  [para(159(a,1),1480(a,1,1,1))].

given #956 (T,wt=14): 4037 (x v (y v z)) ^ (z v (y v x))' = 0.  [para(94(a,1),1480(a,1,1,1)),rewrite(3(2))].

given #957 (A,wt=19): 396 x v (y ^ (z v x)') != 1 | (y ^ (z v x)')' = x.  [para(148(a,1),36(b,1)),rewrite(2(4)),xx(b)].

given #958 (T,wt=14): 4040 (x v y)' ^ (((y ^ z) v x) ^ u) = 0.  [para(1480(a,1),553(a,1,2,2,1,1)),rewrite(79(6),67(6))].

given #959 (T,wt=14): 4041 (x v y)' ^ (z ^ ((y ^ u) v x)) = 0.  [para(1480(a,1),557(a,1,2,2,2,1)),rewrite(79(6),4(6),67(6))].

given #960 (T,wt=14): 4050 ((x ^ y) v z) ^ ((z v y)' ^ u) = 0.  [para(1482(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #961 (T,wt=14): 4054 ((x ^ y) v z) ^ (u ^ (z v y)') = 0.  [para(1482(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #962 (A,wt=19): 399 x ^ ((x ^ y)' v z) != 0 | (x ^ y)' v z = x'.  [para(167(a,1),10(a,1)),flip(c),xx(a)].

given #963 (T,wt=14): 4075 (x v y)' ^ (((z ^ y) v x) ^ u) = 0.  [para(1482(a,1),553(a,1,2,2,1,1)),rewrite(79(6),67(6))].

given #964 (T,wt=14): 4076 (x v y)' ^ (z ^ ((u ^ y) v x)) = 0.  [para(1482(a,1),557(a,1,2,2,2,1)),rewrite(79(6),4(6),67(6))].

given #965 (T,wt=14): 4087 x ^ (y ^ (((y ^ x) v z)' ^ u)) = 0.  [para(1497(a,1),5(a,1,1)),rewrite(80(2),5(6)),flip(a)].

given #966 (T,wt=14): 4090 x ^ (y ^ (z ^ ((z ^ x) v u)')) = 0.  [para(1497(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #967 (A,wt=19): 401 x ^ ((x ^ y)' v z) != 0 | ((x ^ y)' v z)' = x.  [para(167(a,1),34(a,1)),rewrite(4(7)),xx(a)].

given #968 (T,wt=14): 4092 x ^ (y ^ ((y ^ (x v z)) v u)') = 0.  [para(1497(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #969 (T,wt=14): 4097 x ^ (y ^ ((y ^ (z v x)) v u)') = 0.  [para(1497(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #970 (T,wt=14): 4103 x ^ (y ^ (((y v z) ^ x) v u)') = 0.  [para(1497(a,1),117(a,1,2)),rewrite(91(2)),flip(a)].

given #971 (T,wt=14): 4113 (x v (y ^ z)) ^ ((y v x)' ^ u) = 0.  [para(1539(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #972 (A,wt=23): 402 (x v y) ^ ((y ^ z)' v u) != 0 | (x v y)' = (y ^ z)' v u.  [para(167(a,1),35(a,1,2)),rewrite(88(2)),xx(a)].

given #973 (T,wt=14): 4117 (x v (y ^ z)) ^ (u ^ (y v x)') = 0.  [para(1539(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #974 (T,wt=14): 4118 (x v (y ^ (z ^ u))) ^ (z v x)' = 0.  [para(17(a,1),1539(a,1,1,2))].

given #975 (T,wt=14): 4121 ((x ^ (y ^ z)) v (y ^ u)) ^ y' = 0.  [para(73(a,1),1539(a,1,2,1))].

given #976 (T,wt=14): 4122 ((x ^ (y ^ z)) v (z ^ u)) ^ z' = 0.  [para(104(a,1),1539(a,1,2,1))].

given #977 (A,wt=20): 403 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (y ^ x)' = z.  [para(4(a,1),37(a,1,1))].

given #978 (T,wt=14): 4129 (x v (y ^ z)) ^ (z v (u v x))' = 0.  [para(159(a,1),1539(a,1,1,2)),rewrite(3(4))].

given #979 (T,wt=14): 4133 (x v (y ^ z)) ^ (u v (z v x))' = 0.  [para(827(a,1),1539(a,1,1,2)),rewrite(3(4))].

given #980 (T,wt=14): 4140 (x v y)' ^ ((y v (x ^ z)) ^ u) = 0.  [para(1539(a,1),553(a,1,2,2,1,1)),rewrite(79(6),67(6))].

given #981 (T,wt=14): 4141 (x v y)' ^ (z ^ (y v (x ^ u))) = 0.  [para(1539(a,1),557(a,1,2,2,2,1)),rewrite(79(6),4(6),67(6))].

given #982 (A,wt=20): 404 (x ^ y) v z != 1 | y ^ (z ^ x) != 0 | (x ^ y)' = z.  [para(4(a,1),37(b,1)),rewrite(5(6))].

given #983 (T,wt=14): 4214 (x v y)' ^ ((z ^ (x ^ u)) v y) = 0.  [para(17(a,1),1541(a,1,2,1))].

given #984 (T,wt=14): 4218 x' ^ ((x ^ y) v (z ^ (x ^ u))) = 0.  [para(73(a,1),1541(a,1,1,1))].

given #985 (T,wt=14): 4219 x' ^ ((x ^ y) v (z ^ (u ^ x))) = 0.  [para(104(a,1),1541(a,1,1,1))].

given #986 (T,wt=14): 4226 (x v (y v z))' ^ ((u ^ x) v z) = 0.  [para(159(a,1),1541(a,1,2,1)),rewrite(3(2))].

given #987 (A,wt=26): 405 (x ^ (y ^ z)) v u != 1 | x ^ (y ^ (z ^ u)) != 0 | (x ^ (y ^ z))' = u.  [para(5(a,1),37(a,1,1)),rewrite(5(8),5(12))].

given #988 (T,wt=14): 4230 (x v (y v z))' ^ ((u ^ y) v z) = 0.  [para(827(a,1),1541(a,1,2,1)),rewrite(3(2))].

given #989 (T,wt=14): 4232 (x v (y v z))' ^ ((x ^ u) v y) = 0.  [para(1541(a,1),101(a,1,2)),rewrite(4(4),80(4)),flip(a)].

given #990 (T,wt=14): 4240 ((x ^ y) v (x ^ z)) ^ (x' ^ u) = 0.  [para(1543(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #991 (T,wt=14): 4242 ((x ^ y) v (x ^ z)) ^ (u ^ x') = 0.  [para(1543(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #992 (A,wt=18): 406 x v y != 1 | z ^ x != 0 | (z ^ x)' = x v y.  [para(6(a,1),37(b,1,2)),rewrite(15(3),102(3))].

given #993 (T,wt=14): 4251 x' ^ (((x ^ y) v (x ^ z)) ^ u) = 0.  [para(1543(a,1),553(a,1,2,2,1,1)),rewrite(79(6),67(6))].

given #994 (T,wt=14): 4252 x' ^ (y ^ ((x ^ z) v (x ^ u))) = 0.  [para(1543(a,1),557(a,1,2,2,2,1)),rewrite(79(6),4(6),67(6))].

given #995 (T,wt=14): 4257 ((x ^ y) v (z ^ x)) ^ (x' ^ u) = 0.  [para(1548(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #996 (T,wt=14): 4260 ((x ^ y) v (z ^ x)) ^ (u ^ x') = 0.  [para(1548(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #997 (A,wt=26): 407 x v ((y ^ z) v u) != 1 | y ^ (z ^ (x v u)) != 0 | (y ^ z)' = x v u.  [para(15(a,1),37(a,1))].

given #998 (T,wt=14): 4261 ((x ^ (y ^ z)) v (u ^ y)) ^ y' = 0.  [para(17(a,1),1548(a,1,1,1))].

given #999 (T,wt=14): 4288 x' ^ (((x ^ y) v (z ^ x)) ^ u) = 0.  [para(1548(a,1),553(a,1,2,2,1,1)),rewrite(79(6),67(6))].

given #1000 (T,wt=14): 4289 x' ^ (y ^ ((x ^ z) v (u ^ x))) = 0.  [para(1548(a,1),557(a,1,2,2,2,1)),rewrite(79(6),4(6),67(6))].

given #1001 (T,wt=14): 4299 x v ((y v x)' v (z v (y v u))) = 1.  [para(1580(a,1),3(a,1,1)),rewrite(77(2),3(6),3(5)),flip(a)].

given #1002 (A,wt=18): 408 x ^ y != 1 | x ^ y != 0 | (x ^ y)' = x ^ y.  [para(27(a,1),37(a,1)),rewrite(59(5),57(5))].

given #1003 (T,wt=14): 4307 x v (y v ((z ^ (y ^ u)) v x)') = 1.  [para(73(a,1),1580(a,1,2,2)),rewrite(2(5))].

given #1004 (T,wt=14): 4308 x v (y v ((z ^ (u ^ y)) v x)') = 1.  [para(104(a,1),1580(a,1,2,2)),rewrite(2(5))].

given #1005 (T,wt=14): 4321 x v ((y ^ z) v ((z ^ y) v x)') = 1.  [para(230(a,1),1580(a,1,2,2)),rewrite(2(5))].

given #1006 (T,wt=14): 4441 x v (y v (z v ((z v x) ^ u)')) = 1.  [para(1605(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1007 (A,wt=26): 411 (x ^ (y ^ z)) v u != 1 | y ^ (x ^ (z ^ u)) != 0 | (y ^ (x ^ z))' = u.  [para(17(a,1),37(a,1,1)),rewrite(5(7))].

given #1008 (T,wt=14): 4443 x v (y v (z ^ ((y v x) ^ u))') = 1.  [para(17(a,1),1605(a,1,2,2,1))].

given #1009 (T,wt=14): 4444 x v (y v ((y v (x ^ z)) ^ u)') = 1.  [para(1605(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #1010 (T,wt=14): 4449 x v (y v ((y v (z ^ x)) ^ u)') = 1.  [para(1605(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #1011 (T,wt=14): 4455 (x ^ y) v ((y ^ (z ^ x))' v u) = 1.  [para(1616(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #1012 (A,wt=26): 412 (x ^ y) v (z ^ u) != 1 | x ^ (z ^ (y ^ u)) != 0 | (x ^ y)' = z ^ u.  [para(17(a,1),37(b,1,2))].

given #1013 (T,wt=14): 4457 (x ^ y) v (y ^ (z ^ (u ^ x)))' = 1.  [para(5(a,1),1616(a,1,2,1,2))].

given #1014 (T,wt=14): 4460 (x ^ y) v (z v (y ^ (u ^ x))') = 1.  [para(1616(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1015 (T,wt=14): 4463 ((x v (y v z)) ^ u) v (u ^ y)' = 1.  [para(52(a,1),1616(a,1,2,1,2))].

given #1016 (T,wt=14): 4464 ((x v (y v z)) ^ u) v (u ^ z)' = 1.  [para(82(a,1),1616(a,1,2,1,2))].

given #1017 (A,wt=20): 413 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (x ^ y)' = z.  [para(17(a,1),37(b,1))].

given #1018 (T,wt=14): 4477 (x ^ (y ^ z))' v (u v (z ^ x)) = 1.  [para(1616(a,1),95(a,1,1)),rewrite(67(8),1616(11))].

given #1019 (T,wt=14): 4503 ((x v y) ^ z) v ((z ^ x)' v u) = 1.  [para(1623(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #1020 (T,wt=14): 4506 ((x v y) ^ z) v (u v (z ^ x)') = 1.  [para(1623(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1021 (T,wt=14): 4513 ((x v y) ^ z) v (z ^ (y ^ u))' = 1.  [para(186(a,1),1623(a,1,1,1))].

given #1022 (A,wt=22): 416 x ^ y != 1 | z ^ (x ^ y) != 0 | (x ^ y)' = z ^ (x ^ y).  [para(24(a,1),37(a,1)),rewrite(158(6),156(6))].

given #1023 (T,wt=14): 4516 (x ^ y)' v (((y v z) ^ x) v u) = 1.  [para(1623(a,1),94(a,1,1)),rewrite(67(8),4502(11))].

given #1024 (T,wt=14): 4517 (x ^ y)' v (z v ((y v u) ^ x)) = 1.  [para(1623(a,1),95(a,1,1)),rewrite(67(8),1623(11))].

given #1025 (T,wt=14): 4526 ((x v y) ^ z) v ((z ^ y)' v u) = 1.  [para(1625(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #1026 (T,wt=14): 4529 ((x v y) ^ z) v (u v (z ^ y)') = 1.  [para(1625(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1027 (A,wt=23): 417 x ^ (y ^ ((x ^ y)' v z)) != 0 | (x ^ y)' v z = (x ^ y)'.  [para(78(a,1),37(a,1)),flip(c),xx(a)].

given #1028 (T,wt=14): 4544 (x ^ (y ^ z)) v (z ^ (y ^ x))' = 1.  [para(230(a,1),1625(a,1,1,1)),rewrite(5(2))].

given #1029 (T,wt=14): 4546 (x ^ y)' v (((z v y) ^ x) v u) = 1.  [para(1625(a,1),94(a,1,1)),rewrite(67(8),4525(11))].

given #1030 (T,wt=14): 4547 (x ^ y)' v (z v ((u v y) ^ x)) = 1.  [para(1625(a,1),95(a,1,1)),rewrite(67(8),1625(11))].

given #1031 (T,wt=14): 4640 x ^ (y ^ (((z v y) ^ x)' ^ u)) = 0.  [para(833(a,1),140(a,1,2,2,2,1)),rewrite(69(5),2487(11))].

given #1032 (A,wt=28): 418 (x ^ y) v ((y v z) ^ u) != 1 | x ^ (y ^ u) != 0 | (x ^ y)' = (y v z) ^ u.  [para(20(a,1),37(b,1,2))].

given #1033 (T,wt=14): 4663 (x ^ y)' v ((z v (x v u)) ^ y) = 1.  [para(15(a,1),1686(a,1,2,1))].

given #1034 (T,wt=14): 4670 x' v ((x v y) ^ (z v (x v u))) = 1.  [para(52(a,1),1686(a,1,1,1))].

given #1035 (T,wt=14): 4671 x' v ((x v y) ^ (z v (u v x))) = 1.  [para(82(a,1),1686(a,1,1,1))].

given #1036 (T,wt=14): 4679 (x ^ (y ^ z))' v ((u v x) ^ z) = 1.  [para(186(a,1),1686(a,1,2,1)),rewrite(5(2))].

given #1037 (A,wt=19): 419 (x ^ y) v (y' ^ z) != 1 | (x ^ y)' = y' ^ z.  [para(81(a,1),37(b,1,2)),rewrite(91(8)),xx(b)].

given #1038 (T,wt=14): 4682 (x ^ (y ^ z))' v ((u v y) ^ z) = 1.  [para(879(a,1),1686(a,1,2,1)),rewrite(5(2))].

given #1039 (T,wt=14): 4705 (x ^ (y v z)) v ((y ^ x)' v u) = 1.  [para(1688(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #1040 (T,wt=14): 4709 (x ^ (y v z)) v (u v (y ^ x)') = 1.  [para(1688(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1041 (T,wt=14): 4713 ((x v (y v z)) ^ (y v u)) v y' = 1.  [para(52(a,1),1688(a,1,2,1))].

given #1042 (A,wt=23): 420 x ^ (y ^ (z v (x ^ y)')) != 0 | z v (x ^ y)' = (x ^ y)'.  [para(90(a,1),37(a,1)),flip(c),xx(a)].

given #1043 (T,wt=14): 4714 ((x v (y v z)) ^ (z v u)) v z' = 1.  [para(82(a,1),1688(a,1,2,1))].

given #1044 (T,wt=14): 4723 (x ^ (y v z)) v (z ^ (u ^ x))' = 1.  [para(186(a,1),1688(a,1,1,2)),rewrite(5(4))].

given #1045 (T,wt=14): 4726 (x ^ (y v z)) v (u ^ (z ^ x))' = 1.  [para(879(a,1),1688(a,1,1,2)),rewrite(5(4))].

given #1046 (T,wt=14): 4729 (x ^ y)' v ((y ^ (x v z)) v u) = 1.  [para(1688(a,1),94(a,1,1)),rewrite(67(8),4660(11))].

given #1047 (A,wt=19): 421 (x ^ y) v (z ^ y') != 1 | (x ^ y)' = z ^ y'.  [para(92(a,1),37(b,1,2)),rewrite(91(8)),xx(b)].

given #1048 (T,wt=14): 4731 (x ^ y)' v (z v (y ^ (x v u))) = 1.  [para(1688(a,1),95(a,1,1)),rewrite(67(8),1688(11))].

given #1049 (T,wt=14): 4751 ((x v y) ^ (x v z)) v (x' v u) = 1.  [para(1690(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #1050 (T,wt=14): 4753 ((x v y) ^ (x v z)) v (u v x') = 1.  [para(1690(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1051 (T,wt=14): 4761 x' v (((x v y) ^ (x v z)) v u) = 1.  [para(1690(a,1),94(a,1,1)),rewrite(67(8),4662(11))].

given #1052 (A,wt=15): 422 (x ^ y) v x' != 1 | (x ^ y)' = x'.  [para(92(a,1),37(b,1)),xx(b)].

given #1053 (T,wt=14): 4762 x' v (y v ((x v z) ^ (x v u))) = 1.  [para(1690(a,1),95(a,1,1)),rewrite(67(8),1690(11))].

given #1054 (T,wt=14): 4770 ((x v y) ^ (z v x)) v (x' v u) = 1.  [para(1695(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #1055 (T,wt=14): 4773 ((x v y) ^ (z v x)) v (u v x') = 1.  [para(1695(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1056 (T,wt=14): 4774 ((x v (y v z)) ^ (u v y)) v y' = 1.  [para(15(a,1),1695(a,1,1,1))].

given #1057 (A,wt=19): 423 (x ^ y) v (y v z)' != 1 | (y v z)' = (x ^ y)'.  [para(114(a,1),37(b,1,2)),rewrite(91(8)),flip(c),xx(b)].

given #1058 (T,wt=14): 4790 x' v (((x v y) ^ (z v x)) v u) = 1.  [para(1695(a,1),94(a,1,1)),rewrite(67(8),4666(11))].

given #1059 (T,wt=14): 4791 x' v (y v ((x v z) ^ (u v x))) = 1.  [para(1695(a,1),95(a,1,1)),rewrite(67(8),1695(11))].

given #1060 (T,wt=14): 4841 x ^ (y ^ (x ^ ((y ^ x) v z))') = 0.  [para(141(a,1),1497(a,1,2,2,1))].

given #1061 (T,wt=14): 4863 x v (y v (z v ((z ^ u) v x)')) = 1.  [para(1736(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1062 (A,wt=32): 424 (x ^ y) v (z ^ ((y ^ z) v u)) != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z ^ ((y ^ z) v u).  [para(21(a,1),37(b,1,2))].

given #1063 (T,wt=14): 4865 x v (y v ((y ^ z) v (x ^ u))') = 1.  [para(1736(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #1064 (T,wt=14): 4870 x v (y v ((y ^ z) v (u ^ x))') = 1.  [para(1736(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #1065 (T,wt=14): 4871 x v (y v (z v ((u ^ y) v x)')) = 1.  [para(159(a,1),1736(a,1,2,2,1,1)),rewrite(3(5))].

given #1066 (T,wt=14): 4873 x v (y v (z v ((u ^ z) v x)')) = 1.  [para(827(a,1),1736(a,1,2,2,1,1)),rewrite(3(5))].

given #1067 (A,wt=22): 425 (x ^ y) v z != 1 | x ^ y != 0 | (x ^ y)' = (x ^ y) v z.  [para(21(a,1),37(b,1)),rewrite(63(4))].

given #1068 (T,wt=14): 4882 x v (((x ^ y) v (x ^ z))' v u) = 1.  [para(1739(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #1069 (T,wt=14): 4886 x v (y v ((x ^ z) v (x ^ u))') = 1.  [para(1739(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1070 (T,wt=14): 4887 x v ((y ^ (x ^ z)) v (x ^ u))' = 1.  [para(17(a,1),1739(a,1,2,1,1))].

given #1071 (T,wt=14): 4888 x v ((x ^ y) v (z ^ (x ^ u)))' = 1.  [para(17(a,1),1739(a,1,2,1,2))].

given #1072 (A,wt=19): 426 (x ^ y) v (z v y)' != 1 | (z v y)' = (x ^ y)'.  [para(130(a,1),37(b,1,2)),rewrite(91(8)),flip(c),xx(b)].

given #1073 (T,wt=14): 4898 ((x ^ y) v (x ^ z))' v (u v x) = 1.  [para(1739(a,1),95(a,1,1)),rewrite(67(8),1739(11))].

given #1074 (T,wt=14): 4904 x v (((x ^ y) v (z ^ x))' v u) = 1.  [para(1744(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #1075 (T,wt=14): 4907 x v ((x ^ y) v (z ^ (u ^ x)))' = 1.  [para(5(a,1),1744(a,1,2,1,2))].

given #1076 (T,wt=14): 4908 x v (y v (x v ((x v y) ^ z))') = 1.  [para(6(a,1),1744(a,1,2,1,2)),rewrite(2(4),3(6))].

given #1077 (A,wt=24): 428 (x ^ y) v (y ^ z) != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = y ^ z.  [para(57(a,1),37(b,1,2))].

given #1078 (T,wt=14): 4910 x v (y v ((x ^ z) v (u ^ x))') = 1.  [para(1744(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1079 (T,wt=14): 4911 x v ((y ^ (x ^ z)) v (u ^ x))' = 1.  [para(17(a,1),1744(a,1,2,1,1))].

given #1080 (T,wt=14): 4933 ((x ^ y) v (z ^ x))' v (u v x) = 1.  [para(1744(a,1),95(a,1,1)),rewrite(67(8),1744(11))].

given #1081 (T,wt=14): 4954 x ^ (y ^ (z ^ ((z v u) ^ x)')) = 0.  [para(1818(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #1082 (A,wt=24): 429 (x ^ y) v (z ^ y) != 1 | x ^ (z ^ y) != 0 | (x ^ y)' = z ^ y.  [para(59(a,1),37(b,1,2))].

given #1083 (T,wt=14): 4961 x ^ (y ^ (z ^ ((u v y) ^ x)')) = 0.  [para(186(a,1),1818(a,1,2,2,1,1)),rewrite(5(5))].

given #1084 (T,wt=14): 4962 x ^ (y ^ (z ^ ((u v z) ^ x)')) = 0.  [para(879(a,1),1818(a,1,2,2,1,1)),rewrite(5(5))].

given #1085 (T,wt=14): 5066 x ^ (((x v y) ^ (x v z))' ^ u) = 0.  [para(1820(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #1086 (T,wt=14): 5069 x ^ (y ^ ((x v z) ^ (x v u))') = 0.  [para(1820(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #1087 (A,wt=32): 431 (x ^ y) v z != 1 | x ^ (y ^ ((x ^ (y ^ u)) v z)) != 0 | (x ^ y)' = (x ^ (y ^ u)) v z.  [para(22(a,1),37(a,1)),rewrite(5(6),5(15))].

given #1088 (T,wt=14): 5078 ((x v y) ^ (x v z))' ^ (u ^ x) = 0.  [para(1820(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6))].

given #1089 (T,wt=14): 5088 x ^ ((x v y) ^ (z v (u v x)))' = 0.  [para(3(a,1),1825(a,1,2,1,2))].

given #1090 (T,wt=14): 5089 x ^ (((x v y) ^ (z v x))' ^ u) = 0.  [para(1825(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #1091 (T,wt=14): 5093 x ^ (y ^ ((x v z) ^ (u v x))') = 0.  [para(1825(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #1092 (A,wt=23): 432 x ^ (y ^ (x ^ (y ^ z))') != 0 | (x ^ (y ^ z))' = (x ^ y)'.  [para(162(a,1),37(a,1)),rewrite(5(5),5(14)),flip(c),xx(a)].

given #1093 (T,wt=14): 5114 ((x v y) ^ (z v x))' ^ (u ^ x) = 0.  [para(1825(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6))].

given #1094 (T,wt=14): 5123 x ^ ((y ^ x)' ^ (z ^ (y ^ u))) = 0.  [para(1954(a,1),5(a,1,1)),rewrite(80(2),5(6),5(5)),flip(a)].

given #1095 (T,wt=14): 5129 x ^ (y ^ ((z v (u v y)) ^ x)') = 0.  [para(82(a,1),1954(a,1,2,2)),rewrite(4(5))].

given #1096 (T,wt=14): 5138 x ^ ((y v z) ^ ((z v y) ^ x)') = 0.  [para(185(a,1),1954(a,1,2,2)),rewrite(4(5))].

given #1097 (A,wt=23): 433 x ^ (y ^ (z ^ (x ^ y))') != 0 | (z ^ (x ^ y))' = (x ^ y)'.  [para(171(a,1),37(a,1)),flip(c),xx(a)].

given #1098 (T,wt=14): 5178 x v (y v ((z ^ y) v (x ^ u))') = 1.  [para(2431(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #1099 (T,wt=14): 5186 x v (y v ((z ^ y) v (u ^ x))') = 1.  [para(2431(a,1),102(a,1,2)),rewrite(88(2)),flip(a)].

given #1100 (T,wt=14): 5218 x v (((y ^ x) v (x ^ z))' v u) = 1.  [para(2466(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #1101 (T,wt=14): 5220 x v ((y ^ (z ^ x)) v (x ^ u))' = 1.  [para(5(a,1),2466(a,1,2,1,1))].

given #1102 (A,wt=22): 434 x v (y ^ z) != 1 | y ^ z != 0 | (y ^ z)' = x v (y ^ z).  [para(65(a,1),37(a,1)),rewrite(84(8))].

given #1103 (T,wt=14): 5223 x v (y v ((z ^ x) v (x ^ u))') = 1.  [para(2466(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1104 (T,wt=14): 5225 x v ((y ^ x) v (z ^ (x ^ u)))' = 1.  [para(17(a,1),2466(a,1,2,1,2))].

given #1105 (T,wt=14): 5233 ((x ^ y) v (y ^ z))' v (u v y) = 1.  [para(2466(a,1),95(a,1,1)),rewrite(67(8),2466(11))].

given #1106 (T,wt=14): 5240 x ^ (y ^ ((z v y) ^ (x v u))') = 0.  [para(2487(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #1107 (A,wt=36): 435 (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(23(a,1),37(a,1))].

given #1108 (T,wt=14): 5248 x ^ (y ^ ((z v y) ^ (u v x))') = 0.  [para(2487(a,1),83(a,1,2)),rewrite(91(2)),flip(a)].

given #1109 (T,wt=14): 5267 x ^ ((y v (z v x)) ^ (x v u))' = 0.  [para(3(a,1),2528(a,1,2,1,1))].

given #1110 (T,wt=14): 5268 x ^ (((y v x) ^ (x v z))' ^ u) = 0.  [para(2528(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #1111 (T,wt=14): 5272 x ^ (y ^ ((z v x) ^ (x v u))') = 0.  [para(2528(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #1112 (A,wt=27): 439 x ^ (y ^ (z v ((x ^ y) v z)')) != 0 | z v ((x ^ y) v z)' = (x ^ y)'.  [para(29(a,1),37(a,1)),flip(c),xx(a)].

given #1113 (T,wt=14): 5282 ((x v y) ^ (y v z))' ^ (u ^ y) = 0.  [para(2528(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6))].

given #1114 (T,wt=14): 5293 (x v y)' ^ (x v (z ^ (y ^ u))) = 0.  [para(17(a,1),3101(a,1,2,2))].

given #1115 (T,wt=14): 5295 (x v y)' ^ (x v ((x v y) ^ z)) = 0.  [para(63(a,1),3101(a,1,1,1))].

given #1116 (T,wt=14): 5296 (x v y)' ^ (y v ((x v y) ^ z)) = 0.  [para(65(a,1),3101(a,1,1,1))].

given #1117 (A,wt=23): 440 (x ^ y) v (z ^ (y ^ z)') != 1 | (x ^ y)' = z ^ (y ^ z)'.  [para(32(a,1),37(b,1,2)),rewrite(91(9)),xx(b)].

given #1118 (T,wt=14): 5303 (x v (y v z))' ^ (x v (u ^ y)) = 0.  [para(159(a,1),3101(a,1,2,2))].

given #1119 (T,wt=14): 5306 (x v (y v z))' ^ (x v (u ^ z)) = 0.  [para(827(a,1),3101(a,1,2,2))].

given #1120 (T,wt=14): 5355 (x ^ y)' v (x ^ (z v (y v u))) = 1.  [para(15(a,1),3138(a,1,2,2))].

given #1121 (T,wt=14): 5359 (x ^ y)' v (x ^ ((x ^ y) v z)) = 1.  [para(57(a,1),3138(a,1,1,1))].

given #1122 (A,wt=27): 441 x ^ (y ^ (z v ((x ^ y)' v u))) != 0 | z v ((x ^ y)' v u) = (x ^ y)'.  [para(112(a,1),37(a,1)),flip(c),xx(a)].

given #1123 (T,wt=14): 5360 (x ^ y)' v (y ^ ((x ^ y) v z)) = 1.  [para(59(a,1),3138(a,1,1,1))].

given #1124 (T,wt=14): 5368 (x ^ (y ^ z))' v (x ^ (u v y)) = 1.  [para(186(a,1),3138(a,1,2,2))].

given #1125 (T,wt=14): 5371 (x ^ (y ^ z))' v (x ^ (u v z)) = 1.  [para(879(a,1),3138(a,1,2,2))].

given #1126 (T,wt=14): 5385 (x ^ y)' v ((z v (u v x)) ^ y) = 1.  [para(3(a,1),3245(a,1,2,1))].

given #1127 (A,wt=23): 442 (x ^ y) v (z ^ (y' ^ u)) != 1 | (x ^ y)' = z ^ (y' ^ u).  [para(121(a,1),37(b,1,2)),rewrite(91(9)),xx(b)].

given #1128 (T,wt=14): 5396 x' v ((y v x) ^ (z v (x v u))) = 1.  [para(52(a,1),3245(a,1,1,1))].

given #1129 (T,wt=14): 5397 x' v ((y v x) ^ (z v (u v x))) = 1.  [para(82(a,1),3245(a,1,1,1))].

given #1130 (T,wt=14): 5431 (x ^ (y v z)) v ((z ^ x)' v u) = 1.  [para(3247(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #1131 (T,wt=14): 5432 (x ^ (y v (z v u))) v (u ^ x)' = 1.  [para(3(a,1),3247(a,1,1,2))].

given #1132 (A,wt=19): 443 (x ^ y) v (x' ^ z) != 1 | (x ^ y)' = x' ^ z.  [para(121(a,1),37(b,1)),xx(b)].

given #1133 (T,wt=14): 5436 (x ^ (y v z)) v (u v (z ^ x)') = 1.  [para(3247(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1134 (T,wt=14): 5443 (x ^ y) v (z ^ (y ^ (u ^ x)))' = 1.  [para(73(a,1),3247(a,1,1,2)),rewrite(5(4),5(3))].

given #1135 (T,wt=14): 5444 ((x v (y v z)) ^ (u v z)) v z' = 1.  [para(82(a,1),3247(a,1,2,1))].

given #1136 (T,wt=14): 5462 (x ^ y)' v ((y ^ (z v x)) v u) = 1.  [para(3247(a,1),94(a,1,1)),rewrite(67(8),5386(11))].

given #1137 (A,wt=19): 444 (x ^ y') v (z ^ y) != 1 | (x ^ y')' = z ^ y.  [para(268(a,1),37(b,1,2)),rewrite(91(8)),xx(b)].

given #1138 (T,wt=14): 5464 (x ^ y)' v (z v (y ^ (u v x))) = 1.  [para(3247(a,1),95(a,1,1)),rewrite(67(8),3247(11))].

given #1139 (T,wt=14): 5488 ((x v y) ^ (y v z)) v (y' v u) = 1.  [para(3249(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #1140 (T,wt=14): 5490 ((x v y) ^ (y v z)) v (u v y') = 1.  [para(3249(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1141 (T,wt=14): 5497 x' v (((y v x) ^ (x v z)) v u) = 1.  [para(3249(a,1),94(a,1,1)),rewrite(67(8),5388(11))].

given #1142 (A,wt=23): 445 (x ^ y) v ((y v z)' ^ u) != 1 | (x ^ y)' = (y v z)' ^ u.  [para(122(a,1),37(b,1,2)),rewrite(91(9)),xx(b)].

given #1143 (T,wt=14): 5498 x' v (y v ((z v x) ^ (x v u))) = 1.  [para(3249(a,1),95(a,1,1)),rewrite(67(8),3249(11))].

given #1144 (T,wt=14): 5572 ((x v y) ^ (z v y)) v (y' v u) = 1.  [para(3254(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #1145 (T,wt=14): 5574 ((x v y) ^ (z v y)) v (u v y') = 1.  [para(3254(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #1146 (T,wt=14): 5590 x' v (((y v x) ^ (z v x)) v u) = 1.  [para(3254(a,1),94(a,1,1)),rewrite(67(8),5392(11))].

given #1147 (A,wt=27): 446 x ^ (y ^ (z v (u v (x ^ y)'))) != 0 | z v (u v (x ^ y)') = (x ^ y)'.  [para(124(a,1),37(a,1)),flip(c),xx(a)].

given #1148 (T,wt=14): 5591 x' v (y v ((z v x) ^ (u v x))) = 1.  [para(3254(a,1),95(a,1,1)),rewrite(67(8),3254(11))].

given #1149 (T,wt=14): 5600 x ^ ((y v (z v x)) ^ (u v x))' = 0.  [para(3(a,1),3304(a,1,2,1,1))].

given #1150 (T,wt=14): 5601 x ^ ((y v x) ^ (z v (u v x)))' = 0.  [para(3(a,1),3304(a,1,2,1,2))].

given #1151 (T,wt=14): 5602 x ^ (((y v x) ^ (z v x))' ^ u) = 0.  [para(3304(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #1152 (A,wt=23): 447 (x ^ y) v (z ^ (u ^ y')) != 1 | (x ^ y)' = z ^ (u ^ y').  [para(127(a,1),37(b,1,2)),rewrite(91(9)),xx(b)].

given #1153 (T,wt=14): 5604 x ^ (y ^ (x ^ (z v (x ^ y)))') = 0.  [para(7(a,1),3304(a,1,2,1,1)),rewrite(5(6))].

given #1154 (T,wt=14): 5608 x ^ (y ^ ((z v x) ^ (u v x))') = 0.  [para(3304(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #1155 (T,wt=14): 5629 ((x v y) ^ (z v y))' ^ (u ^ y) = 0.  [para(3304(a,1),557(a,1,2,2,2,1)),rewrite(79(6),30(6))].

given #1156 (T,wt=14): 5635 (x ^ y)' v (x ^ (z v (u v y))) = 1.  [para(3(a,1),3352(a,1,2,2))].

given #1157 (A,wt=19): 448 (x ^ y) v (z ^ x') != 1 | (x ^ y)' = z ^ x'.  [para(127(a,1),37(b,1)),xx(b)].

given #1158 (T,wt=14): 5641 (x ^ y)' v (x ^ (z v (x ^ y))) = 1.  [para(57(a,1),3352(a,1,1,1))].

given #1159 (T,wt=14): 5642 (x ^ y)' v (y ^ (z v (x ^ y))) = 1.  [para(59(a,1),3352(a,1,1,1))].

given #1160 (T,wt=14): 5674 (x v (y ^ z)) ^ ((z v x)' ^ u) = 0.  [para(3412(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #1161 (T,wt=14): 5675 (x v (y ^ (z ^ u))) ^ (u v x)' = 0.  [para(5(a,1),3412(a,1,1,2))].

given #1162 (A,wt=23): 449 (x ^ y) v (z ^ (y v u)') != 1 | (x ^ y)' = z ^ (y v u)'.  [para(129(a,1),37(b,1,2)),rewrite(91(9)),xx(b)].

given #1163 (T,wt=14): 5678 (x v (y ^ z)) ^ (u ^ (z v x)') = 0.  [para(3412(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #1164 (T,wt=14): 5684 ((x ^ (y ^ z)) v (u ^ z)) ^ z' = 0.  [para(104(a,1),3412(a,1,2,1))].

given #1165 (T,wt=14): 5709 (x v y)' ^ ((y v (z ^ x)) ^ u) = 0.  [para(3412(a,1),553(a,1,2,2,1,1)),rewrite(79(6),67(6))].

given #1166 (T,wt=14): 5710 (x v y)' ^ (z ^ (y v (u ^ x))) = 0.  [para(3412(a,1),557(a,1,2,2,2,1)),rewrite(79(6),4(6),67(6))].

given #1167 (A,wt=19): 450 (x ^ y) v (x v z)' != 1 | (x v z)' = (x ^ y)'.  [para(129(a,1),37(b,1)),flip(c),xx(b)].

given #1168 (T,wt=14): 5732 (x v y)' ^ ((z ^ (u ^ x)) v y) = 0.  [para(5(a,1),3413(a,1,2,1))].

given #1169 (T,wt=14): 5740 x' ^ ((y ^ x) v (z ^ (x ^ u))) = 0.  [para(73(a,1),3413(a,1,1,1))].

given #1170 (T,wt=14): 5741 x' ^ ((y ^ x) v (z ^ (u ^ x))) = 0.  [para(104(a,1),3413(a,1,1,1))].

given #1171 (T,wt=14): 5752 (x v (y v z))' ^ ((u ^ x) v y) = 0.  [para(3413(a,1),101(a,1,2)),rewrite(4(4),80(4)),flip(a)].

given #1172 (A,wt=23): 451 (x ^ y) v (z v (y v u))' != 1 | (z v (y v u))' = (x ^ y)'.  [para(134(a,1),37(b,1,2)),rewrite(91(9)),flip(c),xx(b)].

given #1173 (T,wt=14): 5763 ((x ^ y) v (y ^ z)) ^ (y' ^ u) = 0.  [para(3415(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #1174 (T,wt=14): 5765 ((x ^ y) v (y ^ z)) ^ (u ^ y') = 0.  [para(3415(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #1175 (T,wt=14): 5773 x' ^ (((y ^ x) v (x ^ z)) ^ u) = 0.  [para(3415(a,1),553(a,1,2,2,1,1)),rewrite(79(6),67(6))].

given #1176 (T,wt=14): 5774 x' ^ (y ^ ((z ^ x) v (x ^ u))) = 0.  [para(3415(a,1),557(a,1,2,2,2,1)),rewrite(79(6),4(6),67(6))].

given #1177 (A,wt=23): 452 (x ^ y) v (z v (u v y))' != 1 | (z v (u v y))' = (x ^ y)'.  [para(143(a,1),37(b,1,2)),rewrite(91(9)),flip(c),xx(b)].

given #1178 (T,wt=14): 5781 ((x ^ y) v (z ^ y)) ^ (y' ^ u) = 0.  [para(3420(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #1179 (T,wt=14): 5783 ((x ^ y) v (z ^ y)) ^ (u ^ y') = 0.  [para(3420(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #1180 (T,wt=14): 5805 x' ^ (((y ^ x) v (z ^ x)) ^ u) = 0.  [para(3420(a,1),553(a,1,2,2,1,1)),rewrite(79(6),67(6))].

given #1181 (T,wt=14): 5806 x' ^ (y ^ ((z ^ x) v (u ^ x))) = 0.  [para(3420(a,1),557(a,1,2,2,2,1)),rewrite(79(6),4(6),67(6))].

given #1182 (A,wt=23): 453 (x ^ y) v ((z v y)' ^ u) != 1 | (x ^ y)' = (z v y)' ^ u.  [pa