============================== Prover9 =============================== Prover9 (32) version 2009-02A, February 2009. Process 11187 was started by mccune on cleo, Wed Feb 25 09:32:06 2009 The command was "/home/mccune/bin/prover9 -f BA3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file BA3.in assign(max_seconds,30). 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) # label(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) # label(distributivity_1) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x v (y 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) # label(distributivity_1). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label distributivity_1 to answer in negative clause Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, v, ^, ' ]). After inverse_order: (no changes). Unfolding symbols: ^/2. Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). kept: 2 x v (y v z) = y v (x v z). [assumption]. kept: 3 x ^ y = (x' v y')'. [assumption]. kept: 4 x v x' = y v y'. [assumption]. 5 (x v y') ^ (x v y) = x. [assumption]. kept: 6 ((x v y')' v (x v y)')' = x. [copy(5),rewrite([3(4)])]. 7 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity_1) # answer(distributivity_1). [deny(1)]. kept: 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)]. NOTE: New constant: x v x' = c_0. [new_symbol(4)]. NOTE: New Function symbol precedence: function_order([ c1, c2, c3, c_0, v, ^, ' ]). kept: 9 x v x' = c_0. [new_symbol(4)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 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)]. 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)])]. 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.01 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=6): 9 x v x' = c_0. [new_symbol(4)]. given #5 (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 #6 (T,wt=10): 15 x v (y v x') = y v c_0. [para(9(a,1),2(a,1,2)),flip(a)]. given #7 (T,wt=10): 16 (c_0' v (x v x)')' = x. [para(9(a,1),6(a,1,1,1,1))]. given #8 (T,wt=11): 41 (c_0' v (x v x)') v x = c_0. [para(16(a,1),9(a,1,2))]. given #9 (T,wt=12): 17 ((x v x'')' v c_0')' = x. [para(9(a,1),6(a,1,1,2,1))]. given #10 (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 #11 (T,wt=13): 39 (x v (c_0' v (x v x))')' = c_0'. [para(16(a,1),6(a,1,1,1))]. given #12 (T,wt=13): 58 ((x v x'')' v c_0') v x = c_0. [para(17(a,1),9(a,1,2))]. given #13 (T,wt=13): 73 (x v (x v (c_0' v x))')' = c_0'. [para(16(a,1),11(a,1,1,1))]. given #14 (T,wt=14): 18 ((x v y')' v (x v y)') v x = c_0. [para(6(a,1),9(a,1,2))]. given #15 (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 #16 (T,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 #17 (T,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 #18 (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 #19 (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 #20 (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 #21 (T,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 #22 (T,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 #23 (T,wt=15): 40 ((c_0' v (x v x)'')' v x)' = c_0'. [para(16(a,1),6(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(16(a,1),15(a,1,2,2))]. given #25 (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 #26 (T,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 #27 (T,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 #28 (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 #29 (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 #30 (A,wt=19): 19 x v (y v (z v (u v w))) = z v (x v (u v (y v w))). [para(10(a,1),2(a,1,2))]. given #31 (T,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 #32 (T,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 #33 (T,wt=11): 322 x v (x v (c_0' v x))' = c_0. [para(2(a,1),314(a,1,2,1))]. given #34 (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 #35 (A,wt=19): 21 x v (y v (z v (u v w))) = u v (x v (y v (z v w))). [para(10(a,2),2(a,1,2))]. given #36 (T,wt=12): 329 c_0'' v (c_0'' v c_0)' = c_0. [para(15(a,1),314(a,1,2,1))]. given #37 (T,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 #38 (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 #39 (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 #40 (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 #41 (T,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 #42 (T,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 #43 (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 #44 (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 #45 (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 #46 (T,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 #47 (T,wt=13): 500 c_0'' v (x v c_0) = x v c_0''. [back_rewrite(393),rewrite([486(5),486(11)])]. given #48 (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 #49 (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 #50 (A,wt=23): 26 x v (y v (z v (u v (w v v5)))) = u v (x v (y v (w v (z v v5)))). [para(10(a,1),10(a,1,2,2))]. given #51 (T,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 #52 (T,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 #53 (T,wt=10): 587 (c_0' v c_0''')' = c_0. [para(585(a,1),9(a,1,2)),rewrite([479(11)])]. given #54 (T,wt=11): 592 (c_0' v c_0''') v c_0 = c_0. [para(587(a,1),9(a,1,2))]. given #55 (A,wt=19): 27 x v (y v (z v (u v w))) = u v (x v (z v (y v w))). [para(10(a,1),10(a,1,2))]. given #56 (T,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 #57 (T,wt=15): 591 ((c_0' v c_0'''')' v c_0)' = c_0'. [para(587(a,1),6(a,1,1,2))]. given #58 (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 #59 (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 #60 (A,wt=23): 28 x v (y v (z v (u v (w v v5)))) = z v (x v (w v (y v (u v v5)))). [para(10(a,1),10(a,2,2,2))]. given #61 (T,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 #62 (T,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 #63 (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 #64 (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 #65 (A,wt=19): 29 x v (y v (z v (u v w))) = z v (u v (x v (y v w))). [para(10(a,1),10(a,2,2))]. given #66 (T,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 #67 (T,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 #68 (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 #69 (T,wt=8): 743 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 #70 (A,wt=23): 30 x v (y v (z v (u v (w v v5)))) = w v (x v (y v (z v (u v v5)))). [para(10(a,2),10(a,1,2,2))]. given #71 (T,wt=7): 755 c_0'' = c_0 v c_0. [para(743(a,1),44(a,1,2)),rewrite([2(11),567(15)])]. given #72 (T,wt=9): 763 (c_0 v c_0) v c_0 = c_0 v c_0. [para(743(a,1),554(a,1,2)),rewrite([755(3)])]. given #73 (T,wt=12): 746 c_0 v (x v (c_0' v c_0)) = x v c_0. [para(743(a,1),2(a,1,2)),flip(a)]. given #74 (T,wt=12): 749 c_0' v (x v (c_0 v c_0)) = x v c_0. [para(743(a,1),10(a,1,2)),flip(a)]. given #75 (A,wt=19): 31 x v (y v (z v (u v w))) = y v (x v (u v (z v w))). [para(10(a,2),10(a,1,2))]. given #76 (T,wt=12): 750 c_0 v (c_0' v (x v c_0)) = x v c_0. [para(743(a,1),10(a,2,2))]. given #77 (T,wt=12): 887 ((c_0 v (c_0 v c_0))' v c_0')' = c_0. [para(755(a,1),17(a,1,1,1,1,2))]. given #78 (T,wt=13): 832 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0). [back_rewrite(545),rewrite([755(3),755(13),2(14),338(13)])]. given #79 (T,wt=13): 844 (c_0 v (x v c_0))' = (x v (c_0 v c_0))'. [back_rewrite(525),rewrite([755(3),832(6),755(8)])]. given #80 (A,wt=23): 32 x v (y v (z v (u v (w v v5)))) = z v (x v (u v (w v (y v v5)))). [para(10(a,2),10(a,2,2,2))]. given #81 (T,wt=13): 888 ((c_0 v (c_0 v c_0))' v c_0') v c_0 = c_0. [para(755(a,1),58(a,1,1,1,1,2))]. given #82 (T,wt=14): 747 ((c_0 v (c_0' v c_0)')' v c_0')' = c_0. [para(743(a,1),6(a,1,1,2,1))]. given #83 (T,wt=14): 796 (x v (c_0 v c_0)) v (c_0 v (x v c_0))' = c_0. [back_rewrite(628),rewrite([755(3),755(7),788(11)])]. given #84 (T,wt=14): 823 (c_0 v c_0) v (x v (c_0' v c_0)) = x v c_0. [back_rewrite(554),rewrite([755(3)])]. given #85 (A,wt=19): 33 x v (y v (z v (u v w))) = u v (y v (x v (z v w))). [para(10(a,2),10(a,2,2)),flip(a)]. given #86 (T,wt=14): 878 (c_0 v (x v c_0)) v (x v (c_0 v c_0))' = c_0. [back_rewrite(797),rewrite([832(6)])]. given #87 (T,wt=14): 894 (c_0' v (c_0 v (c_0 v c_0))')' = c_0 v c_0. [para(763(a,1),37(a,1,1,2,1,2,1)),rewrite([763(10),2(9),763(8),763(15)])]. given #88 (T,wt=14): 982 (c_0 v c_0) v (c_0' v (x v c_0)) = x v c_0. [para(2(a,1),823(a,1,2))]. given #89 (T,wt=15): 752 ((c_0 v (c_0' v c_0)')' v c_0') v c_0 = c_0. [para(743(a,1),18(a,1,1,2,1))]. given #90 (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 #91 (T,wt=15): 805 ((c_0 v c_0)' v (c_0' v c_0)')' = c_0 v c_0. [back_rewrite(601),rewrite([755(3),755(14)])]. given #92 (T,wt=15): 851 ((c_0 v (x v c_0))' v (x v c_0')')' = x. [back_rewrite(514),rewrite([755(3),832(6)])]. given #93 (T,wt=11): 1041 c_0' v (c_0' v c_0')' = c_0. [para(41(a,1),851(a,1,1,2,1)),rewrite([54(12),887(10)]),flip(a)]. given #94 (T,wt=12): 1059 (c_0' v c_0') v c_0 = c_0' v c_0. [para(1041(a,1),15(a,1,2))]. given #95 (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 #96 (T,wt=13): 1054 (c_0' v (c_0' v c_0')'')' = c_0. [para(670(a,1),851(a,1,1,2,1)),rewrite([687(14),1041(10),887(10)]),flip(a)]. given #97 (T,wt=14): 1046 (c_0' v x')' v (c_0' v x)' = c_0. [para(18(a,1),851(a,1,1,2,1)),rewrite([121(13),887(10)]),flip(a)]. given #98 (T,wt=14): 1092 (c_0' v (c_0' v c_0')'') v c_0 = c_0. [para(1054(a,1),9(a,1,2))]. given #99 (T,wt=15): 886 ((x v (c_0 v c_0))' v (x v c_0')')' = x. [para(755(a,1),6(a,1,1,1,1,2))]. given #100 (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 #101 (T,wt=15): 978 (c_0 v (x v c_0)) v c_0 = (x v (c_0 v c_0)) v c_0. [para(796(a,1),15(a,1,2))]. given #102 (T,wt=15): 1057 c_0' v (x v (c_0' v c_0')') = x v c_0. [para(1041(a,1),2(a,1,2)),flip(a)]. given #103 (T,wt=15): 1106 (c_0' v x')' v c_0 = (c_0' v x) v c_0. [para(1046(a,1),15(a,1,2)),flip(a)]. given #104 (T,wt=9): 1242 c_0' v (c_0' v c_0) = c_0. [back_rewrite(1189),rewrite([1205(21),2(20),1190(19)])]. given #105 (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 #106 (T,wt=5): 1265 c_0 v c_0 = c_0. [para(1242(a,1),14(a,1,1,1,1,2,1,1)),rewrite([1263(6),16(8),755(4),1264(5),1205(6),1263(4),1263(9),16(11)])]. given #107 (T,wt=5): 1349 c_0'' = c_0. [back_rewrite(755),rewrite([1265(6)])]. given #108 (T,wt=6): 1313 c_0' v c_0 = c_0. [back_rewrite(1263),rewrite([1265(7)])]. given #109 (T,wt=8): 1293 (c_0' v c_0')' = c_0. [back_rewrite(1205),rewrite([1263(10),1265(9)])]. given #110 (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 #111 (T,wt=9): 1298 (c_0' v c_0') v c_0 = c_0. [back_rewrite(1059),rewrite([1263(11),1265(10)])]. given #112 (T,wt=9): 1304 c_0 v (x v c_0) = x v c_0. [back_rewrite(823),rewrite([1265(3),1263(5),1265(4)])]. given #113 (T,wt=10): 1283 c_0' v (x v c_0) = x v c_0. [back_rewrite(1260),rewrite([1263(6),1265(5)])]. given #114 (T,wt=11): 1372 x v ((x v c_0) v c_0) = x v c_0. [para(1283(a,1),103(a,1,1,2,1,2,2)),rewrite([2(9),2(10),1358(13)])]. given #115 (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 #116 (T,wt=12): 1373 (c_0' v (x v c_0)')' = x v c_0. [para(1283(a,1),37(a,1,1,2,1,2,1)),rewrite([2(9),1372(9),1283(7),1283(12)])]. given #117 (T,wt=12): 1426 ((x v c_0)' v c_0')' = x v c_0. [para(1373(a,1),34(a,1,1,1,1,2)),rewrite([2(5),1372(5),1313(7)])]. given #118 (T,wt=13): 1305 c_0 v (x v (y v c_0)) = x v (y v c_0). [back_rewrite(817),rewrite([1265(3),1263(5),1265(4)])]. given #119 (T,wt=13): 1343 ((x v c_0)' v (x v c_0')')' = x. [back_rewrite(886),rewrite([1265(3)])]. given #120 (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 #121 (T,wt=13): 1352 (c_0' v c_0') v (x v c_0) = x v c_0. [back_rewrite(1185),rewrite([1283(13)])]. given #122 (T,wt=13): 1374 x v ((c_0' v (x v c_0)') v c_0) = c_0. [para(1283(a,1),133(a,1,1,2,1,2,2)),rewrite([2(9),1372(9),2(7),1372(7),2(9)])]. given #123 (T,wt=7): 1489 (x v c_0) v c_0 = c_0. [back_rewrite(1417),rewrite([1472(12)])]. given #124 (T,wt=5): 1512 x v c_0 = c_0. [back_rewrite(1446),rewrite([1494(11),1451(11)]),flip(a)]. given #125 (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 #126 (T,wt=5): 1686 x'' = x. [back_rewrite(1636),rewrite([1678(3),1663(8),1512(3),1678(4)])]. given #127 (T,wt=5): 1702 x v x = x. [back_rewrite(1607),rewrite([1678(5),1686(3)])]. given #128 (T,wt=5): 1703 c_0 v x = c_0. [back_rewrite(1598),rewrite([1678(6),1686(4)])]. given #129 (T,wt=6): 1678 x v c_0' = x. [back_rewrite(1527),rewrite([1635(11)])]. % Operation v is commutative; C redundancy checks enabled. given #130 (A,wt=25): 64 ((x v (y v (z v (u v w)))')' v (z v (x v (u v (y v w))))')' = x. [para(10(a,1),11(a,1,1,1,1,2,1))]. given #131 (T,wt=6): 1695 c_0' v x = x. [back_rewrite(1647),rewrite([1678(7),1686(5)])]. given #132 (T,wt=7): 1801 x v y = y v x. [para(1678(a,1),2(a,1,2)),rewrite([1678(4)])]. given #133 (T,wt=8): 1667 x v (y v x') = c_0. [back_rewrite(15),rewrite([1512(5)])]. given #134 (T,wt=8): 1859 x v (x' v y) = c_0. [back_rewrite(1688),rewrite([1802(3)])]. given #135 (A,wt=25): 65 ((x v (y v (z v (u v w)))')' v (y v (u v (x v (z v w))))')' = x. [para(10(a,1),11(a,1,1,2,1,2))]. given #136 (T,wt=9): 1751 x v (y v x')' = x. [back_rewrite(1697),rewrite([1702(1)])]. given #137 (T,wt=9): 1765 x v (y v x) = y v x. [para(1702(a,1),2(a,1,2)),flip(a)]. given #138 (T,wt=9): 1829 x v (x v y) = x v y. [back_rewrite(1750),rewrite([1801(2),1765(2)])]. given #139 (T,wt=9): 1981 x v (x' v y)' = x. [para(1801(a,1),1751(a,1,2,1))]. given #140 (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 #141 (T,wt=10): 1666 x v (y v (z v x')) = c_0. [back_rewrite(25),rewrite([1512(6),1512(6)])]. given #142 (T,wt=10): 1691 x' v (y v (z v x)) = c_0. [back_rewrite(1602),rewrite([1646(5),1678(3),1678(4)])]. given #143 (T,wt=10): 1837 x v (y v (x v y)') = c_0. [back_rewrite(1708),rewrite([1801(3)])]. given #144 (T,wt=10): 1952 x v (y v (x' v z)) = c_0. [para(1859(a,1),2(a,1,2)),rewrite([1512(2)]),flip(a)]. given #145 (A,wt=25): 67 ((x v (y v (z v (u v w)))')' v (u v (x v (y v (z v w))))')' = x. [para(10(a,2),11(a,1,1,1,1,2,1))]. given #146 (T,wt=10): 1954 x' v (y v (x v z)) = c_0. [para(1859(a,1),10(a,1,2)),rewrite([1512(2)]),flip(a)]. given #147 (T,wt=10): 1980 x' v (y v x)' = x'. [para(1686(a,1),1751(a,1,2,1,2))]. given #148 (T,wt=8): 2115 (x v y) v y' = c_0. [para(1980(a,1),1667(a,1,2))]. given #149 (T,wt=8): 2143 (x v y) v x' = c_0. [para(1801(a,1),2115(a,1,1))]. given #150 (A,wt=25): 68 ((x v (y v (z v (u v w)))')' v (y v (z v (u v (x v w))))')' = x. [para(10(a,2),11(a,1,1,2,1,2))]. given #151 (T,wt=10): 2006 x' v (x v y)' = x'. [para(1686(a,1),1981(a,1,2,1,1))]. given #152 (T,wt=10): 2025 x v ((y v x') v z) = c_0. [para(1801(a,1),1666(a,1,2))]. given #153 (T,wt=10): 2026 x v ((x' v y) v z) = c_0. [para(1981(a,1),1666(a,1,2,2)),rewrite([1802(4)])]. given #154 (T,wt=10): 2059 (x v (y v z)) v z' = c_0. [para(1691(a,1),1801(a,1)),flip(a)]. given #155 (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 #156 (T,wt=10): 2060 x' v ((y v x) v z) = c_0. [para(1801(a,1),1691(a,1,2))]. given #157 (T,wt=10): 2105 (x v (y v z)) v y' = c_0. [para(1954(a,1),1801(a,1)),flip(a)]. given #158 (T,wt=10): 2106 x' v ((x v y) v z) = c_0. [para(1801(a,1),1954(a,1,2))]. given #159 (T,wt=10): 2116 (x v y) v (z v y') = c_0. [para(1980(a,1),1666(a,1,2,2))]. given #160 (A,wt=23): 184 x v (y v (z v (u v (w v v5)))) = w v (x v (y v (u v (z v v5)))). [para(20(a,1),10(a,1,2,2))]. given #161 (T,wt=10): 2144 (x v y) v (z v x') = c_0. [para(2143(a,1),2(a,1,2)),rewrite([1512(2)]),flip(a)]. given #162 (T,wt=10): 2187 (x v y) v (y' v z) = c_0. [para(1980(a,1),2025(a,1,2,1))]. given #163 (T,wt=10): 2188 (x v y) v (x' v z) = c_0. [para(2006(a,1),2025(a,1,2,1))]. given #164 (T,wt=10): 2228 ((x v y) v z) v y' = c_0. [para(1801(a,1),2059(a,1,1))]. given #165 (A,wt=23): 185 x v (y v (z v (u v (w v v5)))) = z v (x v (w v (u v (y v v5)))). [para(20(a,1),10(a,2,2,2))]. given #166 (T,wt=10): 2289 ((x v y) v z) v x' = c_0. [para(1801(a,1),2105(a,1,1))]. given #167 (T,wt=11): 1699 x v (y v (z v x'))' = x. [back_rewrite(1615),rewrite([1678(9),1686(7)])]. given #168 (T,wt=11): 1802 x v (y v z) = z v (x v y). [para(1678(a,1),10(a,1,2,2)),rewrite([1678(5)])]. % Operation v is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 1802 x v (y v z) = z v (x v y). [para(1678(a,1),10(a,1,2,2)),rewrite([1678(5)])]. % back CAC tautology: 185 x v (y v (z v (u v (w v v5)))) = z v (x v (w v (u v (y v v5)))). [para(20(a,1),10(a,2,2,2))]. % back CAC tautology: 184 x v (y v (z v (u v (w v v5)))) = w v (x v (y v (u v (z v v5)))). [para(20(a,1),10(a,1,2,2))]. % back CAC tautology: 33 x v (y v (z v (u v w))) = u v (y v (x v (z v w))). [para(10(a,2),10(a,2,2)),flip(a)]. % back CAC tautology: 32 x v (y v (z v (u v (w v v5)))) = z v (x v (u v (w v (y v v5)))). [para(10(a,2),10(a,2,2,2))]. % back CAC tautology: 31 x v (y v (z v (u v w))) = y v (x v (u v (z v w))). [para(10(a,2),10(a,1,2))]. % back CAC tautology: 30 x v (y v (z v (u v (w v v5)))) = w v (x v (y v (z v (u v v5)))). [para(10(a,2),10(a,1,2,2))]. % back CAC tautology: 29 x v (y v (z v (u v w))) = z v (u v (x v (y v w))). [para(10(a,1),10(a,2,2))]. % back CAC tautology: 28 x v (y v (z v (u v (w v v5)))) = z v (x v (w v (y v (u v v5)))). [para(10(a,1),10(a,2,2,2))]. % back CAC tautology: 27 x v (y v (z v (u v w))) = u v (x v (z v (y v w))). [para(10(a,1),10(a,1,2))]. % back CAC tautology: 26 x v (y v (z v (u v (w v v5)))) = u v (x v (y v (w v (z v v5)))). [para(10(a,1),10(a,1,2,2))]. % back CAC tautology: 21 x v (y v (z v (u v w))) = u v (x v (y v (z v w))). [para(10(a,2),2(a,1,2))]. % back CAC tautology: 19 x v (y v (z v (u v w))) = z v (x v (u v (y v w))). [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: 2554 x v (y v (z v (u v w))) = w v (y v (z v (x v u))). [para(1802(a,2),33(a,2,2,2)),flip(a)]. % back CAC tautology: 2553 x v (y v (z v (u v (w v v5)))) = u v (y v (x v (w v (v5 v z)))). [para(1802(a,2),33(a,2,2,2,2))]. % back CAC tautology: 2551 x v (y v (z v (u v w))) = z v (y v (x v (w v u))). [para(1802(a,2),33(a,1,2,2))]. % back CAC tautology: 2550 x v (y v (z v (u v (w v v5)))) = v5 v (y v (x v (z v (u v w)))). [para(1802(a,2),33(a,1,2,2,2))]. % back CAC tautology: 2547 x v (y v (z v (u v w))) = u v (y v (w v (x v z))). [para(1802(a,1),33(a,2,2,2))]. % back CAC tautology: 2546 x v (y v (z v (u v (w v v5)))) = u v (y v (x v (v5 v (z v w)))). [para(1802(a,1),33(a,2,2,2,2))]. % back CAC tautology: 2543 x v (y v (z v (u v w))) = w v (y v (x v (u v z))). [para(1802(a,1),33(a,1,2,2))]. % back CAC tautology: 2542 x v (y v (z v (u v (w v v5)))) = w v (y v (x v (z v (v5 v u)))). [para(1802(a,1),33(a,1,2,2,2))]. % back CAC tautology: 2533 x v (y v (z v (u v (w v v5)))) = z v (x v (u v (v5 v (w v y)))). [para(1802(a,1),32(a,2,2,2,2))]. % back CAC tautology: 2526 x v (y v (z v (u v w))) = y v (x v (z v (w v u))). [para(1802(a,2),31(a,1,2,2))]. % back CAC tautology: 2525 x v (y v (z v (u v (w v v5)))) = y v (x v (v5 v (z v (u v w)))). [para(1802(a,2),31(a,1,2,2,2))]. % back CAC tautology: 2522 x v (y v (z v (u v w))) = y v (x v (w v (u v z))). [para(1802(a,1),31(a,1,2,2))]. % back CAC tautology: 2521 x v (y v (z v (u v (w v v5)))) = y v (x v (w v (z v (v5 v u)))). [para(1802(a,1),31(a,1,2,2,2))]. % back CAC tautology: 2509 x v (y v (z v (u v (w v v5)))) = v5 v (x v (y v (z v (w v u)))). [para(1802(a,1),30(a,1,2,2,2))]. % back CAC tautology: 2505 x v (y v (z v (u v w))) = w v (z v (x v (y v u))). [para(1802(a,2),29(a,1,2,2))]. % back CAC tautology: 2504 x v (y v (z v (u v (w v v5)))) = z v (v5 v (x v (y v (u v w)))). [para(1802(a,2),29(a,1,2,2,2))]. % back CAC tautology: 2501 x v (y v (z v (u v w))) = u v (w v (x v (y v z))). [para(1802(a,1),29(a,1,2,2))]. % back CAC tautology: 2500 x v (y v (z v (u v (w v v5)))) = z v (w v (x v (y v (v5 v u)))). [para(1802(a,1),29(a,1,2,2,2))]. % back CAC tautology: 2493 x v (y v (z v (u v (w v v5)))) = z v (x v (u v (y v (v5 v w)))). [para(1802(a,2),28(a,1,2,2,2))]. % back CAC tautology: 2489 x v (y v (z v (u v (w v v5)))) = z v (x v (w v (v5 v (y v u)))). [para(1802(a,1),28(a,2,2,2,2))]. % back CAC tautology: 2485 x v (y v (z v (u v (w v v5)))) = z v (x v (v5 v (y v (w v u)))). [para(1802(a,1),28(a,1,2,2,2))]. % back CAC tautology: 2480 x v (y v (z v (u v (w v v5)))) = u v (x v (z v (w v (v5 v y)))). [para(1802(a,2),27(a,2,2,2,2))]. % back CAC tautology: 2478 x v (y v (z v (u v (w v v5)))) = v5 v (x v (z v (y v (u v w)))). [para(1802(a,2),27(a,1,2,2,2))]. % back CAC tautology: 2475 x v (y v (z v (u v w))) = u v (x v (w v (z v y))). [para(1802(a,1),27(a,2,2,2))]. % back CAC tautology: 2474 x v (y v (z v (u v (w v v5)))) = u v (x v (z v (v5 v (y v w)))). [para(1802(a,1),27(a,2,2,2,2))]. % back CAC tautology: 2471 x v (y v (z v (u v w))) = w v (x v (u v (y v z))). [para(1802(a,1),27(a,1,2,2))]. % back CAC tautology: 2470 x v (y v (z v (u v (w v v5)))) = w v (x v (z v (y v (v5 v u)))). [para(1802(a,1),27(a,1,2,2,2))]. % back CAC tautology: 2466 x v (y v (z v (u v (w v v5)))) = u v (x v (y v (z v (v5 v w)))). [para(1802(a,2),26(a,2,2,2,2))]. % back CAC tautology: 2459 x v (y v (z v (u v (w v v5)))) = u v (x v (y v (v5 v (w v z)))). [para(1802(a,1),26(a,2,2,2,2))]. % back CAC tautology: 2455 x v (y v (z v (u v (w v v5)))) = w v (x v (y v (v5 v (z v u)))). [para(1802(a,1),26(a,1,2,2,2))]. % back CAC tautology: 2444 x v (y v (z v (u v w))) = z v (x v (y v (w v u))). [para(1802(a,2),19(a,2,2,2))]. % back CAC tautology: 2439 x v (y v (z v (u v w))) = u v (x v (w v (y v z))). [para(1802(a,1),19(a,1,2,2))]. % back CAC tautology: 2437 x v (y v (z v (u v w))) = x v (w v (y v (z v u))). [para(1802(a,2),22(a,1,2,2))]. % back CAC tautology: 2436 x v (y v (z v u)) = x v (u v (z v y)). [para(1802(a,1),22(a,1,2))]. % back CAC tautology: 2435 x v (y v (z v (u v w))) = x v (u v (y v (w v z))). [para(1802(a,1),22(a,1,2,2))]. % back CAC tautology: 2432 x v (y v (z v u)) = u v (z v (x v y)). [para(1802(a,1),20(a,1,2))]. % back CAC tautology: 2396 x v (y v (z v (u v (w v v5)))) = z v (x v (w v (u v (v5 v y)))). [para(1801(a,1),185(a,2,2,2,2,2))]. % back CAC tautology: 2392 x v (y v (z v (u v (w v v5)))) = z v (x v (v5 v (u v (y v w)))). [para(1801(a,1),185(a,1,2,2,2,2))]. % back CAC tautology: 2389 x v (y v (z v (u v w))) = z v (x v (w v (u v y))). [para(1678(a,1),185(a,1,2,2,2,2)),rewrite([1678(7)])]. % back CAC tautology: 2328 x v (y v (z v (u v (w v v5)))) = w v (x v (y v (u v (v5 v z)))). [para(1801(a,1),184(a,2,2,2,2,2))]. % back CAC tautology: 2324 x v (y v (z v (u v (w v v5)))) = v5 v (x v (y v (u v (z v w)))). [para(1801(a,1),184(a,1,2,2,2,2))]. % back CAC tautology: 2321 x v (y v (z v (u v w))) = w v (x v (y v (u v z))). [para(1678(a,1),184(a,1,2,2,2,2)),rewrite([1678(7)])]. % back CAC tautology: 2318 x v (y v (z v (u v (w v v5)))) = w v (u v (z v (x v (y v v5)))). [para(29(a,1),184(a,2,2))]. % back CAC tautology: 2317 x v (y v (z v (u v (w v v5)))) = w v (u v (y v (z v (x v v5)))). [para(184(a,1),29(a,1))]. % back CAC tautology: 1947 x v (y v (z v (u v w))) = u v (y v (x v (w v z))). [para(1801(a,1),33(a,2,2,2,2))]. % back CAC tautology: 1943 x v (y v (z v (u v w))) = w v (y v (x v (z v u))). [para(1801(a,1),33(a,1,2,2,2))]. % back CAC tautology: 1938 x v (y v (z v (u v (w v v5)))) = z v (x v (u v (w v (v5 v y)))). [para(1801(a,1),32(a,2,2,2,2,2))]. % back CAC tautology: 1933 x v (y v (z v (u v (w v v5)))) = z v (x v (u v (v5 v (y v w)))). [para(1801(a,1),32(a,1,2,2,2,2))]. % back CAC tautology: 1929 x v (y v (z v (u v w))) = y v (x v (w v (z v u))). [para(1801(a,1),31(a,1,2,2,2))]. % back CAC tautology: 1924 x v (y v (z v (u v (w v v5)))) = w v (x v (y v (z v (v5 v u)))). [para(1801(a,1),30(a,2,2,2,2,2))]. % back CAC tautology: 1919 x v (y v (z v (u v (w v v5)))) = v5 v (x v (y v (z v (u v w)))). [para(1801(a,1),30(a,1,2,2,2,2))]. % back CAC tautology: 1915 x v (y v (z v (u v w))) = z v (w v (x v (y v u))). [para(1801(a,1),29(a,1,2,2,2))]. % back CAC tautology: 1910 x v (y v (z v (u v (w v v5)))) = z v (x v (w v (y v (v5 v u)))). [para(1801(a,1),28(a,2,2,2,2,2))]. % back CAC tautology: 1905 x v (y v (z v (u v (w v v5)))) = z v (x v (v5 v (y v (u v w)))). [para(1801(a,1),28(a,1,2,2,2,2))]. % back CAC tautology: 1901 x v (y v (z v (u v w))) = u v (x v (z v (w v y))). [para(1801(a,1),27(a,2,2,2,2))]. % back CAC tautology: 1897 x v (y v (z v (u v w))) = w v (x v (z v (y v u))). [para(1801(a,1),27(a,1,2,2,2))]. % back CAC tautology: 1892 x v (y v (z v (u v (w v v5)))) = u v (x v (y v (w v (v5 v z)))). [para(1801(a,1),26(a,2,2,2,2,2))]. % back CAC tautology: 1887 x v (y v (z v (u v (w v v5)))) = u v (x v (y v (v5 v (z v w)))). [para(1801(a,1),26(a,1,2,2,2,2))]. % back CAC tautology: 1872 x v (y v (z v u)) = x v (u v (y v z)). [para(1801(a,1),22(a,1,2,2))]. % back CAC tautology: 1813 x v (y v (z v u)) = u v (y v (x v z)). [para(1678(a,1),33(a,1,2,2,2)),rewrite([1678(6)])]. % back CAC tautology: 1812 x v (y v (z v (u v w))) = z v (x v (u v (w v y))). [para(1678(a,1),32(a,1,2,2,2,2)),rewrite([1678(7)])]. % back CAC tautology: 1811 x v (y v (z v u)) = y v (x v (u v z)). [para(1678(a,1),31(a,1,2,2,2)),rewrite([1678(6)])]. % back CAC tautology: 1810 x v (y v (z v (u v w))) = w v (x v (y v (z v u))). [para(1678(a,1),30(a,1,2,2,2,2)),rewrite([1678(7)])]. % back CAC tautology: 1809 x v (y v (z v u)) = z v (u v (x v y)). [para(1678(a,1),29(a,1,2,2,2)),rewrite([1678(6)])]. % back CAC tautology: 1808 x v (y v (z v (u v w))) = z v (x v (w v (y v u))). [para(1678(a,1),28(a,1,2,2,2,2)),rewrite([1678(7)])]. % back CAC tautology: 1807 x v (y v (z v u)) = u v (x v (z v y)). [para(1678(a,1),27(a,1,2,2,2)),rewrite([1678(6)])]. % back CAC tautology: 1806 x v (y v (z v (u v w))) = u v (x v (y v (w v z))). [para(1678(a,1),26(a,1,2,2,2,2)),rewrite([1678(7)])]. % back CAC tautology: 1805 x v (y v (z v u)) = u v (x v (y v z)). [para(1678(a,1),21(a,1,2,2,2)),rewrite([1678(6)])]. % back CAC tautology: 1804 x v (y v (z v u)) = z v (x v (u v y)). [para(1678(a,1),19(a,1,2,2,2)),rewrite([1678(6)])]. % back CAC tautology: 1803 x v (y v z) = z v (y v x). [para(1678(a,1),20(a,1,2,2)),rewrite([1678(5)])]. % back CAC tautology: 969 x v (y v (z v (u v (w v v5)))) = w v (z v (y v (u v (x v v5)))). [para(32(a,1),28(a,2))]. % back CAC tautology: 910 x v (y v (z v (u v (w v v5)))) = x v (u v (w v (y v (z v v5)))). [para(31(a,1),26(a,2))]. % back CAC tautology: 881 x v (y v (z v (u v (w v v5)))) = w v (y v (z v (u v (x v v5)))). [para(30(a,1),21(a,1))]. % back CAC tautology: 720 x v (y v (z v (u v (w v v5)))) = u v (w v (z v (x v (y v v5)))). [para(29(a,1),26(a,2,2))]. % back CAC tautology: 666 x v (y v (z v (u v (w v v5)))) = w v (z v (u v (x v (y v v5)))). [para(28(a,1),28(a,2))]. % back CAC tautology: 665 x v (y v (z v (u v (w v v5)))) = x v (w v (u v (z v (y v v5)))). [para(28(a,2),26(a,2))]. % back CAC tautology: 664 x v (y v (z v (u v (w v v5)))) = w v (y v (u v (z v (x v v5)))). [para(28(a,1),26(a,1))]. % back CAC tautology: 622 x v (y v (z v (u v (w v v5)))) = w v (u v (y v (x v (z v v5)))). [para(27(a,1),26(a,2))]. % back CAC tautology: 609 x v (y v (z v (u v (w v v5)))) = x v (w v (z v (u v (y v v5)))). [para(27(a,1),22(a,1,2))]. % back CAC tautology: 608 x v (y v (z v (u v (w v v5)))) = w v (z v (x v (u v (y v v5)))). [para(27(a,1),20(a,1,2))]. % back CAC tautology: 581 x v (y v (z v (u v (w v v5)))) = w v (u v (x v (z v (y v v5)))). [para(26(a,1),26(a,2))]. % back CAC tautology: 579 x v (y v (z v (u v (w v v5)))) = w v (y v (u v (x v (z v v5)))). [para(21(a,2),26(a,2,2)),flip(a)]. % back CAC tautology: 578 x v (y v (z v (u v (w v v5)))) = x v (y v (w v (u v (z v v5)))). [para(26(a,2),21(a,2))]. % back CAC tautology: 577 x v (y v (z v (u v (w v v5)))) = w v (u v (x v (y v (z v v5)))). [para(26(a,2),21(a,1))]. % back CAC tautology: 576 x v (y v (z v (u v (w v v5)))) = x v (y v (z v (w v (u v v5)))). [para(26(a,1),21(a,1))]. % back CAC tautology: 575 x v (y v (z v (u v (w v v5)))) = w v (x v (u v (z v (y v v5)))). [para(19(a,2),26(a,1,2))]. % back CAC tautology: 574 x v (y v (z v (u v (w v v5)))) = u v (w v (x v (z v (y v v5)))). [para(19(a,1),26(a,2,2))]. % back CAC tautology: 573 x v (y v (z v (u v (w v v5)))) = x v (w v (u v (y v (z v v5)))). [para(26(a,2),19(a,2)),flip(a)]. % back CAC tautology: 572 x v (y v (z v (u v (w v v5)))) = u v (w v (y v (x v (z v v5)))). [para(20(a,1),26(a,2,2))]. % back CAC tautology: 571 x v (y v (z v (u v (w v v5)))) = w v (z v (y v (x v (u v v5)))). [para(26(a,1),20(a,1))]. % back CAC tautology: 389 x v (y v (z v (u v (w v v5)))) = w v (y v (z v (x v (u v v5)))). [para(21(a,2),21(a,2,2)),flip(a)]. % back CAC tautology: 388 x v (y v (z v (u v (w v v5)))) = w v (x v (z v (u v (y v v5)))). [para(21(a,1),21(a,1,2))]. % back CAC tautology: 380 x v (y v (z v (u v (w v v5)))) = u v (y v (w v (x v (z v v5)))). [para(19(a,2),21(a,2,2))]. % back CAC tautology: 379 x v (y v (z v (u v (w v v5)))) = y v (x v (z v (w v (u v v5)))). [para(21(a,2),19(a,1,2))]. % back CAC tautology: 378 x v (y v (z v (u v (w v v5)))) = z v (w v (x v (u v (y v v5)))). [para(21(a,1),19(a,2,2))]. % back CAC tautology: 373 x v (y v (z v (u v (w v v5)))) = u v (x v (w v (z v (y v v5)))). [para(20(a,1),21(a,2,2,2))]. % back CAC tautology: 372 x v (y v (z v (u v (w v v5)))) = u v (z v (x v (w v (y v v5)))). [para(21(a,1),20(a,1,2))]. % back CAC tautology: 365 x v (y v (z v (u v w))) = u v (y v (z v (x v w))). [para(21(a,1),10(a,1))]. % back CAC tautology: 364 x v (y v (z v (u v (w v v5)))) = u v (x v (z v (w v (y v v5)))). [para(21(a,1),10(a,1,2))]. % back CAC tautology: 311 x v (y v (z v (u v (w v v5)))) = u v (w v (x v (y v (z v v5)))). [para(19(a,2),19(a,2,2)),flip(a)]. % back CAC tautology: 310 x v (y v (z v (u v (w v v5)))) = y v (x v (w v (u v (z v v5)))). [para(19(a,2),19(a,1,2))]. % back CAC tautology: 309 x v (y v (z v (u v w))) = u v (z v (y v (x v w))). [para(19(a,1),19(a,2))]. % back CAC tautology: 306 x v (y v (z v (u v (w v v5)))) = x v (y v (w v (z v (u v v5)))). [para(19(a,2),22(a,1,2)),flip(a)]. % back CAC tautology: 305 x v (y v (z v (u v (w v v5)))) = x v (w v (z v (y v (u v v5)))). [para(19(a,1),22(a,1,2))]. % back CAC tautology: 304 x v (y v (z v (u v (w v v5)))) = w v (x v (u v (y v (z v v5)))). [para(20(a,1),19(a,1,2,2))]. % back CAC tautology: 303 x v (y v (z v (u v (w v v5)))) = w v (z v (x v (y v (u v v5)))). [para(19(a,1),20(a,1,2))]. % back CAC tautology: 296 x v (y v (z v (u v (w v v5)))) = u v (x v (w v (y v (z v v5)))). [para(10(a,1),19(a,1,2,2))]. % back CAC tautology: 295 x v (y v (z v (u v (w v v5)))) = y v (x v (w v (z v (u v v5)))). [para(19(a,2),10(a,1,2)),flip(a)]. % back CAC tautology: 294 x v (y v (z v (u v (w v v5)))) = z v (w v (x v (y v (u v v5)))). [para(19(a,1),10(a,2,2)),flip(a)]. % back CAC tautology: 293 x v (y v (z v (u v (w v v5)))) = w v (x v (z v (y v (u v v5)))). [para(19(a,1),10(a,1,2))]. % back CAC tautology: 211 x v (y v (z v (u v (w v v5)))) = x v (z v (y v (w v (u v v5)))). [para(22(a,1),22(a,1,2,2))]. % back CAC tautology: 210 x v (y v (z v (u v (w v v5)))) = x v (w v (y v (u v (z v v5)))). [para(20(a,1),22(a,1,2,2))]. % back CAC tautology: 209 x v (y v (z v (u v (w v v5)))) = z v (y v (x v (w v (u v v5)))). [para(22(a,1),20(a,1,2,2))]. % back CAC tautology: 202 x v (y v (z v (u v w))) = x v (y v (u v (z v w))). [para(10(a,2),22(a,1,2))]. % back CAC tautology: 201 x v (y v (z v (u v (w v v5)))) = x v (w v (y v (z v (u v v5)))). [para(10(a,2),22(a,1,2,2))]. % back CAC tautology: 200 x v (y v (z v (u v w))) = x v (u v (z v (y v w))). [para(10(a,1),22(a,1,2))]. % back CAC tautology: 199 x v (y v (z v (u v (w v v5)))) = x v (u v (y v (w v (z v v5)))). [para(10(a,1),22(a,1,2,2))]. % back CAC tautology: 198 x v (y v (z v (u v (w v v5)))) = z v (x v (y v (w v (u v v5)))). [para(22(a,1),10(a,1,2,2))]. % back CAC tautology: 197 x v (y v (z v (u v w))) = x v (u v (y v (z v w))). [para(2(a,1),22(a,1,2,2))]. % back CAC tautology: 196 x v (y v (z v (u v (w v v5)))) = w v (y v (x v (u v (z v v5)))). [para(20(a,1),20(a,1,2,2))]. % back CAC tautology: 188 x v (y v (z v (u v (w v v5)))) = w v (y v (x v (z v (u v v5)))). [para(10(a,2),20(a,1,2,2))]. % back CAC tautology: 187 x v (y v (z v (u v (w v v5)))) = u v (y v (x v (w v (z v v5)))). [para(10(a,1),20(a,1,2,2))]. % back CAC tautology: 186 x v (y v (z v (u v w))) = u v (z v (x v (y v w))). [para(20(a,1),10(a,2,2)),flip(a)]. given #169 (T,wt=11): 1827 x v (x v y)' = x v y'. [back_rewrite(1762),rewrite([1801(4),1751(4)])]. given #170 (A,wt=25): 190 ((x v (y v (z v (u v w)))')' v (u v (x v (z v (y v w))))')' = x. [para(20(a,1),11(a,1,1,1,1,2,1))]. given #171 (T,wt=8): 2705 x' v (y v x) = c_0. [para(1980(a,1),1827(a,1,2,1)),rewrite([1686(3),1801(2),9(2),1686(5)]),flip(a)]. given #172 (T,wt=11): 1998 x v (y v (x' v z))' = x. [para(2(a,1),1981(a,1,2,1))]. given #173 (T,wt=11): 2560 (x v y) v z = x v (y v z). [para(1802(a,2),1801(a,1)),flip(a)]. given #174 (T,wt=11): 2704 x v (y v x)' = x v y'. [para(1801(a,1),1827(a,1,2,1))]. given #175 (A,wt=25): 191 ((x v (y v (z v (u v w)))')' v (y v (u v (z v (x v w))))')' = x. [para(20(a,1),11(a,1,1,2,1,2))]. given #176 (T,wt=12): 1664 x v (y v (z v (u v x'))) = c_0. [back_rewrite(36),rewrite([1512(7),1512(7),1512(7)])]. given #177 (T,wt=12): 1716 x' v (y v (z v (u v x))) = c_0. [back_rewrite(1579),rewrite([1695(3),1678(4)])]. given #178 (T,wt=12): 1953 x v (y v (z v (x' v u))) = c_0. [para(1859(a,1),10(a,1,2,2)),rewrite([1512(2),1512(2)]),flip(a)]. given #179 (T,wt=12): 1955 x' v (y v (z v (x v u))) = c_0. [para(1859(a,1),19(a,1,2)),rewrite([1512(2)]),flip(a)]. given #180 (A,wt=25): 204 ((x v (y v (z v (u v w)))')' v (y v (x v (u v (z v w))))')' = x. [para(22(a,1),11(a,1,1,1,1,2,1))]. given #181 (T,wt=12): 2176 x' v (y v (x v z))' = x'. [para(2(a,1),2006(a,1,2,1))]. given #182 (T,wt=12): 2243 x' v (y v (z v x))' = x'. [para(1691(a,1),77(a,1,1,1,1)),rewrite([2(16),1759(15),1695(9),1686(7)])]. given #183 (T,wt=13): 1689 ((x v y)' v (y' v x)')' = x. [back_rewrite(1604),rewrite([1646(7),1678(5),1678(6)])]. given #184 (T,wt=13): 1700 x v (y v (z v (u v x')))' = x. [back_rewrite(1614),rewrite([1678(10),1686(8)])]. given #185 (A,wt=25): 298 ((x v (y v (z v (u v w)))')' v (z v (y v (u v (x v w))))')' = x. [para(19(a,1),11(a,1,1,2,1))]. given #186 (T,wt=13): 1761 (x v y)' v (x v y')' = x'. [para(12(a,1),1686(a,1,1)),rewrite([1758(9)]),flip(a)]. given #187 (T,wt=13): 1766 x v (y v (z v x)) = y v (z v x). [para(1702(a,1),10(a,1,2,2)),flip(a)]. given #188 (T,wt=13): 1826 x v (y v (x v z)) = y v (x v z). [back_rewrite(1767),rewrite([1801(2),1765(2)])]. given #189 (T,wt=13): 1975 x v (y v (z v x')') = y v x. [para(1751(a,1),2(a,1,2)),flip(a)]. given #190 (A,wt=25): 368 ((x v (y v (z v (u v w)))')' v (u v (y v (x v (z v w))))')' = x. [para(21(a,1),11(a,1,1,2,1))]. given #191 (T,wt=13): 1997 x v (y v (x' v z)') = y v x. [para(1981(a,1),2(a,1,2)),flip(a)]. given #192 (T,wt=13): 2001 x v (y v (z v (x' v u)))' = x. [para(10(a,2),1981(a,1,2,1))]. given #193 (T,wt=13): 2730 x v ((y v x')' v z) = x v z. [para(1751(a,1),2560(a,1,1)),flip(a)]. given #194 (T,wt=13): 2732 x v ((x' v y)' v z) = x v z. [para(1981(a,1),2560(a,1,1)),flip(a)]. given #195 (A,wt=25): 439 ((x v (y v (z v (u v w)))')' v (z v (u v (x v (y v w))))')' = x. [para(10(a,1),23(a,1,1,2,1,2))]. given #196 (T,wt=13): 2746 (x v y)' v (y v x')' = y'. [para(2704(a,1),2704(a,1,2,1)),rewrite([1801(10),1980(10)])]. given #197 (T,wt=13): 2779 (x v y)' v (y' v x)' = x'. [para(1689(a,1),1686(a,1,1)),flip(a)]. given #198 (T,wt=13): 2799 (x v y')' v (y v x)' = x'. [para(2704(a,1),1761(a,1,1,1)),rewrite([1686(6),1765(5)])]. given #199 (T,wt=13): 2800 (x v y')' v (z v y) = z v y. [para(1751(a,1),1766(a,1,2,2)),rewrite([1751(9)])]. given #200 (A,wt=14): 1650 x v (y v (z v (u v (w v x')))) = c_0. [back_rewrite(143),rewrite([1512(8),1512(8),1512(8),1512(8)])]. given #201 (T,wt=13): 2801 (x' v y)' v (z v x) = z v x. [para(1981(a,1),1766(a,1,2,2)),rewrite([1981(9)])]. given #202 (T,wt=13): 2869 (x' v y)' v (y v x)' = y'. [para(1686(a,1),2746(a,1,2,1,2))]. given #203 (T,wt=13): 2870 (x v y)' v (x' v y)' = y'. [para(1801(a,1),2746(a,1,2,1))]. given #204 (T,wt=14): 1755 (x v y)' v (z v (x v (u v y))) = c_0. [back_rewrite(1731),rewrite([1750(3)])]. given #205 (A,wt=17): 1774 x v (y v (z v (u v x))) = y v (z v (u v x)). [para(1702(a,1),21(a,1,2,2,2)),flip(a)]. given #206 (T,wt=14): 1956 x v (y v (z v (u v (x' v w)))) = c_0. [para(1859(a,1),21(a,1,2,2,2)),rewrite([1512(2),1512(2),1512(2)]),flip(a)]. given #207 (T,wt=14): 1957 x' v (y v (z v (u v (x v w)))) = c_0. [para(1859(a,1),26(a,1,2,2)),rewrite([1512(2),1512(2)]),flip(a)]. given #208 (T,wt=14): 1974 x' v (y v (z v (x v u)))' = x'. [para(1859(a,1),65(a,1,1,2,1,2)),rewrite([1512(9),1801(10),1695(10),1686(8)])]. given #209 (T,wt=14): 2027 x' v (y v (z v (u v (w v x)))) = c_0. [para(1691(a,1),10(a,1,2,2)),rewrite([1512(2),1512(2)]),flip(a)]. given #210 (A,wt=21): 1791 x v (y v (z v (u v (w v x)))) = y v (z v (u v (w v x))). [para(1702(a,1),30(a,1,2,2,2,2)),flip(a)]. given #211 (T,wt=14): 2078 x v (y v (z v (u v (x v y)'))) = c_0. [para(1837(a,1),29(a,1,2,2)),rewrite([1512(2),1512(2)]),flip(a)]. given #212 (T,wt=14): 2102 x' v (y v (z v (u v x)))' = x'. [para(1691(a,1),67(a,1,1,2,1,2)),rewrite([1512(9),1801(10),1695(10),1686(8)])]. given #213 (T,wt=14): 2107 x' v (y v (z v x)') = y v x'. [para(1980(a,1),2(a,1,2)),flip(a)]. given #214 (T,wt=14): 2175 x' v (y v (x v z)') = y v x'. [para(2006(a,1),2(a,1,2)),flip(a)]. given #215 (A,wt=21): 1816 x v (y v (z v (u v (x v w)))) = y v (z v (u v (x v w))). [back_rewrite(1792),rewrite([1801(2),1765(2)])]. given #216 (T,wt=14): 2563 (x v y)' v (z v (y v (u v x))) = c_0. [para(1802(a,1),1691(a,1,2,2))]. given #217 (T,wt=12): 3002 (x v y)' v (z v (y v x)) = c_0. [para(1702(a,1),2563(a,1,2,2,2))]. given #218 (T,wt=14): 2564 (x v y)' v (z v (x v (y v u))) = c_0. [para(1802(a,2),1691(a,1,2,2))]. given #219 (T,wt=14): 2572 x v (y v (z v ((x v y)' v u))) = c_0. [para(1802(a,2),2187(a,1,1)),rewrite([2560(6),2560(5)])]. given #220 (A,wt=17): 1821 x v (y v (z v (x v u))) = y v (z v (x v u)). [back_rewrite(1777),rewrite([1801(4),1774(4),1819(6),1820(4)])]. given #221 (T,wt=14): 2733 x' v ((y v x)' v z) = x' v z. [para(1980(a,1),2560(a,1,1)),flip(a)]. given #222 (T,wt=14): 2734 x' v ((x v y)' v z) = x' v z. [para(2006(a,1),2560(a,1,1)),flip(a)]. given #223 (T,wt=14): 2747 x v (y v (z v (u v (y v x)'))) = c_0. [back_rewrite(2671),rewrite([2745(4)])]. given #224 (T,wt=14): 2802 (x v y)' v (z v y') = z v y'. [para(1980(a,1),1766(a,1,2,2)),rewrite([1980(9)])]. given #225 (A,wt=16): 1951 x v (y v (z v (u v (w v (v5 v x'))))) = c_0. [para(1667(a,1),30(a,1,2,2,2,2)),rewrite([1512(2),1512(2),1512(2),1512(2)]),flip(a)]. given #226 (T,wt=14): 2803 (x v y)' v (z v x') = z v x'. [para(2006(a,1),1766(a,1,2,2)),rewrite([2006(9)])]. given #227 (T,wt=14): 2923 (x v y)' v (z v (u v (y v x))) = c_0. [para(1801(a,1),1755(a,1,2,2)),rewrite([2560(4)])]. given #228 (T,wt=14): 3003 (x v y)' v (z v (y v (x v u))) = c_0. [para(1801(a,1),2563(a,1,2,2,2))]. given #229 (T,wt=14): 3040 x v (y v (z v ((y v x)' v u))) = c_0. [para(2572(a,1),2(a,1)),flip(a)]. given #230 (A,wt=16): 1958 x v (y v (z v (u v (w v (x' v v5))))) = c_0. [para(1859(a,1),30(a,1,2,2,2,2)),rewrite([1512(2),1512(2),1512(2),1512(2)]),flip(a)]. given #231 (T,wt=15): 2003 x v (y v (z v (u v (x' v w))))' = x. [para(21(a,2),1981(a,1,2,1))]. given #232 (T,wt=15): 2165 x v (y v (z v (u v (w v x'))))' = x. [para(1667(a,1),68(a,1,1,2,1,2,2,2)),rewrite([1512(10),1512(10),1512(10),1801(11),1695(11),1686(9)])]. given #233 (T,wt=15): 2418 x v (y v (z v (u v x'))') = y v x. [para(1699(a,1),2(a,1,2)),flip(a)]. given #234 (T,wt=15): 2702 x v (y v (x v z)') = y v (x v z'). [para(1827(a,1),2(a,1,2)),flip(a)]. given #235 (A,wt=17): 1977 x v (y v (z v (u v x')')) = y v (z v x). [para(1751(a,1),10(a,1,2,2)),flip(a)]. given #236 (T,wt=15): 2703 x v (y v (x v z))' = x v (y v z)'. [para(2(a,1),1827(a,1,2,1))]. given #237 (T,wt=15): 2728 x v (y v (z v (x' v u))') = y v x. [para(1998(a,1),2(a,1,2)),flip(a)]. given #238 (T,wt=15): 2736 x v ((y v (z v x'))' v u) = x v u. [para(1699(a,1),2560(a,1,1)),flip(a)]. given #239 (T,wt=15): 2737 x v ((x v y)' v z) = x v (y' v z). [para(1827(a,1),2560(a,1,1)),rewrite([2560(3)]),flip(a)]. given #240 (A,wt=21): 1978 x v (y v (z v (u v (w v x')'))) = y v (z v (u v x)). [para(1751(a,1),21(a,1,2,2,2)),flip(a)]. given #241 (T,wt=15): 2739 x v ((y v (x' v z))' v u) = x v u. [para(1998(a,1),2560(a,1,1)),flip(a)]. given #242 (T,wt=15): 2742 x v (y v (z v x)') = y v (x v z'). [para(2704(a,1),2(a,1,2)),flip(a)]. given #243 (T,wt=15): 2743 x v ((y v x)' v z) = x v (y' v z). [para(2704(a,1),2560(a,1,1)),rewrite([2560(3)]),flip(a)]. given #244 (T,wt=15): 2745 x v (y v (z v x))' = x v (y v z)'. [para(2560(a,1),2704(a,1,2,1))]. given #245 (A,wt=25): 1979 x v (y v (z v (u v (w v (v5 v x')')))) = y v (z v (u v (w v x))). [para(1751(a,1),30(a,1,2,2,2,2)),flip(a)]. given #246 (T,wt=15): 2804 (x v (y v z'))' v (u v z) = u v z. [para(1699(a,1),1766(a,1,2,2)),rewrite([1699(11)])]. given #247 (T,wt=15): 2806 (x v (y' v z))' v (u v y) = u v y. [para(1998(a,1),1766(a,1,2,2)),rewrite([1998(11)])]. given #248 (T,wt=15): 3054 (x v y)' v (z v y) = y v (x' v z). [para(2733(a,1),2704(a,1,2,1)),rewrite([2560(7),2704(6),1686(4),1686(9),1801(8),2743(8)])]. given #249 (T,wt=15): 3060 (x v y)' v (z v x) = x v (y' v z). [para(2734(a,1),2704(a,1,2,1)),rewrite([2560(7),2704(6),1686(4),1686(9),1801(8),2737(8)])]. given #250 (A,wt=25): 1988 x v (y v (z v (u v (w v (v5 v x))))) = y v (z v (u v (w v (v5 v x)))). [para(1765(a,1),30(a,1,2,2,2,2)),flip(a)]. given #251 (T,wt=16): 2035 x' v (y v (z v (u v (w v (v5 v x))))) = c_0. [para(1691(a,1),21(a,1,2,2,2)),rewrite([1512(2),1512(2),1512(2)]),flip(a)]. given #252 (T,wt=16): 2103 x' v (y v (z v (u v (w v (x v v5))))) = c_0. [para(1954(a,1),21(a,1,2,2,2)),rewrite([1512(2),1512(2),1512(2)]),flip(a)]. given #253 (T,wt=16): 2108 (x v y)' v (x v (z v y))' = (x v y)'. [para(2(a,1),1980(a,1,2,1))]. given #254 (T,wt=16): 2179 x' v (y v (z v (u v (x v w))))' = x'. [para(21(a,2),2006(a,1,2,1))]. given #255 (A,wt=25): 1996 x v (y v (z v (u v (w v (x v v5))))) = y v (z v (u v (w v (x v v5)))). [para(1829(a,1),30(a,1,2,2,2,2)),flip(a)]. given #256 (T,wt=16): 2566 (x v y)' v (y v (z v x))' = (x v y)'. [para(1802(a,1),1980(a,1,2,1))]. given #257 (T,wt=14): 3371 (x v y)' v (y v x)' = (x v y)'. [para(1702(a,1),2566(a,1,2,1,2))]. given #258 (T,wt=16): 2567 (x v y)' v (x v (y v z))' = (x v y)'. [para(1802(a,2),1980(a,1,2,1))]. given #259 (T,wt=16): 2759 x' v (y v (z v (u v (w v x))))' = x'. [para(2705(a,1),191(a,1,1,2,1,2,2,2)),rewrite([1512(10),1512(10),1512(10),1801(11),1695(11),1686(9)])]. given #260 (A,wt=17): 2000 x v (y v (z v (x' v u)')) = y v (z v x). [para(1981(a,1),10(a,1,2,2)),flip(a)]. given #261 (T,wt=16): 2762 x v (y v (z v (u v ((x v y)' v w)))) = c_0. [para(1953(a,1),2560(a,1)),flip(a)]. given #262 (T,wt=16): 2772 x' v (y v (z v (x v u))') = y v x'. [para(2176(a,1),2(a,1,2)),flip(a)]. given #263 (T,wt=16): 2773 x' v ((y v (x v z))' v u) = x' v u. [para(2176(a,1),2560(a,1,1)),flip(a)]. given #264 (T,wt=16): 2775 x' v (y v (z v (u v x))') = y v x'. [para(2243(a,1),2(a,1,2)),flip(a)]. given #265 (A,wt=21): 2002 x v (y v (z v (u v (x' v w)'))) = y v (z v (u v x)). [para(1981(a,1),21(a,1,2,2,2)),flip(a)]. given #266 (T,wt=16): 2776 x' v ((y v (z v x))' v u) = x' v u. [para(2243(a,1),2560(a,1,1)),flip(a)]. given #267 (T,wt=16): 2808 (x v (y v z))' v (u v y') = u v y'. [para(2176(a,1),1766(a,1,2,2)),rewrite([2176(11)])]. given #268 (T,wt=16): 2809 (x v (y v z))' v (u v z') = u v z'. [para(2243(a,1),1766(a,1,2,2)),rewrite([2243(11)])]. given #269 (T,wt=16): 3026 (x v y)' v (z v (y v x))' = (x v y)'. [para(3002(a,1),1827(a,1,2,1)),rewrite([1801(5),1695(5)]),flip(a)]. given #270 (A,wt=25): 2004 x v (y v (z v (u v (w v (x' v v5)')))) = y v (z v (u v (w v x))). [para(1981(a,1),30(a,1,2,2,2,2)),flip(a)]. given #271 (T,wt=16): 3075 x v (y v (z v (u v ((y v x)' v w)))) = c_0. [para(2747(a,1),2560(a,1,1)),rewrite([1703(2),2560(7),2560(6),2560(5)]),flip(a)]. given #272 (T,wt=16): 3088 (x v y)' v (z v (u v (w v (y v x)))) = c_0. [para(2923(a,1),2(a,1,2)),rewrite([1512(2)]),flip(a)]. given #273 (T,wt=16): 3372 (x v (y v z))' v (z v x)' = (z v x)'. [para(2566(a,1),1801(a,1)),flip(a)]. given #274 (T,wt=16): 3373 (x v y)' v (y v (x v z))' = (x v y)'. [para(1801(a,1),2566(a,1,2,1,2))]. given #275 (A,wt=17): 2005 x v (y v (z v (u v (w v (x' v v5)))))' = x. [para(30(a,2),1981(a,1,2,1))]. given #276 (T,wt=16): 3398 (x v (y v z))' v (y v x)' = (x v y)'. [para(3371(a,1),2732(a,2)),rewrite([1686(5),2560(4),3397(9)])]. given #277 (T,wt=16): 3399 (x v (y v z))' v (z v y)' = (z v y)'. [para(3371(a,1),2800(a,1,2)),rewrite([1686(3),3371(11)])]. given #278 (T,wt=17): 2167 x v (y v (z v (u v (w v (v5 v x')))))' = x. [para(1666(a,1),68(a,1,1,2,1,2,2,2)),rewrite([1512(11),1512(11),1512(11),1801(12),1695(12),1686(10)])]. given #279 (T,wt=17): 2647 x v (y v (z v (u v (w v x')))') = x v y. [back_rewrite(2174),rewrite([2560(7)])]. given #280 (A,wt=18): 2024 x v (y v (z v (u v (w v (v5 v (v6 v x')))))) = c_0. [para(1666(a,1),30(a,1,2,2,2,2)),rewrite([1512(2),1512(2),1512(2),1512(2)]),flip(a)]. given #281 (T,wt=17): 2783 x v ((y v (z v (u v x')))' v w) = x v w. [para(1700(a,1),2560(a,1,1)),flip(a)]. given #282 (T,wt=17): 2795 (x v y)' v (z v (x v y')') = z v x'. [para(1761(a,1),2(a,1,2)),flip(a)]. given #283 (T,wt=17): 2797 (x v y)' v ((x v y')' v z) = x' v z. [para(1761(a,1),2560(a,1,1)),flip(a)]. given #284 (T,wt=17): 2810 (x v (y v (z v u')))' v (w v u) = w v u. [para(1700(a,1),1766(a,1,2,2)),rewrite([1700(13)])]. given #285 (A,wt=18): 2031 (x v (y v z))' v (u v (w v (y v (x v z)))) = c_0. [para(22(a,1),1691(a,1,2,2))]. given #286 (T,wt=17): 2815 x v (y v ((z v x')' v u)) = y v (x v u). [para(1975(a,1),2560(a,1,1)),rewrite([2560(2),2560(7)]),flip(a)]. given #287 (T,wt=17): 2820 (x v y')' v (z v (u v y)) = z v (u v y). [para(1975(a,1),1766(a,1,2,2)),rewrite([2560(7),1821(7),1975(11)])]. given #288 (T,wt=17): 2831 x v (y v ((x' v z)' v u)) = y v (x v u). [para(1997(a,1),2560(a,1,1)),rewrite([2560(2),2560(7)]),flip(a)]. given #289 (T,wt=17): 2836 (x' v y)' v (z v (u v x)) = z v (u v x). [para(1997(a,1),1766(a,1,2,2)),rewrite([2560(7),1821(7),1997(11)])]. given #290 (A,wt=22): 2036 (x v (y v (z v u)))' v (w v (z v (v5 v (x v (y v u))))) = c_0. [para(21(a,1),1691(a,1,2,2))]. given #291 (T,wt=17): 2837 x v (y v (z v (u v (x' v w)))') = y v x. [para(2001(a,1),2(a,1,2)),flip(a)]. given #292 (T,wt=17): 2838 x v ((y v (z v (x' v u)))' v w) = x v w. [para(2001(a,1),2560(a,1,1)),flip(a)]. given #293 (T,wt=17): 2840 (x v (y v (z' v u)))' v (w v z) = w v z. [para(2001(a,1),1766(a,1,2,2)),rewrite([2001(13)])]. given #294 (T,wt=17): 2848 (x v y')' v (z v (y v u)) = z v (y v u). [para(2730(a,1),1766(a,1,2,2)),rewrite([2560(7),1766(6),2730(11)])]. given #295 (A,wt=22): 2042 (x v (y v (z v u)))' v (w v (z v (v5 v (y v (x v u))))) = c_0. [para(27(a,1),1691(a,1,2,2))]. given #296 (T,wt=17): 2856 (x' v y)' v (z v (x v u)) = z v (x v u). [para(2732(a,1),1766(a,1,2,2)),rewrite([2560(7),1766(6),2732(11)])]. given #297 (T,wt=17): 2867 (x v y)' v (z v (y v x')') = z v y'. [para(2746(a,1),2(a,1,2)),flip(a)]. given #298 (T,wt=17): 2871 (x v y)' v ((y v x')' v z) = y' v z. [para(2746(a,1),2560(a,1,1)),flip(a)]. given #299 (T,wt=17): 2882 (x v y)' v (z v (y' v x)') = z v x'. [para(2779(a,1),2(a,1,2)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 2.61 (+ 0.01) seconds: distributivity_1. % Length of proof is 141. % Level of proof is 46. % Maximum clause weight is 29. % Given clauses 299. 1 x ^ (y v z) = (x ^ y) v (x ^ z) # label(distributivity_1) # label(non_clause) # label(goal). [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) # label(distributivity_1) # 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 w))) = u v (x v (y v (z v w))). [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)]. 743 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)]. 755 c_0'' = c_0 v c_0. [para(743(a,1),44(a,1,2)),rewrite([2(11),567(15)])]. 810 (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([755(18)])]. 823 (c_0 v c_0) v (x v (c_0' v c_0)) = x v c_0. [back_rewrite(554),rewrite([755(3)])]. 832 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0). [back_rewrite(545),rewrite([755(3),755(13),2(14),338(13)])]. 851 ((c_0 v (x v c_0))' v (x v c_0')')' = x. [back_rewrite(514),rewrite([755(3),832(6)])]. 872 ((c_0 v ((x v x'')' v c_0))' v x)' = (x v x'')'. [back_rewrite(57),rewrite([755(7),2(8)])]. 887 ((c_0 v (c_0 v c_0))' v c_0')' = c_0. [para(755(a,1),17(a,1,1,1,1,2))]. 1041 c_0' v (c_0' v c_0')' = c_0. [para(41(a,1),851(a,1,1,2,1)),rewrite([54(12),887(10)]),flip(a)]. 1046 (c_0' v x')' v (c_0' v x)' = c_0. [para(18(a,1),851(a,1,1,2,1)),rewrite([121(13),887(10)]),flip(a)]. 1057 c_0' v (x v (c_0' v c_0')') = x v c_0. [para(1041(a,1),2(a,1,2)),flip(a)]. 1106 (c_0' v x')' v c_0 = (c_0' v x) v c_0. [para(1046(a,1),15(a,1,2)),flip(a)]. 1189 (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(1057(a,1),130(a,1,1,2,1,2)),rewrite([1106(16),2(15),1106(14)])]. 1190 (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),1057(a,1,2)),rewrite([1057(28),1106(20),2(19),1106(18)]),flip(a)]. 1205 (c_0' v c_0')' = c_0' v c_0. [para(1106(a,1),13(a,1,1,2,1,2)),rewrite([37(14)]),flip(a)]. 1242 c_0' v (c_0' v c_0) = c_0. [back_rewrite(1189),rewrite([1205(21),2(20),1190(19)])]. 1260 c_0' v (x v (c_0' v c_0)) = x v c_0. [back_rewrite(1057),rewrite([1205(8)])]. 1263 c_0' v c_0 = c_0 v c_0. [para(1242(a,1),44(a,1,2)),rewrite([2(11),810(15)]),flip(a)]. 1264 c_0 v (c_0 v c_0) = c_0. [para(44(a,2),1242(a,1,2)),rewrite([2(11),41(10),1263(6),2(6),1263(5)])]. 1265 c_0 v c_0 = c_0. [para(1242(a,1),14(a,1,1,1,1,2,1,1)),rewrite([1263(6),16(8),755(4),1264(5),1205(6),1263(4),1263(9),16(11)])]. 1271 c_0' v (x v (y v c_0)) = x v (y v c_0). [para(1242(a,1),21(a,1,2,2)),rewrite([1263(9),1265(8)]),flip(a)]. 1283 c_0' v (x v c_0) = x v c_0. [back_rewrite(1260),rewrite([1263(6),1265(5)])]. 1304 c_0 v (x v c_0) = x v c_0. [back_rewrite(823),rewrite([1265(3),1263(5),1265(4)])]. 1313 c_0' v c_0 = c_0. [back_rewrite(1263),rewrite([1265(7)])]. 1349 c_0'' = c_0. [back_rewrite(755),rewrite([1265(6)])]. 1354 (((x v x'')' v c_0)' v x)' = (x v x'')'. [back_rewrite(872),rewrite([1304(8)])]. 1358 (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),1271(12),2(10),2(20),1271(21)])]. 1372 x v ((x v c_0) v c_0) = x v c_0. [para(1283(a,1),103(a,1,1,2,1,2,2)),rewrite([2(9),2(10),1358(13)])]. 1373 (c_0' v (x v c_0)')' = x v c_0. [para(1283(a,1),37(a,1,1,2,1,2,1)),rewrite([2(9),1372(9),1283(7),1283(12)])]. 1374 x v ((c_0' v (x v c_0)') v c_0) = c_0. [para(1283(a,1),133(a,1,1,2,1,2,2)),rewrite([2(9),1372(9),2(7),1372(7),2(9)])]. 1379 x v (y v ((x v c_0) v c_0)) = y v (x v c_0). [para(1372(a,1),2(a,1,2)),flip(a)]. 1417 x v ((x v c_0) v ((c_0' v (x v c_0)') v c_0)) = c_0. [para(1372(a,1),45(a,1,2,1,2,1,2,1)),rewrite([1379(10),2(7),1372(7),2(11)])]. 1426 ((x v c_0)' v c_0')' = x v c_0. [para(1373(a,1),34(a,1,1,1,1,2)),rewrite([2(5),1372(5),1313(7)])]. 1439 ((x v (y v c_0))' v ((y v c_0)' v (x v c_0'))')' = x. [para(1426(a,1),11(a,1,1,1,1,2))]. 1446 ((x v c_0)' v ((x v c_0) v ((x v c_0)' v c_0))')' = x v c_0. [para(1426(a,1),13(a,1,1,2,1,2,1)),rewrite([2(11),1426(21)])]. 1451 ((x v c_0)' v ((x v c_0)' v c_0)')' = c_0. [para(1426(a,1),34(a,1,1,1,1,2)),rewrite([1304(4)])]. 1472 x v (y v ((c_0' v (x v c_0)') v c_0)) = y v c_0. [para(1374(a,1),2(a,1,2)),flip(a)]. 1489 (x v c_0) v c_0 = c_0. [back_rewrite(1417),rewrite([1472(12)])]. 1494 (x v c_0) v (y v c_0) = y v c_0. [para(1489(a,1),2(a,1,2)),flip(a)]. 1512 x v c_0 = c_0. [back_rewrite(1446),rewrite([1494(11),1451(11)]),flip(a)]. 1527 (c_0' v (c_0' v (x v c_0'))')' = x. [back_rewrite(1439),rewrite([1512(2),1512(2),1512(4)])]. 1538 (x v x'')' = (c_0' v x)'. [back_rewrite(1354),rewrite([1512(6)]),flip(a)]. 1604 ((x v y)' v ((y v (z v y')')' v (x v c_0'))')' = x. [back_rewrite(463),rewrite([1512(9)])]. 1607 ((x v x)' v c_0')' = x. [back_rewrite(456),rewrite([1512(10)])]. 1628 ((x v (y v (c_0' v (x v x))')')' v c_0')' = x. [back_rewrite(330),rewrite([1512(11)])]. 1635 (c_0' v (c_0' v x)')' = x. [back_rewrite(243),rewrite([1538(4),1512(6),1349(3),1512(2),1538(6)])]. 1636 ((x v c_0')' v (y v ((c_0' v (z v z)') v (x v z)))')' = x. [back_rewrite(226),rewrite([1512(2)])]. 1646 (x v (y v x')')' = (x v c_0')'. [back_rewrite(180),rewrite([1512(7),1512(2)]),flip(a)]. 1647 ((c_0' v x)' v c_0')' = x. [back_rewrite(175),rewrite([1538(4),1538(8),1512(10),1512(6)])]. 1663 (c_0' v (x v x)') v (y v x) = c_0. [back_rewrite(44),rewrite([1512(9)])]. 1678 x v c_0' = x. [back_rewrite(1527),rewrite([1635(11)])]. 1686 x'' = x. [back_rewrite(1636),rewrite([1678(3),1663(8),1512(3),1678(4)])]. 1689 ((x v y)' v (y' v x)')' = x. [back_rewrite(1604),rewrite([1646(7),1678(5),1678(6)])]. 1695 c_0' v x = x. [back_rewrite(1647),rewrite([1678(7),1686(5)])]. 1697 x v (y v (x v x)')' = x. [back_rewrite(1628),rewrite([1695(4),1678(9),1686(7)])]. 1702 x v x = x. [back_rewrite(1607),rewrite([1678(5),1686(3)])]. 1751 x v (y v x')' = x. [back_rewrite(1697),rewrite([1702(1)])]. 1762 x v (x v ((x v y')' v y))' = x v y'. [para(13(a,1),1686(a,1,1)),rewrite([1686(4)]),flip(a)]. 1801 x v y = y v x. [para(1678(a,1),2(a,1,2)),rewrite([1678(4)])]. 1802 x v (y v z) = z v (x v y). [para(1678(a,1),10(a,1,2,2)),rewrite([1678(5)])]. 1827 x v (x v y)' = x v y'. [back_rewrite(1762),rewrite([1801(4),1751(4)])]. 1975 x v (y v (z v x')') = y v x. [para(1751(a,1),2(a,1,2)),flip(a)]. 1980 x' v (y v x)' = x'. [para(1686(a,1),1751(a,1,2,1,2))]. 1981 x v (x' v y)' = x. [para(1801(a,1),1751(a,1,2,1))]. 1997 x v (y v (x' v z)') = y v x. [para(1981(a,1),2(a,1,2)),flip(a)]. 2108 (x v y)' v (x v (z v y))' = (x v y)'. [para(2(a,1),1980(a,1,2,1))]. 2560 (x v y) v z = x v (y v z). [para(1802(a,2),1801(a,1)),flip(a)]. 2704 x v (y v x)' = x v y'. [para(1801(a,1),1827(a,1,2,1))]. 2733 x' v ((y v x)' v z) = x' v z. [para(1980(a,1),2560(a,1,1)),flip(a)]. 2742 x v (y v (z v x)') = y v (x v z'). [para(2704(a,1),2(a,1,2)),flip(a)]. 2779 (x v y)' v (y' v x)' = x'. [para(1689(a,1),1686(a,1,1)),flip(a)]. 2882 (x v y)' v (z v (y' v x)') = z v x'. [para(2779(a,1),2(a,1,2)),flip(a)]. 2887 (x v (y v z)')' = (x v (z v y'))' v (x v z')'. [para(1975(a,1),2779(a,1,2,1)),rewrite([1686(2),1801(4),2742(4),1686(10)]),flip(a)]. 2896 (c3 v (c1' v c2'))' v (c1' v c3')' != (c1' v c2')' v (c1' v c3')' # answer(distributivity_1). [back_rewrite(8),rewrite([2887(8),2(7)])]. 3053 (x v y)' v ((x v (z v y))' v u) = (x v y)' v u. [para(2(a,1),2733(a,1,2,1,1))]. 3341 (x v (y v z))' v (x v y')' = (x v z)' v (x v y')'. [para(1981(a,1),2108(a,1,2,1,2)),rewrite([2887(5),1686(2),1801(10),3053(10),2887(11),1686(8)]),flip(a)]. 3353 (x v (y v z)')' = (x v y')' v (x v z')'. [back_rewrite(2887),rewrite([3341(12)])]. 3786 (x v (y v z))' v (y v x')' = (y v z)' v (y v x')'. [para(2882(a,1),2779(a,1,2,1)),rewrite([1801(6),2560(6),1997(5),3353(12),1686(9)])]. 3787 $F # answer(distributivity_1). [resolve(3786,a,2896,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=299. Generated=81561. Kept=3783. proofs=1. Usable=138. Sos=695. Demods=819. Limbo=6, Disabled=2948. Hints=0. Kept_by_rule=0, Deleted_by_rule=11032. Forward_subsumed=66746. Back_subsumed=80. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2963 (7 lex), Back_demodulated=2724. Back_unit_deleted=0. Demod_attempts=1506300. Demod_rewrites=242173. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=2.70. User_CPU=2.61, System_CPU=0.01, Wall_clock=3. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11187 exit (max_proofs) Wed Feb 25 09:32:09 2009