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

assign(max_seconds,30).

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

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

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

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

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

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

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

% Clauses before input processing:

formulas(usable).
end_of_list.

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

formulas(demodulators).
end_of_list.

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

No predicates eliminated.

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

Auto_denials:  (no changes).

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

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

Auto_process settings:  (no changes).

% Operation v is commutative; C redundancy checks enabled.

% Operation ^ is commutative; C redundancy checks enabled.

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

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

% Clauses after input processing:

formulas(usable).
end_of_list.

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

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

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

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

% Starting search at 0.00 seconds.

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

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

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

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

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

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

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

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

given #7 (I,wt=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=23): 12 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))).  [copy(11),flip(a)].

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

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

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

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

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

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

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

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

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

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

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

given #22 (T,wt=4): 100 0' = 1.  [hyper(10,a,84,a,b,32,a)].

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

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

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

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

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

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

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

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

given #31 (T,wt=7): 112 0 != x | x' = 1.  [back_rewrite(83),rewrite(111(2)),xx(a)].

given #32 (T,wt=7): 116 1 != x | x' = 0.  [back_rewrite(85),rewrite(114(4)),xx(b)].

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

given #34 (T,wt=8): 99 x v (x' v y) = 1.  [back_rewrite(30),rewrite(98(5))].

given #35 (T,wt=8): 103 x ^ (x' ^ y) = 0.  [back_rewrite(33),rewrite(101(5))].

given #36 (T,wt=8): 113 x v (y v x') = 1.  [back_rewrite(63),rewrite(111(5))].

given #37 (T,wt=8): 115 x ^ (y ^ x') = 0.  [back_rewrite(92),rewrite(114(5))].

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

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

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

given #41 (T,wt=6): 186 c1 ^ c2' = 0.  [para(133(a,1),145(a,1,2,1))].

given #42 (T,wt=8): 180 x ^ (y v x)' = 0.  [para(2(a,1),145(a,1,2,1))].

given #43 (T,wt=8): 187 c1 ^ (c2' ^ x) = 0.  [para(186(a,1),5(a,1,1)),rewrite(101(2)),flip(a)].

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

given #45 (T,wt=8): 190 c1 ^ (x ^ c2') = 0.  [para(186(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

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

given #47 (T,wt=8): 217 x v (y ^ x)' = 1.  [para(4(a,1),203(a,1,2,1))].

given #48 (T,wt=6): 228 c2 v c1' = 1.  [para(13(a,1),217(a,1,2,1))].

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

given #50 (T,wt=8): 233 c2 v (c1' v x) = 1.  [para(228(a,1),3(a,1,1)),rewrite(98(2)),flip(a)].

given #51 (T,wt=8): 236 c2 v (x v c1') = 1.  [para(228(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

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

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

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

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

given #56 (T,wt=8): 263 c1 ^ (c2 v x)' = 0.  [para(145(a,1),57(a,1,2)),rewrite(4(3),101(3)),flip(a)].

given #57 (T,wt=8): 264 c1 ^ (x v c2)' = 0.  [para(180(a,1),57(a,1,2)),rewrite(4(3),101(3)),flip(a)].

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

given #59 (A,wt=10): 31 x v (y v (x v y)') = 1.  [para(8(a,1),3(a,1)),flip(a)].

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

given #61 (T,wt=7): 310 c2 v (c1 ^ x) = c2.  [para(4(a,1),297(a,1,2))].

given #62 (T,wt=8): 300 c2 v (x ^ c1)' = 1.  [para(58(a,1),203(a,1,2,1))].

given #63 (T,wt=8): 320 c2 v (c1 ^ x)' = 1.  [para(4(a,1),300(a,1,2,1))].

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

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

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

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

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

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

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

given #71 (T,wt=8): 377 x' v (y v x) = 1.  [para(356(a,1),113(a,1,2,2))].

given #72 (T,wt=8): 378 x' ^ (y ^ x) = 0.  [para(356(a,1),115(a,1,2,2))].

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

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

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

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

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

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

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

given #80 (T,wt=9): 139 c1 v (c2 v x) = c2 v x.  [para(133(a,1),3(a,1,1)),flip(a)].

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

given #82 (T,wt=9): 142 c1 v (x v c2) = x v c2.  [para(133(a,1),17(a,1,2)),flip(a)].

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

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

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

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

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

given #88 (T,wt=9): 366 c2 ^ c1' != 0 | c2 = c1.  [para(228(a,1),36(a,1)),rewrite(4(7),356(12)),flip(c),xx(a)].

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

given #90 (T,wt=9): 497 c1 v c2' != 1 | c2 = c1.  [para(186(a,1),38(b,1)),rewrite(2(4),356(12)),xx(b)].

given #91 (T,wt=9): 517 c2 v (x v c1) = c2 v x.  [para(140(a,2),2(a,1))].

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

given #93 (T,wt=10): 137 c2 != 1 | c1 != 0 | c1' = c2.  [back_rewrite(59),rewrite(133(3))].

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

given #95 (T,wt=10): 156 x v (y v (x' v z)) = 1.  [para(99(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #96 (T,wt=10): 160 x ^ (y ^ (x' ^ z)) = 0.  [para(103(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #97 (T,wt=10): 161 x ^ ((x v y)' ^ z) = 0.  [para(103(a,1),22(a,1,2)),rewrite(114(2)),flip(a)].

given #98 (T,wt=10): 163 x v (y v (z v x')) = 1.  [para(3(a,1),113(a,1,2))].

given #99 (A,wt=29): 44 x ^ (y v (z v ((x ^ u) v (u ^ (y v (z v v)))))) = x ^ (y v (z v (u ^ (x v v)))).  [para(3(a,1),12(a,1,2,2,2,2)),rewrite(3(7),3(12))].

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

given #101 (T,wt=10): 170 x ^ (y ^ (x v z)') = 0.  [para(115(a,1),22(a,1,2)),rewrite(114(2)),flip(a)].

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

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

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

given #105 (T,wt=10): 192 x ^ ((y v x)' ^ z) = 0.  [para(180(a,1),5(a,1,1)),rewrite(101(2)),flip(a)].

given #106 (T,wt=10): 197 x ^ (y ^ (z v x)') = 0.  [para(180(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #107 (T,wt=10): 200 c1 ^ (x ^ (c2' ^ y)) = 0.  [para(187(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #108 (T,wt=10): 209 x v ((x ^ y)' v z) = 1.  [para(99(a,1),24(a,1,2)),rewrite(111(2)),flip(a)].

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

given #110 (T,wt=10): 210 x v (y v (x ^ z)') = 1.  [para(113(a,1),24(a,1,2)),rewrite(111(2)),flip(a)].

given #111 (T,wt=10): 213 c1 ^ (x ^ (y ^ c2')) = 0.  [para(5(a,1),190(a,1,2))].

given #112 (T,wt=10): 221 x v (y ^ (x ^ z))' = 1.  [para(19(a,1),203(a,1,2,1))].

