============================== Prover9 ===============================
Prover9 (32) version August-2006A, August 2006.
Process 11505 was started by mccune on cleo.thornwood,
Sat Aug 12 21:02:47 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).  [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): 5705 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): 5798 (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): 5862 (x v y)' ^ ((z ^ y) v x) = 0.  [para(3507(a,1),4(a,1)),flip(a)].

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

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

given #335 (T,wt=11): 5942 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): 5963 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): 6758 x v (y v x)' != 1 | (x v y)' = x'.  [para(2(a,1),152(a,1,2,1))].

given #370 (T,wt=12): 6895 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): 6899 x ^ (y ^ x)' != 0 | (x ^ y)' = x'.  [para(4(a,1),204(a,1,2,1))].

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

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

given #375 (T,wt=12): 6952 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): 6960 x ^ (x' v y) != 0 | (y v x')' = x.  [para(2(a,1),306(a,1,2))].

given #378 (F,wt=12): 6962 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): 6963 x ^ (y ^ x)' != 0 | x ^ y = x.  [para(4(a,1),311(a,1,2,1))].

given #380 (T,wt=12): 6966 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): 6968 (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): 6978 x' ^ (x v y) != 0 | y v x = x.  [para(2(a,1),326(a,1,2))].

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

given #385 (T,wt=12): 6987 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): 6993 (x ^ y) v x' != 1 | y ^ x = x.  [para(4(a,1),336(a,1,1))].

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

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

given #390 (T,wt=12): 7001 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): 7003 x v (x' ^ y) != 1 | (y ^ x')' = x.  [para(4(a,1),416(a,1,2))].

given #393 (F,wt=12): 7004 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): 7005 x v (y v x)' != 1 | x v y = x.  [para(2(a,1),418(a,1,2,1))].

given #395 (T,wt=12): 7034 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): 7036 (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): 7040 (x v y) ^ x' != 0 | y v x = x.  [para(2(a,1),427(a,1,1))].

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

given #400 (T,wt=12): 7044 (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): 7060 x' ^ (y v x) != 0 | x v y = x.  [para(2(a,1),1317(a,1,2))].

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

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

given #405 (T,wt=12): 7269 x' ^ (x v y) != 0 | (y v x)' = x'.  [para(301(a,1),6960(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): 7289 (x v y) ^ y' != 0 | y v x = y.  [para(2(a,1),6968(a,1,1))].

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

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

