============================== Prover9 ===============================
Prover9 (32) version November-2006, November 2006.
Process 4013 was started by mccune on cleo.thornwood,
Wed Nov 22 11:27:08 2006
The command was "/home/mccune/bin/prover9 -f lt.in uc.in H27d.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 H27d.in

assign(max_weight,25).

list(weights).
weight(x') = weight(x).
end_of_list.

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).
x ^ (y v z) = (x ^ y) v (x ^ z) # label(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) # label(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 ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49).  [assumption].
(c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity).  [deny(1)].
end_of_list.

formulas(demodulators).
end_of_list.

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

No predicates eliminated.

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

Auto_denials:
  % copying label distributivity to answer in negative clause

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 ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))).  [copy(11),flip(a)].
13 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity) # 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 ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v 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=5): 8 x v x' = 1.  [assumption].

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

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

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

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

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

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

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

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

given #16 (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 #17 (F,wt=5): 61 1 ^ x = x.  [para(30(a,1),4(a,1)),flip(a)].

given #18 (F,wt=3): 76 1' = 0.  [hyper(10,a,33,a,b,61,a)].

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

given #20 (T,wt=3): 79 0' = 1.  [hyper(10,a,64,a,b,30,a)].

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

given #22 (F,wt=5): 77 1 v x = 1.  [para(61(a,1),6(a,1))].

given #23 (F,wt=5): 80 0 ^ x = 0.  [para(64(a,1),6(a,1,2))].

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

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

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

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

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

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

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

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

given #32 (F,wt=7): 82 x ^ (x' ^ y) = 0.  [back_rewrite(31),rewrite(80(5))].

given #33 (F,wt=7): 89 x v (y v x') = 1.  [back_rewrite(72),rewrite(88(5))].

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

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

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

given #37 (F,wt=7): 142 x ^ (x v y)' = 0.  [para(9(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #38 (F,wt=7): 149 x ^ (y v x)' = 0.  [para(2(a,1),142(a,1,2,1))].

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

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

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

given #42 (F,wt=9): 50 x ^ (y ^ x) = y ^ x.  [para(26(a,1),5(a,2,2)),rewrite(4(2))].

given #43 (F,wt=9): 51 1 != x | 0 != x | x' = x.  [para(26(a,1),10(b,1)),rewrite(27(1)),flip(a),flip(b)].

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

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

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

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

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

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

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

given #51 (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 #52 (F,wt=9): 94 x ^ (y v (z v x)) = x.  [para(3(a,1),18(a,1,2))].

given #53 (F,wt=9): 103 x v (y ^ (z ^ x)) = x.  [para(5(a,1),24(a,1,2))].

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

given #55 (T,wt=9): 126 x ^ (y ^ (x' ^ z)) = 0.  [para(82(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

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

given #57 (F,wt=9): 128 x v (y v (z v x')) = 1.  [para(3(a,1),89(a,1,2))].

given #58 (F,wt=9): 132 x ^ (y ^ (z ^ x')) = 0.  [para(5(a,1),92(a,1,2))].

given #59 (T,wt=9): 135 x v (y v (y v x)') = 1.  [para(2(a,1),29(a,1,2,2,1))].

given #60 (T,wt=9): 147 x ^ ((x v y)' ^ z) = 0.  [para(82(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

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

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

given #63 (F,wt=7): 320 x' v (y v x) = 1.  [para(301(a,1),89(a,1,2,2))].

given #64 (T,wt=7): 321 x' ^ (y ^ x) = 0.  [para(301(a,1),92(a,1,2,2))].

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

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

given #67 (F,wt=9): 154 x ^ (y v (x v z))' = 0.  [para(15(a,1),142(a,1,2,1))].

given #68 (F,wt=9): 155 x ^ (y v (z v x))' = 0.  [para(3(a,1),149(a,1,2,1))].

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

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

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

given #72 (F,wt=9): 162 x ^ (y ^ (y ^ x)') = 0.  [para(4(a,1),32(a,1,2,2,1))].

given #73 (F,wt=9): 196 x v ((x ^ y)' v z) = 1.  [para(78(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #74 (T,wt=9): 197 x v (y v (x ^ z)') = 1.  [para(89(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #75 (T,wt=9): 206 x v (y ^ (x ^ z))' = 1.  [para(17(a,1),190(a,1,2,1))].

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

given #77 (F,wt=9): 207 x v ((y ^ x)' v z) = 1.  [para(202(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #78 (F,wt=9): 209 x v (y ^ (z ^ x))' = 1.  [para(5(a,1),202(a,1,2,1))].

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

given #80 (T,wt=9): 322 x' v (y v (x v z)) = 1.  [para(301(a,1),111(a,1,2,2,1))].

given #81 (A,wt=23): 40 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 #82 (F,wt=9): 323 x' ^ (y ^ (x ^ z)) = 0.  [para(301(a,1),126(a,1,2,2,1))].

given #83 (F,wt=9): 324 x' v (y v (z v x)) = 1.  [para(301(a,1),128(a,1,2,2,2))].

given #84 (T,wt=9): 325 x' ^ (y ^ (z ^ x)) = 0.  [para(301(a,1),132(a,1,2,2,2))].

given #85 (T,wt=9): 623 (x ^ y)' v (z v x) = 1.  [para(7(a,1),324(a,1,2,2))].

given #86 (A,wt=23): 41 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 #87 (F,wt=9): 627 (x ^ y)' v (z v y) = 1.  [para(24(a,1),324(a,1,2,2))].

given #88 (F,wt=9): 640 (x v y)' ^ (z ^ x) = 0.  [para(6(a,1),325(a,1,2,2))].

given #89 (T,wt=9): 644 (x v y)' ^ (z ^ y) = 0.  [para(18(a,1),325(a,1,2,2))].

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

given #91 (A,wt=23): 42 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 #92 (F,wt=10): 348 x v y != 1 | (x v y)' = 0.  [para(33(a,1),35(a,1,2)),rewrite(4(6),80(6)),xx(b)].

given #93 (F,wt=10): 470 x ^ y != 0 | (x ^ y)' = 1.  [para(30(a,1),37(b,1,2)),rewrite(2(3),77(3)),xx(a)].

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

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

given #96 (A,wt=23): 43 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 #97 (F,wt=10): 754 x v y != 1 | (y v x)' = 0.  [para(2(a,1),348(a,1))].

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

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

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

given #101 (A,wt=15): 46 x ^ (y v (z ^ (x v y'))) = x ^ (y v z).  [para(8(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)].

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

given #103 (F,wt=11): 95 x ^ ((y v x) ^ z) = x ^ z.  [para(18(a,1),5(a,1,1)),flip(a)].

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

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

given #106 (A,wt=13): 53 1 != x | x ^ y != 0 | x' = x ^ y.  [back_rewrite(39),rewrite(48(4))].

given #107 (F,wt=6): 930 x' != 1 | 0 = x.  [para(321(a,1),53(b,1)),rewrite(301(8),321(9)),flip(a),flip(c),xx(b)].

given #108 (F,wt=10): 931 (x v y)' != 1 | x v y = 0.  [para(640(a,1),53(b,1)),rewrite(301(10),640(12)),flip(a),xx(b)].

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

given #110 (T,wt=10): 934 (x ^ y)' != 1 | x ^ y = 0.  [para(25(a,1),931(a,1,1)),rewrite(25(8))].

given #111 (A,wt=17): 58 x ^ (y v ((y v z) ^ (x v z))) = x ^ (y v z).  [back_rewrite(52),rewrite(54(7))].

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

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

given #114 (T,wt=11): 108 x v (y v ((x v y)' v z)) = 1.  [para(78(a,1),3(a,1)),flip(a)].

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

given #116 (A,wt=13): 59 x v y != 1 | 0 != x | x' = x v y.  [back_rewrite(38),rewrite(54(2))].

given #117 (F,wt=6): 1017 x' != 0 | 1 = x.  [para(320(a,1),59(a,1)),rewrite(301(8),320(9)),flip(b),flip(c),xx(a)].

given #118 (F,wt=10): 1018 (x ^ y)' != 0 | x ^ y = 1.  [para(623(a,1),59(a,1)),rewrite(301(10),623(12)),flip(b),xx(a)].

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

given #120 (T,wt=10): 1021 (x v y)' != 0 | x v y = 1.  [para(19(a,1),1018(a,1,1)),rewrite(19(8))].

given #121 (A,wt=17): 66 x ^ (y v (z ^ (x v y))) = x ^ (y v (z ^ x)).  [para(33(a,1),12(a,1,2,2,2,2)),rewrite(57(5),33(6))].

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

given #123 (F,wt=11): 127 x v (y v (z v (x v y)')) = 1.  [para(89(a,1),3(a,1)),flip(a)].

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

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

given #126 (A,wt=19): 67 x ^ (y v (x' ^ (y v z))) = x ^ (y v (x' ^ (x v z))).  [back_rewrite(47),rewrite(64(5))].

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

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

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

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

given #131 (A,wt=19): 68 x ^ (y v (z ^ (x v (y ^ u)))) = x ^ (y v (z ^ x)).  [back_rewrite(60),rewrite(66(9))].

given #132 (F,wt=11): 160 (x v y) ^ (x v (z v y))' = 0.  [para(15(a,1),149(a,1,2,1))].

given #133 (F,wt=11): 166 x ^ (y ^ (z ^ (x ^ z)')) = 0.  [para(32(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

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

given #135 (T,wt=11): 181 (x v y) ^ (z ^ x) = z ^ x.  [para(50(a,1),20(a,2)),rewrite(180(4))].

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

given #137 (F,wt=11): 187 (x v y) ^ (y v x) = x v y.  [para(56(a,1),19(a,1,2))].

given #138 (F,wt=11): 198 x v (y v ((x ^ z) v y)') = 1.  [para(29(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #139 (T,wt=11): 199 ((x ^ y) v z) ^ (x v z)' = 0.  [para(22(a,1),149(a,1,2,1))].

given #140 (T,wt=11): 200 (x ^ y) v (z v x) = z v x.  [para(56(a,1),22(a,2)),rewrite(185(4))].

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

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

given #143 (F,wt=11): 203 (x ^ y) v (x ^ (y ^ z))' = 1.  [para(5(a,1),190(a,1,2,1))].

given #144 (T,wt=9): 1503 (x ^ y) v (y ^ x)' = 1.  [para(50(a,1),203(a,1,2,1))].

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

given #146 (A,wt=13): 75 x ^ (y v ((x v z) ^ (x v u))) = x.  [back_rewrite(44),rewrite(70(6)),flip(a)].

given #147 (F,wt=11): 214 (x ^ y) v (x ^ (z ^ y))' = 1.  [para(17(a,1),202(a,1,2,1))].

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

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

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

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

given #152 (F,wt=11): 237 x ^ (y v (z v (u v x))) = x.  [para(3(a,1),94(a,1,2,2))].

given #153 (F,wt=11): 249 x v (y ^ (z ^ (u ^ x))) = x.  [para(5(a,1),103(a,1,2,2))].

given #154 (T,wt=11): 258 x v (y v (z v (x' v u))) = 1.  [para(3(a,1),111(a,1,2))].

given #155 (T,wt=11): 261 x v (y v ((x ^ z)' v u)) = 1.  [para(111(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #156 (A,wt=13): 87 x ^ ((x ^ y) v (y ^ z)) = y ^ x.  [back_rewrite(81),rewrite(83(7))].

given #157 (F,wt=11): 263 x ^ (y ^ (z ^ (x' ^ u))) = 0.  [para(5(a,1),126(a,1,2))].

given #158 (F,wt=11): 265 x ^ (y ^ ((x v z)' ^ u)) = 0.  [para(126(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #159 (T,wt=11): 274 (x ^ y) v (y ^ x) = x ^ y.  [para(50(a,1),25(a,1,2))].

given #160 (T,wt=11): 277 x v (y v (z v (u v x'))) = 1.  [para(3(a,1),128(a,1,2,2))].

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

given #162 (F,wt=11): 280 x v (y v (z v (x ^ u)')) = 1.  [para(128(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #163 (F,wt=11): 282 x ^ (y ^ (z ^ (u ^ x'))) = 0.  [para(5(a,1),132(a,1,2,2))].

given #164 (T,wt=11): 284 x ^ (y ^ (z ^ (x v u)')) = 0.  [para(132(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #165 (T,wt=11): 285 x v (y v ((y v x)' v z)) = 1.  [para(135(a,1),3(a,1,1)),rewrite(77(2),3(5)),flip(a)].

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

given #167 (F,wt=11): 290 x v (y v (z v (z v x)')) = 1.  [para(135(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #168 (F,wt=11): 292 x v (y v (y v (x ^ z))') = 1.  [para(135(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].

