============================== Prover9 ===============================
Prover9 (32) version June-2006C, June 2006.
Process 13064 was started by mccune on cleo.thornwood,
Mon Jun 19 16:40:38 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).

clauses(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).

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

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

============================== PROCESS GOALS =========================

% Each goal clause was negated; the result (to be placed in sos):

clauses(negated_goals).
(c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity_1).
end_of_list.

============================== end of process goals ==================

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

% Clauses before input processing:

clauses(usable).
end_of_list.

clauses(sos).
1 x v (y v z) = y v (x v z).  [input].
2 x ^ y = (x ' v y ') '.  [input].
3 x v x ' = y v y '.  [input].
4 (x v y ') ^ (x v y) = x.  [input].
5 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity_1).  [clausify].
end_of_list.

clauses(demodulators).
end_of_list.

Predicate elimination: (none).

Auto_denials:  no changes.

% Restrict denials; moving clauses to denials list:

clauses(denials).
5 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity_1).  [clausify].
end_of_list.

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

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

Auto_process settings:  no changes.

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

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

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

% Clauses after input processing:

clauses(usable).
end_of_list.

clauses(sos).
6 x v (y v z) = y v (x v z).  [input].
7 x ^ y = (x ' v y ') '.  [input].
9 ((x v y ') ' v (x v y) ') ' = x.  [copy(4),demod(7(4))].
10 x v x ' = c_0.  [new_symbol(8)].
end_of_list.

clauses(demodulators).
6 x v (y v z) = y v (x v z).  [input].
        % (lex-dep)
7 x ^ y = (x ' v y ') '.  [input].
9 ((x v y ') ' v (x v y) ') ' = x.  [copy(4),demod(7(4))].
10 x v x ' = c_0.  [new_symbol(8)].
end_of_list.

clauses(denials).
11 (c1 ' v (c2 v c3) ') ' != (c1 ' v c2 ') ' v (c1 ' v c3 ') ' # answer(distributivity_1).  [copy(5),demod(7(3),7(9),7(18)),flip(a)].
end_of_list.

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

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

% Starting search at 0.00 seconds.

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

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

given #3 (I,wt=13): 9 ((x v y ') ' v (x v y) ') ' = x.  [copy(4),demod(7(4))].

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

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

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

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

given #8 (F,wt=11): 43 (c_0 ' v (x v x) ') v x = c_0.  [para(18(a,1),10(a,1,2))].

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

given #10 (T,wt=13): 41 (x v (c_0 ' v (x v x)) ') ' = c_0 '.  [para(18(a,1),9(a,1,1,1))].

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

given #12 (F,wt=13): 60 ((x v x ' ') ' v c_0 ') v x = c_0.  [para(19(a,1),10(a,1,2))].

given #13 (F,wt=13): 63 (x v (x v (c_0 ' v x)) ') ' = c_0 '.  [para(6(a,1),41(a,1,1,2,1))].

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

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

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

given #17 (F,wt=14): 67 (x v (c_0 ' v (x v x)) ') v c_0 ' = c_0.  [para(41(a,1),10(a,1,2))].

given #18 (F,wt=14): 69 (c_0 ' ' v (c_0 ' ' v c_0) ') ' = c_0 '.  [para(17(a,1),41(a,1,1,2,1))].

given #19 (T,wt=14): 107 (x v (x v (c_0 ' v x)) ') v c_0 ' = c_0.  [para(63(a,1),10(a,1,2))].

given #20 (T,wt=15): 25 x v (y v (z v u)) = z v (y v (x v u)).  [para(12(a,1),6(a,1))].

given #21 (A,wt=19): 15 (x v (x v ((x v y ') ' v y)) ') ' = (x v y ') '.  [para(9(a,1),9(a,1,1,1)),demod(6(5))].

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

given #23 (F,wt=15): 42 ((c_0 ' v (x v x) ' ') ' v x) ' = c_0 '.  [para(18(a,1),9(a,1,1,2))].

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

given #25 (T,wt=15): 49 (c_0 ' v (x ' v x ') ') v c_0 = x v c_0.  [para(43(a,1),17(a,1,2)),flip(a)].

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

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

given #28 (F,wt=15): 91 (c_0 ' v (c_0 ' v (x v (x v x))) ') ' = x.  [para(41(a,1),13(a,1,1,1))].

given #29 (T,wt=15): 105 (c_0 ' v (x v (x v (c_0 ' v x))) ') ' = x.  [para(63(a,1),9(a,1,1,1))].

given #30 (T,wt=15): 154 (x v (c_0 ' v (x v x)) ') v c_0 = c_0 v c_0.  [para(67(a,1),17(a,1,2)),flip(a)].

given #31 (A,wt=16): 22 ((x v (y v x ') ') ' v (y v c_0) ') ' = x.  [para(17(a,1),9(a,1,1,2,1))].

given #32 (F,wt=11): 297 x v (c_0 ' v (x v x)) ' = c_0.  [para(154(a,1),9(a,1,1,2,1)),demod(67(9),18(8)),flip(a)].

given #33 (F,wt=11): 321 x v (x v (c_0 ' v x)) ' = c_0.  [para(6(a,1),297(a,1,2,1))].

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

given #35 (T,wt=12): 323 c_0 ' ' v (c_0 ' ' v c_0) ' = c_0.  [para(17(a,1),297(a,1,2,1))].

given #36 (A,wt=18): 23 ((x v y ') ' v (x v y) ') v (z v x) = z v c_0.  [para(9(a,1),17(a,1,2,2))].

given #37 (F,wt=12): 334 (x v (c_0 ' v x)) v c_0 = x v c_0.  [para(321(a,1),17(a,1,2))].

given #38 (F,wt=13): 345 (c_0 ' ' v c_0) v c_0 = c_0 ' ' v c_0.  [para(17(a,1),322(a,1,1))].

given #39 (T,wt=15): 298 c_0 v (x v (y v c_0)) = x v (y v (c_0 v c_0)).  [para(154(a,1),12(a,1,2,2)),demod(297(11)),flip(a)].

given #40 (T,wt=15): 319 x v (y v (c_0 ' v (x v x)) ') = y v c_0.  [para(297(a,1),6(a,1,2)),flip(a)].

given #41 (A,wt=19): 24 x v (y v (z v (u v v))) = z v (x v (u v (y v v))).  [para(12(a,1),6(a,1,2))].

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

given #43 (F,wt=16): 39 (c_0 ' v (x v ((x v y) v y)) ') ' = x v y.  [para(6(a,1),18(a,1,1,2,1))].

given #44 (T,wt=9): 472 c_0 ' ' v c_0 = c_0 ' '.  [para(345(a,1),39(a,1,1,2,1,2,1)),demod(345(14),6(13),345(12),161(14),345(10)),flip(a)].

given #45 (T,wt=13): 484 c_0 ' ' v (x v c_0) = x v c_0 ' '.  [back_demod(362),demod(472(5),472(11))].

given #46 (A,wt=19): 26 x v (y v (z v (u v v))) = u v (x v (y v (z v v))).  [para(12(a,2),6(a,1,2))].

given #47 (F,wt=14): 495 c_0 ' v (c_0 ' ' v (x v c_0)) = x v c_0.  [para(484(a,2),17(a,1,2))].

given #48 (F,wt=14): 568 c_0 ' ' v (x v (c_0 ' v c_0)) = x v c_0.  [para(495(a,1),12(a,2))].

given #49 (T,wt=15): 490 (c_0 ' v (c_0 v c_0) ') v c_0 ' ' = c_0 ' '.  [para(472(a,1),44(a,1,2)),demod(472(16))].

given #50 (T,wt=12): 588 (c_0 ' v c_0 ' ' ') ' ' = c_0 '.  [para(490(a,1),22(a,1,1,1,1,2,1)),demod(43(17),465(11))].

given #51 (A,wt=21): 28 ((x v (y v (z v u)) ') ' v (z v (x v (y v u))) ') ' = x.  [para(12(a,1),9(a,1,1,2,1))].

given #52 (F,wt=10): 590 (c_0 ' v c_0 ' ' ') ' = c_0.  [para(588(a,1),10(a,1,2)),demod(465(11))].

given #53 (F,wt=11): 606 (c_0 ' v c_0 ' ' ') v c_0 = c_0.  [para(590(a,1),10(a,1,2))].

given #54 (T,wt=15): 512 (c_0 ' ' v (x v c_0)) ' = (x v c_0 ' ') '.  [para(484(a,2),15(a,2,1)),demod(15(12)),flip(a)].

given #55 (T,wt=15): 605 ((c_0 ' v c_0 ' ' ' ') ' v c_0) ' = c_0 '.  [para(590(a,1),9(a,1,1,2))].

given #56 (A,wt=21): 29 ((x v (y v (z v u)) ') ' v (y v (z v (x v u))) ') ' = x.  [para(12(a,2),9(a,1,1,2,1))].

given #57 (F,wt=15): 607 (c_0 ' v c_0 ' ' ') v (x v c_0) = x v c_0.  [para(590(a,1),17(a,1,2,2))].

given #58 (F,wt=15): 615 (c_0 ' ' ' v (c_0 ' v c_0) ') ' = c_0 ' '.  [para(590(a,1),22(a,1,1,1,1,2)),demod(472(5))].

given #59 (T,wt=15): 621 (c_0 ' v c_0 ' ' ') v c_0 ' ' = c_0 ' '.  [para(606(a,1),484(a,1,2)),demod(472(5)),flip(a)].

given #60 (T,wt=16): 126 ((c_0 ' v (x v x) ' ') ' v x) v c_0 ' = c_0.  [para(18(a,1),20(a,1,1,2))].

given #61 (A,wt=18): 30 x v (y v (z v (u v x '))) = y v (z v (u v c_0)).  [para(17(a,1),12(a,1,2,2)),flip(a)].

given #62 (F,wt=13): 668 (c_0 ' v (x v x) ' ') ' v x = c_0.  [para(126(a,1),9(a,1,1,1,1)),demod(248(12),18(8)),flip(a)].

given #63 (F,wt=16): 131 (c_0 ' v (x v (c_0 ' v (x v x))) ') v x = c_0.  [para(41(a,1),20(a,1,1,1))].

given #64 (T,wt=16): 135 (c_0 ' v (x v (x v (c_0 ' v x))) ') v x = c_0.  [para(63(a,1),20(a,1,1,1))].

given #65 (T,wt=16): 275 (c_0 ' v (c_0 ' v (x v (x v x))) ') v x = c_0.  [para(91(a,1),10(a,1,2))].

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

given #67 (F,wt=16): 428 (c_0 ' v (x v x)) v (y v c_0) = x v (y v c_0).  [para(319(a,1),21(a,1,2))].

given #68 (F,wt=8): 739 c_0 v (c_0 ' v c_0) = c_0.  [para(428(a,1),39(a,1,1,2,1,2)),demod(6(10),6(9),105(13),6(7)),flip(a)].

given #69 (T,wt=7): 751 c_0 ' ' = c_0 v c_0.  [para(739(a,1),44(a,1,2)),demod(6(11),581(15))].

given #70 (T,wt=9): 757 (c_0 v c_0) v c_0 = c_0 v c_0.  [para(739(a,1),568(a,1,2)),demod(751(3))].

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

given #72 (F,wt=12): 742 c_0 v (x v (c_0 ' v c_0)) = x v c_0.  [para(739(a,1),6(a,1,2)),flip(a)].

given #73 (F,wt=12): 745 c_0 ' v (x v (c_0 v c_0)) = x v c_0.  [para(739(a,1),12(a,1,2)),flip(a)].

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

given #75 (T,wt=12): 876 ((c_0 v (c_0 v c_0)) ' v c_0 ') ' = c_0.  [para(751(a,1),19(a,1,1,1,1,2))].

given #76 (A,wt=23): 33 x v (y v (z v (u v (v v w)))) = v v (x v (y v (z v (u v w)))).  [para(12(a,2),12(a,1,2,2))].

given #77 (F,wt=13): 827 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0).  [back_demod(525),demod(751(3),751(13),6(14),334(13))].

given #78 (F,wt=13): 833 (c_0 v (x v c_0)) ' = (x v (c_0 v c_0)) '.  [back_demod(512),demod(751(3),827(6),751(8))].

given #79 (T,wt=13): 858 ((c_0 v (c_0 v c_0)) ' v c_0 ') v c_0 = c_0.  [back_demod(367),demod(751(10),6(17),20(16))].

given #80 (T,wt=14): 743 ((c_0 v (c_0 ' v c_0) ') ' v c_0 ') ' = c_0.  [para(739(a,1),9(a,1,1,2,1))].

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

given #82 (F,wt=14): 788 (x v (c_0 v c_0)) v (c_0 v (x v c_0)) ' = c_0.  [back_demod(628),demod(751(3),751(7),780(11))].

given #83 (F,wt=14): 811 (c_0 v c_0) v (x v (c_0 ' v c_0)) = x v c_0.  [back_demod(568),demod(751(3))].

given #84 (T,wt=14): 872 (c_0 v (x v c_0)) v (x v (c_0 v c_0)) ' = c_0.  [back_demod(789),demod(827(6))].

given #85 (T,wt=14): 884 (c_0 ' v (c_0 v (c_0 v c_0)) ') ' = c_0 v c_0.  [para(757(a,1),39(a,1,1,2,1,2,1)),demod(757(10),6(9),757(8),757(15))].

given #86 (A,wt=23): 35 x v (y v (z v (u v (v v w)))) = z v (x v (v v (y v (u v w)))).  [para(12(a,1),12(a,2,2,2))].

given #87 (F,wt=14): 994 (c_0 v c_0) v (c_0 ' v (x v c_0)) = x v c_0.  [para(6(a,1),811(a,1,2))].

given #88 (F,wt=15): 748 ((c_0 v (c_0 ' v c_0) ') ' v c_0 ') v c_0 = c_0.  [para(739(a,1),20(a,1,1,2,1))].

given #89 (T,wt=15): 792 ((c_0 v c_0) ' v (c_0 ' v c_0) ') ' = c_0 v c_0.  [back_demod(615),demod(751(3),751(14))].

given #90 (T,wt=15): 845 ((c_0 v (x v c_0)) ' v (x v c_0 ') ') ' = x.  [back_demod(494),demod(751(3),827(6))].

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

given #92 (F,wt=11): 1015 c_0 ' v (c_0 ' v c_0 ') ' = c_0.  [para(43(a,1),845(a,1,1,2,1)),demod(49(12),876(10)),flip(a)].

given #93 (F,wt=12): 1048 (c_0 ' v c_0 ') v c_0 = c_0 ' v c_0.  [para(1015(a,1),17(a,1,2))].

given #94 (T,wt=13): 1028 (c_0 ' v (c_0 ' v c_0 ') ' ') ' = c_0.  [para(668(a,1),845(a,1,1,2,1)),demod(690(14),1015(10),876(10)),flip(a)].

given #95 (T,wt=14): 1020 (c_0 ' v x ') ' v (c_0 ' v x) ' = c_0.  [para(20(a,1),845(a,1,1,2,1)),demod(117(13),876(10)),flip(a)].

given #96 (A,wt=23): 37 x v (y v (z v (u v (v v w)))) = z v (x v (u v (v v (y v w)))).  [para(12(a,2),12(a,2,2,2))].

given #97 (F,wt=14): 1074 (c_0 ' v (c_0 ' v c_0 ') ' ') v c_0 = c_0.  [para(1028(a,1),10(a,1,2))].

given #98 (F,wt=15): 875 ((x v (c_0 v c_0)) ' v (x v c_0 ') ') ' = x.  [para(751(a,1),9(a,1,1,1,1,2))].

given #99 (T,wt=15): 988 (c_0 v (x v c_0)) v c_0 = (x v (c_0 v c_0)) v c_0.  [para(788(a,1),17(a,1,2))].

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

given #101 (A,wt=19): 38 x v (y v (z v (u v v))) = u v (y v (x v (z v v))).  [para(12(a,2),12(a,2,2)),flip(a)].

given #102 (F,wt=15): 1085 (c_0 ' v x ') ' v c_0 = (c_0 ' v x) v c_0.  [para(1020(a,1),17(a,1,2)),flip(a)].

given #103 (F,wt=9): 1232 c_0 ' v (c_0 ' v c_0) = c_0.  [back_demod(1167),demod(1197(21),6(20),1168(19))].

given #104 (T,wt=5): 1255 c_0 v c_0 = c_0.  [para(1232(a,1),16(a,1,1,1,1,2,1,1)),demod(1253(6),18(8),751(4),1254(5),1197(6),1253(4),1253(9),18(11))].

given #105 (T,wt=5): 1339 c_0 ' ' = c_0.  [back_demod(751),demod(1255(6))].

given #106 (A,wt=18): 40 ((x v y) ' v (x v (c_0 ' v (y v y) ')) ') ' = x.  [para(18(a,1),9(a,1,1,1,1,2))].

given #107 (F,wt=6): 1303 c_0 ' v c_0 = c_0.  [back_demod(1253),demod(1255(7))].

given #108 (F,wt=8): 1283 (c_0 ' v c_0 ') ' = c_0.  [back_demod(1197),demod(1253(10),1255(9))].

given #109 (T,wt=9): 1288 (c_0 ' v c_0 ') v c_0 = c_0.  [back_demod(1048),demod(1253(11),1255(10))].

given #110 (T,wt=9): 1294 c_0 v (x v c_0) = x v c_0.  [back_demod(811),demod(1255(3),1253(5),1255(4))].

given #111 (A,wt=22): 45 (c_0 ' v (x v (y v ((y v (x v z)) v z))) ') ' = y v (x v z).  [para(12(a,1),18(a,1,1,2,1)),demod(6(6))].

given #112 (F,wt=10): 1273 c_0 ' v (x v c_0) = x v c_0.  [back_demod(1250),demod(1253(6),1255(5))].

given #113 (F,wt=11): 1370 x v ((x v c_0) v c_0) = x v c_0.  [para(1273(a,1),105(a,1,1,2,1,2,2)),demod(6(9),6(10),1368(13))].

given #114 (T,wt=12): 1372 (c_0 ' v (x v c_0) ') ' = x v c_0.  [para(1273(a,1),39(a,1,1,2,1,2,1)),demod(6(9),1370(9),1273(7),1273(12))].

given #115 (T,wt=12): 1416 ((x v c_0) ' v c_0 ') ' = x v c_0.  [para(1372(a,1),22(a,1,1,1,1,2)),demod(6(5),1370(5),1303(7))].

given #116 (A,wt=22): 46 (c_0 ' v (x v (y v ((x v (y v z)) v z))) ') ' = x v (y v z).  [para(12(a,2),18(a,1,1,2,1))].

given #117 (F,wt=13): 1295 c_0 v (x v (y v c_0)) = x v (y v c_0).  [back_demod(802),demod(1255(3),1253(5),1255(4))].

given #118 (F,wt=13): 1333 ((x v c_0) ' v (x v c_0 ') ') ' = x.  [back_demod(875),demod(1255(3))].

given #119 (T,wt=13): 1342 (c_0 ' v c_0 ') v (x v c_0) = x v c_0.  [back_demod(1162),demod(1273(13))].

given #120 (T,wt=13): 1373 x v ((c_0 ' v (x v c_0) ') v c_0) = c_0.  [para(1273(a,1),135(a,1,1,2,1,2,2)),demod(6(9),1370(9),6(7),1370(7),6(9))].

given #121 (A,wt=17): 47 x v ((c_0 ' v (x v ((x v y) v y)) ') v y) = c_0.  [para(43(a,1),6(a,1)),demod(6(6)),flip(a)].

given #122 (F,wt=7): 1486 (x v c_0) v c_0 = c_0.  [para(1370(a,1),47(a,1,2,1,2,1,2,1)),demod(1377(10),6(7),1370(7),6(11),1462(12))].

given #123 (F,wt=5): 1509 x v c_0 = c_0.  [back_demod(1436),demod(1491(11),1441(11)),flip(a)].

given #124 (T,wt=5): 1683 x ' ' = x.  [back_demod(1633),demod(1675(3),1660(8),1509(3),1675(4))].

given #125 (T,wt=5): 1694 c_0 v x = c_0.  [back_demod(1622),demod(1675(6),1683(4))].

given #126 (A,wt=25): 75 (x v (y v (x v ((x v (y v z) ') ' v z))) ') ' = (x v (y v z) ') '.  [para(13(a,1),9(a,1,1,1)),demod(6(7),6(6))].

given #127 (F,wt=5): 1697 x v x = x.  [back_demod(1594),demod(1675(5),1683(3))].

given #128 (F,wt=6): 1675 x v c_0 ' = x.  [back_demod(1525),demod(1631(11))].

% Operation v is associative-commutative; redundancy checks enabled.

given #129 (T,wt=6): 1692 c_0 ' v x = x.  [back_demod(1641),demod(1675(7),1683(5))].

given #130 (T,wt=7): 1797 x v y = y v x.  [para(1675(a,1),6(a,1,2)),demod(1675(4))].

given #131 (A,wt=21): 76 ((x v y) ' v ((y v z ') ' v (x v (y v z) ')) ') ' = x.  [para(9(a,1),13(a,1,1,1,1,2))].

given #132 (F,wt=8): 1664 x v (y v x ') = c_0.  [back_demod(17),demod(1509(5))].

given #133 (F,wt=8): 1684 x ' v (y v x) = c_0.  [back_demod(1627),demod(1640(5),1675(3),1675(4))].

given #134 (T,wt=8): 1842 x v (x ' v y) = c_0.  [para(1797(a,1),1664(a,1,2))].

given #135 (T,wt=8): 1883 (x v y) v y ' = c_0.  [para(1684(a,1),1797(a,1)),flip(a)].

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

given #137 (F,wt=8): 1918 (x v y) v x ' = c_0.  [para(1797(a,1),1883(a,1,1))].

given #138 (F,wt=9): 1747 x v (y v x ') ' = x.  [back_demod(1695),demod(1697(1))].

given #139 (T,wt=9): 1761 x v (y v x) = y v x.  [para(1697(a,1),6(a,1,2)),flip(a)].

given #140 (T,wt=9): 1814 x v (x v y) = x v y.  [back_demod(1746),demod(1797(2),1761(2))].

given #141 (A,wt=25): 81 ((x v (y v (z v (u v v))) ') ' v (y v (u v (x v (z v v)))) ') ' = x.  [para(12(a,1),13(a,1,1,2,1,2))].

given #142 (F,wt=9): 1951 x v (x ' v y) ' = x.  [para(1797(a,1),1747(a,1,2,1))].

given #143 (F,wt=10): 1663 x v (y v (z v x ')) = c_0.  [back_demod(21),demod(1509(6),1509(6))].

given #144 (T,wt=10): 1687 x ' v (y v (z v x)) = c_0.  [back_demod(1624),demod(1640(5),1675(3),1675(4))].

given #145 (T,wt=10): 1822 x v (y v (x v y) ') = c_0.  [back_demod(1704),demod(1797(3))].

given #146 (A,wt=21): 82 ((x v (y v (z v u)) ') ' v (z v (y v (x v u))) ') ' = x.  [para(12(a,1),13(a,1,1,2,1))].

given #147 (F,wt=10): 1884 x v (y v (x ' v z)) = c_0.  [para(1842(a,1),6(a,1,2)),demod(1509(2)),flip(a)].

given #148 (F,wt=10): 1886 x ' v (y v (x v z)) = c_0.  [para(1842(a,1),12(a,1,2)),demod(1509(2)),flip(a)].

given #149 (T,wt=10): 1891 (x v y) v (z v y ') = c_0.  [para(1883(a,1),6(a,1,2)),demod(1509(2)),flip(a)].

given #150 (T,wt=10): 1937 (x v y) v (z v x ') = c_0.  [para(1918(a,1),6(a,1,2)),demod(1509(2)),flip(a)].

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

given #152 (F,wt=10): 1938 (x v (y v z)) v y ' = c_0.  [para(6(a,1),1918(a,1,1))].

given #153 (F,wt=10): 1950 x ' v (y v x) ' = x '.  [para(1683(a,1),1747(a,1,2,1,2))].

given #154 (T,wt=10): 1997 x ' v (x v y) ' = x '.  [para(1683(a,1),1951(a,1,2,1,1))].

given #155 (T,wt=10): 1999 x v ((y v x ') v z) = c_0.  [para(1797(a,1),1663(a,1,2))].

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

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

given #158 (F,wt=10): 2001 (x ' v y) v (z v x) = c_0.  [para(1951(a,1),1663(a,1,2,2))].

given #159 (T,wt=10): 2023 (x v (y v z)) v z ' = c_0.  [para(1687(a,1),1797(a,1)),flip(a)].

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

given #161 (A,wt=25): 92 ((x v y) ' v ((y v (z v u) ') ' v (x v (z v (y v u)) ')) ') ' = x.  [para(13(a,1),13(a,1,1,1,1,2))].

given #162 (F,wt=10): 2074 x v ((x ' v y) v z) = c_0.  [para(1797(a,1),1884(a,1,2))].

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

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

given #165 (T,wt=10): 2100 (x v y) v (x ' v z) = c_0.  [para(1797(a,1),1937(a,1,2))].

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

given #167 (F,wt=10): 2123 ((x v y) v z) v x ' = c_0.  [para(1797(a,1),1938(a,1,1))].

given #168 (F,wt=10): 2132 ((x v y) v z) v y ' = c_0.  [para(1950(a,1),1937(a,1,2))].

given #169 (T,wt=11): 1698 x v (y v (z v x ')) ' = x.  [back_demod(1589),demod(1675(9),1683(7))].

given #170 (T,wt=11): 1812 x v (x v y) ' = x v y '.  [back_demod(1757),demod(1797(4),1747(4))].

given #171 (A,wt=23): 172 x v (y v (z v (u v (v v w)))) = z v (x v (v v (u v (y v w)))).  [para(25(a,1),12(a,2,2,2))].

given #172 (F,wt=11): 1990 x v (y v (x ' v z)) ' = x.  [para(6(a,1),1951(a,1,2,1))].

given #173 (F,wt=11): 2334 x v ((y v x ') v z) ' = x.  [para(1999(a,1),92(a,1,1,1,1)),demod(6(17),1754(16),1692(9),1683(7))].

given #174 (T,wt=11): 2460 x v (y v x) ' = x v y '.  [para(1797(a,1),1812(a,1,2,1))].

given #175 (T,wt=11): 2462 x v ((x ' v y) v z) ' = x.  [para(2074(a,1),1812(a,1,2,1)),demod(1675(3)),flip(a)].

given #176 (A,wt=19): 173 x v (y v (z v (u v v))) = u v (z v (x v (y v v))).  [para(25(a,1),12(a,2,2)),flip(a)].

given #177 (F,wt=12): 1661 x v (y v (z v (u v x '))) = c_0.  [back_demod(30),demod(1509(7),1509(7),1509(7))].

given #178 (F,wt=12): 1710 x v ((x v y) ' v (z v y)) = c_0.  [back_demod(1653),demod(1692(4),1675(5))].

given #179 (T,wt=12): 1713 x ' v (y v (z v (u v x))) = c_0.  [back_demod(1562),demod(1692(3),1675(4))].

given #180 (T,wt=12): 1885 x v (y v (z v (x ' v u))) = c_0.  [para(1842(a,1),12(a,1,2,2)),demod(1509(2),1509(2)),flip(a)].

given #181 (A,wt=23): 174 x v (y v (z v (u v (v v w)))) = u v (y v (x v (v v (z v w)))).  [para(12(a,1),25(a,1,2,2))].

given #182 (F,wt=12): 1887 x ' v (y v (z v (x v u))) = c_0.  [para(1842(a,1),24(a,1,2)),demod(1509(2)),flip(a)].

given #183 (F,wt=12): 1892 (x v (y v z)) v (x v z) ' = c_0.  [para(6(a,1),1883(a,1,1))].

given #184 (T,wt=12): 1893 (x v y) v (z v (u v y ')) = c_0.  [para(1883(a,1),12(a,1,2,2)),demod(1509(2),1509(2)),flip(a)].

given #185 (T,wt=12): 1939 (x v y) v (z v (u v x ')) = c_0.  [para(1918(a,1),12(a,1,2,2)),demod(1509(2),1509(2)),flip(a)].

given #186 (A,wt=23): 175 x v (y v (z v (u v (v v w)))) = v v (y v (x v (z v (u v w)))).  [para(12(a,2),25(a,1,2,2))].

given #187 (F,wt=12): 1940 (x v (y v (z v u))) v z ' = c_0.  [para(12(a,2),1918(a,1,1))].

given #188 (F,wt=12): 2095 (x v (y v z)) v (u v y ') = c_0.  [para(6(a,1),1937(a,1,1))].

given #189 (T,wt=12): 2134 x ' v (y v (x v z)) ' = x '.  [para(6(a,1),1997(a,1,2,1))].

given #190 (T,wt=12): 2139 x v (y v ((z v x ') v u)) = c_0.  [para(1999(a,1),6(a,1,2)),demod(1509(2)),flip(a)].

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

given #192 (F,wt=12): 2141 (x v y ') v (z v (y v u)) = c_0.  [para(1999(a,1),12(a,1,2)),demod(1509(2)),flip(a)].

given #193 (F,wt=12): 2173 (x v y ') v (z v (u v y)) = c_0.  [para(2000(a,1),6(a,1,2)),demod(1509(2)),flip(a)].

given #194 (T,wt=12): 2214 (x ' v y) v (z v (u v x)) = c_0.  [para(2001(a,1),6(a,1,2)),demod(1509(2)),flip(a)].

given #195 (T,wt=12): 2215 (x v (y ' v z)) v (u v y) = c_0.  [para(6(a,1),2001(a,1,1))].

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

given #197 (F,wt=12): 2262 (x v (y v z)) v (u v z ') = c_0.  [para(2023(a,1),6(a,1,2)),demod(1509(2)),flip(a)].

given #198 (F,wt=12): 2290 x ' v (y v ((z v x) v u)) = c_0.  [para(2024(a,1),6(a,1,2)),demod(1509(2)),flip(a)].

given #199 (T,wt=12): 2293 (x v y) v (z v (y ' v u)) = c_0.  [para(2024(a,1),12(a,1,2)),demod(1509(2)),flip(a)].

given #200 (T,wt=12): 2330 x ' v (y v (z v x)) ' = x '.  [para(1687(a,1),92(a,1,1,1,1)),demod(6(16),1754(15),1692(9),1683(7))].

given #201 (A,wt=23): 183 x v (y v (z v (u v (v v w)))) = v v (y v (x v (u v (z v w)))).  [para(25(a,1),25(a,1,2,2))].

given #202 (F,wt=12): 2337 x ' v ((y v x) v z) ' = x '.  [para(2024(a,1),92(a,1,1,1,1)),demod(6(16),1754(15),1692(9),1683(7))].

given #203 (F,wt=12): 2346 x v (y v ((x ' v z) v u)) = c_0.  [para(2074(a,1),6(a,1,2)),demod(1509(2)),flip(a)].

given #204 (T,wt=12): 2347 x v ((y v (x ' v z)) v u) = c_0.  [para(6(a,1),2074(a,1,2,1))].

given #205 (T,wt=12): 2349 (x ' v y) v (z v (x v u)) = c_0.  [para(2074(a,1),12(a,1,2)),demod(1509(2)),flip(a)].

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

given #207 (F,wt=12): 2357 x ' v (y v ((x v z) v u)) = c_0.  [para(2077(a,1),6(a,1,2)),demod(1509(2)),flip(a)].

given #208 (F,wt=12): 2358 x ' v ((y v (x v z)) v u) = c_0.  [para(6(a,1),2077(a,1,2,1))].

given #209 (T,wt=12): 2360 (x v y) v (z v (x ' v u)) = c_0.  [para(2077(a,1),12(a,1,2)),demod(1509(2)),flip(a)].

given #210 (T,wt=12): 2384 (x v (y v z)) v (y ' v u) = c_0.  [para(6(a,1),2100(a,1,1))].

given #211 (A,wt=23): 200 x v (y v (z v (u v (v v w)))) = z v (x v (y v (v v (u v w)))).  [para(27(a,1),12(a,1,2,2))].

given #212 (F,wt=12): 2409 ((x v y) v z) v (u v x ') = c_0.  [para(2123(a,1),6(a,1,2)),demod(1509(2)),flip(a)].

given #213 (F,wt=12): 2410 ((x v (y v z)) v u) v y ' = c_0.  [para(6(a,1),2123(a,1,1,1))].

given #214 (T,wt=12): 2411 (x v ((y v z) v u)) v y ' = c_0.  [para(6(a,1),2123(a,1,1))].

given #215 (T,wt=12): 2421 ((x v y) v z) v (u v y ') = c_0.  [para(2132(a,1),6(a,1,2)),demod(1509(2)),flip(a)].

given #216 (A,wt=23): 201 x v (y v (z v (u v (v v w)))) = x v (u v (y v (v v (z v w)))).  [para(12(a,1),27(a,1,2,2))].

given #217 (F,wt=12): 2423 (x v ((y v z) v u)) v z ' = c_0.  [para(6(a,1),2132(a,1,1))].

given #218 (F,wt=12): 2449 (x v (y v z ')) v (u v z) = c_0.  [para(1698(a,1),1663(a,1,2,2))].

given #219 (T,wt=12): 2450 x v ((y v (z v x ')) v u) = c_0.  [para(1698(a,1),1937(a,1,2)),demod(1797(5))].

given #220 (T,wt=12): 2463 x ' v ((x v y) v z) ' = x '.  [para(2077(a,1),1812(a,1,2,1)),demod(1675(4)),flip(a)].

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

given #222 (F,wt=12): 2506 ((x v y ') v z) v (u v y) = c_0.  [para(2334(a,1),1663(a,1,2,2))].

given #223 (F,wt=12): 2507 x v (((y v x ') v z) v u) = c_0.  [para(2334(a,1),1937(a,1,2)),demod(1797(5))].

given #224 (T,wt=12): 2508 (x v y) v ((z v y ') v u) = c_0.  [para(2334(a,1),2023(a,1,1,2)),demod(1683(6))].

given #225 (T,wt=12): 2509 (x v y) v ((z v x ') v u) = c_0.  [para(2334(a,1),2132(a,1,1,1)),demod(1683(6))].

given #226 (A,wt=23): 203 x v (y v (z v (u v (v v w)))) = x v (v v (y v (z v (u v w)))).  [para(12(a,2),27(a,1,2,2))].

given #227 (F,wt=12): 2537 ((x ' v y) v z) v (u v x) = c_0.  [para(2462(a,1),1663(a,1,2,2))].

given #228 (F,wt=12): 2538 x v (((x ' v y) v z) v u) = c_0.  [para(2462(a,1),1937(a,1,2)),demod(1797(5))].

given #229 (T,wt=12): 2539 (x v y) v ((y ' v z) v u) = c_0.  [para(2462(a,1),2023(a,1,1,2)),demod(1683(6))].

given #230 (T,wt=12): 2540 (x v y) v ((x ' v z) v u) = c_0.  [para(2462(a,1),2132(a,1,1,1)),demod(1683(6))].

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

given #232 (F,wt=12): 2595 x v ((y v x) ' v (z v y)) = c_0.  [para(1797(a,1),1710(a,1,2,1,1))].

given #233 (F,wt=12): 2596 x v (y v ((x v y) ' v z)) = c_0.  [para(1797(a,1),1710(a,1,2,2)),demod(6(4))].

given #234 (T,wt=12): 2634 (x v (y v (z v u))) v u ' = c_0.  [para(1713(a,1),1797(a,1)),flip(a)].

given #235 (T,wt=12): 2635 x ' v ((y v (z v x)) v u) = c_0.  [para(1797(a,1),1713(a,1,2))].

given #236 (A,wt=25): 206 ((x v (y v (z v (u v v))) ') ' v (y v (x v (u v (z v v)))) ') ' = x.  [para(27(a,1),13(a,1,1,1,1,2,1))].

given #237 (F,wt=12): 2677 (x v (y v z)) v (x v y) ' = c_0.  [para(1797(a,1),1892(a,1,1,2))].

given #238 (F,wt=11): 3985 (x v y) v z = x v (y v z).  [para(2677(a,1),1812(a,1,2,1)),demod(1675(5),1683(7),1797(6),6(6),6(5),2467(5),2466(5)),flip(a)].

given #239 (T,wt=12): 3670 (x v y) ' v (z v (y v x)) = c_0.  [para(2595(a,1),12(a,2))].

given #240 (T,wt=13): 1685 ((x v y) ' v (y ' v x) ') ' = x.  [back_demod(1626),demod(1640(7),1675(5),1675(6))].

given #241 (A,wt=23): 211 x v (y v (z v (u v (v v w)))) = z v (y v (x v (v v (u v w)))).  [para(27(a,1),25(a,1,2,2))].

given #242 (F,wt=13): 1699 x v (y v (z v (u v x '))) ' = x.  [back_demod(1588),demod(1675(10),1683(8))].

given #243 (F,wt=13): 1756 (x v y) ' v (x v y ') ' = x '.  [para(14(a,1),1683(a,1,1)),demod(1753(9)),flip(a)].

given #244 (T,wt=13): 1762 x v (y v (z v x)) = y v (z v x).  [para(1697(a,1),12(a,1,2,2)),flip(a)].

given #245 (T,wt=13): 1810 x v (y v (x v z)) = y v (x v z).  [back_demod(1763),demod(1797(2),1761(2))].

given #246 (A,wt=23): 212 x v (y v (z v (u v (v v w)))) = x v (v v (y v (u v (z v w)))).  [para(25(a,1),27(a,1,2,2))].

given #247 (F,wt=13): 1935 x v (y v (z v (x ' v u))) ' = x.  [para(1842(a,1),80(a,1,1,2,1,2)),demod(1509(9),1797(10),1692(10),1683(8))].

given #248 (F,wt=13): 1945 x v (y v (z v x ') ') = y v x.  [para(1747(a,1),6(a,1,2)),flip(a)].

given #249 (T,wt=13): 1989 x v (y v (x ' v z) ') = y v x.  [para(1951(a,1),6(a,1,2)),flip(a)].

given #250 (T,wt=13): 2525 (x v y) ' v (y v x ') ' = y '.  [para(2460(a,1),2460(a,1,2,1)),demod(1797(10),1950(10))].

given #251 (A,wt=23): 213 x v (y v (z v (u v (v v w)))) = x v (z v (y v (v v (u v w)))).  [para(27(a,1),27(a,1,2,2))].

given #252 (F,wt=13): 4409 x v ((y v x ') ' v z) = x v z.  [para(1747(a,1),3985(a,1,1)),flip(a)].

given #253 (F,wt=13): 4411 x v ((x ' v y) ' v z) = x v z.  [para(1951(a,1),3985(a,1,1)),flip(a)].

given #254 (T,wt=13): 4505 (x v y) ' v (y ' v x) ' = x '.  [para(1685(a,1),1683(a,1,1)),flip(a)].

given #255 (T,wt=13): 4538 (x v y ') ' v (y v x) ' = x '.  [para(2460(a,1),1756(a,1,1,1)),demod(1683(6),1761(5))].

given #256 (A,wt=23): 430 x v (y v (z v (u v (v v w)))) = v v (x v (z v (y v (u v w)))).  [para(24(a,1),12(a,1,2))].

given #257 (F,wt=13): 4547 (x v y ') ' v (z v y) = z v y.  [para(1747(a,1),1762(a,1,2,2)),demod(1747(9))].

given #258 (F,wt=13): 4548 (x ' v y) ' v (z v x) = z v x.  [para(1951(a,1),1762(a,1,2,2)),demod(1951(9))].

given #259 (T,wt=13): 4592 (x ' v y) ' v (y v x) ' = y '.  [para(1683(a,1),2525(a,1,2,1,2))].

given #260 (T,wt=13): 4593 (x v y) ' v (x ' v y) ' = y '.  [para(1797(a,1),2525(a,1,2,1))].

given #261 (A,wt=23): 431 x v (y v (z v (u v (v v w)))) = y v (x v (v v (z v (u v w)))).  [para(24(a,2),12(a,1,2)),flip(a)].

given #262 (F,wt=14): 1649 x v (y v (z v (u v (v v x ')))) = c_0.  [back_demod(137),demod(1509(8),1509(8),1509(8),1509(8))].

given #263 (F,wt=14): 1751 (x v y) ' v (z v (x v (u v y))) = c_0.  [back_demod(1729),demod(1746(3))].

given #264 (T,wt=14): 1850 x ' v (y v (z v (u v (v v x)))) = c_0.  [para(1684(a,1),26(a,1,2,2,2)),demod(1509(2),1509(2),1509(2)),flip(a)].

given #265 (T,wt=14): 1888 x v (y v (z v (u v (x ' v v)))) = c_0.  [para(1842(a,1),26(a,1,2,2,2)),demod(1509(2),1509(2),1509(2)),flip(a)].

given #266 (A,wt=23): 432 x v (y v (z v (u v (v v w)))) = z v (v v (x v (y v (u v w)))).  [para(24(a,1),12(a,2,2)),flip(a)].

given #267 (F,wt=14): 1889 x ' v (y v (z v (u v (x v v)))) = c_0.  [para(1842(a,1),31(a,1,2,2)),demod(1509(2),1509(2)),flip(a)].

given #268 (F,wt=14): 1981 x ' v (y v (z v (u v x))) ' = x '.  [para(1684(a,1),81(a,1,1,2,1,2,2)),demod(1509(9),1509(9),1797(10),1692(10),1683(8))].

given #269 (T,wt=14): 1984 x ' v (y v (z v (x v u))) ' = x '.  [para(1842(a,1),81(a,1,1,2,1,2)),demod(1509(9),1797(10),1692(10),1683(8))].

given #270 (T,wt=14): 2124 x ' v (y v (z v x) ') = y v x '.  [para(1950(a,1),6(a,1,2)),flip(a)].

given #271 (A,wt=23): 433 x v (y v (z v (u v (v v w)))) = u v (x v (v v (y v (z v w)))).  [para(12(a,1),24(a,1,2,2))].

given #272 (F,wt=14): 2133 x ' v (y v (x v z) ') = y v x '.  [para(1997(a,1),6(a,1,2)),flip(a)].

given #273 (F,wt=14): 3668 (x v y) ' v (z v (y v (u v x))) = c_0.  [para(2595(a,1),12(a,1,2)),demod(1509(2)),flip(a)].

given #274 (T,wt=14): 3681 (x v y) ' v (z v (u v (y v x))) = c_0.  [para(2595(a,1),24(a,1,2)),demod(1509(2)),flip(a)].

given #275 (T,wt=14): 3767 x v (y v (z v ((x v y) ' v u))) = c_0.  [para(6(a,1),2596(a,1,2,2))].

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

given #277 (F,wt=14): 3773 x v (y v (z v ((y v x) ' v u))) = c_0.  [para(2596(a,1),25(a,1,2)),demod(1509(2)),flip(a)].

given #278 (F,wt=14): 3779 (x v y) ' v (z v (x v (y v u))) = c_0.  [para(2596(a,1),26(a,1,2)),demod(1509(2)),flip(a)].

given #279 (T,wt=14): 3787 (x v y) ' v (z v (y v (x v u))) = c_0.  [para(2596(a,1),32(a,1,2)),demod(1509(2)),flip(a)].

given #280 (T,wt=14): 4412 x ' v ((y v x) ' v z) = x ' v z.  [para(1950(a,1),3985(a,1,1)),flip(a)].

given #281 (A,wt=23): 440 x v (y v (z v (u v (v v w)))) = v v (x v (u v (y v (z v w)))).  [para(25(a,1),24(a,1,2,2))].

given #282 (F,wt=14): 4413 x ' v ((x v y) ' v z) = x ' v z.  [para(1997(a,1),3985(a,1,1)),flip(a)].

given #283 (F,wt=14): 4549 (x v y) ' v (z v y ') = z v y '.  [para(1950(a,1),1762(a,1,2,2)),demod(1950(9))].

given #284 (T,wt=14): 4550 (x v y) ' v (z v x ') = z v x '.  [para(1997(a,1),1762(a,1,2,2)),demod(1997(9))].

given #285 (T,wt=15): 1994 x v (y v (z v (u v (x ' v v)))) ' = x.  [para(26(a,2),1951(a,1,2,1))].

given #286 (A,wt=23): 441 x v (y v (z v (u v (v v w)))) = x v (v v (z v (y v (u v w)))).  [para(24(a,1),27(a,1,2))].

given #287 (F,wt=15): 2069 x v (y v (z v (u v (v v x ')))) ' = x.  [para(1663(a,1),82(a,1,1,2,1,2,2)),demod(1509(10),1509(10),1797(11),1692(11),1683(9))].

given #288 (F,wt=15): 2444 x v (y v (z v (u v x ')) ') = y v x.  [para(1698(a,1),6(a,1,2)),flip(a)].

given #289 (T,wt=15): 2454 x v (y v (x v z) ') = y v (x v z ').  [para(1812(a,1),6(a,1,2)),flip(a)].

given #290 (T,wt=15): 2455 x v (y v (x v z)) ' = x v (y v z) '.  [para(6(a,1),1812(a,1,2,1))].

given #291 (A,wt=23): 442 x v (y v (z v (u v (v v w)))) = x v (y v (v v (z v (u v w)))).  [para(24(a,2),27(a,1,2)),flip(a)].

given #292 (F,wt=15): 2493 x v (y v (z v (x ' v u)) ') = y v x.  [para(1990(a,1),6(a,1,2)),flip(a)].

given #293 (F,wt=15): 2515 x v (y v (z v x) ') = y v (x v z ').  [para(2460(a,1),6(a,1,2)),flip(a)].

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

given #295 (T,wt=15): 4416 x v ((x v y) ' v z) = x v (y ' v z).  [para(1812(a,1),3985(a,1,1)),demod(3985(3)),flip(a)].

given #296 (A,wt=23): 455 x v (y v (z v (u v (v v w)))) = y v (x v (v v (u v (z v w)))).  [para(24(a,2),24(a,1,2))].

given #297 (F,wt=15): 4418 x v ((y v (x ' v z)) ' v u) = x v u.  [para(1990(a,1),3985(a,1,1)),flip(a)].

given #298 (F,wt=15): 4419 x v (y v (z v x)) ' = x v (y v z) '.  [para(3985(a,1),2460(a,1,2,1))].

given #299 (T,wt=15): 4420 x v ((y v x) ' v z) = x v (y ' v z).  [para(2460(a,1),3985(a,1,1)),demod(3985(3)),flip(a)].

given #300 (T,wt=15): 4427 (x v y) ' v (z v x) = y ' v (z v x).  [back_demod(3739),demod(4412(6)),flip(a)].

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

given #302 (F,wt=15): 4428 (x v y) ' v (z v y) = x ' v (z v y).  [back_demod(2603),demod(4413(6)),flip(a)].

given #303 (F,wt=15): 4551 (x v (y v z ')) ' v (u v z) = u v z.  [para(1698(a,1),1762(a,1,2,2)),demod(1698(11))].

given #304 (T,wt=15): 4553 (x v (y ' v z)) ' v (u v y) = u v y.  [para(1990(a,1),1762(a,1,2,2)),demod(1990(11))].

given #305 (T,wt=16): 1841 x v (y v (z v (u v (v v (w v x '))))) = c_0.  [para(1664(a,1),33(a,1,2,2,2,2)),demod(1509(2),1509(2),1509(2),1509(2)),flip(a)].

given #306 (A,wt=23): 457 x v (y v (z v (u v (v v w)))) = u v (v v (x v (y v (z v w)))).  [para(24(a,2),24(a,2,2)),flip(a)].

given #307 (F,wt=16): 1860 x ' v (y v (z v (u v (v v (w v x))))) = c_0.  [para(1684(a,1),33(a,1,2,2,2,2)),demod(1509(2),1509(2),1509(2),1509(2)),flip(a)].

given #308 (F,wt=16): 1890 x v (y v (z v (u v (v v (x ' v w))))) = c_0.  [para(1842(a,1),33(a,1,2,2,2,2)),demod(1509(2),1509(2),1509(2),1509(2)),flip(a)].

given #309 (T,wt=16): 2070 x ' v (y v (z v (u v (v v x)))) ' = x '.  [para(1687(a,1),82(a,1,1,2,1,2,2)),demod(1509(10),1509(10),1797(11),1692(11),1683(9))].

given #310 (T,wt=16): 2075 x ' v (y v (z v (u v (v v (x v w))))) = c_0.  [para(1886(a,1),26(a,1,2,2,2)),demod(1509(2),1509(2),1509(2)),flip(a)].

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

given #312 (F,wt=16): 2125 (x v y) ' v (x v (z v y)) ' = (x v y) '.  [para(6(a,1),1950(a,1,2,1))].

given #313 (F,wt=16): 2137 x ' v (y v (z v (u v (x v v)))) ' = x '.  [para(26(a,2),1997(a,1,2,1))].

given #314 (T,wt=16): 2748 x ' v (y v (z v (x v u)) ') = y v x '.  [para(2134(a,1),6(a,1,2)),flip(a)].

given #315 (T,wt=16): 3027 x ' v (y v (z v (u v x)) ') = y v x '.  [para(2330(a,1),6(a,1,2)),flip(a)].

given #316 (A,wt=19): 534 x v (y v (z v (u v v))) = u v (y v (z v (x v v))).  [para(26(a,1),12(a,1))].

given #317 (F,wt=16): 3696 (x v y) ' v (z v (u v (v v (y v x)))) = c_0.  [para(2595(a,1),31(a,1,2,2)),demod(1509(2),1509(2)),flip(a)].

given #318 (F,wt=16): 3988 (x v y) ' v (x v (y v z)) ' = (x v y) '.  [para(2677(a,1),2460(a,1,2,1)),demod(1797(5),1692(5)),flip(a)].

given #319 (T,wt=14): 5311 (x v y) ' v (y v x) ' = (x v y) '.  [para(1761(a,1),3988(a,1,2,1))].

given #320 (T,wt=16): 4422 x ' v ((y v (x v z)) ' v u) = x ' v u.  [para(2134(a,1),3985(a,1,1)),flip(a)].

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

given #322 (F,wt=16): 4423 x ' v ((y v (z v x)) ' v u) = x ' v u.  [para(2330(a,1),3985(a,1,1)),flip(a)].

given #323 (F,wt=16): 4464 (x v y) ' v (z v (y v x)) ' = (x v y) '.  [para(3670(a,1),1812(a,1,2,1)),demod(1797(5),1692(5)),flip(a)].

given #324 (T,wt=16): 4515 (x v (y v z)) ' v (z v y) ' = (z v y) '.  [para(3670(a,1),1685(a,1,1,1,1)),demod(1692(10),1683(8))].

given #325 (T,wt=16): 4555 (x v (y v z)) ' v (u v y ') = u v y '.  [para(2134(a,1),1762(a,1,2,2)),demod(2134(11))].

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

given #327 (F,wt=16): 4556 (x v (y v z)) ' v (u v z ') = u v z '.  [para(2330(a,1),1762(a,1,2,2)),demod(2330(11))].

given #328 (F,wt=16): 5239 (x v y) ' v (y v (z v x)) ' = (y v x) '.  [para(1797(a,1),2125(a,1,1,1))].

given #329 (T,wt=16): 5300 (x v y) ' v (y v (x v z)) ' = (x v y) '.  [para(6(a,1),3988(a,1,2,1))].

given #330 (T,wt=16): 5329 (x v (y v z)) ' v (y v x) ' = (x v y) '.  [para(5311(a,1),4411(a,2)),demod(1683(5),3985(4),5328(9))].

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

given #332 (F,wt=16): 5366 (x v (y v z)) ' v (z v x) ' = (z v x) '.  [para(6(a,1),4515(a,1,1,1))].

given #333 (F,wt=17): 1770 x v (y v (z v (u v x))) = y v (z v (u v x)).  [para(1697(a,1),26(a,1,2,2,2)),flip(a)].

given #334 (T,wt=17): 1805 x v (y v (z v (x v u))) = y v (z v (x v u)).  [back_demod(1773),demod(1797(4),1770(4),1803(6),1804(4))].

given #335 (T,wt=17): 1947 x v (y v (z v (u v x ') ')) = y v (z v x).  [para(1747(a,1),12(a,1,2,2)),flip(a)].

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

given #337 (F,wt=17): 1992 x v (y v (z v (x ' v u) ')) = y v (z v x).  [para(1951(a,1),12(a,1,2,2)),flip(a)].

given #338 (F,wt=17): 1996 x v (y v (z v (u v (v v (x ' v w))))) ' = x.  [para(33(a,2),1951(a,1,2,1))].

given #339 (T,wt=17): 2164 x v (y v (z v (u v (v v (w v x '))))) ' = x.  [para(1663(a,1),84(a,1,1,2,1,2,2,2)),demod(1509(11),1509(11),1509(11),1797(12),1692(12),1683(10))].

given #340 (T,wt=17): 4304 x v (y v (z v (u v (x ' v v))) ') = x v y.  [back_demod(2784),demod(3985(7))].

given #341 (A,wt=23): 557 x v (y v (z v (u v (v v w)))) = u v (y v (v v (x v (z v w)))).  [para(24(a,2),26(a,2,2))].

given #342 (F,wt=17): 4393 x v (y v (z v (u v (v v x '))) ') = x v y.  [back_demod(2162),demod(3985(7))].

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

given #344 (T,wt=17): 4520 (x v y) ' v (z v (x v y ') ') = z v x '.  [para(1756(a,1),6(a,1,2)),flip(a)].

given #345 (T,wt=17): 4545 (x v y) ' v ((x v y ') ' v z) = x ' v z.  [para(1756(a,1),3985(a,1,1)),flip(a)].

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

given #347 (F,wt=17): 4557 (x v (y v (z v u '))) ' v (v v u) = v v u.  [para(1699(a,1),1762(a,1,2,2)),demod(1699(13))].

given #348 (F,wt=17): 4564 x v ((y v (z v (x ' v u))) ' v v) = x v v.  [para(1935(a,1),3985(a,1,1)),flip(a)].

given #349 (T,wt=17): 4566 (x v (y v (z ' v u))) ' v (v v z) = v v z.  [para(1935(a,1),1762(a,1,2,2)),demod(1935(13))].

given #350 (T,wt=17): 4572 x v (y v ((z v x ') ' v u)) = y v (x v u).  [para(1945(a,1),3985(a,1,1)),demod(3985(2),3985(7)),flip(a)].

given #351 (A,wt=23): 564 x v (y v (z v (u v (v v w)))) = v v (y v (z v (x v (u v w)))).  [para(26(a,2),26(a,2,2)),flip(a)].

given #352 (F,wt=17): 4574 (x v y ') ' v (z v (u v y)) = z v (u v y).  [para(1945(a,1),1762(a,1,2,2)),demod(3985(7),1805(7),1945(11))].

given #353 (F,wt=17): 4581 x v (y v ((x ' v z) ' v u)) = y v (x v u).  [para(1989(a,1),3985(a,1,1)),demod(3985(2),3985(7)),flip(a)].

given #354 (T,wt=17): 4583 (x ' v y) ' v (z v (u v x)) = z v (u v x).  [para(1989(a,1),1762(a,1,2,2)),demod(3985(7),1805(7),1989(11))].

given #355 (T,wt=17): 4584 (x v y) ' v (z v (y v x ') ') = z v y '.  [para(2525(a,1),6(a,1,2)),flip(a)].

given #356 (A,wt=23): 717 x v (y v (z v (u v (v v w)))) = v v (z v (y v (x v (u v w)))).  [para(31(a,1),25(a,1))].

given #357 (F,wt=17): 4594 (x v y) ' v ((y v x ') ' v z) = y ' v z.  [para(2525(a,1),3985(a,1,1)),flip(a)].

given #358 (F,wt=17): 4602 (x v y ') ' v (z v (y v u)) = z v (y v u).  [para(4409(a,1),12(a,1,2)),flip(a)].

given #359 (T,wt=17): 4620 (x ' v y) ' v (z v (x v u)) = z v (x v u).  [para(4411(a,1),12(a,1,2)),flip(a)].

given #360 (T,wt=17): 4636 (x v y) ' v (z v (y ' v x) ') = z v x '.  [para(4505(a,1),6(a,1,2)),flip(a)].

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

% Proof 1 at 6.61 (+ 0.08) seconds: distributivity_1.
% Length of proof is 152.
% Level of proof is 49.
% Maximum clause weight is 25.
% Given clauses 360.

3 x v x ' = y v y '.  [input].
4 (x v y ') ^ (x v y) = x.  [input].
5 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity_1).  [clausify].
6 x v (y v z) = y v (x v z).  [input].
7 x ^ y = (x ' v y ') '.  [input].
8 x v x ' = y v y '.  [copy(3)].
9 ((x v y ') ' v (x v y) ') ' = x.  [copy(4),demod(7(4))].
10 x v x ' = c_0.  [new_symbol(8)].
11 (c1 ' v (c2 v c3) ') ' != (c1 ' v c2 ') ' v (c1 ' v c3 ') ' # answer(distributivity_1).  [copy(5),demod(7(3),7(9),7(18)),flip(a)].
12 x v (y v (z v u)) = z v (x v (y v u)).  [para(6(a,1),6(a,1,2))].
13 ((x v (y v z) ') ' v (y v (x v z)) ') ' = x.  [para(6(a,1),9(a,1,1,2,1))].
14 ((x v y) ' v (x v ((y v z ') ' v (y v z) ')) ') ' = x.  [para(9(a,1),9(a,1,1,1,1,2))].
15 (x v (x v ((x v y ') ' v y)) ') ' = (x v y ') '.  [para(9(a,1),9(a,1,1,1)),demod(6(5))].
16 (((x v y ') ' v (x v y) ' ') ' v x) ' = (x v y ') '.  [para(9(a,1),9(a,1,1,2))].
17 x v (y v x ') = y v c_0.  [para(10(a,1),6(a,1,2)),flip(a)].
18 (c_0 ' v (x v x) ') ' = x.  [para(10(a,1),9(a,1,1,1,1))].
19 ((x v x ' ') ' v c_0 ') ' = x.  [para(10(a,1),9(a,1,1,2,1))].
20 ((x v y ') ' v (x v y) ') v x = c_0.  [para(9(a,1),10(a,1,2))].
21 x v (y v (z v x ')) = y v (z v c_0).  [para(17(a,1),6(a,1,2)),flip(a)].
22 ((x v (y v x ') ') ' v (y v c_0) ') ' = x.  [para(17(a,1),9(a,1,1,2,1))].
26 x v (y v (z v (u v v))) = u v (x v (y v (z v v))).  [para(12(a,2),6(a,1,2))].
39 (c_0 ' v (x v ((x v y) v y)) ') ' = x v y.  [para(6(a,1),18(a,1,1,2,1))].
41 (x v (c_0 ' v (x v x)) ') ' = c_0 '.  [para(18(a,1),9(a,1,1,1))].
43 (c_0 ' v (x v x) ') v x = c_0.  [para(18(a,1),10(a,1,2))].
44 (c_0 ' v (x v x) ') v (y v x) = y v c_0.  [para(18(a,1),17(a,1,2,2))].
45 (c_0 ' v (x v (y v ((y v (x v z)) v z))) ') ' = y v (x v z).  [para(12(a,1),18(a,1,1,2,1)),demod(6(6))].
47 x v ((c_0 ' v (x v ((x v y) v y)) ') v y) = c_0.  [para(43(a,1),6(a,1)),demod(6(6)),flip(a)].
49 (c_0 ' v (x ' v x ') ') v c_0 = x v c_0.  [para(43(a,1),17(a,1,2)),flip(a)].
59 (((x v x ' ') ' v c_0 ' ') ' v x) ' = (x v x ' ') '.  [para(19(a,1),9(a,1,1,2))].
63 (x v (x v (c_0 ' v x)) ') ' = c_0 '.  [para(6(a,1),41(a,1,1,2,1))].
67 (x v (c_0 ' v (x v x)) ') v c_0 ' = c_0.  [para(41(a,1),10(a,1,2))].
69 (c_0 ' ' v (c_0 ' ' v c_0) ') ' = c_0 '.  [para(17(a,1),41(a,1,1,2,1))].
105 (c_0 ' v (x v (x v (c_0 ' v x))) ') ' = x.  [para(63(a,1),9(a,1,1,1))].
117 ((x ' v y ') ' v (x ' v y) ') v c_0 = x v c_0.  [para(20(a,1),17(a,1,2)),flip(a)].
131 (c_0 ' v (x v (c_0 ' v (x v x))) ') v x = c_0.  [para(41(a,1),20(a,1,1,1))].
135 (c_0 ' v (x v (x v (c_0 ' v x))) ') v x = c_0.  [para(63(a,1),20(a,1,1,1))].
154 (x v (c_0 ' v (x v x)) ') v c_0 = c_0 v c_0.  [para(67(a,1),17(a,1,2)),flip(a)].
161 (c_0 ' v (c_0 ' ' v (c_0 ' ' v c_0)) ') ' = c_0 ' '.  [para(69(a,1),9(a,1,1,1))].
190 ((x v x ' ') ' v (x v ((x v x ' ') ' v c_0)) ') ' = x.  [para(19(a,1),15(a,1,1,2,1,2,1)),demod(6(11),19(22))].
195 (x v (y v ((x v (y v x ') ') ' v c_0)) ') ' = (x v (y v x ') ') '.  [para(21(a,1),15(a,1,1,2,1)),demod(6(8))].
228 ((x v (y v c_0) ') ' v (y v ((c_0 ' v (z v z) ') v (x v z))) ') ' = x.  [para(44(a,2),13(a,1,1,2,1,2))].
251 ((x v ((x v x ' ') ' v c_0) ' ') ' v (x v x ' ') ') ' = x.  [para(19(a,1),16(a,1,1,1,1,1)),demod(19(24))].
297 x v (c_0 ' v (x v x)) ' = c_0.  [para(154(a,1),9(a,1,1,2,1)),demod(67(9),18(8)),flip(a)].
302 ((x v (y v x ') ') ' v (y v c_0) ') v (z v x) = z v c_0.  [para(22(a,1),17(a,1,2,2))].
306 ((x v y) ' v ((y v (z v y ') ') ' v (x v (z v c_0) ')) ') ' = x.  [para(22(a,1),13(a,1,1,1,1,2))].
319 x v (y v (c_0 ' v (x v x)) ') = y v c_0.  [para(297(a,1),6(a,1,2)),flip(a)].
321 x v (x v (c_0 ' v x)) ' = c_0.  [para(6(a,1),297(a,1,2,1))].
322 (c_0 ' v (x v x)) v c_0 = x v c_0.  [para(297(a,1),17(a,1,2))].
323 c_0 ' ' v (c_0 ' ' v c_0) ' = c_0.  [para(17(a,1),297(a,1,2,1))].
329 ((x v (y v (c_0 ' v (x v x)) ') ') ' v (y v c_0) ') ' = x.  [para(297(a,1),13(a,1,1,2,1,2))].
333 x v (y v (x v (c_0 ' v x)) ') = y v c_0.  [para(321(a,1),6(a,1,2)),flip(a)].
334 (x v (c_0 ' v x)) v c_0 = x v c_0.  [para(321(a,1),17(a,1,2))].
345 (c_0 ' ' v c_0) v c_0 = c_0 ' ' v c_0.  [para(17(a,1),322(a,1,1))].
362 (c_0 ' ' v c_0) v (x v c_0) = x v (c_0 ' ' v c_0).  [para(323(a,1),21(a,1,2,2))].
428 (c_0 ' v (x v x)) v (y v c_0) = x v (y v c_0).  [para(319(a,1),21(a,1,2))].
462 ((x v x) ' v ((x v (c_0 ' v x) ') ' v c_0) ') ' = x.  [para(333(a,1),14(a,1,1,2,1))].
472 c_0 ' ' v c_0 = c_0 ' '.  [para(345(a,1),39(a,1,1,2,1,2,1)),demod(345(14),6(13),345(12),161(14),345(10)),flip(a)].
484 c_0 ' ' v (x v c_0) = x v c_0 ' '.  [back_demod(362),demod(472(5),472(11))].
494 ((c_0 ' ' v (x v c_0)) ' v (x v c_0 ') ') ' = x.  [para(484(a,2),9(a,1,1,1,1))].
495 c_0 ' v (c_0 ' ' v (x v c_0)) = x v c_0.  [para(484(a,2),17(a,1,2))].
525 c_0 ' ' v (x v c_0) = (x v (c_0 ' v x)) v c_0 ' '.  [para(334(a,1),484(a,1,2))].
568 c_0 ' ' v (x v (c_0 ' v c_0)) = x v c_0.  [para(495(a,1),12(a,2))].
581 (c_0 ' v (c_0 ' v ((c_0 ' v c_0) v c_0)) ') v c_0 = c_0 ' '.  [para(43(a,1),568(a,1,2)),demod(472(5),6(14)),flip(a)].
739 c_0 v (c_0 ' v c_0) = c_0.  [para(428(a,1),39(a,1,1,2,1,2)),demod(6(10),6(9),105(13),6(7)),flip(a)].
751 c_0 ' ' = c_0 v c_0.  [para(739(a,1),44(a,1,2)),demod(6(11),581(15))].
798 (c_0 ' v (c_0 ' v ((c_0 ' v c_0) v c_0)) ') v c_0 = c_0 v c_0.  [back_demod(581),demod(751(18))].
811 (c_0 v c_0) v (x v (c_0 ' v c_0)) = x v c_0.  [back_demod(568),demod(751(3))].
827 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0).  [back_demod(525),demod(751(3),751(13),6(14),334(13))].
845 ((c_0 v (x v c_0)) ' v (x v c_0 ') ') ' = x.  [back_demod(494),demod(751(3),827(6))].
865 ((c_0 v ((x v x ' ') ' v c_0)) ' v x) ' = (x v x ' ') '.  [back_demod(59),demod(751(7),6(8))].
876 ((c_0 v (c_0 v c_0)) ' v c_0 ') ' = c_0.  [para(751(a,1),19(a,1,1,1,1,2))].
1015 c_0 ' v (c_0 ' v c_0 ') ' = c_0.  [para(43(a,1),845(a,1,1,2,1)),demod(49(12),876(10)),flip(a)].
1020 (c_0 ' v x ') ' v (c_0 ' v x) ' = c_0.  [para(20(a,1),845(a,1,1,2,1)),demod(117(13),876(10)),flip(a)].
1047 c_0 ' v (x v (c_0 ' v c_0 ') ') = x v c_0.  [para(1015(a,1),6(a,1,2)),flip(a)].
1085 (c_0 ' v x ') ' v c_0 = (c_0 ' v x) v c_0.  [para(1020(a,1),17(a,1,2)),flip(a)].
1167 (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(1047(a,1),131(a,1,1,2,1,2)),demod(1085(16),6(15),1085(14))].
1168 (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(131(a,1),1047(a,1,2)),demod(1047(28),1085(20),6(19),1085(18)),flip(a)].
1197 (c_0 ' v c_0 ') ' = c_0 ' v c_0.  [para(1085(a,1),15(a,1,1,2,1,2)),demod(39(14)),flip(a)].
1232 c_0 ' v (c_0 ' v c_0) = c_0.  [back_demod(1167),demod(1197(21),6(20),1168(19))].
1250 c_0 ' v (x v (c_0 ' v c_0)) = x v c_0.  [back_demod(1047),demod(1197(8))].
1253 c_0 ' v c_0 = c_0 v c_0.  [para(1232(a,1),44(a,1,2)),demod(6(11),798(15)),flip(a)].
1254 c_0 v (c_0 v c_0) = c_0.  [para(44(a,2),1232(a,1,2)),demod(6(11),43(10),1253(6),6(6),1253(5))].
1255 c_0 v c_0 = c_0.  [para(1232(a,1),16(a,1,1,1,1,2,1,1)),demod(1253(6),18(8),751(4),1254(5),1197(6),1253(4),1253(9),18(11))].
1261 c_0 ' v (x v (y v c_0)) = x v (y v c_0).  [para(1232(a,1),26(a,1,2,2)),demod(1253(9),1255(8)),flip(a)].
1273 c_0 ' v (x v c_0) = x v c_0.  [back_demod(1250),demod(1253(6),1255(5))].
1294 c_0 v (x v c_0) = x v c_0.  [back_demod(811),demod(1255(3),1253(5),1255(4))].
1303 c_0 ' v c_0 = c_0.  [back_demod(1253),demod(1255(7))].
1339 c_0 ' ' = c_0.  [back_demod(751),demod(1255(6))].
1344 (((x v x ' ') ' v c_0) ' v x) ' = (x v x ' ') '.  [back_demod(865),demod(1294(8))].
1368 (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(428(a,1),45(a,1,1,2,1,2,2)),demod(6(11),1261(12),6(10),6(20),1261(21))].
1370 x v ((x v c_0) v c_0) = x v c_0.  [para(1273(a,1),105(a,1,1,2,1,2,2)),demod(6(9),6(10),1368(13))].
1372 (c_0 ' v (x v c_0) ') ' = x v c_0.  [para(1273(a,1),39(a,1,1,2,1,2,1)),demod(6(9),1370(9),1273(7),1273(12))].
1373 x v ((c_0 ' v (x v c_0) ') v c_0) = c_0.  [para(1273(a,1),135(a,1,1,2,1,2,2)),demod(6(9),1370(9),6(7),1370(7),6(9))].
1377 x v (y v ((x v c_0) v c_0)) = y v (x v c_0).  [para(1370(a,1),6(a,1,2)),flip(a)].
1416 ((x v c_0) ' v c_0 ') ' = x v c_0.  [para(1372(a,1),22(a,1,1,1,1,2)),demod(6(5),1370(5),1303(7))].
1429 ((x v (y v c_0)) ' v ((y v c_0) ' v (x v c_0 ')) ') ' = x.  [para(1416(a,1),13(a,1,1,1,1,2))].
1436 ((x v c_0) ' v ((x v c_0) v ((x v c_0) ' v c_0)) ') ' = x v c_0.  [para(1416(a,1),15(a,1,1,2,1,2,1)),demod(6(11),1416(21))].
1441 ((x v c_0) ' v ((x v c_0) ' v c_0) ') ' = c_0.  [para(1416(a,1),22(a,1,1,1,1,2)),demod(1294(4))].
1462 x v (y v ((c_0 ' v (x v c_0) ') v c_0)) = y v c_0.  [para(1373(a,1),6(a,1,2)),flip(a)].
1486 (x v c_0) v c_0 = c_0.  [para(1370(a,1),47(a,1,2,1,2,1,2,1)),demod(1377(10),6(7),1370(7),6(11),1462(12))].
1491 (x v c_0) v (y v c_0) = y v c_0.  [para(1486(a,1),6(a,1,2)),flip(a)].
1509 x v c_0 = c_0.  [back_demod(1436),demod(1491(11),1441(11)),flip(a)].
1525 (c_0 ' v (c_0 ' v (x v c_0 ')) ') ' = x.  [back_demod(1429),demod(1509(2),1509(2),1509(4))].
1536 (x v x ' ') ' = (c_0 ' v x) '.  [back_demod(1344),demod(1509(6)),flip(a)].
1594 ((x v x) ' v c_0 ') ' = x.  [back_demod(462),demod(1509(10))].
1619 ((x v (y v (c_0 ' v (x v x)) ') ') ' v c_0 ') ' = x.  [back_demod(329),demod(1509(11))].
1626 ((x v y) ' v ((y v (z v y ') ') ' v (x v c_0 ')) ') ' = x.  [back_demod(306),demod(1509(9))].
1627 ((x v (y v x ') ') ' v c_0 ') v (z v x) = c_0.  [back_demod(302),demod(1509(7),1509(12))].
1631 (c_0 ' v (c_0 ' v x) ') ' = x.  [back_demod(251),demod(1536(4),1509(6),1339(3),1509(2),1536(6))].
1633 ((x v c_0 ') ' v (y v ((c_0 ' v (z v z) ') v (x v z))) ') ' = x.  [back_demod(228),demod(1509(2))].
1640 (x v (y v x ') ') ' = (x v c_0 ') '.  [back_demod(195),demod(1509(7),1509(2)),flip(a)].
1641 ((c_0 ' v x) ' v c_0 ') ' = x.  [back_demod(190),demod(1536(4),1536(8),1509(10),1509(6))].
1660 (c_0 ' v (x v x) ') v (y v x) = c_0.  [back_demod(44),demod(1509(9))].
1675 x v c_0 ' = x.  [back_demod(1525),demod(1631(11))].
1683 x ' ' = x.  [back_demod(1633),demod(1675(3),1660(8),1509(3),1675(4))].
1684 x ' v (y v x) = c_0.  [back_demod(1627),demod(1640(5),1675(3),1675(4))].
1685 ((x v y) ' v (y ' v x) ') ' = x.  [back_demod(1626),demod(1640(7),1675(5),1675(6))].
1692 c_0 ' v x = x.  [back_demod(1641),demod(1675(7),1683(5))].
1695 x v (y v (x v x) ') ' = x.  [back_demod(1619),demod(1692(4),1675(9),1683(7))].
1697 x v x = x.  [back_demod(1594),demod(1675(5),1683(3))].
1747 x v (y v x ') ' = x.  [back_demod(1695),demod(1697(1))].
1757 x v (x v ((x v y ') ' v y)) ' = x v y '.  [para(15(a,1),1683(a,1,1)),demod(1683(4)),flip(a)].
1797 x v y = y v x.  [para(1675(a,1),6(a,1,2)),demod(1675(4))].
1812 x v (x v y) ' = x v y '.  [back_demod(1757),demod(1797(4),1747(4))].
1883 (x v y) v y ' = c_0.  [para(1684(a,1),1797(a,1)),flip(a)].
1892 (x v (y v z)) v (x v z) ' = c_0.  [para(6(a,1),1883(a,1,1))].
1918 (x v y) v x ' = c_0.  [para(1797(a,1),1883(a,1,1))].
1937 (x v y) v (z v x ') = c_0.  [para(1918(a,1),6(a,1,2)),demod(1509(2)),flip(a)].
1938 (x v (y v z)) v y ' = c_0.  [para(6(a,1),1918(a,1,1))].
1945 x v (y v (z v x ') ') = y v x.  [para(1747(a,1),6(a,1,2)),flip(a)].
1950 x ' v (y v x) ' = x '.  [para(1683(a,1),1747(a,1,2,1,2))].
1951 x v (x ' v y) ' = x.  [para(1797(a,1),1747(a,1,2,1))].
1989 x v (y v (x ' v z) ') = y v x.  [para(1951(a,1),6(a,1,2)),flip(a)].
2123 ((x v y) v z) v x ' = c_0.  [para(1797(a,1),1938(a,1,1))].
2125 (x v y) ' v (x v (z v y)) ' = (x v y) '.  [para(6(a,1),1950(a,1,2,1))].
2132 ((x v y) v z) v y ' = c_0.  [para(1950(a,1),1937(a,1,2))].
2460 x v (y v x) ' = x v y '.  [para(1797(a,1),1812(a,1,2,1))].
2466 x v ((x v y) v z) = (x v y) v z.  [para(2123(a,1),1812(a,1,2,1)),demod(1675(5),1683(6),1797(5)),flip(a)].
2467 x v ((y v x) v z) = (y v x) v z.  [para(2132(a,1),1812(a,1,2,1)),demod(1675(5),1683(6),1797(5)),flip(a)].
2515 x v (y v (z v x) ') = y v (x v z ').  [para(2460(a,1),6(a,1,2)),flip(a)].
2677 (x v (y v z)) v (x v y) ' = c_0.  [para(1797(a,1),1892(a,1,1,2))].
3985 (x v y) v z = x v (y v z).  [para(2677(a,1),1812(a,1,2,1)),demod(1675(5),1683(7),1797(6),6(6),6(5),2467(5),2466(5)),flip(a)].
4412 x ' v ((y v x) ' v z) = x ' v z.  [para(1950(a,1),3985(a,1,1)),flip(a)].
4505 (x v y) ' v (y ' v x) ' = x '.  [para(1685(a,1),1683(a,1,1)),flip(a)].
4636 (x v y) ' v (z v (y ' v x) ') = z v x '.  [para(4505(a,1),6(a,1,2)),flip(a)].
4667 (x v (y v z) ') ' = (x v (z v y ')) ' v (x v z ') '.  [para(1945(a,1),4505(a,1,2,1)),demod(1683(2),1797(4),2515(4),1683(10)),flip(a)].
4676 (c3 v (c1 ' v c2 ')) ' v (c1 ' v c3 ') ' != (c1 ' v c2 ') ' v (c1 ' v c3 ') ' # answer(distributivity_1).  [back_demod(11),demod(4667(8),6(7))].
4926 (x v y) ' v ((x v (z v y)) ' v u) = (x v y) ' v u.  [para(6(a,1),4412(a,1,2,1,1))].
5240 (x v (y v z)) ' v (x v y ') ' = (x v z) ' v (x v y ') '.  [para(1951(a,1),2125(a,1,2,1,2)),demod(4667(5),1683(2),1797(10),4926(10),4667(11),1683(8)),flip(a)].
5245 (x v (y v z) ') ' = (x v y ') ' v (x v z ') '.  [back_demod(4667),demod(5240(12))].
5626 (x v (y v z)) ' v (y v x ') ' = (y v z) ' v (y v x ') '.  [para(4636(a,1),4505(a,1,2,1)),demod(1797(6),3985(6),1989(5),5245(12),1683(9))].
5627 $F # answer(distributivity_1).  [resolve(5626,a,4676,a)].

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

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

Given=360. Generated=201972. Kept=5621. proofs=1.
Usable=172. Sos=877. Demods=937. Denials=1. Limbo=7, Disabled=4568. Hints=0.
Weight_deleted=24364. Literals_deleted=0.
Forward_subsumed=171987. Back_subsumed=102.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=4990 (3 lex), Back_demodulated=4461. Back_unit_deleted=0.
Demod_attempts=3340010. Demod_rewrites=427900.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=2.81.
User_CPU=6.61, System_CPU=0.08, Wall_clock=7.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 13064 exit (max_proofs) Mon Jun 19 16:40:45 2006