given #113 (T,wt=10): 222 x v ((y ^ x)' v z) = 1.  [para(217(a,1),3(a,1,1)),rewrite(98(2)),flip(a)].

given #114 (A,wt=27): 47 x ^ ((y v ((x ^ z) v (z ^ (y v u)))) ^ v) = x ^ ((y v (z ^ (x v u))) ^ v).  [para(12(a,1),5(a,1,1)),rewrite(5(5)),flip(a)].

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

given #116 (T,wt=10): 229 x v (y v (z ^ x)') = 1.  [para(217(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #117 (T,wt=10): 249 c2 v (x v (c1' v y)) = 1.  [para(233(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #118 (T,wt=10): 250 c2 v (x v (y v c1')) = 1.  [para(3(a,1),236(a,1,2))].

given #119 (A,wt=31): 48 x ^ (y ^ (z v ((x ^ (y ^ u)) v (u ^ (z v v))))) = x ^ (y ^ (z v (u ^ ((x ^ y) v v)))).  [para(12(a,1),5(a,1)),rewrite(5(6),5(8)),flip(a)].

given #120 (T,wt=10): 265 (c2 ^ x) v (c1 ^ x)' = 1.  [para(57(a,1),217(a,1,2,1))].

given #121 (T,wt=10): 286 c1 ^ ((c2 v x)' ^ y) = 0.  [para(263(a,1),5(a,1,1)),rewrite(101(2)),flip(a)].

given #122 (T,wt=10): 289 c1 ^ (x v (c2 v y))' = 0.  [para(17(a,1),263(a,1,2,1))].

given #123 (T,wt=10): 290 c1 ^ (x ^ (c2 v y)') = 0.  [para(263(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #124 (A,wt=29): 49 x ^ (y v ((x ^ (z ^ u)) v (z ^ (u ^ (y v v))))) = x ^ (y v (z ^ (u ^ (x v v)))).  [para(5(a,1),12(a,1,2,2,2)),rewrite(5(11))].

given #125 (T,wt=10): 291 c1 ^ (x v (y v c2))' = 0.  [para(3(a,1),264(a,1,2,1))].

given #126 (T,wt=10): 292 c1 ^ ((x v c2)' ^ y) = 0.  [para(264(a,1),5(a,1,1)),rewrite(101(2)),flip(a)].

given #127 (T,wt=10): 295 c1 ^ (x ^ (y v c2)') = 0.  [para(264(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #128 (T,wt=10): 303 x v (y v (y v x)') = 1.  [para(2(a,1),31(a,1,2,2,1))].

given #129 (A,wt=16): 52 x ^ (y v (z ^ (x v y'))) = x ^ (y v z).  [para(8(a,1),12(a,1,2,2,2,2)),rewrite(32(3),2(2),26(2)),flip(a)].

given #130 (T,wt=10): 319 c2 v ((x ^ c1)' v y) = 1.  [para(300(a,1),3(a,1,1)),rewrite(98(2)),flip(a)].

given #131 (T,wt=10): 321 c2 v (x ^ (y ^ c1))' = 1.  [para(5(a,1),300(a,1,2,1))].

given #132 (T,wt=10): 324 c2 v (x v (y ^ c1)') = 1.  [para(300(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #133 (T,wt=10): 325 c2 v ((c1 ^ x)' v y) = 1.  [para(320(a,1),3(a,1,1)),rewrite(98(2)),flip(a)].

given #134 (A,wt=49): 55 x ^ (y v ((x ^ (z v (u ^ (x v v)))) v ((z v ((x ^ u) v (u ^ (z v v)))) ^ (y v w)))) = x ^ (y v ((z v ((x ^ u) v (u ^ (z v v)))) ^ (x v w))).  [para(12(a,1),12(a,1,2,2,1))].

given #135 (T,wt=10): 328 c2 v (x v (c1 ^ y)') = 1.  [para(320(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #136 (T,wt=10): 329 c2 v (x ^ (c1 ^ y))' = 1.  [para(19(a,1),320(a,1,2,1))].

given #137 (T,wt=10): 330 x ^ (y ^ (y ^ x)') = 0.  [para(4(a,1),34(a,1,2,2,1))].

given #138 (T,wt=10): 337 c1 ^ (x ^ (c2 ^ x)') = 0.  [para(34(a,1),57(a,1,2)),rewrite(4(3),101(3)),flip(a)].

given #139 (A,wt=31): 56 x ^ (y v (z ^ (x v ((z ^ u) v (u ^ (y v v)))))) = x ^ (y v (z ^ (x v (u ^ (z v v))))).  [para(12(a,1),12(a,1,2,2,2)),rewrite(12(8)),flip(a)].

given #140 (T,wt=10): 360 c2 != 1 | c1 != 0 | c2' = c1.  [para(133(a,1),36(a,1)),rewrite(4(6),13(6))].

given #141 (T,wt=10): 379 x' v (y v (x v z)) = 1.  [para(377(a,1),3(a,1,1)),rewrite(98(2),3(4)),flip(a)].

given #142 (T,wt=8): 2216 c1' v (x v c2) = 1.  [para(133(a,1),379(a,1,2,2))].

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

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

given #145 (T,wt=10): 386 x' ^ (y ^ (x ^ z)) = 0.  [para(378(a,1),5(a,1,1)),rewrite(101(2),5(4)),flip(a)].

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

given #147 (T,wt=8): 2321 c2' ^ (x ^ c1) = 0.  [para(13(a,1),387(a,1,2,2))].

given #148 (T,wt=10): 458 (x ^ c2) v (x ^ c1)' = 1.  [para(96(a,1),217(a,1,2,1))].

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

given #150 (T,wt=10): 459 x ^ (c1 ^ (x ^ c2)') = 0.  [para(96(a,1),378(a,1,2)),rewrite(4(6),5(6))].

given #151 (T,wt=10): 521 (x v c1) ^ (x v c2)' = 0.  [para(140(a,1),180(a,1,2,1))].

given #152 (T,wt=10): 525 x v (c2 v (x v c1)') = 1.  [para(140(a,1),377(a,1,2)),rewrite(2(6),3(6))].

given #153 (T,wt=10): 697 (x v c1) ^ (c2 v x)' = 0.  [para(517(a,1),180(a,1,2,1))].

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

given #155 (T,wt=10): 699 c2 v (x v (x v c1)') = 1.  [para(517(a,1),377(a,1,2)),rewrite(2(6),3(6))].

given #156 (T,wt=10): 1550 (x ^ c2) v (c1 ^ x)' = 1.  [para(4(a,1),265(a,1,1))].

given #157 (T,wt=10): 1551 (c2 ^ x) v (x ^ c1)' = 1.  [para(4(a,1),265(a,1,2,1))].

given #158 (T,wt=10): 1552 (c2 ^ (c1 v x)) v c1' = 1.  [para(6(a,1),265(a,1,2,1))].

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

given #160 (T,wt=10): 1558 (c2 ^ (x v c1)) v c1' = 1.  [para(20(a,1),265(a,1,2,1))].