given #169 (T,wt=11): 296 x ^ ((y v (x v z))' ^ u) = 0.  [para(15(a,1),147(a,1,2,1,1))].

given #170 (T,wt=11): 328 x v ((x v y)' v (z v y)) = 1.  [para(15(a,1),320(a,1,2)),rewrite(15(5))].

given #171 (A,wt=13): 98 x ^ (y v ((z v x) ^ (x v u))) = x.  [para(18(a,1),12(a,1,2,2,1)),rewrite(70(6)),flip(a)].

given #172 (F,wt=11): 334 x ^ ((x ^ y)' ^ (z ^ y)) = 0.  [para(17(a,1),321(a,1,2)),rewrite(17(5))].

given #173 (F,wt=11): 340 x ^ (y ^ (z v (x v u))') = 0.  [para(15(a,1),148(a,1,2,2,1))].

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

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

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

given #177 (F,wt=11): 389 x ^ ((y v (z v x))' ^ u) = 0.  [para(155(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

given #178 (F,wt=11): 393 x ^ (y ^ (z v (u v x))') = 0.  [para(155(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

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

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

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

given #182 (F,wt=11): 434 x ^ (y ^ ((y ^ x)' ^ z)) = 0.  [para(162(a,1),5(a,1,1)),rewrite(80(2),5(5)),flip(a)].

given #183 (F,wt=11): 438 x ^ (y ^ (z ^ (z ^ x)')) = 0.  [para(162(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

given #184 (T,wt=11): 440 x ^ (y ^ (y ^ (x v z))') = 0.  [para(162(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].

given #185 (T,wt=11): 447 x v ((y ^ (x ^ z))' v u) = 1.  [para(17(a,1),196(a,1,2,1,1))].

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

given #187 (F,wt=11): 454 x v (y v (z ^ (x ^ u))') = 1.  [para(17(a,1),197(a,1,2,2,1))].

given #188 (F,wt=11): 460 x v (y ^ (z ^ (x ^ u)))' = 1.  [para(5(a,1),206(a,1,2,1))].

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

given #190 (T,wt=11): 521 x v (y v ((z ^ x)' v u)) = 1.  [para(207(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #191 (A,wt=19): 105 x ^ (y v (z ^ (x v (u ^ y)))) = x ^ (y v (z ^ x)).  [para(24(a,1),12(a,1,2,2,2,2)),rewrite(69(5)),flip(a)].

given #192 (F,wt=11): 529 x v (y ^ (z ^ (u ^ x)))' = 1.  [para(5(a,1),209(a,1,2,1,2))].

given #193 (F,wt=11): 533 x v (y v (z ^ (u ^ x))') = 1.  [para(209(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

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

given #195 (T,wt=11): 553 x' v (y v (z v (x v u))) = 1.  [para(3(a,1),322(a,1,2))].

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

given #197 (F,wt=11): 616 x' ^ (y ^ (z ^ (x ^ u))) = 0.  [para(5(a,1),323(a,1,2))].

given #198 (F,wt=11): 622 x' v (y v (z v (u v x))) = 1.  [para(3(a,1),324(a,1,2,2))].

given #199 (T,wt=11): 629 (x ^ (y ^ z))' v (u v y) = 1.  [para(84(a,1),324(a,1,2,2))].

given #200 (T,wt=11): 631 (x ^ (y ^ z))' v (u v z) = 1.  [para(103(a,1),324(a,1,2,2))].

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

given #202 (F,wt=11): 639 x' ^ (y ^ (z ^ (u ^ x))) = 0.  [para(5(a,1),325(a,1,2,2))].

given #203 (F,wt=11): 648 (x v (y v z))' ^ (u ^ y) = 0.  [para(70(a,1),325(a,1,2,2))].

given #204 (T,wt=11): 649 (x v (y v z))' ^ (u ^ z) = 0.  [para(94(a,1),325(a,1,2,2))].

given #205 (T,wt=11): 655 (x ^ y)' v (z v (x v u)) = 1.  [para(623(a,1),3(a,1,1)),rewrite(77(2),3(5)),flip(a)].

given #206 (A,wt=17): 110 x ^ (y v (z ^ (x v (y' v u)))) = x ^ (y v z).  [para(78(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)].

given #207 (F,wt=11): 656 (x ^ y)' v (z v (u v x)) = 1.  [para(3(a,1),623(a,1,2))].

given #208 (F,wt=11): 689 (x ^ y)' v (z v (y v u)) = 1.  [para(627(a,1),3(a,1,1)),rewrite(77(2),3(5)),flip(a)].

given #209 (T,wt=11): 690 (x ^ y)' v (z v (u v y)) = 1.  [para(3(a,1),627(a,1,2))].

given #210 (T,wt=11): 704 (x v y)' ^ (z ^ (x ^ u)) = 0.  [para(640(a,1),5(a,1,1)),rewrite(80(2),5(5)),flip(a)].

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

given #212 (F,wt=11): 705 (x v y)' ^ (z ^ (u ^ x)) = 0.  [para(5(a,1),640(a,1,2))].

given #213 (F,wt=11): 714 (x v y)' ^ (z ^ (y ^ u)) = 0.  [para(644(a,1),5(a,1,1)),rewrite(80(2),5(5)),flip(a)].

given #214 (T,wt=11): 715 (x v y)' ^ (z ^ (u ^ y)) = 0.  [para(5(a,1),644(a,1,2))].

given #215 (T,wt=11): 799 (x v (y ^ z)) ^ (x v y)' = 0.  [para(71(a,1),149(a,1,2,1))].

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

given #217 (F,wt=11): 802 x v (y v (x v (y ^ z))') = 1.  [para(71(a,1),320(a,1,2)),rewrite(2(5),3(5))].

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

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

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

given #221 (A,wt=19): 114 (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 #222 (F,wt=11): 855 (x v y) ^ (z ^ y) = z ^ y.  [para(50(a,1),95(a,2)),rewrite(180(4))].

given #223 (F,wt=11): 857 ((x v y) ^ z) v (y ^ z)' = 1.  [para(95(a,1),202(a,1,2,1))].

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

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

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

given #227 (F,wt=11): 883 x ^ (y ^ (x ^ (z v y))') = 0.  [para(100(a,1),321(a,1,2)),rewrite(4(5),5(5))].

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

given #229 (T,wt=11): 905 ((x ^ y) v z) ^ (y v z)' = 0.  [para(101(a,1),149(a,1,2,1))].

given #230 (T,wt=11): 907 (x ^ y) v (z v y) = z v y.  [para(56(a,1),101(a,2)),rewrite(185(4))].

given #231 (A,wt=19): 117 x ^ (y v ((y v z) ^ (x v (z v u)))) = x ^ (y v z).  [para(19(a,1),12(a,1,2,2,2)),rewrite(2(4),24(4),54(2)),flip(a)].

given #232 (F,wt=11): 911 x v (y v (y v (z ^ x))') = 1.  [para(135(a,1),101(a,1,2)),rewrite(88(2)),flip(a)].

given #233 (F,wt=11): 977 (x v (y ^ z)) ^ (x v z)' = 0.  [para(106(a,1),149(a,1,2,1))].

given #234 (T,wt=11): 981 x v (y v (x v (z ^ y))') = 1.  [para(106(a,1),320(a,1,2)),rewrite(2(5),3(5))].

given #235 (T,wt=11): 1078 x v (y v (z v (y v x)')) = 1.  [para(2(a,1),127(a,1,2,2,2,1))].

given #236 (A,wt=19): 118 (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 #237 (F,wt=11): 1090 x ^ (y ^ (z ^ (y ^ x)')) = 0.  [para(4(a,1),131(a,1,2,2,2,1))].

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

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

given #240 (T,wt=11): 1202 (x v y) ^ ((y v x)' ^ z) = 0.  [para(1197(a,1),5(a,1,1)),rewrite(80(2)),flip(a)].

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

given #242 (F,wt=11): 1204 (x v y) ^ (z ^ (y v x)') = 0.  [para(1197(a,1),17(a,1,2)),rewrite(91(2)),flip(a)].

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

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

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

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

given #247 (F,wt=11): 1284 x ^ (y ^ ((y v z) ^ x)') = 0.  [para(168(a,1),17(a,1)),flip(a)].

given #248 (F,wt=11): 1286 x ^ ((x v y) ^ (x v z))' = 0.  [para(168(a,1),20(a,1)),flip(a)].

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

given #250 (T,wt=11): 1352 x v (y v (z ^ (y v x))') = 1.  [para(187(a,1),209(a,1,2,1,2)),rewrite(3(5))].

given #251 (A,wt=21): 122 x v (y v z) != 1 | x v y != 0 | (x v y)' = x v (y v z).  [back_rewrite(116),rewrite(121(4))].

given #252 (F,wt=11): 1353 (x v y)' ^ (z ^ (y v x)) = 0.  [para(187(a,1),325(a,1,2,2))].

given #253 (F,wt=11): 1354 (x v y)' v (z v (y v x)) = 1.  [para(187(a,1),627(a,1,1,1))].

given #254 (T,wt=11): 1362 x v (y v ((y ^ z) v x)') = 1.  [para(198(a,1),15(a,1)),flip(a)].

given #255 (T,wt=11): 1365 x v ((x ^ y) v (x ^ z))' = 1.  [para(198(a,1),22(a,1)),flip(a)].

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

given #257 (F,wt=11): 1370 x v ((x ^ y) v (z ^ x))' = 1.  [para(198(a,1),101(a,1)),flip(a)].

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

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

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

given #261 (A,wt=23): 125 x ^ (y v (x' ^ (z ^ (y v u)))) = x ^ (y v (x' ^ (z ^ (x v u)))).  [para(82(a,1),12(a,1,2,2,1)),rewrite(5(5),64(6),5(10))].

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

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

given #264 (T,wt=11): 1483 x v (y v ((y v x) ^ z)') = 1.  [para(2(a,1),201(a,1,2,2,1,1))].

given #265 (T,wt=11): 1497 (x ^ y) v (y ^ (x ^ z))' = 1.  [para(4(a,1),203(a,1,1))].

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

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

given #268 (F,wt=11): 1510 ((x v y) ^ z) v (z ^ x)' = 1.  [para(181(a,1),203(a,1,2,1))].

given #269 (T,wt=11): 1513 (x ^ y) v ((y ^ x)' v z) = 1.  [para(1503(a,1),3(a,1,1)),rewrite(77(2)),flip(a)].

given #270 (T,wt=11): 1517 (x ^ y) v (z v (y ^ x)') = 1.  [para(1503(a,1),15(a,1,2)),rewrite(88(2)),flip(a)].

given #271 (A,wt=17): 130 x ^ (y v (z ^ (x v (u v y')))) = x ^ (y v z).  [para(89(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)].

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

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

given #274 (T,wt=11): 1602 (x ^ (y v z)) v (y ^ x)' = 1.  [para(4(a,1),215(a,1,1))].

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

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

given #277 (F,wt=11): 1610 ((x v y) ^ (z v x)) v x' = 1.  [para(18(a,1),215(a,1,2,1))].

given #278 (F,wt=11): 1847 (x ^ y)' v (z v (y ^ x)) = 1.  [para(274(a,1),324(a,1,2,2))].

given #279 (T,wt=11): 1848 (x ^ y)' ^ (z ^ (y ^ x)) = 0.  [para(274(a,1),644(a,1,1,1))].

given #280 (T,wt=11): 1961 x v ((y v x)' v (z v y)) = 1.  [para(29(a,1),290(a,1,2,2,2,1)),rewrite(76(5),33(5),3(5))].

given #281 (A,wt=23): 134 x ^ (y v (z ^ (x' ^ (y v u)))) = x ^ (y v (z ^ (x' ^ (x v u)))).  [para(92(a,1),12(a,1,2,2,1)),rewrite(5(5),64(6),5(10))].

given #282 (F,wt=11): 1968 x v (y v ((z ^ y) v x)') = 1.  [para(101(a,1),290(a,1,2))].

given #283 (F,wt=11): 1990 x v ((y ^ x) v (x ^ z))' = 1.  [para(292(a,1),101(a,1)),flip(a)].

given #284 (T,wt=11): 2086 x ^ ((y ^ x)' ^ (z ^ y)) = 0.  [para(4(a,1),334(a,1,2,1,1))].

given #285 (T,wt=11): 2297 x ^ (y ^ ((z v y) ^ x)') = 0.  [para(95(a,1),438(a,1,2))].

given #286 (A,wt=13): 136 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 #287 (F,wt=11): 2322 x ^ ((y v x) ^ (x v z))' = 0.  [para(440(a,1),95(a,1)),flip(a)].

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

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

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

