============================== Prover9 ===============================
Prover9 (32) version August-2006A, August 2006.
Process 10727 was started by mccune on cleo.thornwood,
Sat Aug 12 20:58:18 2006
The command was "/home/mccune/bin/prover9 -f BA3.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file BA3.in

assign(new_constants,1).
assign(max_weight,25).

formulas(sos).
x v (y v z) = y v (x v z).
x ^ y = (x' v y')'.
x v x' = y v y'.
(x v y') ^ (x v y) = x.
end_of_list.
set(restrict_denials).

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

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

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

% Formulas that are not ordinary clauses:
1 x ^ (y v z) = (x ^ y) v (x ^ z) # answer(distributivity_1).  [goal].

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

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

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
x v (y v z) = y v (x v z).  [assumption].
x ^ y = (x' v y')'.  [assumption].
x v x' = y v y'.  [assumption].
(x v y') ^ (x v y) = x.  [assumption].
(c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity_1).  [deny(1)].
end_of_list.

formulas(demodulators).
end_of_list.

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

No predicates eliminated.

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

Auto_denials:  (no changes).

Term ordering decisions:
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ c1, c2, c3, v, ^, ' ]).
After inverse_order:  (no changes).
Unfolding symbols: ^/2.

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).

Auto_process settings:  (no changes).

NOTE: New constant: x v x' = c_0.  [new_symbol(4)].
NOTE: New Function symbol precedence:  lex([ c1, c2, c3, c_0, v, ^, ' ]).

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

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

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
2 x v (y v z) = y v (x v z).  [assumption].
3 x ^ y = (x' v y')'.  [assumption].
6 ((x v y')' v (x v y)')' = x.  [copy(5),rewrite(3(4))].
8 (c1' v (c2 v c3)')' != (c1' v c2')' v (c1' v c3')' # answer(distributivity_1).  [copy(7),rewrite(3(3),3(9),3(18)),flip(a)].
9 x v x' = c_0.  [new_symbol(4)].
end_of_list.

formulas(demodulators).
2 x v (y v z) = y v (x v z).  [assumption].
        % (lex-dep)
3 x ^ y = (x' v y')'.  [assumption].
6 ((x v y')' v (x v y)')' = x.  [copy(5),rewrite(3(4))].
9 x v x' = c_0.  [new_symbol(4)].
end_of_list.

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

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

% Starting search at 0.00 seconds.

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

given #2 (I,wt=10): 3 x ^ y = (x' v y')'.  [assumption].

given #3 (I,wt=13): 6 ((x v y')' v (x v y)')' = x.  [copy(5),rewrite(3(4))].

given #4 (I,wt=0): 8 (c1' v (c2 v c3)')' != (c1' v c2')' v (c1' v c3')' # answer(distributivity_1).  [copy(7),rewrite(3(3),3(9),3(18)),flip(a)].

given #5 (I,wt=6): 9 x v x' = c_0.  [new_symbol(4)].

given #6 (A,wt=15): 10 x v (y v (z v u)) = z v (x v (y v u)).  [para(2(a,1),2(a,1,2))].

given #7 (F,wt=10): 15 x v (y v x') = y v c_0.  [para(9(a,1),2(a,1,2)),flip(a)].

given #8 (F,wt=10): 16 (c_0' v (x v x)')' = x.  [para(9(a,1),6(a,1,1,1,1))].

given #9 (T,wt=11): 41 (c_0' v (x v x)') v x = c_0.  [para(16(a,1),9(a,1,2))].

given #10 (T,wt=12): 17 ((x v x'')' v c_0')' = x.  [para(9(a,1),6(a,1,1,2,1))].

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

given #12 (F,wt=13): 39 (x v (c_0' v (x v x))')' = c_0'.  [para(16(a,1),6(a,1,1,1))].

given #13 (F,wt=13): 58 ((x v x'')' v c_0') v x = c_0.  [para(17(a,1),9(a,1,2))].

given #14 (T,wt=13): 73 (x v (x v (c_0' v x))')' = c_0'.  [para(16(a,1),11(a,1,1,1))].

given #15 (T,wt=14): 18 ((x v y')' v (x v y)') v x = c_0.  [para(6(a,1),9(a,1,2))].

given #16 (A,wt=21): 12 ((x v y)' v (x v ((y v z')' v (y v z)'))')' = x.  [para(6(a,1),6(a,1,1,1,1,2))].

given #17 (F,wt=14): 25 x v (y v (z v x')) = y v (z v c_0).  [para(9(a,1),10(a,1,2,2)),flip(a)].

given #18 (F,wt=14): 82 (x v (c_0' v (x v x))') v c_0' = c_0.  [para(39(a,1),9(a,1,2))].

given #19 (T,wt=14): 88 (c_0'' v (c_0'' v c_0)')' = c_0'.  [para(15(a,1),39(a,1,1,2,1))].

given #20 (T,wt=14): 105 (x v (x v (c_0' v x))') v c_0' = c_0.  [para(73(a,1),9(a,1,2))].

given #21 (A,wt=19): 13 (x v (x v ((x v y')' v y))')' = (x v y')'.  [para(6(a,1),6(a,1,1,1)),rewrite(2(5))].

given #22 (F,wt=15): 20 x v (y v (z v u)) = z v (y v (x v u)).  [para(10(a,1),2(a,1))].

given #23 (F,wt=15): 22 x v (y v (z v u)) = x v (z v (y v u)).  [para(10(a,2),2(a,1))].

given #24 (T,wt=15): 40 ((c_0' v (x v x)'')' v x)' = c_0'.  [para(16(a,1),6(a,1,1,2))].

given #25 (T,wt=15): 44 (c_0' v (x v x)') v (y v x) = y v c_0.  [para(16(a,1),15(a,1,2,2))].

given #26 (A,wt=21): 14 (((x v y')' v (x v y)'')' v x)' = (x v y')'.  [para(6(a,1),6(a,1,1,2))].

given #27 (F,wt=15): 54 (c_0' v (x' v x')') v c_0 = x v c_0.  [para(41(a,1),15(a,1,2)),flip(a)].

given #28 (F,wt=15): 80 (c_0' v (x v (c_0' v (x v x)))')' = x.  [para(39(a,1),6(a,1,1,1))].

given #29 (T,wt=15): 90 (c_0' v (c_0' v (x v (x v x)))')' = x.  [para(39(a,1),11(a,1,1,1))].

given #30 (T,wt=15): 103 (c_0' v (x v (x v (c_0' v x)))')' = x.  [para(73(a,1),6(a,1,1,1))].

given #31 (A,wt=19): 19 x v (y v (z v (u v v))) = z v (x v (u v (y v v))).  [para(10(a,1),2(a,1,2))].

given #32 (F,wt=15): 154 (x v (c_0' v (x v x))') v c_0 = c_0 v c_0.  [para(82(a,1),15(a,1,2)),flip(a)].

given #33 (F,wt=11): 314 x v (c_0' v (x v x))' = c_0.  [para(154(a,1),6(a,1,1,2,1)),rewrite(82(9),16(8)),flip(a)].

given #34 (T,wt=11): 322 x v (x v (c_0' v x))' = c_0.  [para(2(a,1),314(a,1,2,1))].

given #35 (T,wt=12): 328 (c_0' v (x v x)) v c_0 = x v c_0.  [para(314(a,1),15(a,1,2))].

given #36 (A,wt=19): 21 x v (y v (z v (u v v))) = u v (x v (y v (z v v))).  [para(10(a,2),2(a,1,2))].

given #37 (F,wt=12): 329 c_0'' v (c_0'' v c_0)' = c_0.  [para(15(a,1),314(a,1,2,1))].

given #38 (F,wt=12): 338 (x v (c_0' v x)) v c_0 = x v c_0.  [para(322(a,1),15(a,1,2))].

given #39 (T,wt=13): 353 (c_0'' v c_0) v c_0 = c_0'' v c_0.  [para(15(a,1),328(a,1,1))].

given #40 (T,wt=15): 315 c_0 v (x v (y v c_0)) = x v (y v (c_0 v c_0)).  [para(154(a,1),10(a,1,2,2)),rewrite(314(11)),flip(a)].

given #41 (A,wt=21): 23 ((x v (y v (z v u))')' v (z v (x v (y v u)))')' = x.  [para(10(a,1),6(a,1,1,2,1))].

given #42 (F,wt=15): 320 x v (y v (c_0' v (x v x))') = y v c_0.  [para(314(a,1),2(a,1,2)),flip(a)].

given #43 (F,wt=15): 335 x v (y v (x v (c_0' v x))') = y v c_0.  [para(322(a,1),2(a,1,2)),flip(a)].

given #44 (T,wt=16): 34 ((x v (y v x')')' v (y v c_0)')' = x.  [para(15(a,1),6(a,1,1,2,1))].

given #45 (T,wt=16): 37 (c_0' v (x v ((x v y) v y))')' = x v y.  [para(2(a,1),16(a,1,1,2,1))].

given #46 (A,wt=21): 24 ((x v (y v (z v u))')' v (y v (z v (x v u)))')' = x.  [para(10(a,2),6(a,1,1,2,1))].

given #47 (F,wt=9): 486 c_0'' v c_0 = c_0''.  [para(353(a,1),37(a,1,1,2,1,2,1)),rewrite(353(14),2(13),353(12),159(14),353(10)),flip(a)].

given #48 (F,wt=13): 500 c_0'' v (x v c_0) = x v c_0''.  [back_rewrite(393),rewrite(486(5),486(11))].

given #49 (T,wt=14): 515 c_0' v (c_0'' v (x v c_0)) = x v c_0.  [para(500(a,2),15(a,1,2))].

given #50 (T,wt=14): 554 c_0'' v (x v (c_0' v c_0)) = x v c_0.  [para(515(a,1),10(a,2))].

given #51 (A,wt=23): 26 x v (y v (z v (u v (v v w)))) = u v (x v (y v (v v (z v w)))).  [para(10(a,1),10(a,1,2,2))].

given #52 (F,wt=15): 508 (c_0' v (c_0 v c_0)') v c_0'' = c_0''.  [para(486(a,1),44(a,1,2)),rewrite(486(16))].

given #53 (F,wt=12): 585 (c_0' v c_0''')'' = c_0'.  [para(508(a,1),34(a,1,1,1,1,2,1)),rewrite(41(17),479(11))].

given #54 (T,wt=10): 587 (c_0' v c_0''')' = c_0.  [para(585(a,1),9(a,1,2)),rewrite(479(11))].

given #55 (T,wt=11): 592 (c_0' v c_0''') v c_0 = c_0.  [para(587(a,1),9(a,1,2))].

given #56 (A,wt=19): 27 x v (y v (z v (u v v))) = u v (x v (z v (y v v))).  [para(10(a,1),10(a,1,2))].

given #57 (F,wt=15): 525 (c_0'' v (x v c_0))' = (x v c_0'')'.  [para(500(a,2),13(a,2,1)),rewrite(13(12)),flip(a)].

given #58 (F,wt=15): 591 ((c_0' v c_0'''')' v c_0)' = c_0'.  [para(587(a,1),6(a,1,1,2))].

given #59 (T,wt=15): 593 (c_0' v c_0''') v (x v c_0) = x v c_0.  [para(587(a,1),15(a,1,2,2))].

given #60 (T,wt=15): 601 (c_0''' v (c_0' v c_0)')' = c_0''.  [para(587(a,1),34(a,1,1,1,1,2)),rewrite(486(5))].

given #61 (A,wt=23): 28 x v (y v (z v (u v (v v w)))) = v v (x v (y v (z v (u v w)))).  [para(10(a,2),10(a,1,2,2))].

given #62 (F,wt=15): 605 (c_0' v c_0''') v c_0'' = c_0''.  [para(592(a,1),500(a,1,2)),rewrite(486(5)),flip(a)].

given #63 (F,wt=16): 124 ((c_0' v (x v x)'')' v x) v c_0' = c_0.  [para(16(a,1),18(a,1,1,2))].

given #64 (T,wt=13): 670 (c_0' v (x v x)'')' v x = c_0.  [para(124(a,1),6(a,1,1,1,1)),rewrite(253(12),16(8)),flip(a)].

given #65 (T,wt=16): 130 (c_0' v (x v (c_0' v (x v x)))') v x = c_0.  [para(39(a,1),18(a,1,1,1))].

given #66 (A,wt=19): 29 x v (y v (z v (u v v))) = y v (x v (u v (z v v))).  [para(10(a,2),10(a,1,2))].

given #67 (F,wt=16): 133 (c_0' v (x v (x v (c_0' v x)))') v x = c_0.  [para(73(a,1),18(a,1,1,1))].

given #68 (F,wt=16): 273 (c_0' v (c_0' v (x v (x v x)))') v x = c_0.  [para(90(a,1),9(a,1,2))].

given #69 (T,wt=16): 451 (c_0' v (x v x)) v (y v c_0) = x v (y v c_0).  [para(320(a,1),25(a,1,2))].

given #70 (T,wt=8): 736 c_0 v (c_0' v c_0) = c_0.  [para(451(a,1),37(a,1,1,2,1,2)),rewrite(2(10),2(9),103(13),2(7)),flip(a)].

given #71 (A,wt=23): 30 x v (y v (z v (u v (v v w)))) = z v (x v (v v (y v (u v w)))).  [para(10(a,1),10(a,2,2,2))].

given #72 (F,wt=7): 747 c_0'' = c_0 v c_0.  [para(736(a,1),44(a,1,2)),rewrite(2(11),567(15))].

given #73 (F,wt=9): 755 (c_0 v c_0) v c_0 = c_0 v c_0.  [para(736(a,1),554(a,1,2)),rewrite(747(3))].

given #74 (T,wt=12): 738 c_0 v (x v (c_0' v c_0)) = x v c_0.  [para(736(a,1),2(a,1,2)),flip(a)].

given #75 (T,wt=12): 741 c_0' v (x v (c_0 v c_0)) = x v c_0.  [para(736(a,1),10(a,1,2)),flip(a)].

given #76 (A,wt=19): 31 x v (y v (z v (u v v))) = z v (u v (x v (y v v))).  [para(10(a,1),10(a,2,2))].

given #77 (F,wt=12): 742 c_0 v (c_0' v (x v c_0)) = x v c_0.  [para(736(a,1),10(a,2,2))].

given #78 (F,wt=12): 876 ((c_0 v (c_0 v c_0))' v c_0')' = c_0.  [para(747(a,1),17(a,1,1,1,1,2))].

given #79 (T,wt=13): 823 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0).  [back_rewrite(545),rewrite(747(3),747(13),2(14),338(13))].

given #80 (T,wt=13): 834 (c_0 v (x v c_0))' = (x v (c_0 v c_0))'.  [back_rewrite(525),rewrite(747(3),823(6),747(8))].

given #81 (A,wt=23): 32 x v (y v (z v (u v (v v w)))) = z v (x v (u v (v v (y v w)))).  [para(10(a,2),10(a,2,2,2))].

given #82 (F,wt=13): 877 ((c_0 v (c_0 v c_0))' v c_0') v c_0 = c_0.  [para(747(a,1),58(a,1,1,1,1,2))].

given #83 (F,wt=14): 739 ((c_0 v (c_0' v c_0)')' v c_0')' = c_0.  [para(736(a,1),6(a,1,1,2,1))].

given #84 (T,wt=14): 787 (x v (c_0 v c_0)) v (c_0 v (x v c_0))' = c_0.  [back_rewrite(628),rewrite(747(3),747(7),779(11))].

given #85 (T,wt=14): 814 (c_0 v c_0) v (x v (c_0' v c_0)) = x v c_0.  [back_rewrite(554),rewrite(747(3))].

given #86 (A,wt=19): 33 x v (y v (z v (u v v))) = u v (y v (x v (z v v))).  [para(10(a,2),10(a,2,2)),flip(a)].

given #87 (F,wt=14): 868 (c_0 v (x v c_0)) v (x v (c_0 v c_0))' = c_0.  [back_rewrite(788),rewrite(823(6))].

given #88 (F,wt=14): 883 (c_0' v (c_0 v (c_0 v c_0))')' = c_0 v c_0.  [para(755(a,1),37(a,1,1,2,1,2,1)),rewrite(755(10),2(9),755(8),755(15))].

given #89 (T,wt=14): 979 (c_0 v c_0) v (c_0' v (x v c_0)) = x v c_0.  [para(2(a,1),814(a,1,2))].

given #90 (T,wt=15): 744 ((c_0 v (c_0' v c_0)')' v c_0') v c_0 = c_0.  [para(736(a,1),18(a,1,1,2,1))].

given #91 (A,wt=18): 35 ((x v y')' v (x v y)') v (z v x) = z v c_0.  [para(6(a,1),15(a,1,2,2))].

given #92 (F,wt=15): 796 ((c_0 v c_0)' v (c_0' v c_0)')' = c_0 v c_0.  [back_rewrite(601),rewrite(747(3),747(14))].

given #93 (F,wt=15): 841 ((c_0 v (x v c_0))' v (x v c_0')')' = x.  [back_rewrite(514),rewrite(747(3),823(6))].

given #94 (T,wt=11): 1039 c_0' v (c_0' v c_0')' = c_0.  [para(41(a,1),841(a,1,1,2,1)),rewrite(54(12),876(10)),flip(a)].

given #95 (T,wt=12): 1057 (c_0' v c_0') v c_0 = c_0' v c_0.  [para(1039(a,1),15(a,1,2))].

given #96 (A,wt=18): 36 x v (y v (z v (u v x'))) = y v (z v (u v c_0)).  [para(15(a,1),10(a,1,2,2)),flip(a)].

given #97 (F,wt=13): 1052 (c_0' v (c_0' v c_0')'')' = c_0.  [para(670(a,1),841(a,1,1,2,1)),rewrite(687(14),1039(10),876(10)),flip(a)].

given #98 (F,wt=14): 1044 (c_0' v x')' v (c_0' v x)' = c_0.  [para(18(a,1),841(a,1,1,2,1)),rewrite(121(13),876(10)),flip(a)].

given #99 (T,wt=14): 1090 (c_0' v (c_0' v c_0')'') v c_0 = c_0.  [para(1052(a,1),9(a,1,2))].

given #100 (T,wt=15): 875 ((x v (c_0 v c_0))' v (x v c_0')')' = x.  [para(747(a,1),6(a,1,1,1,1,2))].

given #101 (A,wt=18): 38 ((x v y)' v (x v (c_0' v (y v y)'))')' = x.  [para(16(a,1),6(a,1,1,1,1,2))].

given #102 (F,wt=15): 975 (c_0 v (x v c_0)) v c_0 = (x v (c_0 v c_0)) v c_0.  [para(787(a,1),15(a,1,2))].

given #103 (F,wt=15): 1055 c_0' v (x v (c_0' v c_0')') = x v c_0.  [para(1039(a,1),2(a,1,2)),flip(a)].

given #104 (T,wt=15): 1104 (c_0' v x')' v c_0 = (c_0' v x) v c_0.  [para(1044(a,1),15(a,1,2)),flip(a)].

given #105 (T,wt=9): 1241 c_0' v (c_0' v c_0) = c_0.  [back_rewrite(1188),rewrite(1204(21),2(20),1189(19))].

given #106 (A,wt=22): 42 (c_0' v (x v (y v ((y v (x v z)) v z)))')' = y v (x v z).  [para(10(a,1),16(a,1,1,2,1)),rewrite(2(6))].

given #107 (F,wt=5): 1264 c_0 v c_0 = c_0.  [para(1241(a,1),14(a,1,1,1,1,2,1,1)),rewrite(1262(6),16(8),747(4),1263(5),1204(6),1262(4),1262(9),16(11))].

given #108 (F,wt=5): 1348 c_0'' = c_0.  [back_rewrite(747),rewrite(1264(6))].

given #109 (T,wt=6): 1312 c_0' v c_0 = c_0.  [back_rewrite(1262),rewrite(1264(7))].

given #110 (T,wt=8): 1292 (c_0' v c_0')' = c_0.  [back_rewrite(1204),rewrite(1262(10),1264(9))].

given #111 (A,wt=22): 43 (c_0' v (x v (y v ((x v (y v z)) v z)))')' = x v (y v z).  [para(10(a,2),16(a,1,1,2,1))].

given #112 (F,wt=9): 1297 (c_0' v c_0') v c_0 = c_0.  [back_rewrite(1057),rewrite(1262(11),1264(10))].

given #113 (F,wt=9): 1302 c_0 v (x v c_0) = x v c_0.  [back_rewrite(814),rewrite(1264(3),1262(5),1264(4))].

given #114 (T,wt=10): 1282 c_0' v (x v c_0) = x v c_0.  [back_rewrite(1259),rewrite(1262(6),1264(5))].

given #115 (T,wt=11): 1371 x v ((x v c_0) v c_0) = x v c_0.  [para(1282(a,1),103(a,1,1,2,1,2,2)),rewrite(2(9),2(10),1357(13))].

given #116 (A,wt=17): 45 x v ((c_0' v (x v ((x v y) v y))') v y) = c_0.  [para(41(a,1),2(a,1)),rewrite(2(6)),flip(a)].

given #117 (F,wt=12): 1372 (c_0' v (x v c_0)')' = x v c_0.  [para(1282(a,1),37(a,1,1,2,1,2,1)),rewrite(2(9),1371(9),1282(7),1282(12))].

given #118 (F,wt=12): 1425 ((x v c_0)' v c_0')' = x v c_0.  [para(1372(a,1),34(a,1,1,1,1,2)),rewrite(2(5),1371(5),1312(7))].

given #119 (T,wt=13): 1303 c_0 v (x v (y v c_0)) = x v (y v c_0).  [back_rewrite(808),rewrite(1264(3),1262(5),1264(4))].

given #120 (T,wt=13): 1342 ((x v c_0)' v (x v c_0')')' = x.  [back_rewrite(875),rewrite(1264(3))].

given #121 (A,wt=23): 46 (((c_0' v (x v x)') v x')' v c_0')' = c_0' v (x v x)'.  [para(41(a,1),6(a,1,1,2,1))].

given #122 (F,wt=13): 1351 (c_0' v c_0') v (x v c_0) = x v c_0.  [back_rewrite(1184),rewrite(1282(13))].

given #123 (F,wt=13): 1373 x v ((c_0' v (x v c_0)') v c_0) = c_0.  [para(1282(a,1),133(a,1,1,2,1,2,2)),rewrite(2(9),1371(9),2(7),1371(7),2(9))].

given #124 (T,wt=7): 1488 (x v c_0) v c_0 = c_0.  [back_rewrite(1416),rewrite(1471(12))].

given #125 (T,wt=5): 1511 x v c_0 = c_0.  [back_rewrite(1445),rewrite(1493(11),1450(11)),flip(a)].

given #126 (A,wt=25): 60 ((x v y)' v (x v ((y v (z v u)')' v (z v (y v u))'))')' = x.  [para(11(a,1),6(a,1,1,1,1,2))].

given #127 (F,wt=5): 1685 x'' = x.  [back_rewrite(1635),rewrite(1677(3),1662(8),1511(3),1677(4))].

given #128 (F,wt=5): 1701 x v x = x.  [back_rewrite(1606),rewrite(1677(5),1685(3))].

given #129 (T,wt=5): 1702 c_0 v x = c_0.  [back_rewrite(1597),rewrite(1677(6),1685(4))].

given #130 (T,wt=6): 1677 x v c_0' = x.  [back_rewrite(1526),rewrite(1634(11))].

% Operation v is commutative; C redundancy checks enabled.

given #131 (A,wt=25): 64 ((x v (y v (z v (u v v)))')' v (z v (x v (u v (y v v))))')' = x.  [para(10(a,1),11(a,1,1,1,1,2,1))].

given #132 (F,wt=6): 1694 c_0' v x = x.  [back_rewrite(1646),rewrite(1677(7),1685(5))].

given #133 (F,wt=7): 1800 x v y = y v x.  [para(1677(a,1),2(a,1,2)),rewrite(1677(4))].

given #134 (T,wt=8): 1666 x v (y v x') = c_0.  [back_rewrite(15),rewrite(1511(5))].

given #135 (T,wt=8): 1858 x v (x' v y) = c_0.  [back_rewrite(1687),rewrite(1801(3))].

given #136 (A,wt=25): 65 ((x v (y v (z v (u v v)))')' v (y v (u v (x v (z v v))))')' = x.  [para(10(a,1),11(a,1,1,2,1,2))].

given #137 (F,wt=9): 1750 x v (y v x')' = x.  [back_rewrite(1696),rewrite(1701(1))].

given #138 (F,wt=9): 1764 x v (y v x) = y v x.  [para(1701(a,1),2(a,1,2)),flip(a)].

given #139 (T,wt=9): 1828 x v (x v y) = x v y.  [back_rewrite(1749),rewrite(1800(2),1764(2))].

given #140 (T,wt=9): 1980 x v (x' v y)' = x.  [para(1800(a,1),1750(a,1,2,1))].

given #141 (A,wt=21): 66 ((x v (y v (z v u))')' v (z v (y v (x v u)))')' = x.  [para(10(a,1),11(a,1,1,2,1))].

given #142 (F,wt=10): 1665 x v (y v (z v x')) = c_0.  [back_rewrite(25),rewrite(1511(6),1511(6))].

given #143 (F,wt=10): 1690 x' v (y v (z v x)) = c_0.  [back_rewrite(1601),rewrite(1645(5),1677(3),1677(4))].

given #144 (T,wt=10): 1836 x v (y v (x v y)') = c_0.  [back_rewrite(1707),rewrite(1800(3))].

given #145 (T,wt=10): 1951 x v (y v (x' v z)) = c_0.  [para(1858(a,1),2(a,1,2)),rewrite(1511(2)),flip(a)].

given #146 (A,wt=25): 67 ((x v (y v (z v (u v v)))')' v (u v (x v (y v (z v v))))')' = x.  [para(10(a,2),11(a,1,1,1,1,2,1))].

given #147 (F,wt=10): 1953 x' v (y v (x v z)) = c_0.  [para(1858(a,1),10(a,1,2)),rewrite(1511(2)),flip(a)].

given #148 (F,wt=10): 1979 x' v (y v x)' = x'.  [para(1685(a,1),1750(a,1,2,1,2))].

given #149 (T,wt=8): 2114 (x v y) v y' = c_0.  [para(1979(a,1),1666(a,1,2))].

given #150 (T,wt=8): 2142 (x v y) v x' = c_0.  [para(1800(a,1),2114(a,1,1))].

given #151 (A,wt=25): 68 ((x v (y v (z v (u v v)))')' v (y v (z v (u v (x v v))))')' = x.  [para(10(a,2),11(a,1,1,2,1,2))].

given #152 (F,wt=10): 2005 x' v (x v y)' = x'.  [para(1685(a,1),1980(a,1,2,1,1))].

given #153 (F,wt=10): 2024 x v ((y v x') v z) = c_0.  [para(1800(a,1),1665(a,1,2))].

given #154 (T,wt=10): 2025 x v ((x' v y) v z) = c_0.  [para(1980(a,1),1665(a,1,2,2)),rewrite(1801(4))].

given #155 (T,wt=10): 2058 (x v (y v z)) v z' = c_0.  [para(1690(a,1),1800(a,1)),flip(a)].

given #156 (A,wt=25): 77 ((x v y)' v ((y v (z v u)')' v (x v (z v (y v u))'))')' = x.  [para(11(a,1),11(a,1,1,1,1,2))].

given #157 (F,wt=10): 2059 x' v ((y v x) v z) = c_0.  [para(1800(a,1),1690(a,1,2))].

given #158 (F,wt=10): 2104 (x v (y v z)) v y' = c_0.  [para(1953(a,1),1800(a,1)),flip(a)].

given #159 (T,wt=10): 2105 x' v ((x v y) v z) = c_0.  [para(1800(a,1),1953(a,1,2))].

given #160 (T,wt=10): 2115 (x v y) v (z v y') = c_0.  [para(1979(a,1),1665(a,1,2,2))].

given #161 (A,wt=23): 184 x v (y v (z v (u v (v v w)))) = v v (x v (y v (u v (z v w)))).  [para(20(a,1),10(a,1,2,2))].

given #162 (F,wt=10): 2143 (x v y) v (z v x') = c_0.  [para(2142(a,1),2(a,1,2)),rewrite(1511(2)),flip(a)].

given #163 (F,wt=10): 2186 (x v y) v (y' v z) = c_0.  [para(1979(a,1),2024(a,1,2,1))].

given #164 (T,wt=10): 2187 (x v y) v (x' v z) = c_0.  [para(2005(a,1),2024(a,1,2,1))].

given #165 (T,wt=10): 2227 ((x v y) v z) v y' = c_0.  [para(1800(a,1),2058(a,1,1))].

given #166 (A,wt=23): 185 x v (y v (z v (u v (v v w)))) = z v (x v (v v (u v (y v w)))).  [para(20(a,1),10(a,2,2,2))].

given #167 (F,wt=10): 2288 ((x v y) v z) v x' = c_0.  [para(1800(a,1),2104(a,1,1))].

given #168 (F,wt=11): 1698 x v (y v (z v x'))' = x.  [back_rewrite(1614),rewrite(1677(9),1685(7))].

given #169 (T,wt=11): 1801 x v (y v z) = z v (x v y).  [para(1677(a,1),10(a,1,2,2)),rewrite(1677(5))].

% Operation v is associative-commutative; CAC redundancy checks enabled.
% back CAC tautology: 1801 x v (y v z) = z v (x v y).  [para(1677(a,1),10(a,1,2,2)),rewrite(1677(5))].
% back CAC tautology: 185 x v (y v (z v (u v (v v w)))) = z v (x v (v v (u v (y v w)))).  [para(20(a,1),10(a,2,2,2))].
% back CAC tautology: 184 x v (y v (z v (u v (v v w)))) = v v (x v (y v (u v (z v w)))).  [para(20(a,1),10(a,1,2,2))].
% back CAC tautology: 33 x v (y v (z v (u v v))) = u v (y v (x v (z v v))).  [para(10(a,2),10(a,2,2)),flip(a)].
% back CAC tautology: 32 x v (y v (z v (u v (v v w)))) = z v (x v (u v (v v (y v w)))).  [para(10(a,2),10(a,2,2,2))].
% back CAC tautology: 31 x v (y v (z v (u v v))) = z v (u v (x v (y v v))).  [para(10(a,1),10(a,2,2))].
% back CAC tautology: 30 x v (y v (z v (u v (v v w)))) = z v (x v (v v (y v (u v w)))).  [para(10(a,1),10(a,2,2,2))].
% back CAC tautology: 29 x v (y v (z v (u v v))) = y v (x v (u v (z v v))).  [para(10(a,2),10(a,1,2))].
% back CAC tautology: 28 x v (y v (z v (u v (v v w)))) = v v (x v (y v (z v (u v w)))).  [para(10(a,2),10(a,1,2,2))].
% back CAC tautology: 27 x v (y v (z v (u v v))) = u v (x v (z v (y v v))).  [para(10(a,1),10(a,1,2))].
% back CAC tautology: 26 x v (y v (z v (u v (v v w)))) = u v (x v (y v (v v (z v w)))).  [para(10(a,1),10(a,1,2,2))].
% back CAC tautology: 21 x v (y v (z v (u v v))) = u v (x v (y v (z v v))).  [para(10(a,2),2(a,1,2))].
% back CAC tautology: 19 x v (y v (z v (u v v))) = z v (x v (u v (y v v))).  [para(10(a,1),2(a,1,2))].
% back CAC tautology: 22 x v (y v (z v u)) = x v (z v (y v u)).  [para(10(a,2),2(a,1))].
% back CAC tautology: 20 x v (y v (z v u)) = z v (y v (x v u)).  [para(10(a,1),2(a,1))].
% back CAC tautology: 10 x v (y v (z v u)) = z v (x v (y v u)).  [para(2(a,1),2(a,1,2))].
% back CAC tautology: 2553 x v (y v (z v (u v v))) = v v (y v (z v (x v u))).  [para(1801(a,2),33(a,2,2,2)),flip(a)].
% back CAC tautology: 2552 x v (y v (z v (u v (v v w)))) = u v (y v (x v (v v (w v z)))).  [para(1801(a,2),33(a,2,2,2,2))].
% back CAC tautology: 2549 x v (y v (z v (u v v))) = u v (y v (v v (x v z))).  [para(1801(a,1),33(a,2,2,2))].
% back CAC tautology: 2548 x v (y v (z v (u v (v v w)))) = u v (y v (x v (w v (z v v)))).  [para(1801(a,1),33(a,2,2,2,2))].
% back CAC tautology: 2546 x v (y v (z v (u v v))) = z v (y v (x v (v v u))).  [para(1801(a,2),33(a,1,2,2))].
% back CAC tautology: 2545 x v (y v (z v (u v (v v w)))) = w v (y v (x v (z v (u v v)))).  [para(1801(a,2),33(a,1,2,2,2))].
% back CAC tautology: 2542 x v (y v (z v (u v v))) = v v (y v (x v (u v z))).  [para(1801(a,1),33(a,1,2,2))].
% back CAC tautology: 2541 x v (y v (z v (u v (v v w)))) = v v (y v (x v (z v (w v u)))).  [para(1801(a,1),33(a,1,2,2,2))].
% back CAC tautology: 2535 x v (y v (z v (u v (v v w)))) = z v (x v (u v (w v (v v y)))).  [para(1801(a,1),32(a,2,2,2,2))].
% back CAC tautology: 2525 x v (y v (z v (u v v))) = v v (z v (x v (y v u))).  [para(1801(a,2),31(a,1,2,2))].
% back CAC tautology: 2524 x v (y v (z v (u v (v v w)))) = z v (w v (x v (y v (u v v)))).  [para(1801(a,2),31(a,1,2,2,2))].
% back CAC tautology: 2521 x v (y v (z v (u v v))) = u v (v v (x v (y v z))).  [para(1801(a,1),31(a,1,2,2))].
% back CAC tautology: 2520 x v (y v (z v (u v (v v w)))) = z v (v v (x v (y v (w v u)))).  [para(1801(a,1),31(a,1,2,2,2))].
% back CAC tautology: 2513 x v (y v (z v (u v (v v w)))) = z v (x v (v v (w v (y v u)))).  [para(1801(a,1),30(a,2,2,2,2))].
% back CAC tautology: 2509 x v (y v (z v (u v (v v w)))) = z v (x v (u v (y v (w v v)))).  [para(1801(a,2),30(a,1,2,2,2))].
% back CAC tautology: 2505 x v (y v (z v (u v (v v w)))) = z v (x v (w v (y v (v v u)))).  [para(1801(a,1),30(a,1,2,2,2))].
% back CAC tautology: 2501 x v (y v (z v (u v v))) = y v (x v (z v (v v u))).  [para(1801(a,2),29(a,1,2,2))].
% back CAC tautology: 2500 x v (y v (z v (u v (v v w)))) = y v (x v (w v (z v (u v v)))).  [para(1801(a,2),29(a,1,2,2,2))].
% back CAC tautology: 2497 x v (y v (z v (u v v))) = y v (x v (v v (u v z))).  [para(1801(a,1),29(a,1,2,2))].
% back CAC tautology: 2496 x v (y v (z v (u v (v v w)))) = y v (x v (v v (z v (w v u)))).  [para(1801(a,1),29(a,1,2,2,2))].
% back CAC tautology: 2484 x v (y v (z v (u v (v v w)))) = w v (x v (y v (z v (v v u)))).  [para(1801(a,1),28(a,1,2,2,2))].
% back CAC tautology: 2479 x v (y v (z v (u v (v v w)))) = u v (x v (z v (v v (w v y)))).  [para(1801(a,2),27(a,2,2,2,2))].
% back CAC tautology: 2476 x v (y v (z v (u v v))) = u v (x v (v v (z v y))).  [para(1801(a,1),27(a,2,2,2))].
% back CAC tautology: 2475 x v (y v (z v (u v (v v w)))) = u v (x v (z v (w v (y v v)))).  [para(1801(a,1),27(a,2,2,2,2))].
% back CAC tautology: 2473 x v (y v (z v (u v (v v w)))) = w v (x v (z v (y v (u v v)))).  [para(1801(a,2),27(a,1,2,2,2))].
% back CAC tautology: 2470 x v (y v (z v (u v v))) = v v (x v (u v (y v z))).  [para(1801(a,1),27(a,1,2,2))].
% back CAC tautology: 2469 x v (y v (z v (u v (v v w)))) = v v (x v (z v (y v (w v u)))).  [para(1801(a,1),27(a,1,2,2,2))].
% back CAC tautology: 2465 x v (y v (z v (u v (v v w)))) = u v (x v (y v (z v (w v v)))).  [para(1801(a,2),26(a,2,2,2,2))].
% back CAC tautology: 2461 x v (y v (z v (u v (v v w)))) = u v (x v (y v (w v (v v z)))).  [para(1801(a,1),26(a,2,2,2,2))].
% back CAC tautology: 2454 x v (y v (z v (u v (v v w)))) = v v (x v (y v (w v (z v u)))).  [para(1801(a,1),26(a,1,2,2,2))].
% back CAC tautology: 2443 x v (y v (z v (u v v))) = z v (x v (y v (v v u))).  [para(1801(a,2),19(a,2,2,2))].
% back CAC tautology: 2438 x v (y v (z v (u v v))) = u v (x v (v v (y v z))).  [para(1801(a,1),19(a,1,2,2))].
% back CAC tautology: 2436 x v (y v (z v (u v v))) = x v (v v (y v (z v u))).  [para(1801(a,2),22(a,1,2,2))].
% back CAC tautology: 2435 x v (y v (z v u)) = x v (u v (z v y)).  [para(1801(a,1),22(a,1,2))].
% back CAC tautology: 2434 x v (y v (z v (u v v))) = x v (u v (y v (v v z))).  [para(1801(a,1),22(a,1,2,2))].
% back CAC tautology: 2431 x v (y v (z v u)) = u v (z v (x v y)).  [para(1801(a,1),20(a,1,2))].
% back CAC tautology: 2395 x v (y v (z v (u v (v v w)))) = z v (x v (v v (u v (w v y)))).  [para(1800(a,1),185(a,2,2,2,2,2))].
% back CAC tautology: 2391 x v (y v (z v (u v (v v w)))) = z v (x v (w v (u v (y v v)))).  [para(1800(a,1),185(a,1,2,2,2,2))].
% back CAC tautology: 2388 x v (y v (z v (u v v))) = z v (x v (v v (u v y))).  [para(1677(a,1),185(a,1,2,2,2,2)),rewrite(1677(7))].
% back CAC tautology: 2327 x v (y v (z v (u v (v v w)))) = v v (x v (y v (u v (w v z)))).  [para(1800(a,1),184(a,2,2,2,2,2))].
% back CAC tautology: 2323 x v (y v (z v (u v (v v w)))) = w v (x v (y v (u v (z v v)))).  [para(1800(a,1),184(a,1,2,2,2,2))].
% back CAC tautology: 2320 x v (y v (z v (u v v))) = v v (x v (y v (u v z))).  [para(1677(a,1),184(a,1,2,2,2,2)),rewrite(1677(7))].
% back CAC tautology: 2317 x v (y v (z v (u v (v v w)))) = v v (u v (z v (x v (y v w)))).  [para(31(a,1),184(a,2,2))].
% back CAC tautology: 2316 x v (y v (z v (u v (v v w)))) = v v (u v (y v (z v (x v w)))).  [para(184(a,1),31(a,1))].
% back CAC tautology: 1946 x v (y v (z v (u v v))) = u v (y v (x v (v v z))).  [para(1800(a,1),33(a,2,2,2,2))].
% back CAC tautology: 1942 x v (y v (z v (u v v))) = v v (y v (x v (z v u))).  [para(1800(a,1),33(a,1,2,2,2))].
% back CAC tautology: 1937 x v (y v (z v (u v (v v w)))) = z v (x v (u v (v v (w v y)))).  [para(1800(a,1),32(a,2,2,2,2,2))].
% back CAC tautology: 1932 x v (y v (z v (u v (v v w)))) = z v (x v (u v (w v (y v v)))).  [para(1800(a,1),32(a,1,2,2,2,2))].
% back CAC tautology: 1928 x v (y v (z v (u v v))) = z v (v v (x v (y v u))).  [para(1800(a,1),31(a,1,2,2,2))].
% back CAC tautology: 1923 x v (y v (z v (u v (v v w)))) = z v (x v (v v (y v (w v u)))).  [para(1800(a,1),30(a,2,2,2,2,2))].
% back CAC tautology: 1918 x v (y v (z v (u v (v v w)))) = z v (x v (w v (y v (u v v)))).  [para(1800(a,1),30(a,1,2,2,2,2))].
% back CAC tautology: 1914 x v (y v (z v (u v v))) = y v (x v (v v (z v u))).  [para(1800(a,1),29(a,1,2,2,2))].
% back CAC tautology: 1909 x v (y v (z v (u v (v v w)))) = v v (x v (y v (z v (w v u)))).  [para(1800(a,1),28(a,2,2,2,2,2))].
% back CAC tautology: 1904 x v (y v (z v (u v (v v w)))) = w v (x v (y v (z v (u v v)))).  [para(1800(a,1),28(a,1,2,2,2,2))].
% back CAC tautology: 1900 x v (y v (z v (u v v))) = u v (x v (z v (v v y))).  [para(1800(a,1),27(a,2,2,2,2))].
% back CAC tautology: 1896 x v (y v (z v (u v v))) = v v (x v (z v (y v u))).  [para(1800(a,1),27(a,1,2,2,2))].
% back CAC tautology: 1891 x v (y v (z v (u v (v v w)))) = u v (x v (y v (v v (w v z)))).  [para(1800(a,1),26(a,2,2,2,2,2))].
% back CAC tautology: 1886 x v (y v (z v (u v (v v w)))) = u v (x v (y v (w v (z v v)))).  [para(1800(a,1),26(a,1,2,2,2,2))].
% back CAC tautology: 1871 x v (y v (z v u)) = x v (u v (y v z)).  [para(1800(a,1),22(a,1,2,2))].
% back CAC tautology: 1812 x v (y v (z v u)) = u v (y v (x v z)).  [para(1677(a,1),33(a,1,2,2,2)),rewrite(1677(6))].
% back CAC tautology: 1811 x v (y v (z v (u v v))) = z v (x v (u v (v v y))).  [para(1677(a,1),32(a,1,2,2,2,2)),rewrite(1677(7))].
% back CAC tautology: 1810 x v (y v (z v u)) = z v (u v (x v y)).  [para(1677(a,1),31(a,1,2,2,2)),rewrite(1677(6))].
% back CAC tautology: 1809 x v (y v (z v (u v v))) = z v (x v (v v (y v u))).  [para(1677(a,1),30(a,1,2,2,2,2)),rewrite(1677(7))].
% back CAC tautology: 1808 x v (y v (z v u)) = y v (x v (u v z)).  [para(1677(a,1),29(a,1,2,2,2)),rewrite(1677(6))].
% back CAC tautology: 1807 x v (y v (z v (u v v))) = v v (x v (y v (z v u))).  [para(1677(a,1),28(a,1,2,2,2,2)),rewrite(1677(7))].
% back CAC tautology: 1806 x v (y v (z v u)) = u v (x v (z v y)).  [para(1677(a,1),27(a,1,2,2,2)),rewrite(1677(6))].
% back CAC tautology: 1805 x v (y v (z v (u v v))) = u v (x v (y v (v v z))).  [para(1677(a,1),26(a,1,2,2,2,2)),rewrite(1677(7))].
% back CAC tautology: 1804 x v (y v (z v u)) = u v (x v (y v z)).  [para(1677(a,1),21(a,1,2,2,2)),rewrite(1677(6))].
% back CAC tautology: 1803 x v (y v (z v u)) = z v (x v (u v y)).  [para(1677(a,1),19(a,1,2,2,2)),rewrite(1677(6))].
% back CAC tautology: 1802 x v (y v z) = z v (y v x).  [para(1677(a,1),20(a,1,2,2)),rewrite(1677(5))].
% back CAC tautology: 966 x v (y v (z v (u v (v v w)))) = v v (z v (y v (u v (x v w)))).  [para(32(a,1),30(a,2))].
% back CAC tautology: 905 x v (y v (z v (u v (v v w)))) = u v (v v (z v (x v (y v w)))).  [para(31(a,1),26(a,2,2))].
% back CAC tautology: 874 x v (y v (z v (u v (v v w)))) = v v (z v (u v (x v (y v w)))).  [para(30(a,2),30(a,1))].
% back CAC tautology: 873 x v (y v (z v (u v (v v w)))) = x v (v v (u v (z v (y v w)))).  [para(30(a,2),26(a,2))].
% back CAC tautology: 713 x v (y v (z v (u v (v v w)))) = x v (u v (v v (y v (z v w)))).  [para(29(a,1),26(a,2))].
% back CAC tautology: 666 x v (y v (z v (u v (v v w)))) = v v (y v (u v (z v (x v w)))).  [para(28(a,1),27(a,1))].
% back CAC tautology: 661 x v (y v (z v (u v (v v w)))) = v v (y v (z v (u v (x v w)))).  [para(28(a,1),21(a,1))].
% back CAC tautology: 622 x v (y v (z v (u v (v v w)))) = v v (u v (y v (x v (z v w)))).  [para(27(a,1),26(a,2))].
% back CAC tautology: 609 x v (y v (z v (u v (v v w)))) = x v (v v (z v (u v (y v w)))).  [para(27(a,1),22(a,1,2))].
% back CAC tautology: 608 x v (y v (z v (u v (v v w)))) = v v (z v (x v (u v (y v w)))).  [para(27(a,1),20(a,1,2))].
% back CAC tautology: 581 x v (y v (z v (u v (v v w)))) = v v (u v (x v (z v (y v w)))).  [para(26(a,2),26(a,1))].
% back CAC tautology: 579 x v (y v (z v (u v (v v w)))) = v v (y v (u v (x v (z v w)))).  [para(21(a,2),26(a,2,2)),flip(a)].
% back CAC tautology: 578 x v (y v (z v (u v (v v w)))) = x v (y v (v v (u v (z v w)))).  [para(26(a,2),21(a,2))].
% back CAC tautology: 577 x v (y v (z v (u v (v v w)))) = v v (u v (x v (y v (z v w)))).  [para(26(a,2),21(a,1))].
% back CAC tautology: 576 x v (y v (z v (u v (v v w)))) = x v (y v (z v (v v (u v w)))).  [para(26(a,1),21(a,1))].
% back CAC tautology: 575 x v (y v (z v (u v (v v w)))) = u v (v v (x v (z v (y v w)))).  [para(19(a,1),26(a,2,2))].
% back CAC tautology: 574 x v (y v (z v (u v (v v w)))) = v v (x v (u v (z v (y v w)))).  [para(19(a,2),26(a,1,2))].
% back CAC tautology: 573 x v (y v (z v (u v (v v w)))) = x v (v v (u v (y v (z v w)))).  [para(26(a,2),19(a,2)),flip(a)].
% back CAC tautology: 572 x v (y v (z v (u v (v v w)))) = u v (v v (y v (x v (z v w)))).  [para(20(a,1),26(a,2,2))].
% back CAC tautology: 571 x v (y v (z v (u v (v v w)))) = v v (z v (y v (x v (u v w)))).  [para(26(a,1),20(a,1))].
% back CAC tautology: 389 x v (y v (z v (u v (v v w)))) = v v (y v (z v (x v (u v w)))).  [para(21(a,2),21(a,2,2)),flip(a)].
% back CAC tautology: 388 x v (y v (z v (u v (v v w)))) = v v (x v (z v (u v (y v w)))).  [para(21(a,1),21(a,1,2))].
% back CAC tautology: 380 x v (y v (z v (u v (v v w)))) = u v (y v (v v (x v (z v w)))).  [para(19(a,2),21(a,2,2))].
% back CAC tautology: 379 x v (y v (z v (u v (v v w)))) = z v (v v (x v (u v (y v w)))).  [para(21(a,1),19(a,2,2))].
% back CAC tautology: 378 x v (y v (z v (u v (v v w)))) = y v (x v (z v (v v (u v w)))).  [para(21(a,2),19(a,1,2))].
% back CAC tautology: 373 x v (y v (z v (u v (v v w)))) = u v (x v (v v (z v (y v w)))).  [para(20(a,1),21(a,2,2,2))].
% back CAC tautology: 372 x v (y v (z v (u v (v v w)))) = u v (z v (x v (v v (y v w)))).  [para(21(a,1),20(a,1,2))].
% back CAC tautology: 365 x v (y v (z v (u v v))) = u v (y v (z v (x v v))).  [para(21(a,1),10(a,1))].
% back CAC tautology: 364 x v (y v (z v (u v (v v w)))) = u v (x v (z v (v v (y v w)))).  [para(21(a,1),10(a,1,2))].
% back CAC tautology: 311 x v (y v (z v (u v (v v w)))) = u v (v v (x v (y v (z v w)))).  [para(19(a,2),19(a,2,2)),flip(a)].
% back CAC tautology: 310 x v (y v (z v (u v v))) = u v (z v (y v (x v v))).  [para(19(a,2),19(a,1))].
% back CAC tautology: 309 x v (y v (z v (u v (v v w)))) = y v (x v (v v (u v (z v w)))).  [para(19(a,2),19(a,1,2))].
% back CAC tautology: 306 x v (y v (z v (u v (v v w)))) = x v (y v (v v (z v (u v w)))).  [para(19(a,2),22(a,1,2)),flip(a)].
% back CAC tautology: 305 x v (y v (z v (u v (v v w)))) = x v (v v (z v (y v (u v w)))).  [para(19(a,1),22(a,1,2))].
% back CAC tautology: 304 x v (y v (z v (u v (v v w)))) = v v (x v (u v (y v (z v w)))).  [para(20(a,1),19(a,1,2,2))].
% back CAC tautology: 303 x v (y v (z v (u v (v v w)))) = v v (z v (x v (y v (u v w)))).  [para(19(a,1),20(a,1,2))].
% back CAC tautology: 296 x v (y v (z v (u v (v v w)))) = u v (x v (v v (y v (z v w)))).  [para(10(a,1),19(a,1,2,2))].
% back CAC tautology: 295 x v (y v (z v (u v (v v w)))) = z v (v v (x v (y v (u v w)))).  [para(19(a,1),10(a,2,2)),flip(a)].
% back CAC tautology: 294 x v (y v (z v (u v (v v w)))) = y v (x v (v v (z v (u v w)))).  [para(19(a,2),10(a,1,2)),flip(a)].
% back CAC tautology: 293 x v (y v (z v (u v (v v w)))) = v v (x v (z v (y v (u v w)))).  [para(19(a,1),10(a,1,2))].
% back CAC tautology: 211 x v (y v (z v (u v (v v w)))) = x v (z v (y v (v v (u v w)))).  [para(22(a,1),22(a,1,2,2))].
% back CAC tautology: 210 x v (y v (z v (u v (v v w)))) = x v (v v (y v (u v (z v w)))).  [para(20(a,1),22(a,1,2,2))].
% back CAC tautology: 209 x v (y v (z v (u v (v v w)))) = z v (y v (x v (v v (u v w)))).  [para(22(a,1),20(a,1,2,2))].
% back CAC tautology: 202 x v (y v (z v (u v v))) = x v (y v (u v (z v v))).  [para(10(a,2),22(a,1,2))].
% back CAC tautology: 201 x v (y v (z v (u v (v v w)))) = x v (v v (y v (z v (u v w)))).  [para(10(a,2),22(a,1,2,2))].
% back CAC tautology: 200 x v (y v (z v (u v v))) = x v (u v (z v (y v v))).  [para(10(a,1),22(a,1,2))].
% back CAC tautology: 199 x v (y v (z v (u v (v v w)))) = x v (u v (y v (v v (z v w)))).  [para(10(a,1),22(a,1,2,2))].
% back CAC tautology: 198 x v (y v (z v (u v (v v w)))) = z v (x v (y v (v v (u v w)))).  [para(22(a,1),10(a,1,2,2))].
% back CAC tautology: 197 x v (y v (z v (u v v))) = x v (u v (y v (z v v))).  [para(2(a,1),22(a,1,2,2))].
% back CAC tautology: 196 x v (y v (z v (u v (v v w)))) = v v (y v (x v (u v (z v w)))).  [para(20(a,1),20(a,1,2,2))].
% back CAC tautology: 188 x v (y v (z v (u v (v v w)))) = v v (y v (x v (z v (u v w)))).  [para(10(a,2),20(a,1,2,2))].
% back CAC tautology: 187 x v (y v (z v (u v (v v w)))) = u v (y v (x v (v v (z v w)))).  [para(10(a,1),20(a,1,2,2))].
% back CAC tautology: 186 x v (y v (z v (u v v))) = u v (z v (x v (y v v))).  [para(20(a,1),10(a,2,2)),flip(a)].

given #170 (T,wt=11): 1826 x v (x v y)' = x v y'.  [back_rewrite(1761),rewrite(1800(4),1750(4))].

given #171 (A,wt=25): 190 ((x v (y v (z v (u v v)))')' v (u v (x v (z v (y v v))))')' = x.  [para(20(a,1),11(a,1,1,1,1,2,1))].

given #172 (F,wt=8): 2704 x' v (y v x) = c_0.  [para(1979(a,1),1826(a,1,2,1)),rewrite(1685(3),1800(2),9(2),1685(5)),flip(a)].

given #173 (F,wt=11): 1997 x v (y v (x' v z))' = x.  [para(2(a,1),1980(a,1,2,1))].

given #174 (T,wt=11): 2559 (x v y) v z = x v (y v z).  [para(1801(a,2),1800(a,1)),flip(a)].

given #175 (T,wt=11): 2703 x v (y v x)' = x v y'.  [para(1800(a,1),1826(a,1,2,1))].

given #176 (A,wt=25): 191 ((x v (y v (z v (u v v)))')' v (y v (u v (z v (x v v))))')' = x.  [para(20(a,1),11(a,1,1,2,1,2))].

given #177 (F,wt=12): 1663 x v (y v (z v (u v x'))) = c_0.  [back_rewrite(36),rewrite(1511(7),1511(7),1511(7))].

given #178 (F,wt=12): 1715 x' v (y v (z v (u v x))) = c_0.  [back_rewrite(1578),rewrite(1694(3),1677(4))].

given #179 (T,wt=12): 1952 x v (y v (z v (x' v u))) = c_0.  [para(1858(a,1),10(a,1,2,2)),rewrite(1511(2),1511(2)),flip(a)].

given #180 (T,wt=12): 1954 x' v (y v (z v (x v u))) = c_0.  [para(1858(a,1),19(a,1,2)),rewrite(1511(2)),flip(a)].

given #181 (A,wt=25): 204 ((x v (y v (z v (u v v)))')' v (y v (x v (u v (z v v))))')' = x.  [para(22(a,1),11(a,1,1,1,1,2,1))].

given #182 (F,wt=12): 2175 x' v (y v (x v z))' = x'.  [para(2(a,1),2005(a,1,2,1))].

given #183 (F,wt=12): 2242 x' v (y v (z v x))' = x'.  [para(1690(a,1),77(a,1,1,1,1)),rewrite(2(16),1758(15),1694(9),1685(7))].

given #184 (T,wt=13): 1688 ((x v y)' v (y' v x)')' = x.  [back_rewrite(1603),rewrite(1645(7),1677(5),1677(6))].

given #185 (T,wt=13): 1699 x v (y v (z v (u v x')))' = x.  [back_rewrite(1613),rewrite(1677(10),1685(8))].

given #186 (A,wt=25): 298 ((x v (y v (z v (u v v)))')' v (z v (y v (u v (x v v))))')' = x.  [para(19(a,1),11(a,1,1,2,1))].

given #187 (F,wt=13): 1760 (x v y)' v (x v y')' = x'.  [para(12(a,1),1685(a,1,1)),rewrite(1757(9)),flip(a)].

given #188 (F,wt=13): 1765 x v (y v (z v x)) = y v (z v x).  [para(1701(a,1),10(a,1,2,2)),flip(a)].

given #189 (T,wt=13): 1825 x v (y v (x v z)) = y v (x v z).  [back_rewrite(1766),rewrite(1800(2),1764(2))].

given #190 (T,wt=13): 1974 x v (y v (z v x')') = y v x.  [para(1750(a,1),2(a,1,2)),flip(a)].

given #191 (A,wt=25): 368 ((x v (y v (z v (u v v)))')' v (u v (y v (x v (z v v))))')' = x.  [para(21(a,1),11(a,1,1,2,1))].

given #192 (F,wt=13): 1996 x v (y v (x' v z)') = y v x.  [para(1980(a,1),2(a,1,2)),flip(a)].

given #193 (F,wt=13): 2000 x v (y v (z v (x' v u)))' = x.  [para(10(a,2),1980(a,1,2,1))].

given #194 (T,wt=13): 2729 x v ((y v x')' v z) = x v z.  [para(1750(a,1),2559(a,1,1)),flip(a)].

given #195 (T,wt=13): 2731 x v ((x' v y)' v z) = x v z.  [para(1980(a,1),2559(a,1,1)),flip(a)].

given #196 (A,wt=25): 439 ((x v (y v (z v (u v v)))')' v (z v (u v (x v (y v v))))')' = x.  [para(10(a,1),23(a,1,1,2,1,2))].

given #197 (F,wt=13): 2745 (x v y)' v (y v x')' = y'.  [para(2703(a,1),2703(a,1,2,1)),rewrite(1800(10),1979(10))].

given #198 (F,wt=13): 2778 (x v y)' v (y' v x)' = x'.  [para(1688(a,1),1685(a,1,1)),flip(a)].

given #199 (T,wt=13): 2798 (x v y')' v (y v x)' = x'.  [para(2703(a,1),1760(a,1,1,1)),rewrite(1685(6),1764(5))].

given #200 (T,wt=13): 2799 (x v y')' v (z v y) = z v y.  [para(1750(a,1),1765(a,1,2,2)),rewrite(1750(9))].

given #201 (A,wt=14): 1649 x v (y v (z v (u v (v v x')))) = c_0.  [back_rewrite(143),rewrite(1511(8),1511(8),1511(8),1511(8))].

given #202 (F,wt=0): 2895 (c3 v (c1' v c2'))' v (c1' v c3')' != (c1' v c2')' v (c1' v c3')' # answer(distributivity_1).  [back_rewrite(8),rewrite(2886(8),2(7))].

given #203 (F,wt=13): 2800 (x' v y)' v (z v x) = z v x.  [para(1980(a,1),1765(a,1,2,2)),rewrite(1980(9))].

given #204 (T,wt=13): 2868 (x' v y)' v (y v x)' = y'.  [para(1685(a,1),2745(a,1,2,1,2))].

given #205 (T,wt=13): 2869 (x v y)' v (x' v y)' = y'.  [para(1800(a,1),2745(a,1,2,1))].

given #206 (A,wt=14): 1754 (x v y)' v (z v (x v (u v y))) = c_0.  [back_rewrite(1730),rewrite(1749(3))].

given #207 (F,wt=14): 1955 x v (y v (z v (u v (x' v v)))) = c_0.  [para(1858(a,1),21(a,1,2,2,2)),rewrite(1511(2),1511(2),1511(2)),flip(a)].

given #208 (F,wt=14): 1956 x' v (y v (z v (u v (x v v)))) = c_0.  [para(1858(a,1),26(a,1,2,2)),rewrite(1511(2),1511(2)),flip(a)].

given #209 (T,wt=14): 1973 x' v (y v (z v (x v u)))' = x'.  [para(1858(a,1),65(a,1,1,2,1,2)),rewrite(1511(9),1800(10),1694(10),1685(8))].

given #210 (T,wt=14): 2026 x' v (y v (z v (u v (v v x)))) = c_0.  [para(1690(a,1),10(a,1,2,2)),rewrite(1511(2),1511(2)),flip(a)].

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

given #212 (F,wt=14): 2079 x v (y v (z v (u v (x v y)'))) = c_0.  [para(1836(a,1),31(a,1,2,2)),rewrite(1511(2),1511(2)),flip(a)].

given #213 (F,wt=14): 2101 x' v (y v (z v (u v x)))' = x'.  [para(1690(a,1),67(a,1,1,2,1,2)),rewrite(1511(9),1800(10),1694(10),1685(8))].

given #214 (T,wt=14): 2106 x' v (y v (z v x)') = y v x'.  [para(1979(a,1),2(a,1,2)),flip(a)].

given #215 (T,wt=14): 2174 x' v (y v (x v z)') = y v x'.  [para(2005(a,1),2(a,1,2)),flip(a)].

given #216 (A,wt=21): 1786 x v (y v (z v (u v (v v x)))) = y v (z v (u v (v v x))).  [para(1701(a,1),28(a,1,2,2,2,2)),flip(a)].

given #217 (F,wt=14): 2562 (x v y)' v (z v (y v (u v x))) = c_0.  [para(1801(a,1),1690(a,1,2,2))].

given #218 (F,wt=12): 2995 (x v y)' v (z v (y v x)) = c_0.  [para(1701(a,1),2562(a,1,2,2,2))].

given #219 (T,wt=14): 2563 (x v y)' v (z v (x v (y v u))) = c_0.  [para(1801(a,2),1690(a,1,2,2))].

given #220 (T,wt=14): 2571 x v (y v (z v ((x v y)' v u))) = c_0.  [para(1801(a,2),2186(a,1,1)),rewrite(2559(6),2559(5))].

given #221 (A,wt=21): 1816 x v (y v (z v (u v (x v v)))) = y v (z v (u v (x v v))).  [back_rewrite(1787),rewrite(1800(2),1764(2))].

given #222 (F,wt=14): 2732 x' v ((y v x)' v z) = x' v z.  [para(1979(a,1),2559(a,1,1)),flip(a)].

given #223 (F,wt=14): 2733 x' v ((x v y)' v z) = x' v z.  [para(2005(a,1),2559(a,1,1)),flip(a)].

given #224 (T,wt=14): 2746 x v (y v (z v (u v (y v x)'))) = c_0.  [back_rewrite(2670),rewrite(2744(4))].

given #225 (T,wt=14): 2801 (x v y)' v (z v y') = z v y'.  [para(1979(a,1),1765(a,1,2,2)),rewrite(1979(9))].

given #226 (A,wt=17): 1820 x v (y v (z v (x v u))) = y v (z v (x v u)).  [back_rewrite(1776),rewrite(1800(4),1773(4),1818(6),1819(4))].

given #227 (F,wt=14): 2802 (x v y)' v (z v x') = z v x'.  [para(2005(a,1),1765(a,1,2,2)),rewrite(2005(9))].

given #228 (F,wt=14): 2922 (x v y)' v (z v (u v (y v x))) = c_0.  [para(1800(a,1),1754(a,1,2,2)),rewrite(2559(4))].

given #229 (T,wt=14): 2996 (x v y)' v (z v (y v (x v u))) = c_0.  [para(1800(a,1),2562(a,1,2,2,2))].

given #230 (T,wt=14): 3031 x v (y v (z v ((y v x)' v u))) = c_0.  [para(2571(a,1),2(a,1)),flip(a)].

given #231 (A,wt=16): 1950 x v (y v (z v (u v (v v (w v x'))))) = c_0.  [para(1666(a,1),28(a,1,2,2,2,2)),rewrite(1511(2),1511(2),1511(2),1511(2)),flip(a)].

given #232 (F,wt=15): 2002 x v (y v (z v (u v (x' v v))))' = x.  [para(21(a,2),1980(a,1,2,1))].

given #233 (F,wt=15): 2164 x v (y v (z v (u v (v v x'))))' = x.  [para(1666(a,1),68(a,1,1,2,1,2,2,2)),rewrite(1511(10),1511(10),1511(10),1800(11),1694(11),1685(9))].

given #234 (T,wt=15): 2417 x v (y v (z v (u v x'))') = y v x.  [para(1698(a,1),2(a,1,2)),flip(a)].

given #235 (T,wt=15): 2701 x v (y v (x v z)') = y v (x v z').  [para(1826(a,1),2(a,1,2)),flip(a)].

given #236 (A,wt=16): 1957 x v (y v (z v (u v (v v (x' v w))))) = c_0.  [para(1858(a,1),28(a,1,2,2,2,2)),rewrite(1511(2),1511(2),1511(2),1511(2)),flip(a)].

given #237 (F,wt=15): 2702 x v (y v (x v z))' = x v (y v z)'.  [para(2(a,1),1826(a,1,2,1))].

given #238 (F,wt=15): 2727 x v (y v (z v (x' v u))') = y v x.  [para(1997(a,1),2(a,1,2)),flip(a)].

given #239 (T,wt=15): 2735 x v ((y v (z v x'))' v u) = x v u.  [para(1698(a,1),2559(a,1,1)),flip(a)].

given #240 (T,wt=15): 2736 x v ((x v y)' v z) = x v (y' v z).  [para(1826(a,1),2559(a,1,1)),rewrite(2559(3)),flip(a)].

given #241 (A,wt=17): 1976 x v (y v (z v (u v x')')) = y v (z v x).  [para(1750(a,1),10(a,1,2,2)),flip(a)].

given #242 (F,wt=15): 2738 x v ((y v (x' v z))' v u) = x v u.  [para(1997(a,1),2559(a,1,1)),flip(a)].

given #243 (F,wt=15): 2741 x v (y v (z v x)') = y v (x v z').  [para(2703(a,1),2(a,1,2)),flip(a)].

given #244 (T,wt=15): 2742 x v ((y v x)' v z) = x v (y' v z).  [para(2703(a,1),2559(a,1,1)),rewrite(2559(3)),flip(a)].

given #245 (T,wt=15): 2744 x v (y v (z v x))' = x v (y v z)'.  [para(2559(a,1),2703(a,1,2,1))].

given #246 (A,wt=21): 1977 x v (y v (z v (u v (v v x')'))) = y v (z v (u v x)).  [para(1750(a,1),21(a,1,2,2,2)),flip(a)].

given #247 (F,wt=15): 2803 (x v (y v z'))' v (u v z) = u v z.  [para(1698(a,1),1765(a,1,2,2)),rewrite(1698(11))].

given #248 (F,wt=15): 2805 (x v (y' v z))' v (u v y) = u v y.  [para(1997(a,1),1765(a,1,2,2)),rewrite(1997(11))].

given #249 (T,wt=15): 3051 (x v y)' v (z v y) = y v (x' v z).  [para(2732(a,1),2703(a,1,2,1)),rewrite(2559(7),2703(6),1685(4),1685(9),1800(8),2742(8))].

given #250 (T,wt=15): 3057 (x v y)' v (z v x) = x v (y' v z).  [para(2733(a,1),2703(a,1,2,1)),rewrite(2559(7),2703(6),1685(4),1685(9),1800(8),2736(8))].

given #251 (A,wt=25): 1978 x v (y v (z v (u v (v v (w v x')')))) = y v (z v (u v (v v x))).  [para(1750(a,1),28(a,1,2,2,2,2)),flip(a)].

given #252 (F,wt=16): 2034 x' v (y v (z v (u v (v v (w v x))))) = c_0.  [para(1690(a,1),21(a,1,2,2,2)),rewrite(1511(2),1511(2),1511(2)),flip(a)].

given #253 (F,wt=16): 2102 x' v (y v (z v (u v (v v (x v w))))) = c_0.  [para(1953(a,1),21(a,1,2,2,2)),rewrite(1511(2),1511(2),1511(2)),flip(a)].

given #254 (T,wt=16): 2107 (x v y)' v (x v (z v y))' = (x v y)'.  [para(2(a,1),1979(a,1,2,1))].

given #255 (T,wt=16): 2178 x' v (y v (z v (u v (x v v))))' = x'.  [para(21(a,2),2005(a,1,2,1))].

given #256 (A,wt=25): 1984 x v (y v (z v (u v (v v (w v x))))) = y v (z v (u v (v v (w v x)))).  [para(1764(a,1),28(a,1,2,2,2,2)),flip(a)].

given #257 (F,wt=16): 2565 (x v y)' v (y v (z v x))' = (x v y)'.  [para(1801(a,1),1979(a,1,2,1))].

given #258 (F,wt=14): 3363 (x v y)' v (y v x)' = (x v y)'.  [para(1701(a,1),2565(a,1,2,1,2))].

given #259 (T,wt=16): 2566 (x v y)' v (x v (y v z))' = (x v y)'.  [para(1801(a,2),1979(a,1,2,1))].

given #260 (T,wt=16): 2758 x' v (y v (z v (u v (v v x))))' = x'.  [para(2704(a,1),191(a,1,1,2,1,2,2,2)),rewrite(1511(10),1511(10),1511(10),1800(11),1694(11),1685(9))].

given #261 (A,wt=25): 1995 x v (y v (z v (u v (v v (x v w))))) = y v (z v (u v (v v (x v w)))).  [para(1828(a,1),28(a,1,2,2,2,2)),flip(a)].

given #262 (F,wt=16): 2761 x v (y v (z v (u v ((x v y)' v v)))) = c_0.  [para(1952(a,1),2559(a,1)),flip(a)].

given #263 (F,wt=16): 2771 x' v (y v (z v (x v u))') = y v x'.  [para(2175(a,1),2(a,1,2)),flip(a)].

given #264 (T,wt=16): 2772 x' v ((y v (x v z))' v u) = x' v u.  [para(2175(a,1),2559(a,1,1)),flip(a)].

given #265 (T,wt=16): 2774 x' v (y v (z v (u v x))') = y v x'.  [para(2242(a,1),2(a,1,2)),flip(a)].

given #266 (A,wt=17): 1999 x v (y v (z v (x' v u)')) = y v (z v x).  [para(1980(a,1),10(a,1,2,2)),flip(a)].

given #267 (F,wt=16): 2775 x' v ((y v (z v x))' v u) = x' v u.  [para(2242(a,1),2559(a,1,1)),flip(a)].

given #268 (F,wt=16): 2807 (x v (y v z))' v (u v y') = u v y'.  [para(2175(a,1),1765(a,1,2,2)),rewrite(2175(11))].

given #269 (T,wt=16): 2808 (x v (y v z))' v (u v z') = u v z'.  [para(2242(a,1),1765(a,1,2,2)),rewrite(2242(11))].

given #270 (T,wt=16): 3019 (x v y)' v (z v (y v x))' = (x v y)'.  [para(2995(a,1),1826(a,1,2,1)),rewrite(1800(5),1694(5)),flip(a)].

given #271 (A,wt=21): 2001 x v (y v (z v (u v (x' v v)'))) = y v (z v (u v x)).  [para(1980(a,1),21(a,1,2,2,2)),flip(a)].

given #272 (F,wt=16): 3072 x v (y v (z v (u v ((y v x)' v v)))) = c_0.  [para(2746(a,1),2559(a,1,1)),rewrite(1702(2),2559(7),2559(6),2559(5)),flip(a)].

given #273 (F,wt=16): 3087 (x v y)' v (z v (u v (v v (y v x)))) = c_0.  [para(2922(a,1),2(a,1,2)),rewrite(1511(2)),flip(a)].

given #274 (T,wt=16): 3364 (x v (y v z))' v (z v x)' = (z v x)'.  [para(2565(a,1),1800(a,1)),flip(a)].

given #275 (T,wt=16): 3365 (x v y)' v (y v (x v z))' = (x v y)'.  [para(1800(a,1),2565(a,1,2,1,2))].

given #276 (A,wt=25): 2003 x v (y v (z v (u v (v v (x' v w)')))) = y v (z v (u v (v v x))).  [para(1980(a,1),28(a,1,2,2,2,2)),flip(a)].

given #277 (F,wt=16): 3390 (x v (y v z))' v (y v x)' = (x v y)'.  [para(3363(a,1),2731(a,2)),rewrite(1685(5),2559(4),3389(9))].

given #278 (F,wt=16): 3391 (x v (y v z))' v (z v y)' = (z v y)'.  [para(3363(a,1),2799(a,1,2)),rewrite(1685(3),3363(11))].

given #279 (T,wt=17): 2004 x v (y v (z v (u v (v v (x' v w)))))' = x.  [para(28(a,2),1980(a,1,2,1))].

given #280 (T,wt=17): 2166 x v (y v (z v (u v (v v (w v x')))))' = x.  [para(1665(a,1),68(a,1,1,2,1,2,2,2)),rewrite(1511(11),1511(11),1511(11),1800(12),1694(12),1685(10))].

given #281 (A,wt=18): 2023 x v (y v (z v (u v (v v (w v (v6 v x')))))) = c_0.  [para(1665(a,1),28(a,1,2,2,2,2)),rewrite(1511(2),1511(2),1511(2),1511(2)),flip(a)].

given #282 (F,wt=17): 2646 x v (y v (z v (u v (v v x')))') = x v y.  [back_rewrite(2173),rewrite(2559(7))].

given #283 (F,wt=17): 2782 x v ((y v (z v (u v x')))' v v) = x v v.  [para(1699(a,1),2559(a,1,1)),flip(a)].

given #284 (T,wt=17): 2794 (x v y)' v (z v (x v y')') = z v x'.  [para(1760(a,1),2(a,1,2)),flip(a)].

given #285 (T,wt=17): 2796 (x v y)' v ((x v y')' v z) = x' v z.  [para(1760(a,1),2559(a,1,1)),flip(a)].

given #286 (A,wt=18): 2030 (x v (y v z))' v (u v (v v (y v (x v z)))) = c_0.  [para(22(a,1),1690(a,1,2,2))].

given #287 (F,wt=17): 2809 (x v (y v (z v u')))' v (v v u) = v v u.  [para(1699(a,1),1765(a,1,2,2)),rewrite(1699(13))].

given #288 (F,wt=17): 2814 x v (y v ((z v x')' v u)) = y v (x v u).  [para(1974(a,1),2559(a,1,1)),rewrite(2559(2),2559(7)),flip(a)].

given #289 (T,wt=17): 2819 (x v y')' v (z v (u v y)) = z v (u v y).  [para(1974(a,1),1765(a,1,2,2)),rewrite(2559(7),1820(7),1974(11))].

given #290 (T,wt=17): 2830 x v (y v ((x' v z)' v u)) = y v (x v u).  [para(1996(a,1),2559(a,1,1)),rewrite(2559(2),2559(7)),flip(a)].

given #291 (A,wt=22): 2035 (x v (y v (z v u)))' v (v v (z v (w v (x v (y v u))))) = c_0.  [para(21(a,1),1690(a,1,2,2))].

given #292 (F,wt=17): 2835 (x' v y)' v (z v (u v x)) = z v (u v x).  [para(1996(a,1),1765(a,1,2,2)),rewrite(2559(7),1820(7),1996(11))].

given #293 (F,wt=17): 2836 x v (y v (z v (u v (x' v v)))') = y v x.  [para(2000(a,1),2(a,1,2)),flip(a)].

given #294 (T,wt=17): 2837 x v ((y v (z v (x' v u)))' v v) = x v v.  [para(2000(a,1),2559(a,1,1)),flip(a)].

given #295 (T,wt=17): 2839 (x v (y v (z' v u)))' v (v v z) = v v z.  [para(2000(a,1),1765(a,1,2,2)),rewrite(2000(13))].

given #296 (A,wt=22): 2041 (x v (y v (z v u)))' v (v v (z v (w v (y v (x v u))))) = c_0.  [para(27(a,1),1690(a,1,2,2))].

given #297 (F,wt=17): 2847 (x v y')' v (z v (y v u)) = z v (y v u).  [para(2729(a,1),1765(a,1,2,2)),rewrite(2559(7),1765(6),2729(11))].

given #298 (F,wt=17): 2855 (x' v y)' v (z v (x v u)) = z v (x v u).  [para(2731(a,1),1765(a,1,2,2)),rewrite(2559(7),1765(6),2731(11))].

given #299 (T,wt=17): 2866 (x v y)' v (z v (y v x')') = z v y'.  [para(2745(a,1),2(a,1,2)),flip(a)].

given #300 (T,wt=17): 2870 (x v y)' v ((y v x')' v z) = y' v z.  [para(2745(a,1),2559(a,1,1)),flip(a)].

given #301 (A,wt=18): 2044 x' v (y v (z v (u v (v v (w v (v6 v x)))))) = c_0.  [para(1690(a,1),28(a,1,2,2,2,2)),rewrite(1511(2),1511(2),1511(2),1511(2)),flip(a)].

given #302 (F,wt=17): 2881 (x v y)' v (z v (y' v x)') = z v x'.  [para(2778(a,1),2(a,1,2)),flip(a)].

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

% Proof 1 at 2.41 (+ 0.04) seconds: distributivity_1.
% Length of proof is 141.
% Level of proof is 46.
% Maximum clause weight is 25.
% Given clauses 302.

1 x ^ (y v z) = (x ^ y) v (x ^ z) # answer(distributivity_1).  [goal].
2 x v (y v z) = y v (x v z).  [assumption].
3 x ^ y = (x' v y')'.  [assumption].
4 x v x' = y v y'.  [assumption].
5 (x v y') ^ (x v y) = x.  [assumption].
6 ((x v y')' v (x v y)')' = x.  [copy(5),rewrite(3(4))].
7 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity_1).  [deny(1)].
8 (c1' v (c2 v c3)')' != (c1' v c2')' v (c1' v c3')' # answer(distributivity_1).  [copy(7),rewrite(3(3),3(9),3(18)),flip(a)].
9 x v x' = c_0.  [new_symbol(4)].
10 x v (y v (z v u)) = z v (x v (y v u)).  [para(2(a,1),2(a,1,2))].
11 ((x v (y v z)')' v (y v (x v z))')' = x.  [para(2(a,1),6(a,1,1,2,1))].
12 ((x v y)' v (x v ((y v z')' v (y v z)'))')' = x.  [para(6(a,1),6(a,1,1,1,1,2))].
13 (x v (x v ((x v y')' v y))')' = (x v y')'.  [para(6(a,1),6(a,1,1,1)),rewrite(2(5))].
14 (((x v y')' v (x v y)'')' v x)' = (x v y')'.  [para(6(a,1),6(a,1,1,2))].
15 x v (y v x') = y v c_0.  [para(9(a,1),2(a,1,2)),flip(a)].
16 (c_0' v (x v x)')' = x.  [para(9(a,1),6(a,1,1,1,1))].
17 ((x v x'')' v c_0')' = x.  [para(9(a,1),6(a,1,1,2,1))].
18 ((x v y')' v (x v y)') v x = c_0.  [para(6(a,1),9(a,1,2))].
21 x v (y v (z v (u v v))) = u v (x v (y v (z v v))).  [para(10(a,2),2(a,1,2))].
25 x v (y v (z v x')) = y v (z v c_0).  [para(9(a,1),10(a,1,2,2)),flip(a)].
34 ((x v (y v x')')' v (y v c_0)')' = x.  [para(15(a,1),6(a,1,1,2,1))].
37 (c_0' v (x v ((x v y) v y))')' = x v y.  [para(2(a,1),16(a,1,1,2,1))].
39 (x v (c_0' v (x v x))')' = c_0'.  [para(16(a,1),6(a,1,1,1))].
41 (c_0' v (x v x)') v x = c_0.  [para(16(a,1),9(a,1,2))].
42 (c_0' v (x v (y v ((y v (x v z)) v z)))')' = y v (x v z).  [para(10(a,1),16(a,1,1,2,1)),rewrite(2(6))].
44 (c_0' v (x v x)') v (y v x) = y v c_0.  [para(16(a,1),15(a,1,2,2))].
45 x v ((c_0' v (x v ((x v y) v y))') v y) = c_0.  [para(41(a,1),2(a,1)),rewrite(2(6)),flip(a)].
54 (c_0' v (x' v x')') v c_0 = x v c_0.  [para(41(a,1),15(a,1,2)),flip(a)].
57 (((x v x'')' v c_0'')' v x)' = (x v x'')'.  [para(17(a,1),6(a,1,1,2))].
73 (x v (x v (c_0' v x))')' = c_0'.  [para(16(a,1),11(a,1,1,1))].
82 (x v (c_0' v (x v x))') v c_0' = c_0.  [para(39(a,1),9(a,1,2))].
88 (c_0'' v (c_0'' v c_0)')' = c_0'.  [para(15(a,1),39(a,1,1,2,1))].
103 (c_0' v (x v (x v (c_0' v x)))')' = x.  [para(73(a,1),6(a,1,1,1))].
121 ((x' v y')' v (x' v y)') v c_0 = x v c_0.  [para(18(a,1),15(a,1,2)),flip(a)].
130 (c_0' v (x v (c_0' v (x v x)))') v x = c_0.  [para(39(a,1),18(a,1,1,1))].
133 (c_0' v (x v (x v (c_0' v x)))') v x = c_0.  [para(73(a,1),18(a,1,1,1))].
154 (x v (c_0' v (x v x))') v c_0 = c_0 v c_0.  [para(82(a,1),15(a,1,2)),flip(a)].
159 (c_0' v (c_0'' v (c_0'' v c_0))')' = c_0''.  [para(88(a,1),6(a,1,1,1))].
175 ((x v x'')' v (x v ((x v x'')' v c_0))')' = x.  [para(17(a,1),13(a,1,1,2,1,2,1)),rewrite(2(11),17(22))].
180 (x v (y v ((x v (y v x')')' v c_0))')' = (x v (y v x')')'.  [para(25(a,1),13(a,1,1,2,1)),rewrite(2(8))].
226 ((x v (y v c_0)')' v (y v ((c_0' v (z v z)') v (x v z)))')' = x.  [para(44(a,2),11(a,1,1,2,1,2))].
243 ((x v ((x v x'')' v c_0)'')' v (x v x'')')' = x.  [para(17(a,1),14(a,1,1,1,1,1)),rewrite(17(24))].
314 x v (c_0' v (x v x))' = c_0.  [para(154(a,1),6(a,1,1,2,1)),rewrite(82(9),16(8)),flip(a)].
320 x v (y v (c_0' v (x v x))') = y v c_0.  [para(314(a,1),2(a,1,2)),flip(a)].
322 x v (x v (c_0' v x))' = c_0.  [para(2(a,1),314(a,1,2,1))].
328 (c_0' v (x v x)) v c_0 = x v c_0.  [para(314(a,1),15(a,1,2))].
329 c_0'' v (c_0'' v c_0)' = c_0.  [para(15(a,1),314(a,1,2,1))].
330 ((x v (y v (c_0' v (x v x))')')' v (y v c_0)')' = x.  [para(314(a,1),11(a,1,1,2,1,2))].
335 x v (y v (x v (c_0' v x))') = y v c_0.  [para(322(a,1),2(a,1,2)),flip(a)].
338 (x v (c_0' v x)) v c_0 = x v c_0.  [para(322(a,1),15(a,1,2))].
353 (c_0'' v c_0) v c_0 = c_0'' v c_0.  [para(15(a,1),328(a,1,1))].
393 (c_0'' v c_0) v (x v c_0) = x v (c_0'' v c_0).  [para(329(a,1),25(a,1,2,2))].
451 (c_0' v (x v x)) v (y v c_0) = x v (y v c_0).  [para(320(a,1),25(a,1,2))].
456 ((x v x)' v ((x v (c_0' v x)')' v c_0)')' = x.  [para(335(a,1),12(a,1,1,2,1))].
463 ((x v y)' v ((y v (z v y')')' v (x v (z v c_0)'))')' = x.  [para(34(a,1),11(a,1,1,1,1,2))].
486 c_0'' v c_0 = c_0''.  [para(353(a,1),37(a,1,1,2,1,2,1)),rewrite(353(14),2(13),353(12),159(14),353(10)),flip(a)].
500 c_0'' v (x v c_0) = x v c_0''.  [back_rewrite(393),rewrite(486(5),486(11))].
514 ((c_0'' v (x v c_0))' v (x v c_0')')' = x.  [para(500(a,2),6(a,1,1,1,1))].
515 c_0' v (c_0'' v (x v c_0)) = x v c_0.  [para(500(a,2),15(a,1,2))].
545 c_0'' v (x v c_0) = (x v (c_0' v x)) v c_0''.  [para(338(a,1),500(a,1,2))].
554 c_0'' v (x v (c_0' v c_0)) = x v c_0.  [para(515(a,1),10(a,2))].
567 (c_0' v (c_0' v ((c_0' v c_0) v c_0))') v c_0 = c_0''.  [para(41(a,1),554(a,1,2)),rewrite(486(5),2(14)),flip(a)].
736 c_0 v (c_0' v c_0) = c_0.  [para(451(a,1),37(a,1,1,2,1,2)),rewrite(2(10),2(9),103(13),2(7)),flip(a)].
747 c_0'' = c_0 v c_0.  [para(736(a,1),44(a,1,2)),rewrite(2(11),567(15))].
801 (c_0' v (c_0' v ((c_0' v c_0) v c_0))') v c_0 = c_0 v c_0.  [back_rewrite(567),rewrite(747(18))].
814 (c_0 v c_0) v (x v (c_0' v c_0)) = x v c_0.  [back_rewrite(554),rewrite(747(3))].
823 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0).  [back_rewrite(545),rewrite(747(3),747(13),2(14),338(13))].
841 ((c_0 v (x v c_0))' v (x v c_0')')' = x.  [back_rewrite(514),rewrite(747(3),823(6))].
862 ((c_0 v ((x v x'')' v c_0))' v x)' = (x v x'')'.  [back_rewrite(57),rewrite(747(7),2(8))].
876 ((c_0 v (c_0 v c_0))' v c_0')' = c_0.  [para(747(a,1),17(a,1,1,1,1,2))].
1039 c_0' v (c_0' v c_0')' = c_0.  [para(41(a,1),841(a,1,1,2,1)),rewrite(54(12),876(10)),flip(a)].
1044 (c_0' v x')' v (c_0' v x)' = c_0.  [para(18(a,1),841(a,1,1,2,1)),rewrite(121(13),876(10)),flip(a)].
1055 c_0' v (x v (c_0' v c_0')') = x v c_0.  [para(1039(a,1),2(a,1,2)),flip(a)].
1104 (c_0' v x')' v c_0 = (c_0' v x) v c_0.  [para(1044(a,1),15(a,1,2)),flip(a)].
1188 (c_0' v ((c_0' v c_0) v ((c_0' v c_0) v c_0))') v (c_0' v c_0')' = c_0.  [para(1055(a,1),130(a,1,1,2,1,2)),rewrite(1104(16),2(15),1104(14))].
1189 (c_0' v ((c_0' v c_0) v ((c_0' v c_0) v c_0))') v c_0 = c_0' v c_0.  [para(130(a,1),1055(a,1,2)),rewrite(1055(28),1104(20),2(19),1104(18)),flip(a)].
1204 (c_0' v c_0')' = c_0' v c_0.  [para(1104(a,1),13(a,1,1,2,1,2)),rewrite(37(14)),flip(a)].
1241 c_0' v (c_0' v c_0) = c_0.  [back_rewrite(1188),rewrite(1204(21),2(20),1189(19))].
1259 c_0' v (x v (c_0' v c_0)) = x v c_0.  [back_rewrite(1055),rewrite(1204(8))].
1262 c_0' v c_0 = c_0 v c_0.  [para(1241(a,1),44(a,1,2)),rewrite(2(11),801(15)),flip(a)].
1263 c_0 v (c_0 v c_0) = c_0.  [para(44(a,2),1241(a,1,2)),rewrite(2(11),41(10),1262(6),2(6),1262(5))].
1264 c_0 v c_0 = c_0.  [para(1241(a,1),14(a,1,1,1,1,2,1,1)),rewrite(1262(6),16(8),747(4),1263(5),1204(6),1262(4),1262(9),16(11))].
1270 c_0' v (x v (y v c_0)) = x v (y v c_0).  [para(1241(a,1),21(a,1,2,2)),rewrite(1262(9),1264(8)),flip(a)].
1282 c_0' v (x v c_0) = x v c_0.  [back_rewrite(1259),rewrite(1262(6),1264(5))].
1302 c_0 v (x v c_0) = x v c_0.  [back_rewrite(814),rewrite(1264(3),1262(5),1264(4))].
1312 c_0' v c_0 = c_0.  [back_rewrite(1262),rewrite(1264(7))].
1348 c_0'' = c_0.  [back_rewrite(747),rewrite(1264(6))].
1353 (((x v x'')' v c_0)' v x)' = (x v x'')'.  [back_rewrite(862),rewrite(1302(8))].
1357 (c_0' v (x v ((x v c_0) v ((x v c_0) v c_0)))')' = x v ((x v c_0) v c_0).  [para(451(a,1),42(a,1,1,2,1,2,2)),rewrite(2(11),1270(12),2(10),2(20),1270(21))].
1371 x v ((x v c_0) v c_0) = x v c_0.  [para(1282(a,1),103(a,1,1,2,1,2,2)),rewrite(2(9),2(10),1357(13))].
1372 (c_0' v (x v c_0)')' = x v c_0.  [para(1282(a,1),37(a,1,1,2,1,2,1)),rewrite(2(9),1371(9),1282(7),1282(12))].
1373 x v ((c_0' v (x v c_0)') v c_0) = c_0.  [para(1282(a,1),133(a,1,1,2,1,2,2)),rewrite(2(9),1371(9),2(7),1371(7),2(9))].
1378 x v (y v ((x v c_0) v c_0)) = y v (x v c_0).  [para(1371(a,1),2(a,1,2)),flip(a)].
1416 x v ((x v c_0) v ((c_0' v (x v c_0)') v c_0)) = c_0.  [para(1371(a,1),45(a,1,2,1,2,1,2,1)),rewrite(1378(10),2(7),1371(7),2(11))].
1425 ((x v c_0)' v c_0')' = x v c_0.  [para(1372(a,1),34(a,1,1,1,1,2)),rewrite(2(5),1371(5),1312(7))].
1438 ((x v (y v c_0))' v ((y v c_0)' v (x v c_0'))')' = x.  [para(1425(a,1),11(a,1,1,1,1,2))].
1445 ((x v c_0)' v ((x v c_0) v ((x v c_0)' v c_0))')' = x v c_0.  [para(1425(a,1),13(a,1,1,2,1,2,1)),rewrite(2(11),1425(21))].
1450 ((x v c_0)' v ((x v c_0)' v c_0)')' = c_0.  [para(1425(a,1),34(a,1,1,1,1,2)),rewrite(1302(4))].
1471 x v (y v ((c_0' v (x v c_0)') v c_0)) = y v c_0.  [para(1373(a,1),2(a,1,2)),flip(a)].
1488 (x v c_0) v c_0 = c_0.  [back_rewrite(1416),rewrite(1471(12))].
1493 (x v c_0) v (y v c_0) = y v c_0.  [para(1488(a,1),2(a,1,2)),flip(a)].
1511 x v c_0 = c_0.  [back_rewrite(1445),rewrite(1493(11),1450(11)),flip(a)].
1526 (c_0' v (c_0' v (x v c_0'))')' = x.  [back_rewrite(1438),rewrite(1511(2),1511(2),1511(4))].
1537 (x v x'')' = (c_0' v x)'.  [back_rewrite(1353),rewrite(1511(6)),flip(a)].
1603 ((x v y)' v ((y v (z v y')')' v (x v c_0'))')' = x.  [back_rewrite(463),rewrite(1511(9))].
1606 ((x v x)' v c_0')' = x.  [back_rewrite(456),rewrite(1511(10))].
1627 ((x v (y v (c_0' v (x v x))')')' v c_0')' = x.  [back_rewrite(330),rewrite(1511(11))].
1634 (c_0' v (c_0' v x)')' = x.  [back_rewrite(243),rewrite(1537(4),1511(6),1348(3),1511(2),1537(6))].
1635 ((x v c_0')' v (y v ((c_0' v (z v z)') v (x v z)))')' = x.  [back_rewrite(226),rewrite(1511(2))].
1645 (x v (y v x')')' = (x v c_0')'.  [back_rewrite(180),rewrite(1511(7),1511(2)),flip(a)].
1646 ((c_0' v x)' v c_0')' = x.  [back_rewrite(175),rewrite(1537(4),1537(8),1511(10),1511(6))].
1662 (c_0' v (x v x)') v (y v x) = c_0.  [back_rewrite(44),rewrite(1511(9))].
1677 x v c_0' = x.  [back_rewrite(1526),rewrite(1634(11))].
1685 x'' = x.  [back_rewrite(1635),rewrite(1677(3),1662(8),1511(3),1677(4))].
1688 ((x v y)' v (y' v x)')' = x.  [back_rewrite(1603),rewrite(1645(7),1677(5),1677(6))].
1694 c_0' v x = x.  [back_rewrite(1646),rewrite(1677(7),1685(5))].
1696 x v (y v (x v x)')' = x.  [back_rewrite(1627),rewrite(1694(4),1677(9),1685(7))].
1701 x v x = x.  [back_rewrite(1606),rewrite(1677(5),1685(3))].
1750 x v (y v x')' = x.  [back_rewrite(1696),rewrite(1701(1))].
1761 x v (x v ((x v y')' v y))' = x v y'.  [para(13(a,1),1685(a,1,1)),rewrite(1685(4)),flip(a)].
1800 x v y = y v x.  [para(1677(a,1),2(a,1,2)),rewrite(1677(4))].
1801 x v (y v z) = z v (x v y).  [para(1677(a,1),10(a,1,2,2)),rewrite(1677(5))].
1826 x v (x v y)' = x v y'.  [back_rewrite(1761),rewrite(1800(4),1750(4))].
1974 x v (y v (z v x')') = y v x.  [para(1750(a,1),2(a,1,2)),flip(a)].
1979 x' v (y v x)' = x'.  [para(1685(a,1),1750(a,1,2,1,2))].
1980 x v (x' v y)' = x.  [para(1800(a,1),1750(a,1,2,1))].
1996 x v (y v (x' v z)') = y v x.  [para(1980(a,1),2(a,1,2)),flip(a)].
2107 (x v y)' v (x v (z v y))' = (x v y)'.  [para(2(a,1),1979(a,1,2,1))].
2559 (x v y) v z = x v (y v z).  [para(1801(a,2),1800(a,1)),flip(a)].
2703 x v (y v x)' = x v y'.  [para(1800(a,1),1826(a,1,2,1))].
2732 x' v ((y v x)' v z) = x' v z.  [para(1979(a,1),2559(a,1,1)),flip(a)].
2741 x v (y v (z v x)') = y v (x v z').  [para(2703(a,1),2(a,1,2)),flip(a)].
2778 (x v y)' v (y' v x)' = x'.  [para(1688(a,1),1685(a,1,1)),flip(a)].
2881 (x v y)' v (z v (y' v x)') = z v x'.  [para(2778(a,1),2(a,1,2)),flip(a)].
2886 (x v (y v z)')' = (x v (z v y'))' v (x v z')'.  [para(1974(a,1),2778(a,1,2,1)),rewrite(1685(2),1800(4),2741(4),1685(10)),flip(a)].
2895 (c3 v (c1' v c2'))' v (c1' v c3')' != (c1' v c2')' v (c1' v c3')' # answer(distributivity_1).  [back_rewrite(8),rewrite(2886(8),2(7))].
3050 (x v y)' v ((x v (z v y))' v u) = (x v y)' v u.  [para(2(a,1),2732(a,1,2,1,1))].
3333 (x v (y v z))' v (x v y')' = (x v z)' v (x v y')'.  [para(1980(a,1),2107(a,1,2,1,2)),rewrite(2886(5),1685(2),1800(10),3050(10),2886(11),1685(8)),flip(a)].
3345 (x v (y v z)')' = (x v y')' v (x v z')'.  [back_rewrite(2886),rewrite(3333(12))].
3782 (x v (y v z))' v (y v x')' = (y v z)' v (y v x')'.  [para(2881(a,1),2778(a,1,2,1)),rewrite(1800(6),2559(6),1996(5),3345(12),1685(9))].
3783 $F # answer(distributivity_1).  [resolve(3782,a,2895,a)].

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

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

Given=302. Generated=84030. Kept=3779. proofs=1.
Usable=139. Sos=696. Demods=820. Limbo=6, Disabled=2942. Hints=0.
Weight_deleted=11272. Literals_deleted=0.
Forward_subsumed=68979. Back_subsumed=82.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=2956 (7 lex), Back_demodulated=2716. Back_unit_deleted=0.
Demod_attempts=1543153. Demod_rewrites=248108.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=1.67.
User_CPU=2.41, System_CPU=0.04, Wall_clock=2.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 10727 exit (max_proofs) Sat Aug 12 20:58:20 2006