given #161 (T,wt=10): 2022 c1 ^ (x ^ (x ^ c2)') = 0.  [para(330(a,1),57(a,1,2)),rewrite(4(3),101(3)),flip(a)].

given #162 (T,wt=10): 2041 x ^ (c1 ^ (c2 ^ x)') = 0.  [para(337(a,1),19(a,1)),flip(a)].

given #163 (T,wt=10): 2043 c1 ^ (c2 ^ (c1 v x))' = 0.  [para(337(a,1),22(a,1)),flip(a)].

given #164 (A,wt=11): 67 c1 ^ (x v (c2 ^ (c1 v y))) = c1.  [back_rewrite(60),rewrite(61(8)),flip(a)].

given #165 (T,wt=10): 2221 c1' v (x v (c2 v y)) = 1.  [para(139(a,1),379(a,1,2,2))].

given #166 (T,wt=10): 2222 c1' v (x v (y v c2)) = 1.  [para(142(a,1),379(a,1,2,2))].

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

given #168 (T,wt=10): 2248 (x ^ y)' v (z v y) = 1.  [para(26(a,1),380(a,1,2,2))].

given #169 (A,wt=13): 68 x ^ (y v ((x v z) ^ (x v u))) = x.  [back_rewrite(50),rewrite(61(6)),flip(a)].

given #170 (T,wt=10): 2252 (x ^ c1)' v (y v c2) = 1.  [para(297(a,1),380(a,1,2,2))].

given #171 (T,wt=10): 2253 (c1 ^ x)' v (y v c2) = 1.  [para(310(a,1),380(a,1,2,2))].

given #172 (T,wt=10): 2302 c2' ^ (x ^ (y ^ c1)) = 0.  [para(58(a,1),386(a,1,2,2))].

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

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

given #175 (T,wt=7): 3243 c1 != 1 | c1' = 0.  [para(186(a,1),74(b,1)),rewrite(186(12)),flip(a),xx(b)].

given #176 (T,wt=7): 3245 x' != 1 | 0 = x.  [para(378(a,1),74(b,1)),rewrite(356(8),378(9)),flip(a),flip(c),xx(b)].

given #177 (T,wt=7): 3247 c2' != 1 | c2 = 0.  [para(2321(a,1),74(b,1)),rewrite(356(10),2321(13)),flip(a),xx(b)].

given #178 (T,wt=10): 2323 (x v y)' ^ (z ^ y) = 0.  [para(20(a,1),387(a,1,2,2))].

given #179 (A,wt=17): 79 x ^ (y v ((y v z) ^ (x v z))) = x ^ (y v z).  [back_rewrite(73),rewrite(75(7))].

given #180 (F,wt=10): 3251 (c1 ^ (c1' v c2'))' != 1.  [ur(3245,b,152,a(flip))].

given #181 (T,wt=10): 2328 (c2 v x)' ^ (y ^ c1) = 0.  [para(254(a,1),387(a,1,2,2))].

given #182 (T,wt=10): 2329 (x v c2)' ^ (y ^ c1) = 0.  [para(259(a,1),387(a,1,2,2))].

given #183 (T,wt=10): 2359 c2' ^ (x ^ (c1 ^ y)) = 0.  [para(2321(a,1),5(a,1,1)),rewrite(101(2),5(6)),flip(a)].

given #184 (T,wt=10): 2459 (c1 v x) ^ (x v c2)' = 0.  [para(2(a,1),521(a,1,1))].

given #185 (A,wt=14): 80 x v y != 1 | 0 != x | x' = x v y.  [back_rewrite(40),rewrite(75(2))].

given #186 (T,wt=7): 3419 c2 != 0 | c2' = 1.  [para(228(a,1),80(a,1)),rewrite(228(12)),flip(b),xx(a)].

given #187 (T,wt=7): 3421 x' != 0 | 1 = x.  [para(377(a,1),80(a,1)),rewrite(356(8),377(9)),flip(b),flip(c),xx(a)].

given #188 (T,wt=7): 3423 c1' != 0 | c1 = 1.  [para(2216(a,1),80(a,1)),rewrite(356(10),2216(13)),flip(b),xx(a)].

given #189 (T,wt=10): 2477 x v (c2 v (c1 v x)') = 1.  [para(2(a,1),525(a,1,2,2,1))].

given #190 (A,wt=17): 86 x ^ (y v (z ^ (x v y))) = x ^ (y v (z ^ x)).  [para(35(a,1),12(a,1,2,2,2,2)),rewrite(78(5),35(6))].

given #191 (T,wt=10): 2501 (c1 v x) ^ (c2 v x)' = 0.  [para(2(a,1),697(a,1,1))].

given #192 (T,wt=10): 2502 (c1 v (c2 ^ x)) ^ c2' = 0.  [para(7(a,1),697(a,1,2,1)),rewrite(2(4))].

given #193 (T,wt=10): 2506 (c1 v (x ^ c2)) ^ c2' = 0.  [para(26(a,1),697(a,1,2,1)),rewrite(2(4))].

given #194 (T,wt=10): 2673 c2 v (x v (c1 v x)') = 1.  [para(2(a,1),699(a,1,2,2,1))].

given #195 (A,wt=21): 87 x ^ (y v (x' ^ (y v z))) = x ^ (y v (x' ^ (x v z))).  [back_rewrite(53),rewrite(84(5))].

given #196 (T,wt=10): 2676 c2 v (c1 v (c2 ^ x))' = 1.  [para(699(a,1),24(a,1)),rewrite(2(6)),flip(a)].

given #197 (T,wt=10): 2720 c1' v (c2 ^ (c1 v x)) = 1.  [para(1552(a,1),2(a,1)),flip(a)].

given #198 (T,wt=10): 2938 c1' v (c2 ^ (x v c1)) = 1.  [para(1558(a,1),2(a,1)),flip(a)].

given #199 (T,wt=10): 2989 c1 ^ (c2 ^ (x v c1))' = 0.  [para(2(a,1),2043(a,1,2,1,2))].

given #200 (A,wt=19): 88 x ^ (y v (z ^ (x v (y ^ u)))) = x ^ (y v (z ^ x)).  [back_rewrite(81),rewrite(86(9))].

given #201 (T,wt=10): 3241 c1 != 1 | c1 != 0 | c1' = c1.  [para(13(a,1),74(b,1)),rewrite(13(11)),flip(a)].

given #202 (T,wt=10): 3420 c2 != 1 | c2 != 0 | c2' = c2.  [para(297(a,1),80(a,1)),rewrite(297(12)),flip(b)].

given #203 (T,wt=10): 3591 c2' ^ (c1 v (c2 ^ x)) = 0.  [para(2502(a,1),4(a,1)),flip(a)].

given #204 (T,wt=10): 3609 c2' ^ (c1 v (x ^ c2)) = 0.  [para(2506(a,1),4(a,1)),flip(a)].

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