given #291 (A,wt=16): 137 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 #292 (F,wt=11): 3248 ((x v y) ^ z) v (z ^ y)' = 1.  [para(855(a,1),203(a,1,2,1))].

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

given #294 (T,wt=11): 3264 (x ^ (y v z)) v (z ^ x)' = 1.  [para(4(a,1),857(a,1,1))].

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

given #296 (A,wt=19): 138 x ^ (y v (z ^ (x v (u v (y v u)')))) = x ^ (y v z).  [para(29(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)].

given #297 (F,wt=11): 3272 ((x v y) ^ (z v y)) v y' = 1.  [para(18(a,1),857(a,1,2,1))].

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

given #299 (T,wt=11): 3484 x v ((y ^ x) v (z ^ x))' = 1.  [para(903(a,1),101(a,1)),flip(a)].

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

given #301 (A,wt=13): 140 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 #302 (F,wt=11): 3507 ((x ^ y) v z) ^ (z v y)' = 0.  [para(2(a,1),905(a,1,2,1))].

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

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

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

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

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

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

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

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

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

given #312 (F,wt=11): 4344 x' ^ ((x ^ y) v (z ^ x)) = 0.  [para(24(a,1),1380(a,1,1,1))].

given #313 (F,wt=11): 4544 x ^ ((x' ^ y) v (x' ^ z)) = 0.  [para(301(a,1),1382(a,1,2)),rewrite(4(6))].

given #314 (T,wt=11): 4566 x ^ ((x' ^ y) v (z ^ x')) = 0.  [para(301(a,1),1387(a,1,2)),rewrite(4(6))].

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

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

given #317 (F,wt=11): 4825 (x ^ y)' v (y ^ (x v z)) = 1.  [para(4(a,1),1600(a,1,2))].

given #318 (F,wt=11): 4827 x' v ((x v y) ^ (x v z)) = 1.  [para(6(a,1),1600(a,1,1,1))].

given #319 (T,wt=11): 4831 x' v ((x v y) ^ (z v x)) = 1.  [para(18(a,1),1600(a,1,1,1))].

given #320 (T,wt=11): 4932 x v ((x' v y) ^ (x' v z)) = 1.  [para(301(a,1),1604(a,1,2)),rewrite(2(6))].

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

given #322 (F,wt=11): 4958 x v ((x' v y) ^ (z v x')) = 1.  [para(301(a,1),1610(a,1,2)),rewrite(2(6))].

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

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

given #325 (T,wt=11): 5513 x' v ((y v x) ^ (x v z)) = 1.  [para(6(a,1),3262(a,1,1,1))].

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

given #327 (F,wt=11): 5517 x' v ((y v x) ^ (z v x)) = 1.  [para(18(a,1),3262(a,1,1,1))].

given #328 (F,wt=11): 5624 x v ((y v x') ^ (x' v z)) = 1.  [para(301(a,1),3266(a,1,2)),rewrite(2(6))].

given #329 (T,wt=11): 5714 x v ((y v x') ^ (z v x')) = 1.  [para(301(a,1),3272(a,1,2)),rewrite(2(6))].

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

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

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

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

given #334 (T,wt=11): 5931 x' ^ ((y ^ x) v (z ^ x)) = 0.  [para(24(a,1),3509(a,1,1,1))].

given #335 (T,wt=11): 5965 x ^ ((y ^ x') v (x' ^ z)) = 0.  [para(301(a,1),3511(a,1,2)),rewrite(4(6))].

given #336 (A,wt=23): 153 x ^ (y v ((x v z)' ^ (y v u))) = x ^ (y v ((x v z)' ^ (x v u))).  [para(142(a,1),12(a,1,2,2,1)),rewrite(64(6))].

given #337 (F,wt=11): 5986 x ^ ((y ^ x') v (z ^ x')) = 0.  [para(301(a,1),3516(a,1,2)),rewrite(4(6))].

given #338 (F,wt=12): 158 x v (y v x)' != 1 | (y v x)' = x'.  [para(149(a,1),10(b,1)),flip(c),xx(b)].

given #339 (T,wt=12): 204 x ^ (x ^ y)' != 0 | (x ^ y)' = x'.  [para(190(a,1),10(a,1)),flip(c),xx(a)].

given #340 (T,wt=12): 210 x ^ (y ^ x)' != 0 | (y ^ x)' = x'.  [para(202(a,1),10(a,1)),flip(c),xx(a)].

given #341 (A,wt=23): 159 x ^ (y v ((z v x)' ^ (y v u))) = x ^ (y v ((z v x)' ^ (x v u))).  [para(149(a,1),12(a,1,2,2,1)),rewrite(64(6))].

given #342 (F,wt=12): 305 x ^ (x' v y) != 0 | (x' v y)' = x.  [para(78(a,1),34(a,1)),rewrite(4(6)),xx(a)].

given #343 (F,wt=12): 306 x ^ (y v x') != 0 | (y v x')' = x.  [para(89(a,1),34(a,1)),rewrite(4(6)),xx(a)].

given #344 (T,wt=12): 311 x ^ (x ^ y)' != 0 | x ^ y = x.  [para(190(a,1),34(a,1)),rewrite(4(6),301(11)),xx(a)].

given #345 (T,wt=12): 312 x ^ (y ^ x)' != 0 | y ^ x = x.  [para(202(a,1),34(a,1)),rewrite(4(6),301(11)),xx(a)].

given #346 (A,wt=13): 163 x ^ (y ^ (z ^ (x ^ (y ^ z))')) = 0.  [para(32(a,1),5(a,1)),rewrite(5(3)),flip(a)].

given #347 (F,wt=12): 326 x' ^ (y v x) != 0 | y v x = x.  [para(320(a,1),10(a,1)),rewrite(301(10)),flip(c),xx(a)].

given #348 (F,wt=12): 330 (x v y) ^ y' != 0 | (x v y)' = y'.  [para(320(a,1),34(a,1)),xx(a)].

given #349 (T,wt=12): 331 x' v (y ^ x) != 1 | y ^ x = x.  [para(321(a,1),10(b,1)),rewrite(301(10)),flip(c),xx(b)].

given #350 (T,wt=12): 336 (x ^ y) v y' != 1 | x ^ y = y.  [para(321(a,1),34(b,1)),rewrite(301(10)),flip(c),xx(b)].

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

given #352 (F,wt=12): 358 (x v y) ^ x' != 0 | (x v y)' = x'.  [para(89(a,1),35(a,1)),xx(a)].

given #353 (F,wt=12): 415 x v (x' ^ y) != 1 | (x' ^ y)' = x.  [para(82(a,1),36(b,1)),rewrite(2(3)),xx(b)].

given #354 (T,wt=12): 416 x v (y ^ x') != 1 | (y ^ x')' = x.  [para(92(a,1),36(b,1)),rewrite(2(3)),xx(b)].

given #355 (T,wt=12): 418 x v (x v y)' != 1 | x v y = x.  [para(142(a,1),36(b,1)),rewrite(2(3),301(11)),xx(b)].

given #356 (A,wt=25): 165 x ^ ((y v ((x ^ z) v (z ^ (y v u)))) ^ (x ^ (y v (z ^ (x v u))))') = 0.  [para(12(a,1),32(a,1,2,2,1))].

given #357 (F,wt=12): 419 x v (y v x)' != 1 | y v x = x.  [para(149(a,1),36(b,1)),rewrite(2(3),301(11)),xx(b)].

given #358 (F,wt=12): 427 (x v y) ^ y' != 0 | x v y = y.  [para(320(a,1),36(a,1)),rewrite(301(10)),flip(c),xx(a)].

given #359 (T,wt=12): 428 (x ^ y) v y' != 1 | (x ^ y)' = y'.  [para(321(a,1),36(b,1)),xx(b)].

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

given #361 (A,wt=13): 167 x ^ (y ^ (z ^ (y ^ (x ^ z))')) = 0.  [para(17(a,1),32(a,1,2,2,1)),rewrite(5(5))].

given #362 (F,wt=12): 1317 x' ^ (x v y) != 0 | x v y = x.  [para(78(a,1),73(a,1)),rewrite(301(10)),flip(c),xx(a)].

given #363 (F,wt=12): 1668 x' v (x ^ y) != 1 | x ^ y = x.  [para(82(a,1),86(b,1)),rewrite(301(10)),flip(c),xx(b)].

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

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

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

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

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

given #369 (T,wt=12): 6869 x v (y v x)' != 1 | (x v y)' = x'.  [para(2(a,1),152(a,1,2,1))].

given #370 (T,wt=12): 7093 x v (x v y)' != 1 | (y v x)' = x'.  [para(2(a,1),158(a,1,2,1))].

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

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

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

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

given #375 (T,wt=12): 7229 x' ^ (x v y) != 0 | (x v y)' = x'.  [para(301(a,1),305(a,1,2,1)),rewrite(301(7))].

given #376 (A,wt=19): 172 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 #377 (F,wt=12): 7245 x ^ (x' v y) != 0 | (y v x')' = x.  [para(2(a,1),306(a,1,2))].

given #378 (F,wt=12): 7247 x' ^ (y v x) != 0 | (y v x)' = x'.  [para(301(a,1),306(a,1,2,2)),rewrite(301(7))].

given #379 (T,wt=12): 7248 x ^ (y ^ x)' != 0 | x ^ y = x.  [para(4(a,1),311(a,1,2,1))].

given #380 (T,wt=12): 7253 x ^ (x ^ y)' != 0 | y ^ x = x.  [para(4(a,1),312(a,1,2,1))].

given #381 (A,wt=25): 173 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 #382 (F,wt=12): 7255 (x v y) ^ x' != 0 | x v y = x.  [para(6(a,1),312(a,1,2,1)),rewrite(6(7)),flip(b)].

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

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

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

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

given #387 (F,wt=12): 7304 (x ^ y) v x' != 1 | y ^ x = x.  [para(4(a,1),336(a,1,1))].

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

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

given #390 (T,wt=12): 7313 x' v (x ^ y) != 1 | (x ^ y)' = x'.  [para(301(a,1),415(a,1,2,1)),rewrite(301(7))].

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

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

given #393 (F,wt=12): 7318 x' v (y ^ x) != 1 | (y ^ x)' = x'.  [para(301(a,1),416(a,1,2,2)),rewrite(301(7))].

given #394 (T,wt=12): 7319 x v (y v x)' != 1 | x v y = x.  [para(2(a,1),418(a,1,2,1))].

given #395 (T,wt=12): 7369 x v (x v y)' != 1 | y v x = x.  [para(2(a,1),419(a,1,2,1))].

given #396 (A,wt=19): 176 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 #397 (F,wt=12): 7371 (x ^ y) v x' != 1 | x ^ y = x.  [para(7(a,1),419(a,1,2,1)),rewrite(7(7)),flip(b)].

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

given #399 (T,wt=12): 7379 (x ^ y) v x' != 1 | (y ^ x)' = x'.  [para(4(a,1),428(a,1,1))].

given #400 (T,wt=12): 7387 (x ^ y) v y' != 1 | (y ^ x)' = y'.  [para(4(a,1),482(a,1,1))].

given #401 (A,wt=19): 177 (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 #402 (F,wt=12): 7414 x' ^ (y v x) != 0 | x v y = x.  [para(2(a,1),1317(a,1,2))].

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

given #404 (T,wt=12): 7557 x' ^ (y v x) != 0 | (x v y)' = x'.  [para(301(a,1),7225(a,1,2,2)),rewrite(301(7))].

given #405 (T,wt=12): 7649 x' ^ (x v y) != 0 | (y v x)' = x'.  [para(301(a,1),7245(a,1,2,1)),rewrite(301(7))].

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

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

given #408 (F,wt=12): 7809 x' v (y ^ x) != 1 | (x ^ y)' = x'.  [para(301(a,1),7311(a,1,2,2)),rewrite(301(7))].

given #409 (T,wt=12): 7944 x' v (x ^ y) != 1 | (y ^ x)' = x'.  [para(301(a,1),7317(a,1,2,1)),rewrite(301(7))].

given #410 (T,wt=12): 8042 (x ^ y) v y' != 1 | y ^ x = y.  [para(4(a,1),7371(a,1,1))].

given #411 (A,wt=13): 180 x ^ (y ^ (z ^ x)) = y ^ (z ^ x).  [para(5(a,1),50(a,1,2)),rewrite(5(5))].

given #412 (F,wt=13): 182 x v (y v (x v z)) = y v (x v z).  [para(54(a,1),3(a,2,2)),rewrite(15(3),3(2))].

given #413 (F,wt=13): 185 x v (y v (z v x)) = y v (z v x).  [para(3(a,1),56(a,1,2)),rewrite(3(5))].

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

given #415 (T,wt=13): 216 (x ^ ((y ^ x) v z)) v (y ^ x)' = 1.  [para(21(a,1),202(a,1,2,1))].