given #410 (T,wt=12): 7515 (x ^ y) v y' != 1 | y ^ x = y.  [para(4(a,1),7036(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)].

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 117 (0.00 of 6.52 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): 10451 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): 10465 x v (x' v y)' = x.  [hyper(6978,a,10451,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): 10475 x v (y v x')' = x.  [para(2(a,1),10465(a,1,2,1))].

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

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

given #535 (T,wt=9): 10480 x v (y v (x' v z))' = x.  [para(15(a,1),10465(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): 10481 x ^ (x' v y)' = (x' v y)'.  [para(10465(a,1),18(a,1,2)),rewrite(4(4))].

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

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

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

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): 10489 x v (y ^ (x' v z)')' = 1.  [para(10465(a,1),627(a,1,2)),rewrite(2(6))].

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

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

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

low water: id=6717, wt=24

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): 10538 x v (y v (z v x'))' = x.  [para(185(a,1),10465(a,1,2,1))].

low water: id=7266, wt=23

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

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

given #550 (T,wt=9): 10613 (x v y')' ^ (z v y)' = 0.  [para(10475(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): 10615 x v ((y v x')' ^ z)' = 1.  [para(10475(a,1),623(a,1,2)),rewrite(2(6))].

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

low water: id=8273, wt=21

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

given #555 (T,wt=9): 10624 x v ((y v x')' ^ z) = x.  [para(10475(a,1),200(a,1,2)),rewrite(2(5),10475(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): 10645 x v (y ^ (z v x')') = x.  [para(10475(a,1),907(a,1,2)),rewrite(2(5),10475(9))].

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

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

given #560 (T,wt=9): 10696 (x v y)' ^ (z v x')' = 0.  [para(10485(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): 10698 x' v ((x v y)' ^ z)' = 1.  [para(10485(a,1),623(a,1,2)),rewrite(2(6))].

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

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

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

low water: id=8671, wt=20

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): 10729 x' v (y ^ (x v z)') = x'.  [para(10485(a,1),907(a,1,2)),rewrite(2(5),10485(9))].

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

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

low water: id=9729, wt=19

given #570 (T,wt=7): 11929 x' ^ (x ^ y)' = x'.  [para(10781(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): 12012 x' ^ (y ^ x)' = x'.  [para(4(a,1),11929(a,1,2,1))].

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

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

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

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): 10786 x' v (y ^ x)' = (y ^ x)'.  [para(24(a,1),10612(a,1,2,1)),rewrite(2(4))].

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

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

given #580 (T,wt=9): 10796 x' v (y ^ (z v x)')' = 1.  [para(10612(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): 10806 x' v ((y v x)' ^ z) = x'.  [para(10612(a,1),200(a,1,2)),rewrite(2(5),10612(9))].

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

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

given #585 (T,wt=9): 10936 x ^ (y' v (y ^ x))' = 0.  [para(10481(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): 10983 x' ^ ((x ^ y)' v z)' = 0.  [para(10482(a,1),149(a,1,2,1)),rewrite(4(6))].

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

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

given #590 (T,wt=9): 11047 x' ^ ((y ^ x)' v z)' = 0.  [para(24(a,1),10486(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): 11300 x ^ ((x ^ y) v y')' = 0.  [para(10608(a,1),151(a,1,2))].

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

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

given #595 (T,wt=9): 11350 x' ^ ((y ^ x)' v z) = x'.  [para(10492(a,1),10608(a,1,2,1)),rewrite(4(5),10492(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): 11354 x' ^ (y v (x ^ z)')' = 0.  [para(10609(a,1),149(a,1,2,1)),rewrite(4(6))].

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

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

given #600 (T,wt=9): 11415 x' ^ (y v (z ^ x)')' = 0.  [para(24(a,1),10613(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): 11536 x' ^ (y v (z ^ x)') = x'.  [para(10619(a,1),10608(a,1,2,1)),rewrite(4(5),10619(10))].

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

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

given #605 (T,wt=9): 11746 (x v y)' ^ (x' v z)' = 0.  [para(2(a,1),10696(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): 11934 x v (x' ^ y)' = (x' ^ y)'.  [para(301(a,1),10781(a,1,1))].

low water: id=7195, wt=18

low water: id=10866, wt=17

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

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

given #610 (T,wt=9): 12014 x' ^ (y ^ (x ^ z))' = x'.  [para(17(a,1),11929(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): 12017 (x ^ y)' v (z ^ x')' = 1.  [para(11929(a,1),209(a,1,2,1,2))].

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

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

given #615 (T,wt=9): 12114 x ^ (y ^ (x' ^ z))' = x.  [para(17(a,1),12016(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): 12115 x ^ ((x v y)' ^ z)' = x.  [para(12016(a,1),20(a,1,2)),rewrite(6(2)),flip(a)].

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

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

given #620 (T,wt=9): 12120 x ^ (y v (x' ^ z)')' = 0.  [para(12016(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): 12121 x ^ ((y v x)' ^ z)' = x.  [para(12016(a,1),95(a,1,2)),rewrite(18(2)),flip(a)].

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

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

given #625 (T,wt=9): 12161 x ^ (y ^ (z ^ x'))' = x.  [para(180(a,1),12016(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): 12186 x v (y ^ x')' = (y ^ x')'.  [para(12059(a,1),24(a,1,2)),rewrite(2(4))].

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

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

given #630 (T,wt=9): 12192 x ^ ((y ^ x')' v z)' = 0.  [para(12059(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): 12193 x ^ (y v (z ^ x')')' = 0.  [para(12059(a,1),644(a,1,2)),rewrite(4(6))].

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

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

given #635 (T,wt=9): 12209 x ^ (y v (z ^ x')') = x.  [para(12059(a,1),855(a,1,2)),rewrite(4(5),12059(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): 12382 (x ^ y)' v (x' ^ z)' = 1.  [para(7(a,1),10795(a,1,2,1,1,1))].

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

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

given #640 (T,wt=9): 12992 x v (y' ^ (y v x))' = 1.  [para(11934(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): 13142 (x ^ y')' v (y ^ z)' = 1.  [para(12017(a,1),2(a,1)),flip(a)].

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

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

given #645 (T,wt=9): 13480 x v ((y v x) ^ y')' = 1.  [para(12186(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): 13646 (x' ^ (x v y))' = (y ^ x')'.  [hyper(37,a,12979,a,b,335,a),rewrite(2(7),819(8)),flip(a)].

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

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

given #650 (T,wt=9): 13731 (x' ^ (x v y))' = (x' ^ y)'.  [para(4(a,1),13646(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): 13736 (x' ^ (y v (x v y)'))' = x.  [para(29(a,1),13646(a,1,1,2)),rewrite(4(3),61(3),301(2),4(5)),flip(a)].

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

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

given #655 (T,wt=9): 13800 (x v y) ^ (x' ^ y)' = x.  [para(13646(a,1),164(a,1,2,2)),rewrite(12199(7),13731(8),301(10)),xx(a)].

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

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

given #658 (F,wt=9): 13882 (x' ^ (y v x))' = (x' ^ y)'.  [para(4(a,1),13729(a,2,1))].

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

given #660 (T,wt=9): 13913 (x v y) ^ (y' ^ x)' = y.  [para(13729(a,1),164(a,1,2,2)),rewrite(12210(7),13882(8),301(10)),xx(a)].

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

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

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

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

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

given #666 (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 #667 (F,wt=9): 14034 x ^ (x' v y) = y ^ x.  [para(13741(a,1),301(a,1,1)),rewrite(301(3)),flip(a)].

given #668 (F,wt=9): 14077 (x' v y) ^ (y ^ x)' = x'.  [para(13741(a,1),164(a,1,2,2)),rewrite(12067(6),14034(8)),xx(a)].

given #669 (T,wt=7): 14725 (x v y)' = y' ^ x'.  [para(6(a,1),14077(a,1,2,1)),rewrite(2(3),14602(3),13928(4)),flip(a)].

given #670 (T,wt=7): 14927 (x' ^ y')' = y v x.  [back_rewrite(13902),rewrite(14725(5),17(7),13146(7))].

given #671 (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 #672 (F,wt=7): 16858 (x ^ y')' = y v x'.  [para(301(a,1),14927(a,1,1,1))].

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

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

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

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

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

given #678 (F,wt=9): 14631 (x v y) ^ (x v y') = x.  [para(6(a,1),14034(a,2)),rewrite(2(4),14602(4))].

given #679 (T,wt=9): 14634 (x v y) ^ (y v x') = y.  [para(18(a,1),14034(a,2)),rewrite(2(4),14573(4))].

given #680 (T,wt=9): 14861 x v (y' ^ x') = x v y'.  [back_rewrite(14602),rewrite(14725(2))].

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

given #682 (F,wt=9): 14868 x v (x' ^ y') = x v y'.  [back_rewrite(14573),rewrite(14725(2))].

given #683 (F,wt=9): 16622 (x ^ y) v (x ^ y') = x.  [back_rewrite(12922),rewrite(14735(4))].

given #684 (T,wt=9): 16684 x ^ ((y ^ x) v y') = x.  [back_rewrite(12921),rewrite(14793(4),14614(4))].

given #685 (T,wt=9): 16875 (x v y') ^ (y v x) = x.  [para(14927(a,1),13800(a,1,2))].

given #686 (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 #687 (F,wt=9): 16877 (x v y) ^ (x' v y) = y.  [para(14927(a,1),13913(a,1,2)),rewrite(4(4))].

given #688 (F,wt=9): 17065 (x v y) ^ (y' v x) = x.  [back_rewrite(13800),rewrite(16859(4))].

given #689 (T,wt=9): 19365 (x ^ y) v (x' v y') = 1.  [back_rewrite(1503),rewrite(17179(3))].

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

given #691 (A,wt=19): 569 x ^ (y' v (z v (u ^ (x v y)))) = x ^ (y' v (z v u)).  [para(78(a,1),40(a,1,2,2,2,2)),rewrite(30(5),2(4),24(4),3(3),3(9)),flip(a)].

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

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

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

given #695 (T,wt=9): 20293 (x ^ y) v (y ^ x') = y.  [para(4(a,1),16622(a,1,1))].

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

% Proof 1 at 13.15 (+ 0.15) seconds: distributivity.
% Length of proof is 97.
% Level of proof is 24.
% Maximum clause weight is 23.
% Given clauses 695.

1 x ^ (y v z) = (x ^ y) v (x ^ z) # label(distributivity).  [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))].
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)].
24 x v (y ^ x) = x.  [para(4(a,1),7(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))].
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))].
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)].
54 x v (x v y) = x v y.  [para(27(a,1),3(a,1,1)),flip(a)].
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)].
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)].
101 x v ((y ^ x) v z) = x v z.  [para(24(a,1),3(a,1,1)),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)].
142 x ^ (x v y)' = 0.  [para(9(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].
147 x ^ ((x v y)' ^ z) = 0.  [para(82(a,1),20(a,1,2)),rewrite(91(2)),flip(a)].
149 x ^ (y v x)' = 0.  [para(2(a,1),142(a,1,2,1))].
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))].
157 x ^ (y ^ (z v (x ^ y))') = 0.  [para(149(a,1),5(a,1)),flip(a)].
164 x v (y ^ (x ^ y)') != 1 | y ^ (x ^ y)' = x'.  [para(32(a,1),10(b,1)),flip(c),xx(b)].
190 x v (x ^ y)' = 1.  [para(8(a,1),22(a,1,2)),rewrite(88(2)),flip(a)].
198 x v (y v ((x ^ z) v y)') = 1.  [para(29(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))].
298 x v y != 1 | x ^ y != 0 | y' = x.  [para(4(a,1),34(b,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))].
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))].
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))].
819 x' ^ (x v (y ^ x')) = x' ^ (x v y).  [para(27(a,1),46(a,1,2,2,2))].
1365 x v ((x ^ y) v (x ^ z))' = 1.  [para(198(a,1),22(a,1)),flip(a)].
2817 x' ^ (x v (y ^ (x' v z))) = x' ^ (x v y).  [para(54(a,1),110(a,1,2,2,2))].
6978 x' ^ (x v y) != 0 | y v x = x.  [para(2(a,1),326(a,1,2))].
10451 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)].
10465 x v (x' v y)' = x.  [hyper(6978,a,10451,a),rewrite(2(4))].
10475 x v (y v x')' = x.  [para(2(a,1),10465(a,1,2,1))].
10485 x' v (x v y)' = x'.  [para(301(a,1),10465(a,1,2,1,1))].
10612 x' v (y v x)' = x'.  [para(301(a,1),10475(a,1,2,1,2))].
10693 x' ^ (x v y)' = (x v y)'.  [para(10485(a,1),18(a,1,2)),rewrite(4(4))].
10781 x' v (x ^ y)' = (x ^ y)'.  [para(7(a,1),10612(a,1,2,1)),rewrite(2(4))].
11693 x ^ (y v (x ^ y'))' = 0.  [para(10693(a,1),157(a,1,2))].
11929 x' ^ (x ^ y)' = x'.  [para(10781(a,1),6(a,1,2))].
11934 x v (x' ^ y)' = (x' ^ y)'.  [para(301(a,1),10781(a,1,1))].
12012 x' ^ (y ^ x)' = x'.  [para(4(a,1),11929(a,1,2,1))].
12067 x v ((x' v y) ^ (z ^ x)') = 1.  [para(12012(a,1),215(a,1,2,1)),rewrite(301(7),2(6))].
12922 (x ^ y) v (x ^ (x ^ y)') = x.  [hyper(298,a,1365,a,b,11693,a),rewrite(301(7))].
12979 x v (y' ^ (x v y))' = 1.  [para(11934(a,1),208(a,1,2))].
13646 (x' ^ (x v y))' = (y ^ x')'.  [hyper(37,a,12979,a,b,335,a),rewrite(2(7),819(8)),flip(a)].
13730 ((x v y) ^ x')' = (y ^ x')'.  [para(4(a,1),13646(a,1,1))].
13741 (x ^ (x' v y))' = (y ^ x)'.  [para(301(a,1),13646(a,1,1,1)),rewrite(301(6))].
13928 (x v y) ^ x' = y ^ x'.  [para(13730(a,1),301(a,1,1)),rewrite(301(4)),flip(a)].
14034 x ^ (x' v y) = y ^ x.  [para(13741(a,1),301(a,1,1)),rewrite(301(3)),flip(a)].
14077 (x' v y) ^ (y ^ x)' = x'.  [para(13741(a,1),164(a,1,2,2)),rewrite(12067(6),14034(8)),xx(a)].
14380 ((x ^ y) v z) ^ y' = z ^ y'.  [para(101(a,1),13928(a,1,1)),rewrite(13928(3)),flip(a)].
14735 x ^ (x ^ y)' = x ^ y'.  [para(14077(a,1),95(a,1,2)),flip(a)].
16622 (x ^ y) v (x ^ y') = x.  [back_rewrite(12922),rewrite(14735(4))].
20293 (x ^ y) v (y ^ x') = y.  [para(4(a,1),16622(a,1,1))].
21099 (x ^ y) v (x ^ (z ^ y')) = x ^ (y v z).  [para(83(a,1),20293(a,1,1)),rewrite(5(5),13928(4))].
21127 (x ^ y) v (x ^ z) = x ^ (y v z).  [para(733(a,1),20293(a,1,1)),rewrite(14380(6),5(4),21099(5)),flip(a)].
21128 $F # answer(distributivity).  [resolve(21127,a,13,a)].

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

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

Given=695. Generated=534647. Kept=21125. proofs=1.
Usable=188. Sos=3747. Demods=2947. Limbo=37, Disabled=17163. Hints=0.
Weight_deleted=18349. Literals_deleted=0.
Forward_subsumed=476166. Back_subsumed=83.
Sos_limit_deleted=19007. Sos_displaced=2337. Sos_removed=0.
New_demodulators=17717 (6 lex), Back_demodulated=14730. Back_unit_deleted=0.
Demod_attempts=9924559. Demod_rewrites=2503304.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=276905. Nonunit_bsub_feature_tests=59964.
Megabytes=11.77.
User_CPU=13.15, System_CPU=0.15, Wall_clock=13.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 11505 exit (max_proofs) Sat Aug 12 21:03:00 2006