given #206 (T,wt=10): 3835 c2 v (c1 v (x ^ c2))' = 1.  [para(4(a,1),2676(a,1,2,1,2))].

given #207 (T,wt=11): 105 x ^ ((y v x) ^ z) = x ^ z.  [para(20(a,1),5(a,1,1)),flip(a)].

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

given #209 (T,wt=11): 127 x v ((y ^ x) v z) = x v z.  [para(26(a,1),3(a,1,1)),flip(a)].

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

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

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

given #213 (T,wt=11): 188 c1 v c2' != 1 | c2' = c1'.  [para(186(a,1),10(b,1)),flip(c),xx(b)].

given #214 (T,wt=11): 234 c2 ^ c1' != 0 | c2' = c1'.  [para(228(a,1),10(a,1)),xx(a)].

given #215 (A,wt=29): 94 x ^ (y v ((z ^ (x ^ u)) v (z ^ (u ^ (y v v))))) = x ^ (y v (z ^ (u ^ (x v v)))).  [para(19(a,1),12(a,1,2,2,1)),rewrite(5(5),5(11))].

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

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

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

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

given #220 (A,wt=27): 95 x ^ (y ^ (z v ((x ^ u) v (u ^ (z v v))))) = y ^ (x ^ (z v (u ^ (x v v)))).  [para(12(a,1),19(a,1,2)),flip(a)].

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

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

given #223 (T,wt=11): 302 (c2 ^ x) v (x ^ c1) = c2 ^ x.  [para(58(a,1),27(a,1,2))].

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

given #225 (A,wt=13): 102 x ^ ((x ^ y) v (y ^ z)) = y ^ x.  [para(84(a,1),12(a,1,2,2,2,2)),rewrite(84(5),84(8),90(7))].

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

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

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

given #229 (T,wt=11): 349 (x v y) ^ (z ^ x) = z ^ x.  [para(71(a,1),22(a,2)),rewrite(348(4))].

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

given #231 (T,wt=11): 350 (x ^ y) v (y ^ x) = x ^ y.  [para(71(a,1),27(a,1,2))].

given #232 (T,wt=10): 5407 (x ^ y) v (y ^ x)' = 1.  [para(350(a,1),377(a,1,2)),rewrite(2(4))].

given #233 (T,wt=11): 397 (x v y) ^ (y v x) = x v y.  [para(77(a,1),21(a,1,2))].

given #234 (T,wt=10): 5477 (x v y) ^ (y v x)' = 0.  [para(397(a,1),378(a,1,2)),rewrite(4(4))].

given #235 (A,wt=14): 107 x v y != 1 | 0 != y | y' = x v y.  [para(20(a,1),10(b,1)),rewrite(77(2)),flip(b)].

given #236 (T,wt=11): 398 (x ^ y) v (z v x) = z v x.  [para(77(a,1),24(a,2)),rewrite(395(4))].

given #237 (T,wt=11): 410 x v y != 0 | (x v y)' = 1.  [para(32(a,1),37(b,1)),rewrite(111(2),111(2)),xx(a)].

given #238 (T,wt=11): 411 x v y != 1 | (x v y)' = 0.  [para(35(a,1),37(a,1,2)),rewrite(4(6),101(6)),xx(b)].

given #239 (T,wt=7): 5591 c2 != 1 | c2' = 0.  [para(133(a,1),411(a,1)),rewrite(133(6))].

given #240 (A,wt=13): 108 x ^ (y v ((z v x) ^ (x v u))) = x.  [para(20(a,1),12(a,1,2,2,1)),rewrite(61(6)),flip(a)].

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

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

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

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

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

given #246 (T,wt=11): 535 (c1 v x) ^ (x v c2) = c1 v x.  [para(142(a,1),21(a,1,2))].

given #247 (T,wt=11): 538 c1 ^ (x v (y v (c2 v z))) = c1.  [para(3(a,1),269(a,1,2))].

given #248 (T,wt=11): 551 x ^ y != 0 | (x ^ y)' = 1.  [para(32(a,1),39(b,1,2)),rewrite(2(3),98(3)),xx(a)].

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

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

given #251 (T,wt=11): 552 x ^ y != 1 | (x ^ y)' = 0.  [para(35(a,1),39(a,1)),rewrite(114(5),114(5)),xx(b)].

given #252 (T,wt=11): 598 c1 ^ (x v (y v (z v c2))) = c1.  [para(3(a,1),281(a,1,2,2))].

given #253 (T,wt=11): 606 c2 v (x ^ (y ^ (z ^ c1))) = c2.  [para(5(a,1),311(a,1,2,2))].

given #254 (T,wt=11): 613 c2 v (x ^ (y ^ (c1 ^ z))) = c2.  [para(5(a,1),318(a,1,2))].

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

given #256 (T,wt=11): 696 (x v c1) ^ (c2 v x) = x v c1.  [para(517(a,1),20(a,1,2))].

given #257 (T,wt=11): 3006 c1 ^ (x v (c2 ^ (y v c1))) = c1.  [para(2(a,1),67(a,1,2,2,2))].

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

given #259 (T,wt=11): 3250 (x v y)' != 1 | x v y = 0.  [para(2317(a,1),74(b,1)),rewrite(356(10),2317(12)),flip(a),xx(b)].

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

given #261 (T,wt=11): 3424 (x ^ y)' != 0 | x ^ y = 1.  [para(2244(a,1),80(a,1)),rewrite(356(10),2244(12)),flip(b),xx(a)].

given #262 (T,wt=11): 4087 (x v y) ^ (z ^ y) = z ^ y.  [para(71(a,1),105(a,2)),rewrite(348(4))].

given #263 (T,wt=11): 4199 (x ^ y) v (z v y) = z v y.  [para(77(a,1),127(a,2)),rewrite(395(4))].

given #264 (T,wt=11): 4614 (x ^ c1) v (c2 ^ x) = c2 ^ x.  [para(4(a,1),260(a,1,1))].

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

given #266 (T,wt=11): 4615 (c1 ^ x) v (x ^ c2) = c2 ^ x.  [para(4(a,1),260(a,1,2))].

given #267 (T,wt=11): 4699 (c2 v x) ^ (y ^ c1) = y ^ c1.  [para(71(a,1),261(a,2)),rewrite(348(7))].

given #268 (T,wt=11): 4781 (x v c2) ^ (y ^ c1) = y ^ c1.  [para(71(a,1),282(a,2)),rewrite(348(7))].

given #269 (T,wt=11): 5011 (x ^ c1) v (y v c2) = y v c2.  [para(77(a,1),299(a,2)),rewrite(395(7))].

given #270 (A,wt=19): 123 x ^ (y v ((y v z) ^ (x v (z v u)))) = x ^ (y v z).  [para(21(a,1),12(a,1,2,2,2)),rewrite(2(4),26(4),75(2)),flip(a)].

given #271 (T,wt=11): 5221 (c1 ^ x) v (y v c2) = y v c2.  [para(77(a,1),314(a,2)),rewrite(395(7))].

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

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