given #416 (A,wt=21): 183 x ^ (y v (z ^ (x v (y v u)))) = x ^ (y v (z ^ (x v u))).  [para(54(a,1),12(a,1,2,2,2,2)),rewrite(12(6)),flip(a)].

given #417 (F,wt=13): 221 x ^ (y ^ (z v (x v u))) = y ^ x.  [para(70(a,1),17(a,1,2)),flip(a)].

given #418 (F,wt=13): 227 x v (y v (z ^ (x ^ u))) = y v x.  [para(84(a,1),15(a,1,2)),flip(a)].

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

given #420 (T,wt=13): 235 (x v ((y v x) ^ z)) ^ (y v x)' = 0.  [para(23(a,1),149(a,1,2,1))].

given #421 (A,wt=21): 186 x ^ (y v (z ^ (x v (u v y)))) = x ^ (y v (z ^ (x v u))).  [para(56(a,1),12(a,1,2,2,2,2)),rewrite(40(6)),flip(a)].

given #422 (F,wt=13): 238 x ^ ((y v (z v x)) ^ u) = x ^ u.  [para(94(a,1),5(a,1,1)),flip(a)].

given #423 (F,wt=13): 244 x ^ (y ^ (z v (u v x))) = y ^ x.  [para(94(a,1),17(a,1,2)),flip(a)].

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

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

given #426 (A,wt=17): 188 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 #427 (F,wt=13): 257 x v (y v (z v ((x v y)' v u))) = 1.  [para(111(a,1),3(a,1)),flip(a)].

given #428 (F,wt=13): 262 x ^ (y ^ (z ^ ((x ^ y)' ^ u))) = 0.  [para(126(a,1),5(a,1)),flip(a)].

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

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

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

given #432 (F,wt=13): 276 x v (y v (z v (u v (x v y)'))) = 1.  [para(128(a,1),3(a,1)),flip(a)].

given #433 (F,wt=13): 281 x ^ (y ^ (z ^ (u ^ (x ^ y)'))) = 0.  [para(132(a,1),5(a,1)),flip(a)].

given #434 (T,wt=13): 286 x v (y v (z v (z v (x v y))')) = 1.  [para(135(a,1),3(a,1)),flip(a)].

given #435 (T,wt=13): 287 x v (y v (z v (y v (z v x))')) = 1.  [para(3(a,1),135(a,1,2,2,1)),rewrite(3(5))].

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

given #437 (F,wt=13): 291 x v (y v (z v (x v (z v y))')) = 1.  [para(15(a,1),135(a,1,2,2,1)),rewrite(3(6))].

given #438 (F,wt=13): 293 (x v y) ^ ((x v (y v z))' ^ u) = 0.  [para(3(a,1),147(a,1,2,1,1))].

given #439 (T,wt=13): 294 x ^ (y ^ (((x ^ y) v z)' ^ u)) = 0.  [para(147(a,1),5(a,1)),flip(a)].

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

given #441 (A,wt=23): 192 x ^ (y v (z ^ (x v ((y ^ u) v v)))) = x ^ (y v (z ^ (x v v))).  [para(22(a,1),12(a,1,2,2,2,2)),rewrite(12(6)),flip(a)].

given #442 (F,wt=13): 300 1 != x | x ^ y != 0 | (x ^ y)' = x.  [para(7(a,1),34(a,1)),rewrite(4(4),48(4)),flip(a)].

given #443 (F,wt=13): 304 1 != x | y ^ x != 0 | (y ^ x)' = x.  [para(24(a,1),34(a,1)),rewrite(4(4),50(4)),flip(a)].

given #444 (T,wt=13): 308 x v y != 1 | 0 != x | (x v y)' = x.  [para(54(a,1),34(a,1)),rewrite(4(5),6(5)),flip(b)].

given #445 (T,wt=13): 309 x v y != 1 | 0 != y | (x v y)' = y.  [para(56(a,1),34(a,1)),rewrite(4(5),18(5)),flip(b)].

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

given #447 (F,wt=13): 329 x v (y v (y v ((x v y) ^ z))') = 1.  [para(23(a,1),320(a,1,2)),rewrite(2(6),3(6))].

given #448 (F,wt=13): 335 x ^ (y ^ (y ^ ((x ^ y) v z))') = 0.  [para(21(a,1),321(a,1,2)),rewrite(4(6),5(6))].

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

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

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

given #452 (F,wt=13): 368 x v y != 1 | 0 != y | (y v x)' = y.  [para(56(a,1),35(a,1)),rewrite(4(5),6(5)),flip(b)].

given #453 (F,wt=13): 383 (x v y) ^ (z v (x v (y v u)))' = 0.  [para(3(a,1),154(a,1,2,1,2))].

given #454 (T,wt=13): 385 x ^ (y ^ (z v ((x ^ y) v u))') = 0.  [para(154(a,1),5(a,1)),flip(a)].

given #455 (T,wt=13): 390 x ^ (y ^ (z v (u v (x ^ y)))') = 0.  [para(155(a,1),5(a,1)),flip(a)].

given #456 (A,wt=17): 205 x ^ (y v (z ^ (x v (y ^ u)'))) = x ^ (y v z).  [para(190(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)].

given #457 (F,wt=13): 392 (x v y) ^ (z v (x v (u v y)))' = 0.  [para(15(a,1),155(a,1,2,1,2))].

given #458 (F,wt=13): 394 ((x ^ y) v z) ^ (u v (x v z))' = 0.  [para(22(a,1),155(a,1,2,1,2))].

given #459 (T,wt=13): 396 x ^ (y ^ (z ^ (u v (x ^ y))')) = 0.  [para(25(a,1),155(a,1,2,1,2)),rewrite(5(6),5(5))].

given #460 (T,wt=13): 398 x ^ (y ^ ((z v (x ^ y))' ^ u)) = 0.  [para(156(a,1),5(a,1)),flip(a)].

given #461 (A,wt=17): 211 x ^ (y v (z ^ (x v (u ^ y)'))) = x ^ (y v z).  [para(202(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)].

given #462 (F,wt=13): 400 (x v y) ^ ((x v (z v y))' ^ u) = 0.  [para(15(a,1),156(a,1,2,1,1))].

given #463 (F,wt=13): 402 ((x ^ y) v z) ^ ((x v z)' ^ u) = 0.  [para(22(a,1),156(a,1,2,1,1))].

given #464 (T,wt=13): 407 (x v y) ^ (z ^ (x v (u v y))') = 0.  [para(15(a,1),161(a,1,2,2,1))].

given #465 (T,wt=13): 408 ((x ^ y) v z) ^ (u ^ (x v z)') = 0.  [para(22(a,1),161(a,1,2,2,1))].

given #466 (A,wt=23): 212 x v ((y ^ z) v ((z ^ (x v u)) v (y ^ (x v (z ^ (y v u))))')) = 1.  [para(12(a,1),202(a,1,2,1)),rewrite(3(11),3(10))].

given #467 (F,wt=13): 435 x ^ (y ^ (z ^ (z ^ (x ^ y))')) = 0.  [para(162(a,1),5(a,1)),flip(a)].

given #468 (F,wt=13): 436 x ^ (y ^ (z ^ (y ^ (z ^ x))')) = 0.  [para(5(a,1),162(a,1,2,2,1)),rewrite(5(5))].

given #469 (T,wt=13): 439 x ^ (y ^ (z ^ (x ^ (z ^ y))')) = 0.  [para(17(a,1),162(a,1,2,2,1)),rewrite(5(6))].

given #470 (T,wt=13): 443 x v (y v (((x v y) ^ z)' v u)) = 1.  [para(196(a,1),3(a,1)),flip(a)].

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

given #472 (F,wt=13): 444 (x ^ y) v ((x ^ (y ^ z))' v u) = 1.  [para(5(a,1),196(a,1,2,1,1))].

given #473 (F,wt=13): 450 x v (y v (z v ((x v y) ^ u)')) = 1.  [para(197(a,1),3(a,1)),flip(a)].

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

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

given #476 (A,wt=17): 219 x v (y v z) != 1 | 0 != y | y' = x v (y v z).  [para(70(a,1),10(b,1)),rewrite(182(3)),flip(b)].

given #477 (F,wt=13): 459 (x ^ y) v (z ^ (x ^ (y ^ u)))' = 1.  [para(5(a,1),206(a,1,2,1,2))].

given #478 (F,wt=13): 490 1 != x | y ^ x != 0 | (x ^ y)' = x.  [para(50(a,1),37(b,1)),rewrite(2(2),7(2)),flip(a)].

given #479 (T,wt=13): 516 x v (y v ((z ^ (x v y))' v u)) = 1.  [para(207(a,1),3(a,1)),flip(a)].

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

given #481 (A,wt=15): 220 x ^ (y v ((z v (x v u)) ^ (x v v))) = x.  [para(70(a,1),12(a,1,2,2,1)),rewrite(70(7)),flip(a)].

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

given #482 (F,wt=13): 523 ((x v y) ^ z) v ((x ^ z)' v u) = 1.  [para(20(a,1),207(a,1,2,1,1))].

given #483 (F,wt=13): 528 x v (y v (z ^ (u ^ (x v y)))') = 1.  [para(209(a,1),3(a,1)),flip(a)].

given #484 (T,wt=13): 534 (x ^ y) v (z ^ (x ^ (u ^ y)))' = 1.  [para(17(a,1),209(a,1,2,1,2))].

given #485 (T,wt=13): 535 x v (y v (z v (u ^ (x v y))')) = 1.  [para(19(a,1),209(a,1,2,1,2)),rewrite(3(6),3(5))].

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

given #487 (F,wt=13): 536 ((x v y) ^ z) v (u ^ (x ^ z))' = 1.  [para(20(a,1),209(a,1,2,1,2))].

given #488 (F,wt=13): 545 (x ^ y) v (z v (x ^ (u ^ y))') = 1.  [para(17(a,1),213(a,1,2,2,1))].

given #489 (T,wt=13): 546 ((x v y) ^ z) v (u v (x ^ z)') = 1.  [para(20(a,1),213(a,1,2,2,1))].

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

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

given #492 (F,wt=13): 615 (x ^ y)' ^ (z ^ (x ^ (y ^ u))) = 0.  [para(5(a,1),323(a,1,2,2))].

given #493 (F,wt=13): 626 (x v y)' v (z v (x v (u v y))) = 1.  [para(15(a,1),324(a,1,2,2))].

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

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

given #496 (A,wt=17): 225 1 != x | y ^ (x ^ z) != 0 | x' = y ^ (x ^ z).  [para(84(a,1),10(a,1)),rewrite(170(5)),flip(a)].

given #497 (F,wt=13): 643 (x ^ y)' ^ (z ^ (x ^ (u ^ y))) = 0.  [para(17(a,1),325(a,1,2,2))].

given #498 (F,wt=13): 645 (x v (y v z))' ^ (u ^ (x v y)) = 0.  [para(19(a,1),325(a,1,2,2))].

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

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

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

given #501 (A,wt=19): 229 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 #502 (F,wt=13): 660 x v (y v (((x ^ z) v y) ^ u)') = 1.  [para(22(a,1),623(a,1,2)),rewrite(2(6),3(6))].

given #503 (F,wt=13): 668 x ^ ((y ^ z) v (x ^ y)) = y ^ x.  [para(64(a,1),41(a,1,2,2,1,2)),rewrite(64(5),64(8),83(7))].

given #504 (T,wt=13): 694 x v ((y ^ (x v z))' v (u v z)) = 1.  [para(15(a,1),627(a,1,2)),rewrite(15(6))].

given #505 (T,wt=13): 695 (x ^ (y ^ z))' v (u v (x ^ z)) = 1.  [para(17(a,1),627(a,1,1,1))].

given #506 (A,wt=25): 230 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 #507 (F,wt=13): 696 (x ^ y)' v (z v ((x v u) ^ y)) = 1.  [para(20(a,1),627(a,1,1,1))].

given #508 (F,wt=13): 698 x v (y v (z ^ ((x ^ u) v y))') = 1.  [para(22(a,1),627(a,1,2)),rewrite(2(6),3(6))].

given #509 (T,wt=13): 708 x ^ (((x ^ y) v z)' ^ (u ^ y)) = 0.  [para(17(a,1),640(a,1,2)),rewrite(17(6))].

given #510 (T,wt=13): 709 x ^ (y ^ (((x v z) ^ y) v u)') = 0.  [para(20(a,1),640(a,1,2)),rewrite(4(6),5(6))].

given #511 (A,wt=25): 231 x ^ (y v (z ^ (x v (u v ((y v u) ^ v))))) = x ^ (y v (z ^ (x v u))).  [para(23(a,1),12(a,1,2,2,2,2)),rewrite(12(6)),flip(a)].

given #512 (F,wt=13): 718 (x v (y v z))' ^ (u ^ (x v z)) = 0.  [para(15(a,1),644(a,1,1,1))].

given #513 (F,wt=13): 719 x ^ ((y v (x ^ z))' ^ (u ^ z)) = 0.  [para(17(a,1),644(a,1,2)),rewrite(17(6))].

given #514 (T,wt=13): 720 x ^ (y ^ (z v ((x v u) ^ y))') = 0.  [para(20(a,1),644(a,1,2)),rewrite(4(6),5(6))].

given #515 (T,wt=13): 722 (x v y)' ^ (z ^ ((x ^ u) v y)) = 0.  [para(22(a,1),644(a,1,1,1))].

given #516 (A,wt=17): 232 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 #517 (F,wt=13): 733 x ^ ((y ^ x) v (y ^ z)) = y ^ x.  [para(64(a,1),42(a,1,2,2,2,2)),rewrite(64(5),64(8),83(7))].

given #518 (F,wt=13): 765 x ^ ((x ^ y) v (z ^ y)) = y ^ x.  [para(64(a,1),43(a,1,2,2,2,1)),rewrite(64(5),64(8),83(7))].

given #519 (T,wt=13): 804 (x v (y ^ z)) ^ (u v (x v y))' = 0.  [para(71(a,1),155(a,1,2,1,2))].

given #520 (T,wt=13): 805 (x v (y ^ z)) ^ ((x v y)' ^ u) = 0.  [para(71(a,1),156(a,1,2,1,1))].

given #521 (A,wt=19): 233 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 #522 (F,wt=13): 806 (x v (y ^ z)) ^ (u ^ (x v y)') = 0.  [para(71(a,1),161(a,1,2,2,1))].

given #523 (F,wt=13): 807 (x v (y ^ z))' v (u v (x v y)) = 1.  [para(71(a,1),324(a,1,2,2))].

given #524 (T,wt=13): 808 x v (y v ((x v (y ^ z)) ^ u)') = 1.  [para(71(a,1),623(a,1,2)),rewrite(2(6),3(6))].

given #525 (T,wt=13): 809 x v (y v (z ^ (x v (y ^ u)))') = 1.  [para(71(a,1),627(a,1,2)),rewrite(2(6),3(6))].

given #526 (A,wt=19): 234 (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 #527 (F,wt=13): 810 (x v y)' ^ (z ^ (x v (y ^ u))) = 0.  [para(71(a,1),644(a,1,1,1))].

given #528 (F,wt=13): 819 x' ^ (x v (y ^ x')) = x' ^ (x v y).  [para(27(a,1),46(a,1,2,2,2))].

given #529 (T,wt=9): 13466 x' ^ (x v (x' v y)') = 0.  [para(153(a,1),819(a,2)),rewrite(4(8),147(8),33(3),4(2),9(2),2817(10)),flip(a)].

given #530 (T,wt=7): 13521 x v (x' v y)' = x.  [hyper(7278,a,13466,a),rewrite(2(4))].

given #531 (A,wt=15): 236 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 #532 (F,wt=7): 13539 x v (y v x')' = x.  [para(2(a,1),13521(a,1,2,1))].

given #533 (F,wt=7): 13550 x' v (x v y)' = x'.  [para(301(a,1),13521(a,1,2,1,1))].

given #534 (T,wt=7): 13759 x' v (y v x)' = x'.  [para(301(a,1),13539(a,1,2,1,2))].

given #535 (T,wt=9): 13545 x v (y v (x' v z))' = x.  [para(15(a,1),13521(a,1,2,1))].

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

given #537 (F,wt=9): 13546 x ^ (x' v y)' = (x' v y)'.  [para(13521(a,1),18(a,1,2)),rewrite(4(4))].

given #538 (F,wt=9): 13547 x v ((x ^ y)' v z)' = x.  [para(13521(a,1),22(a,1,2)),rewrite(7(2)),flip(a)].

given #539 (T,wt=9): 13552 (x' v y)' ^ (z v x)' = 0.  [para(13521(a,1),155(a,1,2,1,2))].

given #540 (T,wt=9): 13554 x v ((x' v y)' ^ z)' = 1.  [para(13521(a,1),623(a,1,2)),rewrite(2(6))].

Low Water (keep): wt=24, part=0.85, limit=24

given #541 (A,wt=17): 240 x v (y v z) != 1 | 0 != z | z' = x v (y v z).  [para(94(a,1),10(b,1)),rewrite(185(3)),flip(b)].

given #542 (F,wt=9): 13555 x v (y ^ (x' v z)')' = 1.  [para(13521(a,1),627(a,1,2)),rewrite(2(6))].

given #543 (F,wt=9): 13559 x v ((y ^ x)' v z)' = x.  [para(13521(a,1),101(a,1,2)),rewrite(24(2)),flip(a)].

given #544 (T,wt=9): 13564 x v ((x' v y)' ^ z) = x.  [para(13521(a,1),200(a,1,2)),rewrite(2(5),13521(9))].

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

given #545 (T,wt=9): 13586 x v (y ^ (x' v z)') = x.  [para(13521(a,1),907(a,1,2)),rewrite(2(5),13521(9))].

given #546 (A,wt=15): 241 x ^ (y v ((z v (u v x)) ^ (x v v))) = x.  [para(94(a,1),12(a,1,2,2,1)),rewrite(70(7)),flip(a)].

given #547 (F,wt=9): 13608 x v (y v (z v x'))' = x.  [para(185(a,1),13521(a,1,2,1))].

given #548 (F,wt=9): 13755 x ^ (y v x')' = (y v x')'.  [para(13539(a,1),18(a,1,2)),rewrite(4(4))].

given #549 (T,wt=9): 13756 x v (y v (x ^ z)')' = x.  [para(13539(a,1),22(a,1,2)),rewrite(7(2)),flip(a)].

given #550 (T,wt=9): 13761 (x v y')' ^ (z v y)' = 0.  [para(13539(a,1),155(a,1,2,1,2))].

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

given #552 (F,wt=9): 13763 x v ((y v x')' ^ z)' = 1.  [para(13539(a,1),623(a,1,2)),rewrite(2(6))].

given #553 (F,wt=9): 13764 x v (y ^ (z v x')')' = 1.  [para(13539(a,1),627(a,1,2)),rewrite(2(6))].

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

given #555 (T,wt=9): 13774 x v ((y v x')' ^ z) = x.  [para(13539(a,1),200(a,1,2)),rewrite(2(5),13539(9))].

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

given #557 (F,wt=9): 13796 x v (y ^ (z v x')') = x.  [para(13539(a,1),907(a,1,2)),rewrite(2(5),13539(9))].

given #558 (F,wt=9): 13856 x' v (y v (x v z))' = x'.  [para(15(a,1),13550(a,1,2,1))].

given #559 (T,wt=9): 13857 x' ^ (x v y)' = (x v y)'.  [para(13550(a,1),18(a,1,2)),rewrite(4(4))].

given #560 (T,wt=9): 13861 (x v y)' ^ (z v x')' = 0.  [para(13550(a,1),155(a,1,2,1,2))].

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

given #562 (F,wt=9): 13863 x' v ((x v y)' ^ z)' = 1.  [para(13550(a,1),623(a,1,2)),rewrite(2(6))].

given #563 (F,wt=9): 13864 x' v (y ^ (x v z)')' = 1.  [para(13550(a,1),627(a,1,2)),rewrite(2(6))].

given #564 (T,wt=9): 13868 x' != 1 | x' != 0 | x' = x.  [para(13550(a,1),59(a,1)),rewrite(301(8),13550(10)),flip(b),flip(c)].

given #565 (T,wt=9): 13874 x' v ((x v y)' ^ z) = x'.  [para(13550(a,1),200(a,1,2)),rewrite(2(5),13550(9))].

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

given #567 (F,wt=9): 13897 x' v (y ^ (x v z)') = x'.  [para(13550(a,1),907(a,1,2)),rewrite(2(5),13550(9))].

given #568 (F,wt=9): 13924 x' v (y v (z v x))' = x'.  [para(185(a,1),13550(a,1,2,1))].

given #569 (T,wt=9): 13958 x' v (x ^ y)' = (x ^ y)'.  [para(7(a,1),13759(a,1,2,1)),rewrite(2(4))].

given #570 (T,wt=7): 16177 x' ^ (x ^ y)' = x'.  [para(13958(a,1),6(a,1,2))].

given #571 (A,wt=17): 250 1 != x | y ^ (z ^ x) != 0 | x' = y ^ (z ^ x).  [para(103(a,1),10(a,1)),rewrite(180(5)),flip(a)].

given #572 (F,wt=7): 16282 x' ^ (y ^ x)' = x'.  [para(4(a,1),16177(a,1,2,1))].

given #573 (F,wt=7): 16286 x ^ (x' ^ y)' = x.  [para(301(a,1),16177(a,1,1)),rewrite(301(6))].

given #574 (T,wt=7): 16342 x ^ (y ^ x')' = x.  [para(301(a,1),16282(a,1,1)),rewrite(301(6))].

given #575 (T,wt=9): 13963 x' ^ (y v x)' = (y v x)'.  [para(13759(a,1),18(a,1,2)),rewrite(4(4))].

Low Water (keep): wt=21, part=0.75, limit=21

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

given #577 (F,wt=9): 13964 x' v (y ^ x)' = (y ^ x)'.  [para(24(a,1),13759(a,1,2,1)),rewrite(2(4))].

given #578 (F,wt=9): 13973 (x v y)' ^ (z v y')' = 0.  [para(13759(a,1),155(a,1,2,1,2))].

given #579 (T,wt=9): 13975 x' v ((y v x)' ^ z)' = 1.  [para(13759(a,1),623(a,1,2)),rewrite(2(6))].

given #580 (T,wt=9): 13976 x' v (y ^ (z v x)')' = 1.  [para(13759(a,1),627(a,1,2)),rewrite(2(6))].

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

given #582 (F,wt=9): 13988 x' v ((y v x)' ^ z) = x'.  [para(13759(a,1),200(a,1,2)),rewrite(2(5),13759(9))].

given #583 (F,wt=9): 14012 x' v (y ^ (z v x)') = x'.  [para(13759(a,1),907(a,1,2)),rewrite(2(5),13759(9))].

given #584 (T,wt=9): 14246 x ^ (y' v (x ^ y))' = 0.  [para(13546(a,1),157(a,1,2))].

given #585 (T,wt=9): 14258 x ^ (y' v (y ^ x))' = 0.  [para(13546(a,1),1216(a,1,2))].

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

given #587 (F,wt=9): 14316 x' ^ ((x ^ y)' v z)' = 0.  [para(13547(a,1),149(a,1,2,1)),rewrite(4(6))].

given #588 (F,wt=9): 14403 (x' v y)' ^ (x v z)' = 0.  [para(2(a,1),13552(a,1,2,1))].

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

given #590 (T,wt=9): 14407 x' ^ ((y ^ x)' v z)' = 0.  [para(24(a,1),13552(a,1,2,1)),rewrite(4(6))].

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

given #592 (F,wt=9): 14944 x ^ ((x ^ y) v y')' = 0.  [para(13755(a,1),151(a,1,2))].

given #593 (F,wt=9): 14955 x ^ ((y ^ x) v y')' = 0.  [para(13755(a,1),1207(a,1,2))].

given #594 (T,wt=9): 15004 x' ^ ((x ^ y)' v z) = x'.  [para(13547(a,1),13755(a,1,2,1)),rewrite(4(5),13547(10))].

given #595 (T,wt=9): 15005 x' ^ ((y ^ x)' v z) = x'.  [para(13559(a,1),13755(a,1,2,1)),rewrite(4(5),13559(10))].

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

given #597 (F,wt=9): 15011 x' ^ (y v (x ^ z)')' = 0.  [para(13756(a,1),149(a,1,2,1)),rewrite(4(6))].

given #598 (F,wt=9): 15094 x' ^ (y v (x ^ z)') = x'.  [para(13756(a,1),13755(a,1,2,1)),rewrite(4(5),13756(10))].

given #599 (T,wt=9): 15096 (x v y')' ^ (y v z)' = 0.  [para(2(a,1),13761(a,1,2,1))].

given #600 (T,wt=9): 15099 x' ^ (y v (z ^ x)')' = 0.  [para(24(a,1),13761(a,1,2,1)),rewrite(4(6))].

given #601 (A,wt=19): 260 x ^ (y v (z ^ (x v (u v (y' v v))))) = x ^ (y v z).  [para(111(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)].

given #602 (F,wt=9): 15350 x' ^ (y v (z ^ x)') = x'.  [para(13768(a,1),13755(a,1,2,1)),rewrite(4(5),13768(10))].