given #274 (T,wt=11): 5859 (c1 v x) ^ (c2 v x) = c1 v x.  [para(139(a,1),109(a,1,2))].

given #275 (A,wt=19): 124 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z).  [para(17(a,1),21(a,1,1)),rewrite(3(4))].

given #276 (T,wt=11): 5901 (x v c2) ^ (c1 v x) = c1 v x.  [para(535(a,1),4(a,1)),flip(a)].

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

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

given #279 (T,wt=11): 6157 (c2 v x) ^ (x v c1) = x v c1.  [para(696(a,1),4(a,1)),flip(a)].

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

given #281 (T,wt=11): 6199 c1 ^ ((c2 ^ (x v c1)) v y) = c1.  [para(2(a,1),3006(a,1,2))].

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

given #283 (T,wt=11): 6264 (x ^ y)' != 1 | x ^ y = 0.  [para(27(a,1),3250(a,1,1)),rewrite(27(8))].

given #284 (T,wt=7): 7067 c1' != 1 | c1 = 0.  [para(13(a,1),6264(a,1,1)),rewrite(13(7))].

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

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

given #287 (T,wt=11): 6314 (x v y)' != 0 | x v y = 1.  [para(21(a,1),3424(a,1,1)),rewrite(21(8))].

given #288 (T,wt=7): 7133 c2' != 0 | c2 = 1.  [para(133(a,1),6314(a,1,1)),rewrite(133(7))].

given #289 (T,wt=11): 6574 (x ^ c2) v (c1 ^ x) = c2 ^ x.  [para(4615(a,1),2(a,1)),flip(a)].

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

given #291 (T,wt=11): 7066 (x ^ y)' != 1 | y ^ x = 0.  [para(350(a,1),6262(a,1,1)),rewrite(350(7))].

given #292 (T,wt=11): 7131 (x v y)' != 0 | y v x = 1.  [para(397(a,1),6312(a,1,1)),rewrite(397(7))].

given #293 (T,wt=12): 153 x v (y v ((x v y)' v z)) = 1.  [para(99(a,1),3(a,1)),flip(a)].

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

given #295 (A,wt=14): 130 1 != x | y ^ x != 0 | x' = y ^ x.  [para(26(a,1),10(a,1)),rewrite(71(4)),flip(a)].

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

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

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

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

given #300 (A,wt=19): 131 x ^ (y v (z ^ (x v (u ^ y)))) = x ^ (y v (z ^ x)).  [para(26(a,1),12(a,1,2,2,2,2)),rewrite(89(5)),flip(a)].

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

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

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

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

given #305 (A,wt=33): 132 x v ((y ^ z) v ((z ^ (x v u)) v (y ^ (x v (z ^ (y v u)))))) = x v ((y ^ z) v (z ^ (x v u))).  [para(12(a,1),26(a,1,2)),rewrite(2(10),17(10),17(9),2(8))].

given #306 (T,wt=11): 7816 x v (c2 ^ (x v c1)) = x v c1.  [para(254(a,1),132(a,1,2,2,2,2,2)),rewrite(4(3),13(3),24(10),4624(6),4(8),13(8),7(10))].

given #307 (T,wt=11): 8103 x v (c2 ^ (c1 v x)) = x v c1.  [para(2(a,1),7816(a,1,2,2))].

given #308 (T,wt=11): 8109 x ^ (c1 v (x ^ c2)) = c2 ^ x.  [para(7816(a,1),12(a,1,2,2)),rewrite(2(6),77(7),102(13))].

given #309 (T,wt=11): 8116 x ^ (c1 v (c2 ^ x)) = c2 ^ x.  [para(7816(a,1),42(a,1,2,2)),rewrite(2(5),75(6),8109(5),7(7)),flip(a)].

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

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

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

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

given #314 (T,wt=12): 231 ((x v y) ^ z) v (x ^ z)' = 1.  [para(22(a,1),217(a,1,2,1))].

given #315 (A,wt=22): 138 x v (y v z) != 1 | x v y != 0 | (x v y)' = x v (y v z).  [back_rewrite(121),rewrite(136(4))].

given #316 (T,wt=12): 307 x v (y v (z v (x v z)')) = 1.  [para(31(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #317 (T,wt=12): 309 x v (y v ((x ^ z) v y)') = 1.  [para(31(a,1),24(a,1,2)),rewrite(111(2)),flip(a)].

given #318 (T,wt=12): 334 x ^ (y ^ (z ^ (x ^ z)')) = 0.  [para(34(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #319 (T,wt=12): 336 x ^ (y ^ ((x v z) ^ y)') = 0.  [para(34(a,1),22(a,1,2)),rewrite(114(2)),flip(a)].

given #320 (A,wt=21): 141 x ^ (c1 v ((x ^ y) v (y ^ c2))) = x ^ (c1 v (y ^ (x v c2))).  [para(133(a,1),12(a,1,2,2,2,2))].

given #321 (T,wt=12): 383 x v ((x v y)' v (z v y)) = 1.  [para(17(a,1),377(a,1,2)),rewrite(17(5))].

given #322 (T,wt=12): 391 x ^ ((x ^ y)' ^ (z ^ y)) = 0.  [para(19(a,1),378(a,1,2)),rewrite(19(5))].

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

given #324 (T,wt=12): 768 x v (y v ((x ^ z)' v u)) = 1.  [para(156(a,1),24(a,1,2)),rewrite(111(2)),flip(a)].

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

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

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

given #328 (T,wt=12): 789 x ^ ((y v (x v z))' ^ u) = 0.  [para(17(a,1),161(a,1,2,1,1))].

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

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

given #331 (T,wt=12): 798 x v (y v (z v (x ^ u)')) = 1.  [para(163(a,1),24(a,1,2)),rewrite(111(2)),flip(a)].

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

given #333 (T,wt=12): 914 x ^ (y ^ (z ^ (x v u)')) = 0.  [para(167(a,1),22(a,1,2)),rewrite(114(2)),flip(a)].

given #334 (T,wt=12): 925 x ^ (y ^ (z v (x v u))') = 0.  [para(17(a,1),170(a,1,2,2,1))].

given #335 (A,wt=31): 147 x ^ (y v ((x ^ z) v ((x v u) ^ (z ^ (y v v))))) = x ^ (y v ((x v u) ^ (z ^ (x v v)))).  [para(22(a,1),12(a,1,2,2,1)),rewrite(5(5),5(12))].

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

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

given #338 (T,wt=12): 943 x ^ ((y v (z v x))' ^ u) = 0.  [para(191(a,1),5(a,1,1)),rewrite(101(2)),flip(a)].

given #339 (T,wt=12): 948 x ^ (y ^ (z v (u v x))') = 0.  [para(191(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #340 (A,wt=27): 148 x ^ (y v (((x v z) ^ u) v (u ^ (y v v)))) = x ^ (y v (u ^ (x v (z v v)))).  [para(12(a,1),22(a,1,2)),rewrite(3(3),22(7)),flip(a)].