given #603 (F,wt=9): 15681 x ^ (y v (x ^ y'))' = 0.  [para(13857(a,1),157(a,1,2))].

given #604 (T,wt=9): 15696 x ^ (y v (y' ^ x))' = 0.  [para(13857(a,1),1216(a,1,2))].

given #605 (T,wt=9): 15742 (x v y)' ^ (x' v z)' = 0.  [para(2(a,1),13861(a,1,2,1))].

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

given #607 (F,wt=9): 16182 x v (x' ^ y)' = (x' ^ y)'.  [para(301(a,1),13958(a,1,1))].

given #608 (F,wt=9): 16196 x v (y ^ (x v y'))' = 1.  [para(13958(a,1),208(a,1,2))].

given #609 (T,wt=9): 16225 x v (y ^ (y' v x))' = 1.  [para(13958(a,1),1352(a,1,2))].

given #610 (T,wt=9): 16284 x' ^ (y ^ (x ^ z))' = x'.  [para(17(a,1),16177(a,1,2,1))].

given #611 (A,wt=19): 268 (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 #612 (F,wt=9): 16288 (x ^ y)' v (z ^ x')' = 1.  [para(16177(a,1),209(a,1,2,1,2))].

given #613 (F,wt=9): 16309 x' ^ (y ^ (z ^ x))' = x'.  [para(180(a,1),16177(a,1,2,1))].

given #614 (T,wt=9): 16345 (x ^ y)' v (z ^ y')' = 1.  [para(16282(a,1),209(a,1,2,1,2))].

given #615 (T,wt=9): 16428 x ^ (y ^ (x' ^ z))' = x.  [para(17(a,1),16286(a,1,2,1))].

given #616 (A,wt=21): 269 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),170(6),48(6))].

given #617 (F,wt=9): 16429 x ^ ((x v y)' ^ z)' = x.  [para(16286(a,1),20(a,1,2)),rewrite(6(2)),flip(a)].

given #618 (F,wt=9): 16433 (x' ^ y)' v (z ^ x)' = 1.  [para(16286(a,1),209(a,1,2,1,2))].

Low Water (keep): wt=20, part=0.67, limit=20

given #619 (T,wt=9): 16434 x ^ ((x' ^ y)' v z)' = 0.  [para(16286(a,1),640(a,1,2)),rewrite(4(6))].

given #620 (T,wt=9): 16435 x ^ (y v (x' ^ z)')' = 0.  [para(16286(a,1),644(a,1,2)),rewrite(4(6))].

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

given #622 (F,wt=9): 16437 x ^ ((y v x)' ^ z)' = x.  [para(16286(a,1),95(a,1,2)),rewrite(18(2)),flip(a)].

given #623 (F,wt=9): 16440 x ^ ((x' ^ y)' v z) = x.  [para(16286(a,1),181(a,1,2)),rewrite(4(5),16286(9))].

given #624 (T,wt=9): 16455 x ^ (y v (x' ^ z)') = x.  [para(16286(a,1),855(a,1,2)),rewrite(4(5),16286(9))].

given #625 (T,wt=9): 16482 x ^ (y ^ (z ^ x'))' = x.  [para(180(a,1),16286(a,1,2,1))].

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

given #627 (F,wt=9): 16508 x v (y ^ x')' = (y ^ x')'.  [para(16342(a,1),24(a,1,2)),rewrite(2(4))].

given #628 (F,wt=9): 16509 x ^ (y ^ (x v z)')' = x.  [para(16342(a,1),20(a,1,2)),rewrite(6(2)),flip(a)].

given #629 (T,wt=9): 16514 (x ^ y')' v (z ^ y)' = 1.  [para(16342(a,1),209(a,1,2,1,2))].

given #630 (T,wt=9): 16515 x ^ ((y ^ x')' v z)' = 0.  [para(16342(a,1),640(a,1,2)),rewrite(4(6))].

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

given #632 (F,wt=9): 16516 x ^ (y v (z ^ x')')' = 0.  [para(16342(a,1),644(a,1,2)),rewrite(4(6))].

given #633 (F,wt=9): 16518 x ^ (y ^ (z v x)')' = x.  [para(16342(a,1),95(a,1,2)),rewrite(18(2)),flip(a)].

Low Water (keep): wt=19, part=0.64, limit=19

given #634 (T,wt=9): 16521 x ^ ((y ^ x')' v z) = x.  [para(16342(a,1),181(a,1,2)),rewrite(4(5),16342(9))].

given #635 (T,wt=9): 16535 x ^ (y v (z ^ x')') = x.  [para(16342(a,1),855(a,1,2)),rewrite(4(5),16342(9))].

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

given #637 (F,wt=9): 16785 (x ^ y)' v (x' ^ z)' = 1.  [para(7(a,1),13975(a,1,2,1,1,1))].

given #638 (F,wt=9): 16789 (x ^ y)' v (y' ^ z)' = 1.  [para(24(a,1),13975(a,1,2,1,1,1))].

given #639 (T,wt=9): 17831 x v (y' ^ (x v y))' = 1.  [para(16182(a,1),208(a,1,2))].

given #640 (T,wt=9): 17849 x v (y' ^ (y v x))' = 1.  [para(16182(a,1),1352(a,1,2))].

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

given #642 (F,wt=9): 18082 (x ^ y')' v (y ^ z)' = 1.  [para(16288(a,1),2(a,1)),flip(a)].

given #643 (F,wt=9): 18357 (x' ^ y)' v (x ^ z)' = 1.  [para(4(a,1),16433(a,1,2,1))].

given #644 (T,wt=9): 18788 x v ((x v y) ^ y')' = 1.  [para(16508(a,1),201(a,1,2))].

given #645 (T,wt=9): 18807 x v ((y v x) ^ y')' = 1.  [para(16508(a,1),1483(a,1,2))].

given #646 (A,wt=19): 279 x ^ (y v (z ^ (x v (u v (v v y'))))) = x ^ (y v z).  [para(128(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)].

given #647 (F,wt=9): 19214 (x' ^ (x v y))' = (y ^ x')'.  [hyper(37,a,17831,a,b,335,a),rewrite(2(7),819(8)),flip(a)].

given #648 (F,wt=9): 19344 (x' ^ (y v x))' = (y ^ x')'.  [para(2(a,1),19214(a,1,1,2))].

given #649 (T,wt=9): 19346 ((x v y) ^ x')' = (y ^ x')'.  [para(4(a,1),19214(a,1,1))].

given #650 (T,wt=9): 19347 (x' ^ (x v y))' = (x' ^ y)'.  [para(4(a,1),19214(a,2,1))].

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

given #652 (F,wt=9): 19352 (x' ^ (y v (x v y)'))' = x.  [para(29(a,1),19214(a,1,1,2)),rewrite(4(3),61(3),301(2),4(5)),flip(a)].

given #653 (F,wt=9): 19358 (x' ^ (y v (y v x)'))' = x.  [para(135(a,1),19214(a,1,1,2)),rewrite(4(3),61(3),301(2),4(5)),flip(a)].

given #654 (T,wt=9): 19360 (x ^ (x' v y))' = (y ^ x)'.  [para(301(a,1),19214(a,1,1,1)),rewrite(301(6))].

given #655 (T,wt=9): 19476 (x v y) ^ (x' ^ y)' = x.  [para(19214(a,1),164(a,1,2,2)),rewrite(16523(7),19347(8),301(10)),xx(a)].

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

given #657 (F,wt=9): 19727 ((x v y) ^ y')' = (x ^ y')'.  [para(4(a,1),19344(a,1,1))].

given #658 (F,wt=9): 19740 (x ^ (y v x'))' = (y ^ x)'.  [para(301(a,1),19344(a,1,1,1)),rewrite(301(6))].

given #659 (T,wt=9): 19821 (x v y) ^ (y' ^ x)' = y.  [para(19344(a,1),164(a,1,2,2)),rewrite(16536(7),19728(8),301(10)),xx(a)].

given #660 (T,wt=9): 19948 (x v y) ^ x' = y ^ x'.  [para(19346(a,1),301(a,1,1)),rewrite(301(4)),flip(a)].

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

given #662 (F,wt=9): 19993 x' ^ (x v y) = x' ^ y.  [para(19347(a,1),301(a,1,1)),rewrite(301(4)),flip(a)].

given #663 (F,wt=9): 20218 x' ^ (y v x) = x' ^ y.  [back_rewrite(17018),rewrite(20212(8))].

given #664 (T,wt=9): 20237 x' ^ (y v (x v y)') = x'.  [para(19352(a,1),301(a,1,1)),flip(a)].

given #665 (T,wt=9): 20265 x' ^ (y v (y v x)') = x'.  [para(19358(a,1),301(a,1,1)),flip(a)].

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

given #667 (F,wt=9): 20308 x ^ (x' v y) = y ^ x.  [para(19360(a,1),301(a,1,1)),rewrite(301(3)),flip(a)].

given #668 (F,wt=9): 20359 (x' v y) ^ (y ^ x)' = x'.  [para(19360(a,1),164(a,1,2,2)),rewrite(16353(6),20308(8)),xx(a)].

given #669 (T,wt=7): 21840 (x v y)' = y' ^ x'.  [para(6(a,1),20359(a,1,2,1)),rewrite(2(3),21582(3),19948(4)),flip(a)].

given #670 (T,wt=7): 22231 (x' ^ y')' = y v x.  [back_rewrite(19786),rewrite(21840(5),17(7),18093(7))].

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

given #672 (F,wt=7): 26266 (x ^ y')' = y v x'.  [para(301(a,1),22231(a,1,1,1))].

given #673 (F,wt=7): 27229 (x ^ y)' = y' v x'.  [para(301(a,1),26266(a,1,1,2))].

given #674 (T,wt=9): 20697 (x v y) ^ y' = x ^ y'.  [para(19727(a,1),301(a,1,1)),rewrite(301(4)),flip(a)].

given #675 (T,wt=9): 20716 x ^ (y v x') = y ^ x.  [para(19740(a,1),301(a,1,1)),rewrite(301(3)),flip(a)].

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

given #677 (F,wt=9): 21706 (x v y) ^ (x v y') = x.  [para(6(a,1),20308(a,2)),rewrite(2(4),21582(4))].

given #678 (F,wt=9): 21709 (x v y) ^ (y v x') = y.  [para(18(a,1),20308(a,2)),rewrite(2(4),21454(4))].

given #679 (T,wt=9): 22013 x v (y' ^ x') = x v y'.  [back_rewrite(21582),rewrite(21840(2))].

given #680 (T,wt=9): 22032 x v (x' ^ y') = x v y'.  [back_rewrite(21454),rewrite(21840(2))].

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

given #682 (F,wt=9): 26077 (x ^ y) v (x ^ y') = x.  [back_rewrite(17751),rewrite(21851(4))].

given #683 (F,wt=9): 26292 (x v y') ^ (y v x) = x.  [para(22231(a,1),19476(a,1,2))].

given #684 (T,wt=9): 26294 (x v y) ^ (x' v y) = y.  [para(22231(a,1),19821(a,1,2)),rewrite(4(4))].

given #685 (T,wt=9): 26768 (x v y) ^ (y' v x) = x.  [back_rewrite(19476),rewrite(26267(4))].

given #686 (A,wt=21): 571 (x v y) ^ (z v ((x v (y v u)) ^ (x v (y v v)))) = x v y.  [para(19(a,1),40(a,1,2,2,1)),rewrite(3(7),217(9),3(6)),flip(a)].

given #687 (F,wt=9): 27222 x v ((y ^ x') v y') = 1.  [para(26266(a,1),8(a,1,2)),rewrite(15(5))].

given #688 (F,wt=9): 30926 x' v y' = (y' ^ x) v x'.  [para(20308(a,1),27229(a,1,1)),rewrite(27229(2),21840(6),301(6))].

given #689 (T,wt=9): 31252 (x' v y) ^ (y v x) = y.  [para(301(a,1),21709(a,1,2,2))].

given #690 (T,wt=9): 31281 x v (y ^ x') = x v y.  [para(301(a,1),22013(a,1,2,1)),rewrite(301(5))].

given #691 (A,wt=23): 590 x ^ (y v (z' v (u v (v ^ (x v z))))) = x ^ (y v (z' v (u v v))).  [para(111(a,1),40(a,1,2,2,2,2)),rewrite(30(6),2(5),24(5),3(4),3(3),3(11),3(10)),flip(a)].

given #692 (F,wt=9): 31336 x' v (x ^ y') = x' v y'.  [para(301(a,1),22032(a,1,2,1))].

given #693 (F,wt=9): 31337 x v (x' ^ y) = x v y.  [para(301(a,1),22032(a,1,2,2)),rewrite(301(5))].

given #694 (T,wt=9): 31460 x ^ ((x ^ y) v y') = x.  [para(4(a,1),26077(a,1,2)),rewrite(20467(4))].

given #695 (T,wt=9): 31601 (x ^ y) v x' = y v x'.  [para(27222(a,1),26294(a,1,2)),rewrite(301(2),101(4),4(4),61(4),301(4)),flip(a)].

given #696 (A,wt=23): 592 x ^ (y v (z v (u' v (v ^ (x v u))))) = x ^ (y v (z v (u' v v))).  [para(128(a,1),40(a,1,2,2,2,2)),rewrite(30(6),2(5),24(5),3(4),3(3),3(11),3(10)),flip(a)].

given #697 (F,wt=9): 31733 x' v (y ^ x) = x' v y.  [para(301(a,1),31281(a,1,2,2))].

given #698 (F,wt=9): 31905 x' v (x ^ y) = x' v y.  [para(301(a,1),31336(a,1,2,2)),rewrite(301(6))].

given #699 (T,wt=9): 32242 (x ^ y) v y' = x v y'.  [para(31460(a,1),24(a,1,2)),rewrite(2(4),22(4)),flip(a)].

given #700 (T,wt=10): 19975 x ^ y' != 0 | x v y = y.  [back_rewrite(7377),rewrite(19948(3))].

given #701 (A,wt=23): 613 x ^ (y v (z v (u v (v ^ (x v z'))))) = x ^ (y v (z v (u v v))).  [para(322(a,1),40(a,1,2,2,2,2)),rewrite(30(5),2(4),24(4),3(3),3(2),3(10),3(9)),flip(a)].

given #702 (F,wt=10): 19977 x ^ y' != 0 | y v x = y.  [back_rewrite(7255),rewrite(19948(3))].

given #703 (F,wt=10): 20027 0 != x | x v y = x' ^ y.  [para(19347(a,1),312(a,1,2)),rewrite(19476(5),19993(5)),flip(a),flip(b)].

given #704 (T,wt=10): 20031 0 != x | x v y = y ^ x'.  [para(19347(a,1),7248(a,1,2)),rewrite(19476(5),19948(5)),flip(a),flip(b)].

given #705 (T,wt=10): 20193 x' ^ y != 0 | y v x = x.  [back_rewrite(7278),rewrite(19993(3))].

given #706 (A,wt=17): 739 x ^ (y ^ (z v (x ^ ((x ^ y) v u)))) = x ^ y.  [para(48(a,1),42(a,1,2,2,1)),rewrite(70(7),5(7)),flip(a)].

given #707 (F,wt=10): 20200 x' ^ y != 0 | x v y = x.  [back_rewrite(1317),rewrite(19993(3))].

given #708 (F,wt=10): 20363 x' != 0 | x' v y = y ^ x.  [para(19360(a,1),7248(a,1,2)),rewrite(20359(5),4(6),20308(6)),flip(b)].

given #709 (T,wt=10): 20436 x ^ y != 0 | x v y' = y'.  [back_rewrite(4635),rewrite(20308(3))].

given #710 (T,wt=10): 20442 x ^ y != 0 | y' v x = y'.  [back_rewrite(109),rewrite(20308(3))].

given #711 (A,wt=17): 740 x ^ (y ^ (z v (y ^ ((x ^ y) v u)))) = x ^ y.  [para(50(a,1),42(a,1,2,2,1)),rewrite(70(7),5(7)),flip(a)].

given #712 (F,wt=10): 20733 x' != 0 | y v x' = y ^ x.  [para(19740(a,1),7248(a,1,2)),rewrite(20731(5),4(6),20716(6)),flip(b)].

given #713 (F,wt=10): 20748 0 != x | y v x = y ^ x'.  [back_rewrite(20698),rewrite(20747(5)),flip(a)].

given #714 (T,wt=10): 20749 0 != x | y v x = x' ^ y.  [back_rewrite(20228),rewrite(20747(5)),flip(a)].

given #715 (T,wt=10): 20948 x ^ y != 0 | x ^ y' = x.  [back_rewrite(20578),rewrite(20803(7),18(6),20697(6))].

given #716 (A,wt=23): 775 x ^ (y v ((y v z) ^ (u ^ (x v z)))) = x ^ (y v ((y v z) ^ u)).  [para(48(a,1),43(a,1,2,2,2)),rewrite(2(6),24(6),5(8)),flip(a)].

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

% Proof 1 at 16.04 (+ 0.16) seconds: distributivity.
% Length of proof is 167.
% Level of proof is 26.
% Maximum clause weight is 23.
% Given clauses 716.