given #341 (T,wt=12): 956 (x v c1) ^ (y v (c2 v x))' = 0.  [para(517(a,1),191(a,1,2,1,2))].

given #342 (T,wt=12): 1027 x ^ (y ^ ((z v x)' ^ u)) = 0.  [para(192(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #343 (T,wt=12): 1034 (x v c1) ^ ((c2 v x)' ^ y) = 0.  [para(517(a,1),192(a,1,2,1,1))].

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

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

given #346 (T,wt=12): 1048 (x v c1) ^ (y ^ (c2 v x)') = 0.  [para(517(a,1),197(a,1,2,2,1))].

given #347 (T,wt=12): 1051 c1 ^ (x ^ (y ^ (c2' ^ z))) = 0.  [para(5(a,1),200(a,1,2))].

given #348 (T,wt=12): 1064 x v ((y ^ (x ^ z))' v u) = 1.  [para(19(a,1),209(a,1,2,1,1))].

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

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

given #351 (T,wt=12): 1167 c1 ^ (x ^ (y ^ (z ^ c2'))) = 0.  [para(5(a,1),213(a,1,2,2))].

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

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

given #354 (T,wt=12): 1192 x v (y v ((z ^ x)' v u)) = 1.  [para(222(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

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

Low Water (keep, True_semantics): wt=71

given #356 (T,wt=12): 1196 (c2 ^ x) v ((c1 ^ x)' v y) = 1.  [para(57(a,1),222(a,1,2,1,1))].

Low Water (keep, True_semantics): wt=67

given #357 (T,wt=12): 1199 (x ^ c2) v ((x ^ c1)' v y) = 1.  [para(96(a,1),222(a,1,2,1,1))].

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

given #359 (T,wt=12): 1348 x v (y v (z ^ (u ^ x))') = 1.  [para(224(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

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

given #361 (T,wt=12): 1353 (c2 ^ x) v (y ^ (c1 ^ x))' = 1.  [para(57(a,1),224(a,1,2,1,2))].

given #362 (T,wt=12): 1356 (x ^ c2) v (y ^ (x ^ c1))' = 1.  [para(96(a,1),224(a,1,2,1,2))].

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

given #364 (T,wt=12): 1373 (c2 ^ x) v (y v (c1 ^ x)') = 1.  [para(57(a,1),229(a,1,2,2,1))].

given #365 (A,wt=18): 155 x ^ (y v (z ^ (x v (y' v u)))) = x ^ (y v z).  [para(99(a,1),12(a,1,2,2,2,2)),rewrite(32(3),2(2),26(2)),flip(a)].

Low Water (keep, True_semantics): wt=63

Low Water (keep, True_semantics): wt=59

given #366 (T,wt=12): 1377 (x ^ c2) v (y v (x ^ c1)') = 1.  [para(96(a,1),229(a,1,2,2,1))].

given #367 (T,wt=12): 1388 c2 v (x v (y v (c1' v z))) = 1.  [para(3(a,1),249(a,1,2))].

given #368 (T,wt=12): 1399 c2 v (x v (y v (z v c1'))) = 1.  [para(3(a,1),250(a,1,2,2))].

given #369 (T,wt=12): 1561 (c2 ^ (x v (c1 v y))) v c1' = 1.  [para(61(a,1),265(a,1,2,1))].

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

given #371 (T,wt=12): 1564 (c2 ^ (x v (y v c1))) v c1' = 1.  [para(104(a,1),265(a,1,2,1))].

given #372 (T,wt=12): 1577 c1 ^ ((x v (c2 v y))' ^ z) = 0.  [para(17(a,1),286(a,1,2,1,1))].

given #373 (T,wt=12): 1578 c1 ^ (x ^ ((c2 v y)' ^ z)) = 0.  [para(286(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #374 (T,wt=12): 1587 c1 ^ (x v (y v (c2 v z)))' = 0.  [para(3(a,1),289(a,1,2,1))].

given #375 (A,wt=25): 159 x ^ (y v (x' ^ (z ^ (y v u)))) = x ^ (y v (x' ^ (z ^ (x v u)))).  [para(103(a,1),12(a,1,2,2,1)),rewrite(5(5),84(6),5(10))].

Low Water (keep, True_semantics): wt=55

given #376 (T,wt=12): 1590 c1 ^ (x ^ (y v (c2 v z))') = 0.  [para(289(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #377 (T,wt=12): 1599 c1 ^ (x ^ (y ^ (c2 v z)')) = 0.  [para(5(a,1),290(a,1,2))].

given #378 (T,wt=12): 1705 c1 ^ (x v (y v (z v c2)))' = 0.  [para(3(a,1),291(a,1,2,1,2))].

given #379 (T,wt=12): 1706 c1 ^ ((x v (y v c2))' ^ z) = 0.  [para(291(a,1),5(a,1,1)),rewrite(101(2)),flip(a)].

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

given #381 (T,wt=12): 1709 c1 ^ (x ^ (y v (z v c2))') = 0.  [para(291(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #382 (T,wt=12): 1720 c1 ^ (x ^ ((y v c2)' ^ z)) = 0.  [para(292(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #383 (T,wt=12): 1729 c1 ^ (x ^ (y ^ (z v c2)')) = 0.  [para(5(a,1),295(a,1,2))].

given #384 (T,wt=12): 1742 x v (y v ((y v x)' v z)) = 1.  [para(303(a,1),3(a,1,1)),rewrite(98(2),3(5)),flip(a)].

given #385 (A,wt=18): 165 x ^ (y v (z ^ (x v (u v y')))) = x ^ (y v z).  [para(113(a,1),12(a,1,2,2,2,2)),rewrite(32(3),2(2),26(2)),flip(a)].

Low Water (keep, True_semantics): wt=49

given #386 (T,wt=12): 1747 x v (y v (z v (z v x)')) = 1.  [para(303(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #387 (T,wt=12): 1749 x v (y v (y v (x ^ z))') = 1.  [para(303(a,1),24(a,1,2)),rewrite(111(2)),flip(a)].

given #388 (T,wt=12): 1791 c2 v ((x ^ (y ^ c1))' v z) = 1.  [para(5(a,1),319(a,1,2,1,1))].

given #389 (T,wt=12): 1794 c2 v (x v ((y ^ c1)' v z)) = 1.  [para(319(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

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

given #391 (T,wt=12): 1802 c2 v (x ^ (y ^ (z ^ c1)))' = 1.  [para(5(a,1),321(a,1,2,1,2))].

given #392 (T,wt=12): 1805 c2 v (x v (y ^ (z ^ c1))') = 1.  [para(321(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #393 (T,wt=12): 1813 c2 v (x v (y v (z ^ c1)')) = 1.  [para(3(a,1),324(a,1,2))].

given #394 (T,wt=12): 1827 c2 v (x v ((c1 ^ y)' v z)) = 1.  [para(325(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #395 (A,wt=25): 169 x ^ (y v (z ^ (x' ^ (y v u)))) = x ^ (y v (z ^ (x' ^ (x v u)))).  [para(115(a,1),12(a,1,2,2,1)),rewrite(5(5),84(6),5(10))].

Low Water (keep, True_semantics): wt=47

given #396 (T,wt=12): 1828 c2 v ((x ^ (c1 ^ y))' v z) = 1.  [para(19(a,1),325(a,1,2,1,1))].

given #397 (T,wt=12): 1989 c2 v (x v (y v (c1 ^ z)')) = 1.  [para(3(a,1),328(a,1,2))].

given #398 (T,wt=12): 1992 c2 v (x v (y ^ (c1 ^ z))') = 1.  [para(19(a,1),328(a,1,2,2,1))].

given #399 (T,wt=12): 2003 c2 v (x ^ (y ^ (c1 ^ z)))' = 1.  [para(5(a,1),329(a,1,2,1))].

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

Low Water (keep, True_semantics): wt=43

given #401 (T,wt=12): 2014 x ^ (y ^ ((y ^ x)' ^ z)) = 0.  [para(330(a,1),5(a,1,1)),rewrite(101(2),5(5)),flip(a)].

given #402 (T,wt=12): 2019 x ^ (y ^ (z ^ (z ^ x)')) = 0.  [para(330(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #403 (T,wt=12): 2021 x ^ (y ^ (y ^ (x v z))') = 0.  [para(330(a,1),22(a,1,2)),rewrite(114(2)),flip(a)].

given #404 (T,wt=12): 2036 c1 ^ (x ^ ((c2 ^ x)' ^ y)) = 0.  [para(337(a,1),5(a,1,1)),rewrite(101(2),5(7)),flip(a)].

Low Water (keep, True_semantics): wt=41

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

given #406 (T,wt=12): 2040 c1 ^ (x ^ (y ^ (c2 ^ y)')) = 0.  [para(337(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

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

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

given #409 (T,wt=12): 2257 (x ^ (y ^ z))' v (u v y) = 1.  [para(91(a,1),380(a,1,2,2))].

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

Low Water (keep, True_semantics): wt=40

given #411 (T,wt=12): 2258 (x ^ (y ^ z))' v (u v z) = 1.  [para(129(a,1),380(a,1,2,2))].

given #412 (T,wt=12): 2260 (x ^ (y ^ c1))' v (z v c2) = 1.  [para(311(a,1),380(a,1,2,2))].

Low Water (keep, True_semantics): wt=39

given #413 (T,wt=12): 2261 (x ^ (c1 ^ y))' v (z v c2) = 1.  [para(318(a,1),380(a,1,2,2))].

given #414 (T,wt=12): 2264 (x v c1)' v (y v (c2 v x)) = 1.  [para(517(a,1),380(a,1,2,2))].

given #415 (A,wt=35): 174 x ^ (y v ((x ^ z) v (z ^ (((x ^ z) v u) ^ (y v v))))) = x ^ (y v (z ^ (((x ^ z) v u) ^ (x v v)))).  [para(23(a,1),12(a,1,2,2,1)),rewrite(5(6),5(14))].

given #416 (T,wt=12): 2277 (x v (y ^ z)) ^ (x v y)' = 0.  [para(62(a,1),180(a,1,2,1))].

given #417 (T,wt=12): 2279 x v (y v (x v (y ^ z))') = 1.  [para(62(a,1),377(a,1,2)),rewrite(2(5),3(5))].

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

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

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

Low Water (keep, True_semantics): wt=38

given #421 (T,wt=12): 2327 (c2 ^ x)' ^ (y ^ (c1 ^ x)) = 0.  [para(57(a,1),387(a,1,2,2))].

given #422 (T,wt=12): 2330 (x v (y v z))' ^ (u ^ y) = 0.  [para(61(a,1),387(a,1,2,2))].

given #423 (T,wt=12): 2332 (x ^ c2)' ^ (y ^ (x ^ c1)) = 0.  [para(96(a,1),387(a,1,2,2))].

Low Water (keep, True_semantics): wt=37

given #424 (T,wt=12): 2333 (x v (y v z))' ^ (u ^ z) = 0.  [para(104(a,1),387(a,1,2,2))].

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

given #426 (T,wt=12): 2335 (x v (c2 v y))' ^ (z ^ c1) = 0.  [para(269(a,1),387(a,1,2,2))].

given #427 (T,wt=12): 2338 (x v (y v c2))' ^ (z ^ c1) = 0.  [para(281(a,1),387(a,1,2,2))].

given #428 (T,wt=12): 2436 x ^ (c1 ^ ((x ^ c2)' ^ y)) = 0.  [para(459(a,1),5(a,1,1)),rewrite(101(2),5(7)),flip(a)].

given #429 (T,wt=12): 2438 c1 ^ (x ^ (y ^ (y ^ c2)')) = 0.  [para(459(a,1),5(a,2,2)),rewrite(19(7),5(6),114(9))].

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

given #431 (T,wt=12): 2442 x ^ (y ^ (c1 ^ (x ^ c2)')) = 0.  [para(459(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

given #432 (T,wt=12): 2443 x ^ (c1 ^ (c2 ^ (x v y))') = 0.  [para(459(a,1),22(a,1,2)),rewrite(114(2),4(5)),flip(a)].

given #433 (T,wt=12): 2462 (x v c1) ^ ((x v c2)' ^ y) = 0.  [para(521(a,1),5(a,1,1)),rewrite(101(2)),flip(a)].

given #434 (T,wt=12): 2465 (x v c1) ^ (y ^ (x v c2)') = 0.  [para(521(a,1),19(a,1,2)),rewrite(114(2)),flip(a)].

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

Low Water (keep, True_semantics): wt=36

given #436 (T,wt=12): 2478 x v (c2 v ((x v c1)' v y)) = 1.  [para(525(a,1),3(a,1,1)),rewrite(98(2),3(7)),flip(a)].

given #437 (T,wt=12): 2480 c2 v (x v (y v (y v c1)')) = 1.  [para(525(a,1),3(a,2,2)),rewrite(17(7),3(6),111(9))].

given #438 (T,wt=12): 2484 x v (y v (c2 v (x v c1)')) = 1.  [para(525(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #439 (T,wt=12): 2485 x v (c2 v (c1 v (x ^ y))') = 1.  [para(525(a,1),24(a,1,2)),rewrite(111(2),2(5)),flip(a)].

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

given #441 (T,wt=12): 2509 (c1 v (x ^ (c2 ^ y))) ^ c2' = 0.  [para(91(a,1),697(a,1,2,1)),rewrite(2(5))].

given #442 (T,wt=12): 2510 (c1 v (x ^ (y ^ c2))) ^ c2' = 0.  [para(129(a,1),697(a,1,2,1)),rewrite(2(5))].

given #443 (T,wt=12): 2674 c2 v (x v ((x v c1)' v y)) = 1.  [para(699(a,1),3(a,1,1)),rewrite(98(2),3(7)),flip(a)].