1 x ^ (y v z) = (x ^ y) v (x ^ z) # label(distributivity) # 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) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity) # answer(distributivity).  [deny(1)].
15 x v (y v z) = y v (x v z).  [para(2(a,1),3(a,1,1)),rewrite(3(2))].
17 x ^ (y ^ z) = y ^ (x ^ z).  [para(4(a,1),5(a,1,1)),rewrite(5(2))].
18 x ^ (y v x) = x.  [para(2(a,1),6(a,1,2))].
19 (x v y) ^ (x v (y v z)) = x v y.  [para(3(a,1),6(a,1,2))].
20 x ^ ((x v y) ^ z) = x ^ z.  [para(6(a,1),5(a,1,1)),flip(a)].
21 x ^ (y ^ ((x ^ y) v z)) = x ^ y.  [para(6(a,1),5(a,1)),flip(a)].
22 x v ((x ^ y) v z) = x v z.  [para(7(a,1),3(a,1,1)),flip(a)].
23 x v (y v ((x v y) ^ z)) = x v y.  [para(7(a,1),3(a,1)),flip(a)].
24 x v (y ^ x) = x.  [para(4(a,1),7(a,1,2))].
26 x ^ x = x.  [para(7(a,1),6(a,1,2))].
27 x v x = x.  [para(6(a,1),7(a,1,2))].
28 x v (x' v y) = 1 v y.  [para(8(a,1),3(a,1,1)),flip(a)].
29 x v (y v (x v y)') = 1.  [para(8(a,1),3(a,1)),flip(a)].
30 x ^ 1 = x.  [para(8(a,1),6(a,1,2))].
31 x ^ (x' ^ y) = 0 ^ y.  [para(9(a,1),5(a,1,1)),flip(a)].
32 x ^ (y ^ (x ^ y)') = 0.  [para(9(a,1),5(a,1)),flip(a)].
33 x v 0 = x.  [para(9(a,1),7(a,1,2))].
34 x v y != 1 | y ^ x != 0 | y' = x.  [para(2(a,1),10(a,1))].
37 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z.  [para(5(a,1),10(b,1))].
43 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))].
46 x ^ (y v (z ^ (x v y'))) = x ^ (y v z).  [para(8(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)].
48 x ^ (x ^ y) = x ^ y.  [para(26(a,1),5(a,1,1)),flip(a)].
50 x ^ (y ^ x) = y ^ x.  [para(26(a,1),5(a,2,2)),rewrite(4(2))].
54 x v (x v y) = x v y.  [para(27(a,1),3(a,1,1)),flip(a)].
57 x ^ (y v ((x ^ z) v (z ^ y))) = x ^ (y v (z ^ (x v y))).  [para(27(a,1),12(a,1,2,2,2,2))].
61 1 ^ x = x.  [para(30(a,1),4(a,1)),flip(a)].
64 0 v x = x.  [para(33(a,1),2(a,1)),flip(a)].
66 x ^ (y v (z ^ (x v y))) = x ^ (y v (z ^ x)).  [para(33(a,1),12(a,1,2,2,2,2)),rewrite(57(5),33(6))].
71 x v (y v (x ^ z)) = y v x.  [para(7(a,1),15(a,1,2)),flip(a)].
72 x v (y v x') = y v 1.  [para(8(a,1),15(a,1,2)),flip(a)].
77 1 v x = 1.  [para(61(a,1),6(a,1))].
78 x v (x' v y) = 1.  [back_rewrite(28),rewrite(77(5))].
80 0 ^ x = 0.  [para(64(a,1),6(a,1,2))].
82 x ^ (x' ^ y) = 0.  [back_rewrite(31),rewrite(80(5))].
83 x ^ (y ^ (x v z)) = y ^ x.  [para(6(a,1),17(a,1,2)),flip(a)].
85 x ^ (y ^ x') = y ^ 0.  [para(9(a,1),17(a,1,2)),flip(a)].
88 x v 1 = 1.  [para(77(a,1),2(a,1)),flip(a)].
89 x v (y v x') = 1.  [back_rewrite(72),rewrite(88(5))].
91 x ^ 0 = 0.  [para(80(a,1),4(a,1)),flip(a)].
92 x ^ (y ^ x') = 0.  [back_rewrite(85),rewrite(91(5))].
95 x ^ ((y v x) ^ z) = x ^ z.  [para(18(a,1),5(a,1,1)),flip(a)].
99 (x v y) ^ (x v (z v y)) = x v y.  [para(15(a,1),18(a,1,2))].
101 x v ((y ^ x) v z) = x v z.  [para(24(a,1),3(a,1,1)),flip(a)].
102 x v (y v (z ^ (x v y))) = x v y.  [para(24(a,1),3(a,1)),flip(a)].
103 x v (y ^ (z ^ x)) = x.  [para(5(a,1),24(a,1,2))].
106 x v (y v (z ^ x)) = y v x.  [para(24(a,1),15(a,1,2)),flip(a)].
110 x ^ (y v (z ^ (x v (y' v u)))) = x ^ (y v z).  [para(78(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)].
112 (x v y) ^ (y v (x v z)) = y v x.  [para(2(a,1),19(a,1,1))].
128 x v (y v (z v x')) = 1.  [para(3(a,1),89(a,1,2))].
135 x v (y v (y v x)') = 1.  [para(2(a,1),29(a,1,2,2,1))].
142 x ^ (x v y)' = 0.  [para(9(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].
145 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u).  [para(20(a,1),17(a,1,2)),flip(a)].
147 x ^ ((x v y)' ^ z) = 0.  [para(82(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].
153 x ^ (y v ((x v z)' ^ (y v u))) = x ^ (y v ((x v z)' ^ (x v u))).  [para(142(a,1),12(a,1,2,2,1)),rewrite(64(6))].
164 x v (y ^ (x ^ y)') != 1 | y ^ (x ^ y)' = x'.  [para(32(a,1),10(b,1)),flip(c),xx(b)].
170 x ^ (y ^ (x ^ z)) = y ^ (x ^ z).  [para(48(a,1),5(a,2,2)),rewrite(17(3),5(2))].
180 x ^ (y ^ (z ^ x)) = y ^ (z ^ x).  [para(5(a,1),50(a,1,2)),rewrite(5(5))].
190 x v (x ^ y)' = 1.  [para(8(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].
202 x v (y ^ x)' = 1.  [para(4(a,1),190(a,1,2,1))].
208 x v (y v (z ^ (x v y))') = 1.  [para(202(a,1),3(a,1)),flip(a)].
215 ((x v y) ^ z) v (x ^ z)' = 1.  [para(20(a,1),202(a,1,2,1))].
228 x v (y v ((y v x) ^ z)) = x v y.  [para(2(a,1),23(a,1,2,2,1))].
301 x'' = x.  [para(8(a,1),34(a,1)),rewrite(4(5),9(5)),xx(a),xx(b)].
320 x' v (y v x) = 1.  [para(301(a,1),89(a,1,2,2))].
321 x' ^ (y ^ x) = 0.  [para(301(a,1),92(a,1,2,2))].
324 x' v (y v (z v x)) = 1.  [para(301(a,1),128(a,1,2,2,2))].
326 x' ^ (y v x) != 0 | y v x = x.  [para(320(a,1),10(a,1)),rewrite(301(10)),flip(c),xx(a)].
335 x ^ (y ^ (y ^ ((x ^ y) v z))') = 0.  [para(21(a,1),321(a,1,2)),rewrite(4(6),5(6))].
631 (x ^ (y ^ z))' v (u v z) = 1.  [para(103(a,1),324(a,1,2,2))].
775 x ^ (y v ((y v z) ^ (u ^ (x v z)))) = x ^ (y v ((y v z) ^ u)).  [para(48(a,1),43(a,1,2,2,2)),rewrite(2(6),24(6),5(8)),flip(a)].
807 (x v (y ^ z))' v (u v (x v y)) = 1.  [para(71(a,1),324(a,1,2,2))].
819 x' ^ (x v (y ^ x')) = x' ^ (x v y).  [para(27(a,1),46(a,1,2,2,2))].
850 (x v y) ^ ((x v (z v y)) ^ u) = (x v y) ^ u.  [para(15(a,1),95(a,1,2,1))].
857 ((x v y) ^ z) v (y ^ z)' = 1.  [para(95(a,1),202(a,1,2,1))].
903 x v (y v ((z ^ x) v y)') = 1.  [para(29(a,1),101(a,1,2)),rewrite(88(2)),flip(a)].
1039 x ^ (x' v (y v (z ^ x))) = x ^ (x' v (y v z)).  [para(78(a,1),66(a,1,2,2,2)),rewrite(30(4),3(3),3(8)),flip(a)].
1602 (x ^ (y v z)) v (y ^ x)' = 1.  [para(4(a,1),215(a,1,1))].
2237 (x v y) ^ (y v (z ^ (x v y))) = y v (z ^ (x v y)).  [para(102(a,1),18(a,1,2)),rewrite(4(5))].
2268 (x v y) ^ (x v (z ^ (x v y))) = x v (z ^ (x v y)).  [para(102(a,1),99(a,1,2)),rewrite(4(5))].
2817 x' ^ (x v (y ^ (x' v z))) = x' ^ (x v y).  [para(54(a,1),110(a,1,2,2,2))].
7278 x' ^ (x v y) != 0 | y v x = x.  [para(2(a,1),326(a,1,2))].
7442 (x v y) ^ (z ^ (y v x)) = z ^ (y v x).  [para(112(a,1),170(a,1,2,2)),rewrite(112(8))].
8658 (x v ((x v y) ^ z)) ^ (y v x) = x v ((x v y) ^ z).  [para(228(a,1),18(a,1,2))].
13466 x' ^ (x v (x' v y)') = 0.  [para(153(a,1),819(a,2)),rewrite(4(8),147(8),33(3),4(2),9(2),2817(10)),flip(a)].
13521 x v (x' v y)' = x.  [hyper(7278,a,13466,a),rewrite(2(4))].
13539 x v (y v x')' = x.  [para(2(a,1),13521(a,1,2,1))].
13546 x ^ (x' v y)' = (x' v y)'.  [para(13521(a,1),18(a,1,2)),rewrite(4(4))].
13550 x' v (x v y)' = x'.  [para(301(a,1),13521(a,1,2,1,1))].
13759 x' v (y v x)' = x'.  [para(301(a,1),13539(a,1,2,1,2))].
13855 x' v (y v (x v z)') = y v x'.  [para(13550(a,1),15(a,1,2)),flip(a)].
13958 x' v (x ^ y)' = (x ^ y)'.  [para(7(a,1),13759(a,1,2,1)),rewrite(2(4))].
13961 x' v (y v (z v x)') = y v x'.  [para(13759(a,1),15(a,1,2)),flip(a)].
14264 x' v (y v ((x' v y)' ^ (x v z))) = 1.  [para(13546(a,1),1602(a,1,2,1)),rewrite(301(9),2(8),3(8))].
16177 x' ^ (x ^ y)' = x'.  [para(13958(a,1),6(a,1,2))].
16182 x v (x' ^ y)' = (x' ^ y)'.  [para(301(a,1),13958(a,1,1))].
16282 x' ^ (y ^ x)' = x'.  [para(4(a,1),16177(a,1,2,1))].
16309 x' ^ (y ^ (z ^ x))' = x'.  [para(180(a,1),16177(a,1,2,1))].
16342 x ^ (y ^ x')' = x.  [para(301(a,1),16282(a,1,1)),rewrite(301(6))].
16353 x v ((x' v y) ^ (z ^ x)') = 1.  [para(16282(a,1),215(a,1,2,1)),rewrite(301(7),2(6))].
16536 x' v ((y v x) ^ (z ^ x')') = 1.  [para(16342(a,1),857(a,1,2,1)),rewrite(2(7))].
17831 x v (y' ^ (x v y))' = 1.  [para(16182(a,1),208(a,1,2))].
18093 x' ^ ((y ^ (z ^ x))' ^ u) = x' ^ u.  [para(16309(a,1),5(a,1,1)),flip(a)].
19214 (x' ^ (x v y))' = (y ^ x')'.  [hyper(37,a,17831,a,b,335,a),rewrite(2(7),819(8)),flip(a)].
19344 (x' ^ (y v x))' = (y ^ x')'.  [para(2(a,1),19214(a,1,1,2))].
19346 ((x v y) ^ x')' = (y ^ x')'.  [para(4(a,1),19214(a,1,1))].
19352 (x' ^ (y v (x v y)'))' = x.  [para(29(a,1),19214(a,1,1,2)),rewrite(4(3),61(3),301(2),4(5)),flip(a)].
19358 (x' ^ (y v (y v x)'))' = x.  [para(135(a,1),19214(a,1,1,2)),rewrite(4(3),61(3),301(2),4(5)),flip(a)].
19360 (x ^ (x' v y))' = (y ^ x)'.  [para(301(a,1),19214(a,1,1,1)),rewrite(301(6))].
19727 ((x v y) ^ y')' = (x ^ y')'.  [para(4(a,1),19344(a,1,1))].
19728 (x' ^ (y v x))' = (x' ^ y)'.  [para(4(a,1),19344(a,2,1))].
19740 (x ^ (y v x'))' = (y ^ x)'.  [para(301(a,1),19344(a,1,1,1)),rewrite(301(6))].
19786 ((x ^ (y ^ z))' ^ (u v z)')' = u v z.  [para(631(a,1),19344(a,1,1,2)),rewrite(4(4),61(4),301(3)),flip(a)].
19794 (x ^ (y v ((z ^ x) v y)')')' = y v ((z ^ x) v y)'.  [para(903(a,1),19344(a,1,1,2)),rewrite(4(7),61(7),301(6)),flip(a)].
19821 (x v y) ^ (y' ^ x)' = y.  [para(19344(a,1),164(a,1,2,2)),rewrite(16536(7),19728(8),301(10)),xx(a)].
19948 (x v y) ^ x' = y ^ x'.  [para(19346(a,1),301(a,1,1)),rewrite(301(4)),flip(a)].
20237 x' ^ (y v (x v y)') = x'.  [para(19352(a,1),301(a,1,1)),flip(a)].
20265 x' ^ (y v (y v x)') = x'.  [para(19358(a,1),301(a,1,1)),flip(a)].
20308 x ^ (x' v y) = y ^ x.  [para(19360(a,1),301(a,1,1)),rewrite(301(3)),flip(a)].
20359 (x' v y) ^ (y ^ x)' = x'.  [para(19360(a,1),164(a,1,2,2)),rewrite(16353(6),20308(8)),xx(a)].
20440 x ^ (y v (z ^ x)) = (y v z) ^ x.  [back_rewrite(1039),rewrite(20308(5),4(3),20308(7))].
20473 x v (y ^ (x v z)) = (x v y) ^ (x v z).  [back_rewrite(2268),rewrite(20440(5)),flip(a)].
20474 x v (y ^ (z v x)) = (x v y) ^ (z v x).  [back_rewrite(2237),rewrite(20440(5)),flip(a)].
20697 (x v y) ^ y' = x ^ y'.  [para(19727(a,1),301(a,1,1)),rewrite(301(4)),flip(a)].
20716 x ^ (y v x') = y ^ x.  [para(19740(a,1),301(a,1,1)),rewrite(301(3)),flip(a)].
20765 (x v y) ^ (y ^ (x v (z ^ y))')' = x v (z ^ y).  [para(106(a,1),19821(a,1,1)),rewrite(4(5))].
20802 (x' v y)' = x ^ (y ^ x)'.  [para(13521(a,1),19821(a,1,1)),rewrite(301(4),4(3),20308(3)),flip(a)].
20803 (x v y')' = y ^ (x ^ y)'.  [para(13539(a,1),19821(a,1,1)),rewrite(301(4),4(3),20716(3)),flip(a)].
20935 x' v (y v (x ^ (y ^ x)')) = 1.  [back_rewrite(14264),rewrite(20802(4),5(6),83(6),4(4))].
20960 (x ^ (y ^ z'))' = z v ((x ^ y) v z)'.  [back_rewrite(19794),rewrite(20803(5),18(5),20697(4),5(3),170(4))].
21193 (x v (y v z)) ^ (y v (z ^ u)) = y v (z ^ u).  [para(807(a,1),19948(a,1,1)),rewrite(301(5),61(4),301(8)),flip(a)].
21454 x v (y v x)' = x v y'.  [para(20237(a,1),24(a,1,2)),rewrite(2(5),13855(5)),flip(a)].
21476 (x ^ (y ^ z'))' = z v (x ^ y)'.  [back_rewrite(20960),rewrite(21454(8))].
21582 x v (x v y)' = x v y'.  [para(20265(a,1),24(a,1,2)),rewrite(2(5),13961(5)),flip(a)].
21840 (x v y)' = y' ^ x'.  [para(6(a,1),20359(a,1,2,1)),rewrite(2(3),21582(3),19948(4)),flip(a)].
21904 x ^ (y ^ x)' = y' ^ x.  [para(20359(a,1),164(a,1,2,2,1)),rewrite(301(6),4(5),3(6),20935(6),20359(10),301(7),4(6),21840(9),301(9)),xx(a)].
22013 x v (y' ^ x') = x v y'.  [back_rewrite(21582),rewrite(21840(2))].
22032 x v (x' ^ y') = x v y'.  [back_rewrite(21454),rewrite(21840(2))].
22170 (x v y) ^ (x v (z' ^ y)') = x v (z ^ y).  [back_rewrite(20765),rewrite(21840(4),21476(7),21904(4))].
22231 (x' ^ y')' = y v x.  [back_rewrite(19786),rewrite(21840(5),17(7),18093(7))].
26267 (x' ^ y)' = y' v x.  [para(301(a,1),22231(a,1,1,2))].
26294 (x v y) ^ (x' v y) = y.  [para(22231(a,1),19821(a,1,2)),rewrite(4(4))].
26646 (x v y) ^ (x v (y' v z)) = x v (z ^ y).  [back_rewrite(22170),rewrite(26267(4))].
31281 x v (y ^ x') = x v y.  [para(301(a,1),22013(a,1,2,1)),rewrite(301(5))].
31337 x v (x' ^ y) = x v y.  [para(301(a,1),22032(a,1,2,2)),rewrite(301(5))].
31523 (x' v y) ^ (x v ((z ^ x') v y)) = (z ^ x') v y.  [para(101(a,1),26294(a,1,2)),rewrite(4(7))].
31730 x v ((y ^ x') v z) = x v (y v z).  [para(31281(a,1),3(a,1,1)),rewrite(3(2)),flip(a)].
31763 (x ^ y') v z = (y' v z) ^ (y v (x v z)).  [back_rewrite(31523),rewrite(31730(6)),flip(a)].
31966 x v (y ^ (x' ^ z)) = x v (y ^ z).  [para(17(a,1),31337(a,1,2))].
31987 x v (y ^ ((x' v z) ^ u)) = x v (y ^ u).  [para(145(a,1),31337(a,1,2)),rewrite(31966(4)),flip(a)].
32647 x ^ (y v ((y v z) ^ u)) = x ^ ((y v u) ^ (y v z)).  [para(4(a,1),775(a,2,2,2)),rewrite(775(6),20473(7))].
32649 x v ((x v y) ^ z) = (x v z) ^ (x v y).  [para(26(a,1),775(a,2)),rewrite(2(8),228(8),7442(7),20474(6),17(7),8658(6),32647(5),48(5)),flip(a)].
32663 x ^ (y v (z ^ u)) = x ^ ((y v z) ^ (y v u)).  [para(20308(a,1),775(a,2,2,2)),rewrite(21840(3),31763(5),5(9),31987(11),32649(8),32649(6),4(8),850(8),26646(5),20473(6))].
32906 x v (y ^ z) = (x v y) ^ (x v z).  [back_rewrite(21193),rewrite(32663(5),17(6),95(6)),flip(a)].
33497 $F # answer(distributivity).  [back_rewrite(13),rewrite(32906(7),2(5),7(5),2(6),32906(6),2(4),2(7),20(9)),xx(a)].

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

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

Given=716. Generated=552985. Kept=33494. proofs=1.
Usable=152. Sos=3190. Demods=2561. Limbo=591, Disabled=29572. Hints=0.
Weight_deleted=18869. Literals_deleted=0.
Forward_subsumed=493879. Back_subsumed=98.
Sos_limit_deleted=6742. Sos_displaced=0. Sos_removed=0.
New_demodulators=27358 (6 lex), Back_demodulated=29461. Back_unit_deleted=0.
Demod_attempts=10338615. Demod_rewrites=2585980.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=668044. Nonunit_bsub_feature_tests=74329.
Megabytes=24.43.
User_CPU=16.05, System_CPU=0.16, Wall_clock=17.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 4013 exit (max_proofs) Wed Nov 22 11:27:25 2006