given #444 (T,wt=12): 2690 (x ^ c2) v ((c1 ^ x)' v y) = 1.  [para(1550(a,1),3(a,1,1)),rewrite(98(2)),flip(a)].

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

given #446 (T,wt=12): 2693 (x ^ c2) v (y v (c1 ^ x)') = 1.  [para(1550(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #447 (T,wt=12): 2705 (c2 ^ x) v ((x ^ c1)' v y) = 1.  [para(1551(a,1),3(a,1,1)),rewrite(98(2)),flip(a)].

given #448 (T,wt=12): 2708 (c2 ^ x) v (y v (x ^ c1)') = 1.  [para(1551(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #449 (T,wt=12): 2721 (c2 ^ (c1 v x)) v (c1' v y) = 1.  [para(1552(a,1),3(a,1,1)),rewrite(98(2)),flip(a)].

given #450 (A,wt=25): 184 x ^ (y v ((x v z)' ^ (y v u))) = x ^ (y v ((x v z)' ^ (x v u))).  [para(145(a,1),12(a,1,2,2,1)),rewrite(84(6))].

Low Water (keep, True_semantics): wt=35

given #451 (T,wt=12): 2724 (c2 ^ (c1 v x)) v (y v c1') = 1.  [para(1552(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #452 (T,wt=12): 2939 (c2 ^ (x v c1)) v (c1' v y) = 1.  [para(1558(a,1),3(a,1,1)),rewrite(98(2)),flip(a)].

given #453 (T,wt=12): 2942 (c2 ^ (x v c1)) v (y v c1') = 1.  [para(1558(a,1),17(a,1,2)),rewrite(111(2)),flip(a)].

given #454 (T,wt=12): 2956 c1 ^ (x ^ ((x ^ c2)' ^ y)) = 0.  [para(2022(a,1),5(a,1,1)),rewrite(101(2),5(7)),flip(a)].

given #455 (A,wt=21): 189 c1 ^ (x v (c2' ^ (c1 v y))) = c1 ^ (x v (c2' ^ (x v y))).  [para(186(a,1),12(a,1,2,2,1)),rewrite(84(7)),flip(a)].

Low Water (keep, True_semantics): wt=34

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

% Proof 1 at 5.56 (+ 0.06) seconds.
% Length of proof is 47.
% Level of proof is 10.
% Maximum clause weight is 23.
% Given clauses 455.

1 (all x all y (x ^ y = x -> x' v y' = x')) # label(goal).  [goal].
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].
11 x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49).  [assumption].
12 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))).  [copy(11),flip(a)].
13 c1 ^ c2 = c1.  [deny(1)].
14 c1' != c1' v c2'.  [deny(1)].
15 c1' v c2' != c1'.  [copy(14),flip(a)].
19 x ^ (y ^ z) = y ^ (x ^ z).  [para(4(a,1),5(a,1,1)),rewrite(5(2))].
20 x ^ (y v x) = x.  [para(2(a,1),6(a,1,2))].
22 x ^ ((x v y) ^ z) = x ^ z.  [para(6(a,1),5(a,1,1)),flip(a)].
24 x v ((x ^ y) v z) = x v z.  [para(7(a,1),3(a,1,1)),flip(a)].
26 x v (y ^ x) = x.  [para(4(a,1),7(a,1,2))].
30 x v (x' v y) = 1 v y.  [para(8(a,1),3(a,1,1)),flip(a)].
32 x ^ 1 = x.  [para(8(a,1),6(a,1,2))].
33 x ^ (x' ^ y) = 0 ^ y.  [para(9(a,1),5(a,1,1)),flip(a)].
35 x v 0 = x.  [para(9(a,1),7(a,1,2))].
57 c1 ^ (c2 ^ x) = c1 ^ x.  [para(13(a,1),5(a,1,1)),flip(a)].
82 1 ^ x = x.  [para(32(a,1),4(a,1)),flip(a)].
84 0 v x = x.  [para(35(a,1),2(a,1)),flip(a)].
98 1 v x = 1.  [para(82(a,1),6(a,1))].
99 x v (x' v y) = 1.  [back_rewrite(30),rewrite(98(5))].
101 0 ^ x = 0.  [para(84(a,1),6(a,1,2))].
103 x ^ (x' ^ y) = 0.  [back_rewrite(33),rewrite(101(5))].
111 x v 1 = 1.  [para(20(a,1),82(a,1)),flip(a)].
114 x ^ 0 = 0.  [para(101(a,1),4(a,1)),flip(a)].
133 c1 v c2 = c2.  [para(13(a,1),26(a,1,2)),rewrite(2(3))].
145 x ^ (x v y)' = 0.  [para(9(a,1),22(a,1,2)),rewrite(114(2)),flip(a)].
152 c1 ^ (c1' v c2') != 0.  [ur(10,a,99,a,c,15,a(flip))].
186 c1 ^ c2' = 0.  [para(133(a,1),145(a,1,2,1))].
189 c1 ^ (x v (c2' ^ (c1 v y))) = c1 ^ (x v (c2' ^ (x v y))).  [para(186(a,1),12(a,1,2,2,1)),rewrite(84(7)),flip(a)].
203 x v (x ^ y)' = 1.  [para(8(a,1),24(a,1,2)),rewrite(111(2)),flip(a)].
217 x v (y ^ x)' = 1.  [para(4(a,1),203(a,1,2,1))].
260 (c1 ^ x) v (c2 ^ x) = c2 ^ x.  [para(57(a,1),26(a,1,2)),rewrite(2(5))].
265 (c2 ^ x) v (c1 ^ x)' = 1.  [para(57(a,1),217(a,1,2,1))].
1552 (c2 ^ (c1 v x)) v c1' = 1.  [para(6(a,1),265(a,1,2,1))].
2720 c1' v (c2 ^ (c1 v x)) = 1.  [para(1552(a,1),2(a,1)),flip(a)].
4616 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x).  [para(6(a,1),260(a,1,1))].
15889 c1 ^ (c1' v c2') = 0.  [para(2720(a,1),189(a,2,2,2,2)),rewrite(4616(11),19(10),103(10),2(5),84(5),9(4),4(8),82(8)),flip(a)].
15890 $F.  [resolve(15889,a,152,a)].

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

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

Given=455. Generated=152019. Kept=15886. proofs=1.
Usable=453. Sos=14805. Demods=10914. Limbo=85, Disabled=554. Hints=0.
Weight_deleted=58. Literals_deleted=0.
Forward_subsumed=134152. Back_subsumed=91.
Sos_limit_deleted=1923. Sos_displaced=0. Sos_removed=0.
New_demodulators=11234 (6 lex), Back_demodulated=449. Back_unit_deleted=0.
Demod_attempts=2614949. Demod_rewrites=513458.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=275556. Nonunit_bsub_feature_tests=85297.
Megabytes=22.93.
User_CPU=5.56, System_CPU=0.06, Wall_clock=6.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 27250 exit (max_proofs) Fri Apr 13 09:26:06 2007