============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11425 was started by mccune on cleo.thornwood, Sat Aug 12 21:01:14 2006 The command was "/home/mccune/bin/prover9 -f ba-4basis.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file ba-4basis.in assign(new_constants,1). formulas(sos). x v (y v z) = y v (x v z) # label(AJ). x ^ y = (x' v y')' # label(DM). x v x' = y v y' # label(ONE). (x v y') ^ (x v y) = x # label(CUT). end_of_list. formulas(goals). x'' = x # answer(CC). x v (x ^ y) = x # answer(B1). x ^ (y v z) = (x ^ y) v (x ^ z) # answer(DIST1). x v (y ^ (x v z)) = x v (z ^ (x v y)) # answer(MOD). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x'' = x # answer(CC). [goal]. 2 x v (x ^ y) = x # answer(B1). [goal]. 3 x ^ (y v z) = (x ^ y) v (x ^ z) # answer(DIST1). [goal]. 4 x v (y ^ (x v z)) = x v (z ^ (x v y)) # answer(MOD). [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) # label(AJ). [assumption]. x ^ y = (x' v y')' # label(DM). [assumption]. x v x' = y v y' # label(ONE). [assumption]. (x v y') ^ (x v y) = x # label(CUT). [assumption]. c1'' != c1 # answer(CC). [deny(1)]. c2 v (c2 ^ c3) != c2 # answer(B1). [deny(2)]. (c4 ^ c5) v (c4 ^ c6) != c4 ^ (c5 v c6) # answer(DIST1). [deny(3)]. c7 v (c9 ^ (c7 v c8)) != c7 v (c8 ^ (c7 v c9)) # answer(MOD). [deny(4)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 4). % (Horn set with more than one neg. clause) Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, v, ^, ' ]). After inverse_order: (no changes). Unfolding symbols: ^/2. Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). NOTE: New constant: x v x' = c_0. [new_symbol(7)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c_0, v, ^, ' ]). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 5 x v (y v z) = y v (x v z) # label(AJ). [assumption]. 6 x ^ y = (x' v y')' # label(DM). [assumption]. 9 ((x v y')' v (x v y)')' = x. [copy(8),rewrite(6(4))]. 10 c1'' != c1 # answer(CC). [deny(1)]. 12 c2 v (c2' v c3')' != c2 # answer(B1). [copy(11),rewrite(6(4))]. 14 (c4' v (c5 v c6)')' != (c4' v c5')' v (c4' v c6')' # answer(DIST1). [copy(13),rewrite(6(3),6(9),6(18)),flip(a)]. 16 c7 v (c8' v (c7 v c9)')' != c7 v (c9' v (c7 v c8)')' # answer(MOD). [copy(15),rewrite(6(6),6(16)),flip(a)]. 17 x v x' = c_0. [new_symbol(7)]. end_of_list. formulas(demodulators). 5 x v (y v z) = y v (x v z) # label(AJ). [assumption]. % (lex-dep) 6 x ^ y = (x' v y')' # label(DM). [assumption]. 9 ((x v y')' v (x v y)')' = x. [copy(8),rewrite(6(4))]. 17 x v x' = c_0. [new_symbol(7)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 5 x v (y v z) = y v (x v z) # label(AJ). [assumption]. given #2 (I,wt=10): 6 x ^ y = (x' v y')' # label(DM). [assumption]. given #3 (I,wt=13): 9 ((x v y')' v (x v y)')' = x. [copy(8),rewrite(6(4))]. given #4 (I,wt=5): 10 c1'' != c1 # answer(CC). [deny(1)]. given #5 (I,wt=10): 12 c2 v (c2' v c3')' != c2 # answer(B1). [copy(11),rewrite(6(4))]. given #6 (I,wt=22): 14 (c4' v (c5 v c6)')' != (c4' v c5')' v (c4' v c6')' # answer(DIST1). [copy(13),rewrite(6(3),6(9),6(18)),flip(a)]. given #7 (I,wt=21): 16 c7 v (c8' v (c7 v c9)')' != c7 v (c9' v (c7 v c8)')' # answer(MOD). [copy(15),rewrite(6(6),6(16)),flip(a)]. given #8 (I,wt=6): 17 x v x' = c_0. [new_symbol(7)]. given #9 (T,wt=10): 23 x v (y v x') = y v c_0. [para(17(a,1),5(a,1,2)),flip(a)]. given #10 (T,wt=10): 24 (c_0' v (x v x)')' = x. [para(17(a,1),9(a,1,1,1,1))]. given #11 (A,wt=15): 18 x v (y v (z v u)) = z v (x v (y v u)). [para(5(a,1),5(a,1,2))]. given #12 (F,wt=11): 34 (c_0' v (x v x)') v x = c_0. [para(24(a,1),17(a,1,2))]. given #13 (F,wt=12): 25 ((x v x'')' v c_0')' = x. [para(17(a,1),9(a,1,1,2,1))]. given #14 (T,wt=13): 32 (x v (c_0' v (x v x))')' = c_0'. [para(24(a,1),9(a,1,1,1))]. given #15 (T,wt=13): 68 ((x v x'')' v c_0') v x = c_0. [para(25(a,1),17(a,1,2))]. given #16 (A,wt=17): 19 ((x v (y v z)')' v (y v (x v z))')' = x. [para(5(a,1),9(a,1,1,2,1))]. given #17 (F,wt=13): 72 (x v (x v (c_0' v x))')' = c_0'. [para(5(a,1),32(a,1,1,2,1))]. given #18 (F,wt=14): 26 ((x v y')' v (x v y)') v x = c_0. [para(9(a,1),17(a,1,2))]. given #19 (T,wt=14): 27 x v (y v (z v x')) = y v (z v c_0). [para(23(a,1),5(a,1,2)),flip(a)]. given #20 (T,wt=14): 76 (x v (c_0' v (x v x))') v c_0' = c_0. [para(32(a,1),17(a,1,2))]. given #21 (A,wt=21): 20 ((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 #22 (F,wt=11): 193 x v (c_0' v (x v x))' = c_0. [back_rewrite(183),rewrite(184(10),24(8)),flip(a)]. given #23 (F,wt=11): 253 x v (x v (c_0' v x))' = c_0. [para(5(a,1),193(a,1,2,1))]. given #24 (T,wt=12): 254 (c_0' v (x v x)) v c_0 = x v c_0. [para(193(a,1),23(a,1,2))]. given #25 (T,wt=12): 255 c_0'' v (c_0'' v c_0)' = c_0. [para(23(a,1),193(a,1,2,1))]. given #26 (A,wt=19): 21 (x v (x v ((x v y')' v y))')' = (x v y')'. [para(9(a,1),9(a,1,1,1)),rewrite(5(5))]. given #27 (F,wt=12): 270 (x v (c_0' v x)) v c_0 = x v c_0. [para(253(a,1),23(a,1,2))]. given #28 (F,wt=13): 280 (c_0'' v c_0) v c_0 = c_0'' v c_0. [para(23(a,1),254(a,1,1))]. given #29 (T,wt=15): 33 ((c_0' v (x v x)'')' v x)' = c_0'. [para(24(a,1),9(a,1,1,2))]. given #30 (T,wt=15): 35 (c_0' v (x v x)') v (y v x) = y v c_0. [para(24(a,1),23(a,1,2,2))]. given #31 (A,wt=21): 22 (((x v y')' v (x v y)'')' v x)' = (x v y')'. [para(9(a,1),9(a,1,1,2))]. given #32 (F,wt=15): 37 x v (y v (z v u)) = z v (y v (x v u)). [para(18(a,1),5(a,1))]. given #33 (F,wt=15): 39 x v (y v (z v u)) = x v (z v (y v u)). [para(18(a,2),5(a,1))]. given #34 (T,wt=15): 56 (c_0' v (x' v x')') v c_0 = x v c_0. [para(34(a,1),23(a,1,2)),flip(a)]. given #35 (T,wt=15): 74 (c_0' v (x v (c_0' v (x v x)))')' = x. [para(32(a,1),9(a,1,1,1))]. given #36 (A,wt=16): 28 ((x v (y v x')')' v (y v c_0)')' = x. [para(23(a,1),9(a,1,1,2,1))]. given #37 (F,wt=15): 118 (c_0' v (c_0' v (x v (x v x)))')' = x. [para(32(a,1),19(a,1,1,1))]. given #38 (F,wt=15): 126 (c_0' v (x v (x v (c_0' v x)))')' = x. [para(72(a,1),9(a,1,1,1))]. given #39 (T,wt=15): 251 x v (y v (c_0' v (x v x))') = y v c_0. [para(193(a,1),5(a,1,2)),flip(a)]. given #40 (T,wt=15): 269 x v (y v (x v (c_0' v x))') = y v c_0. [para(253(a,1),5(a,1,2)),flip(a)]. given #41 (A,wt=18): 29 ((x v y')' v (x v y)') v (z v x) = z v c_0. [para(9(a,1),23(a,1,2,2))]. given #42 (F,wt=16): 30 (c_0' v (x v ((x v y) v y))')' = x v y. [para(5(a,1),24(a,1,1,2,1))]. given #43 (F,wt=9): 821 c_0'' v c_0 = c_0''. [para(280(a,1),30(a,1,1,2,1,2,1)),rewrite(280(14),5(13),280(12),294(14),280(10)),flip(a)]. given #44 (T,wt=13): 851 c_0'' v (x v c_0) = x v c_0''. [back_rewrite(300),rewrite(821(5),821(11))]. given #45 (T,wt=14): 858 c_0' v (c_0'' v (x v c_0)) = x v c_0. [para(851(a,2),23(a,1,2))]. given #46 (A,wt=18): 31 ((x v y)' v (x v (c_0' v (y v y)'))')' = x. [para(24(a,1),9(a,1,1,1,1,2))]. given #47 (F,wt=14): 907 c_0'' v (x v (c_0' v c_0)) = x v c_0. [para(858(a,1),18(a,2))]. given #48 (F,wt=15): 853 (c_0' v (c_0 v c_0)') v c_0'' = c_0''. [para(821(a,1),35(a,1,2)),rewrite(821(16))]. given #49 (T,wt=12): 1019 (c_0' v c_0''')'' = c_0'. [para(853(a,1),28(a,1,1,1,1,2,1)),rewrite(34(17),812(11))]. given #50 (T,wt=10): 1024 (c_0' v c_0''')' = c_0. [para(1019(a,1),17(a,1,2)),rewrite(812(11))]. given #51 (A,wt=19): 36 x v (y v (z v (u v v))) = z v (x v (u v (y v v))). [para(18(a,1),5(a,1,2))]. given #52 (F,wt=11): 1030 (c_0' v c_0''') v c_0 = c_0. [para(1024(a,1),17(a,1,2))]. given #53 (F,wt=15): 881 (c_0'' v (x v c_0))' = (x v c_0'')'. [para(851(a,2),21(a,2,1)),rewrite(21(12)),flip(a)]. given #54 (T,wt=15): 1029 ((c_0' v c_0'''')' v c_0)' = c_0'. [para(1024(a,1),9(a,1,1,2))]. given #55 (T,wt=15): 1031 (c_0' v c_0''') v (x v c_0) = x v c_0. [para(1024(a,1),23(a,1,2,2))]. given #56 (A,wt=19): 38 x v (y v (z v (u v v))) = u v (x v (y v (z v v))). [para(18(a,2),5(a,1,2))]. given #57 (F,wt=15): 1042 (c_0''' v (c_0' v c_0)')' = c_0''. [para(1024(a,1),28(a,1,1,1,1,2)),rewrite(821(5))]. given #58 (F,wt=15): 1187 (c_0' v c_0''') v c_0'' = c_0''. [para(1030(a,1),851(a,1,2)),rewrite(821(5)),flip(a)]. given #59 (T,wt=16): 144 ((c_0' v (x v x)'')' v x) v c_0' = c_0. [para(24(a,1),26(a,1,1,2))]. given #60 (T,wt=13): 1447 (c_0' v (x v x)'')' v x = c_0. [para(144(a,1),9(a,1,1,1,1)),rewrite(540(12),24(8)),flip(a)]. given #61 (A,wt=21): 40 ((x v (y v (z v u))')' v (z v (x v (y v u)))')' = x. [para(18(a,1),9(a,1,1,2,1))]. given #62 (F,wt=13): 1453 (c_0' v (c_0' v c_0')'')' = c_0. [para(144(a,1),30(a,1,1,2,1,2)),rewrite(359(18),1447(25))]. given #63 (F,wt=14): 1594 (c_0' v (c_0' v c_0')'') v c_0 = c_0. [para(1453(a,1),17(a,1,2))]. given #64 (T,wt=16): 158 (c_0' v (x v (c_0' v (x v x)))') v x = c_0. [para(32(a,1),26(a,1,1,1))]. given #65 (T,wt=16): 169 (c_0' v (x v (x v (c_0' v x)))') v x = c_0. [para(72(a,1),26(a,1,1,1))]. given #66 (A,wt=21): 41 ((x v (y v (z v u))')' v (y v (z v (x v u)))')' = x. [para(18(a,2),9(a,1,1,2,1))]. given #67 (F,wt=16): 618 (c_0' v (c_0' v (x v (x v x)))') v x = c_0. [para(118(a,1),17(a,1,2))]. given #68 (F,wt=16): 676 (c_0' v (x v x)) v (y v c_0) = x v (y v c_0). [para(251(a,1),27(a,1,2))]. given #69 (T,wt=8): 1916 c_0 v (c_0' v c_0) = c_0. [para(676(a,1),30(a,1,1,2,1,2)),rewrite(5(10),5(9),126(13),5(7)),flip(a)]. given #70 (T,wt=7): 1948 c_0'' = c_0 v c_0. [para(1916(a,1),35(a,1,2)),rewrite(5(11),995(15))]. given #71 (A,wt=18): 42 x v (y v (z v (u v x'))) = y v (z v (u v c_0)). [para(23(a,1),18(a,1,2,2)),flip(a)]. given #72 (F,wt=9): 1952 (c_0 v c_0) v c_0 = c_0 v c_0. [para(1916(a,1),907(a,1,2)),rewrite(1948(3))]. given #73 (F,wt=12): 1939 c_0 v (x v (c_0' v c_0)) = x v c_0. [para(1916(a,1),5(a,1,2)),flip(a)]. given #74 (T,wt=12): 1942 c_0' v (x v (c_0 v c_0)) = x v c_0. [para(1916(a,1),18(a,1,2)),flip(a)]. given #75 (T,wt=12): 1943 c_0 v (c_0' v (x v c_0)) = x v c_0. [para(1916(a,1),18(a,2,2))]. given #76 (A,wt=22): 43 (c_0' v (x v (y v ((y v (x v z)) v z)))')' = y v (x v z). [para(18(a,1),24(a,1,1,2,1)),rewrite(5(6))]. given #77 (F,wt=12): 2028 ((c_0 v (c_0 v c_0))' v c_0')' = c_0. [back_rewrite(1224),rewrite(1948(5),1447(11),1948(4),1948(15),1447(21))]. given #78 (F,wt=13): 2027 ((c_0 v (c_0 v c_0))' v c_0') v c_0 = c_0. [back_rewrite(1225),rewrite(1948(5),1948(14),1447(20),1948(13),5(21),1447(20))]. given #79 (T,wt=13): 2107 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0). [back_rewrite(894),rewrite(1948(3),1948(16),5(17),56(16))]. given #80 (T,wt=13): 2113 (c_0 v (x v c_0))' = (x v (c_0 v c_0))'. [back_rewrite(881),rewrite(1948(3),2107(6),1948(8))]. given #81 (A,wt=22): 44 (c_0' v (x v (y v ((x v (y v z)) v z)))')' = x v (y v z). [para(18(a,2),24(a,1,1,2,1))]. given #82 (F,wt=14): 1940 ((c_0 v (c_0' v c_0)')' v c_0')' = c_0. [para(1916(a,1),9(a,1,1,2,1))]. given #83 (F,wt=14): 2052 (x v (c_0 v c_0)) v (c_0 v (x v c_0))' = c_0. [back_rewrite(1194),rewrite(1948(3),1948(7),2034(11))]. given #84 (T,wt=14): 2096 (c_0 v c_0) v (x v (c_0' v c_0)) = x v c_0. [back_rewrite(907),rewrite(1948(3))]. given #85 (T,wt=14): 2172 (c_0 v (x v c_0)) v (x v (c_0 v c_0))' = c_0. [back_rewrite(2053),rewrite(2107(6))]. given #86 (A,wt=23): 45 x v (y v (z v (u v (v v w)))) = u v (x v (y v (v v (z v w)))). [para(18(a,1),18(a,1,2,2))]. given #87 (F,wt=14): 2316 c_0' v (x v ((x v c_0) v c_0)) = x v c_0. [para(676(a,1),43(a,1,1,2,1,2,2)),rewrite(5(11),545(16),5(9)),flip(a)]. given #88 (F,wt=14): 2318 (c_0' v (c_0 v (x v c_0))')' = x v c_0. [para(1943(a,1),43(a,1,1,2,1,2,2,1)),rewrite(5(10),5(12),2316(11),1943(16))]. given #89 (T,wt=11): 2800 (c_0' v c_0')' = c_0' v c_0. [para(1916(a,1),2318(a,1,1,2,1))]. given #90 (T,wt=11): 2803 (c_0' v c_0') v c_0 = c_0 v c_0. [back_rewrite(2074),rewrite(2793(15),1916(8))]. given #91 (A,wt=19): 46 x v (y v (z v (u v v))) = u v (x v (z v (y v v))). [para(18(a,1),18(a,1,2))]. given #92 (F,wt=11): 2837 (c_0' v (c_0' v c_0)')' = c_0. [back_rewrite(1453),rewrite(2800(8))]. given #93 (F,wt=11): 2840 (c_0' v (c_0' v c_0))' = c_0'. [para(2800(a,1),9(a,1,1,2)),rewrite(1948(5),5(6),1916(6))]. given #94 (T,wt=9): 3052 c_0' v (c_0' v c_0) = c_0. [para(2840(a,1),25(a,1,1,1,1,2,1)),rewrite(1948(10),5(11),2854(10),2028(10)),flip(a)]. given #95 (T,wt=5): 3065 c_0 v c_0 = c_0. [para(3052(a,1),22(a,1,1,1,1,2,1,1)),rewrite(3063(6),24(8),1948(4),3064(5),2800(6),3063(4),3063(9),24(11))]. given #96 (A,wt=23): 47 x v (y v (z v (u v (v v w)))) = v v (x v (y v (z v (u v w)))). [para(18(a,2),18(a,1,2,2))]. given #97 (F,wt=5): 3177 c_0'' = c_0. [back_rewrite(1948),rewrite(3065(6))]. given #98 (F,wt=6): 3135 c_0' v c_0 = c_0. [back_rewrite(3063),rewrite(3065(7))]. given #99 (T,wt=8): 3100 (c_0' v c_0')' = c_0. [back_rewrite(2800),rewrite(3063(10),3065(9))]. given #100 (T,wt=9): 3120 c_0 v (x v c_0) = x v c_0. [back_rewrite(2096),rewrite(3065(3),3063(5),3065(4))]. given #101 (A,wt=19): 48 x v (y v (z v (u v v))) = y v (x v (u v (z v v))). [para(18(a,2),18(a,1,2))]. given #102 (F,wt=9): 3137 (c_0' v c_0') v c_0 = c_0. [back_rewrite(2803),rewrite(3065(10))]. given #103 (F,wt=10): 3076 c_0' v (x v c_0) = x v c_0. [back_rewrite(3057),rewrite(3063(6),3065(5))]. given #104 (T,wt=11): 3106 x v ((x v c_0) v c_0) = x v c_0. [back_rewrite(2742),rewrite(3063(6),3065(5))]. given #105 (T,wt=12): 3136 (c_0' v (x v c_0)')' = x v c_0. [back_rewrite(2883),rewrite(3065(10),3091(12),3106(7),3065(10))]. given #106 (A,wt=23): 49 x v (y v (z v (u v (v v w)))) = z v (x v (v v (y v (u v w)))). [para(18(a,1),18(a,2,2,2))]. given #107 (F,wt=12): 3193 ((x v c_0)' v c_0')' = x v c_0. [back_rewrite(3101),rewrite(3120(4),3106(5),3120(11))]. given #108 (F,wt=13): 3091 (c_0' v c_0') v (x v c_0) = x v c_0. [back_rewrite(2841),rewrite(3063(9),3065(8))]. given #109 (T,wt=13): 3121 c_0 v (x v (y v c_0)) = x v (y v c_0). [back_rewrite(2077),rewrite(3065(3),3063(5),3065(4))]. given #110 (T,wt=13): 3125 x v ((c_0' v (x v c_0)') v c_0) = c_0. [back_rewrite(2067),rewrite(3063(8),3065(7),3076(9),3106(7),3065(12))]. given #111 (A,wt=19): 50 x v (y v (z v (u v v))) = z v (u v (x v (y v v))). [para(18(a,1),18(a,2,2))]. given #112 (F,wt=7): 3948 (x v c_0) v c_0 = c_0. [back_rewrite(3191),rewrite(3924(12))]. ============================== PROOF ================================= % Proof 1 at 0.96 (+ 0.01) seconds: CC. % Length of proof is 115. % Level of proof is 30. % Maximum clause weight is 39. % Given clauses 112. 1 x'' = x # answer(CC). [goal]. 5 x v (y v z) = y v (x v z) # label(AJ). [assumption]. 6 x ^ y = (x' v y')' # label(DM). [assumption]. 7 x v x' = y v y' # label(ONE). [assumption]. 8 (x v y') ^ (x v y) = x # label(CUT). [assumption]. 9 ((x v y')' v (x v y)')' = x. [copy(8),rewrite(6(4))]. 10 c1'' != c1 # answer(CC). [deny(1)]. 17 x v x' = c_0. [new_symbol(7)]. 18 x v (y v (z v u)) = z v (x v (y v u)). [para(5(a,1),5(a,1,2))]. 19 ((x v (y v z)')' v (y v (x v z))')' = x. [para(5(a,1),9(a,1,1,2,1))]. 21 (x v (x v ((x v y')' v y))')' = (x v y')'. [para(9(a,1),9(a,1,1,1)),rewrite(5(5))]. 22 (((x v y')' v (x v y)'')' v x)' = (x v y')'. [para(9(a,1),9(a,1,1,2))]. 23 x v (y v x') = y v c_0. [para(17(a,1),5(a,1,2)),flip(a)]. 24 (c_0' v (x v x)')' = x. [para(17(a,1),9(a,1,1,1,1))]. 25 ((x v x'')' v c_0')' = x. [para(17(a,1),9(a,1,1,2,1))]. 26 ((x v y')' v (x v y)') v x = c_0. [para(9(a,1),17(a,1,2))]. 27 x v (y v (z v x')) = y v (z v c_0). [para(23(a,1),5(a,1,2)),flip(a)]. 28 ((x v (y v x')')' v (y v c_0)')' = x. [para(23(a,1),9(a,1,1,2,1))]. 30 (c_0' v (x v ((x v y) v y))')' = x v y. [para(5(a,1),24(a,1,1,2,1))]. 32 (x v (c_0' v (x v x))')' = c_0'. [para(24(a,1),9(a,1,1,1))]. 33 ((c_0' v (x v x)'')' v x)' = c_0'. [para(24(a,1),9(a,1,1,2))]. 34 (c_0' v (x v x)') v x = c_0. [para(24(a,1),17(a,1,2))]. 35 (c_0' v (x v x)') v (y v x) = y v c_0. [para(24(a,1),23(a,1,2,2))]. 36 x v (y v (z v (u v v))) = z v (x v (u v (y v v))). [para(18(a,1),5(a,1,2))]. 40 ((x v (y v (z v u))')' v (z v (x v (y v u)))')' = x. [para(18(a,1),9(a,1,1,2,1))]. 41 ((x v (y v (z v u))')' v (y v (z v (x v u)))')' = x. [para(18(a,2),9(a,1,1,2,1))]. 42 x v (y v (z v (u v x'))) = y v (z v (u v c_0)). [para(23(a,1),18(a,1,2,2)),flip(a)]. 43 (c_0' v (x v (y v ((y v (x v z)) v z)))')' = y v (x v z). [para(18(a,1),24(a,1,1,2,1)),rewrite(5(6))]. 56 (c_0' v (x' v x')') v c_0 = x v c_0. [para(34(a,1),23(a,1,2)),flip(a)]. 65 (x v ((x v x'')' v c_0)')' = (x v x'')'. [para(25(a,1),9(a,1,1,1))]. 68 ((x v x'')' v c_0') v x = c_0. [para(25(a,1),17(a,1,2))]. 72 (x v (x v (c_0' v x))')' = c_0'. [para(5(a,1),32(a,1,1,2,1))]. 74 (c_0' v (x v (c_0' v (x v x)))')' = x. [para(32(a,1),9(a,1,1,1))]. 76 (x v (c_0' v (x v x))') v c_0' = c_0. [para(32(a,1),17(a,1,2))]. 126 (c_0' v (x v (x v (c_0' v x)))')' = x. [para(72(a,1),9(a,1,1,1))]. 144 ((c_0' v (x v x)'')' v x) v c_0' = c_0. [para(24(a,1),26(a,1,1,2))]. 169 (c_0' v (x v (x v (c_0' v x)))') v x = c_0. [para(72(a,1),26(a,1,1,1))]. 183 (c_0' v ((x v (c_0' v (x v x))') v c_0)')' = x v (c_0' v (x v x))'. [para(76(a,1),9(a,1,1,1,1))]. 184 (x v (c_0' v (x v x))') v c_0 = c_0 v c_0. [para(76(a,1),23(a,1,2)),flip(a)]. 193 x v (c_0' v (x v x))' = c_0. [back_rewrite(183),rewrite(184(10),24(8)),flip(a)]. 251 x v (y v (c_0' v (x v x))') = y v c_0. [para(193(a,1),5(a,1,2)),flip(a)]. 254 (c_0' v (x v x)) v c_0 = x v c_0. [para(193(a,1),23(a,1,2))]. 255 c_0'' v (c_0'' v c_0)' = c_0. [para(23(a,1),193(a,1,2,1))]. 280 (c_0'' v c_0) v c_0 = c_0'' v c_0. [para(23(a,1),254(a,1,1))]. 294 (c_0' v (c_0'' v (c_0'' v c_0))')' = c_0''. [para(255(a,1),9(a,1,1,1,1))]. 300 (c_0'' v c_0) v (x v c_0) = x v (c_0'' v c_0). [para(255(a,1),27(a,1,2,2))]. 540 ((c_0' v (x v x)'')' v x) v c_0 = c_0 v c_0. [para(33(a,1),56(a,1,1,2,1,1)),rewrite(33(13),56(11)),flip(a)]. 545 (c_0' v ((x v y) v (c_0' v (x v ((x v y) v y))))')' = x v y. [para(5(a,1),74(a,1,1,2,1,2,2))]. 676 (c_0' v (x v x)) v (y v c_0) = x v (y v c_0). [para(251(a,1),27(a,1,2))]. 812 (c_0' v c_0''')' v c_0' = (c_0' v c_0''')'. [para(68(a,1),30(a,1,1,2,1,2)),rewrite(65(15)),flip(a)]. 821 c_0'' v c_0 = c_0''. [para(280(a,1),30(a,1,1,2,1,2,1)),rewrite(280(14),5(13),280(12),294(14),280(10)),flip(a)]. 851 c_0'' v (x v c_0) = x v c_0''. [back_rewrite(300),rewrite(821(5),821(11))]. 853 (c_0' v (c_0 v c_0)') v c_0'' = c_0''. [para(821(a,1),35(a,1,2)),rewrite(821(16))]. 858 c_0' v (c_0'' v (x v c_0)) = x v c_0. [para(851(a,2),23(a,1,2))]. 907 c_0'' v (x v (c_0' v c_0)) = x v c_0. [para(858(a,1),18(a,2))]. 995 (c_0' v (c_0' v ((c_0' v c_0) v c_0))') v c_0 = c_0''. [para(34(a,1),907(a,1,2)),rewrite(821(5),5(14)),flip(a)]. 1002 x v ((c_0' v (x v (c_0' v ((x v (c_0' v c_0)) v c_0)))') v c_0) = c_0''. [para(907(a,1),35(a,1,2)),rewrite(5(13),5(12),5(18),821(23))]. 1019 (c_0' v c_0''')'' = c_0'. [para(853(a,1),28(a,1,1,1,1,2,1)),rewrite(34(17),812(11))]. 1024 (c_0' v c_0''')' = c_0. [para(1019(a,1),17(a,1,2)),rewrite(812(11))]. 1029 ((c_0' v c_0'''')' v c_0)' = c_0'. [para(1024(a,1),9(a,1,1,2))]. 1224 ((((c_0' v c_0'''')' v c_0) v c_0'')' v c_0')' = (c_0' v c_0'''')' v c_0. [para(1029(a,1),25(a,1,1,1,1,2,1))]. 1447 (c_0' v (x v x)'')' v x = c_0. [para(144(a,1),9(a,1,1,1,1)),rewrite(540(12),24(8)),flip(a)]. 1462 (c_0' v (x v x)'')' v (y v x) = y v c_0. [para(1447(a,1),5(a,1,2)),flip(a)]. 1519 ((x v (y v (z v (u v x')))')' v (z v (y v (u v c_0)))')' = x. [para(27(a,1),40(a,1,1,2,1,2))]. 1822 ((x v (y v c_0)')' v (y v ((c_0' v (z v z)'')' v (x v z)))')' = x. [para(1447(a,1),41(a,1,1,1,1,2,1,2))]. 1916 c_0 v (c_0' v c_0) = c_0. [para(676(a,1),30(a,1,1,2,1,2)),rewrite(5(10),5(9),126(13),5(7)),flip(a)]. 1943 c_0 v (c_0' v (x v c_0)) = x v c_0. [para(1916(a,1),18(a,2,2))]. 1948 c_0'' = c_0 v c_0. [para(1916(a,1),35(a,1,2)),rewrite(5(11),995(15))]. 2028 ((c_0 v (c_0 v c_0))' v c_0')' = c_0. [back_rewrite(1224),rewrite(1948(5),1447(11),1948(4),1948(15),1447(21))]. 2067 x v ((c_0' v (x v (c_0' v ((x v (c_0' v c_0)) v c_0)))') v c_0) = c_0 v c_0. [back_rewrite(1002),rewrite(1948(21))]. 2074 (c_0' v (c_0' v ((c_0' v c_0) v c_0))') v c_0 = c_0 v c_0. [back_rewrite(995),rewrite(1948(18))]. 2096 (c_0 v c_0) v (x v (c_0' v c_0)) = x v c_0. [back_rewrite(907),rewrite(1948(3))]. 2204 (((x v (y v (z v (u v x')))')' v (y v (z v (u v c_0)))'')' v x)' = (x v (y v (z v (u v x')))')'. [para(42(a,1),22(a,1,1,1,1,2,1,1))]. 2316 c_0' v (x v ((x v c_0) v c_0)) = x v c_0. [para(676(a,1),43(a,1,1,2,1,2,2)),rewrite(5(11),545(16),5(9)),flip(a)]. 2318 (c_0' v (c_0 v (x v c_0))')' = x v c_0. [para(1943(a,1),43(a,1,1,2,1,2,2,1)),rewrite(5(10),5(12),2316(11),1943(16))]. 2742 x v ((x v c_0) v (c_0' v c_0)) = x v c_0. [para(2316(a,1),18(a,2))]. 2759 x v (y v ((x v c_0) v (c_0' v c_0))) = y v (x v c_0). [para(2316(a,1),36(a,1,2)),flip(a)]. 2767 x v ((x v c_0) v ((c_0' v (x v ((x v ((x v c_0) v c_0)) v ((x v ((x v c_0) v c_0)) v c_0)))') v c_0)) = c_0. [para(2316(a,1),169(a,1,1,2,1,2,2)),rewrite(5(15),5(16),5(24),5(23))]. 2793 (c_0' v (x v ((x v c_0) v c_0))') v c_0 = (c_0' v (c_0 v (x v c_0))') v c_0. [para(2318(a,1),56(a,1,1,2,1,1)),rewrite(2318(13),5(7))]. 2795 ((x v ((c_0 v (x v c_0)) v c_0))' v (c_0' v c_0)')' = c_0 v (x v c_0). [para(2318(a,1),28(a,1,1,1,1,2)),rewrite(5(7))]. 2800 (c_0' v c_0')' = c_0' v c_0. [para(1916(a,1),2318(a,1,1,2,1))]. 2803 (c_0' v c_0') v c_0 = c_0 v c_0. [back_rewrite(2074),rewrite(2793(15),1916(8))]. 2840 (c_0' v (c_0' v c_0))' = c_0'. [para(2800(a,1),9(a,1,1,2)),rewrite(1948(5),5(6),1916(6))]. 2854 (c_0' v (c_0' v c_0)) v c_0 = c_0 v c_0. [para(2800(a,1),56(a,1,1,2))]. 3052 c_0' v (c_0' v c_0) = c_0. [para(2840(a,1),25(a,1,1,1,1,2,1)),rewrite(1948(10),5(11),2854(10),2028(10)),flip(a)]. 3057 c_0' v (x v (c_0' v c_0)) = x v c_0. [para(3052(a,1),5(a,1,2)),flip(a)]. 3063 c_0' v c_0 = c_0 v c_0. [para(3052(a,1),35(a,1,2)),rewrite(5(11),2793(15),1916(8),2803(7)),flip(a)]. 3064 c_0 v (c_0 v c_0) = c_0. [para(35(a,2),3052(a,1,2)),rewrite(5(11),34(10),3063(6),5(6),3063(5))]. 3065 c_0 v c_0 = c_0. [para(3052(a,1),22(a,1,1,1,1,2,1,1)),rewrite(3063(6),24(8),1948(4),3064(5),2800(6),3063(4),3063(9),24(11))]. 3076 c_0' v (x v c_0) = x v c_0. [back_rewrite(3057),rewrite(3063(6),3065(5))]. 3101 ((x v ((c_0 v (x v c_0)) v c_0))' v c_0')' = c_0 v (x v c_0). [back_rewrite(2795),rewrite(3063(12),3065(11))]. 3104 x v (y v ((x v c_0) v c_0)) = y v (x v c_0). [back_rewrite(2759),rewrite(3063(6),3065(5))]. 3106 x v ((x v c_0) v c_0) = x v c_0. [back_rewrite(2742),rewrite(3063(6),3065(5))]. 3120 c_0 v (x v c_0) = x v c_0. [back_rewrite(2096),rewrite(3065(3),3063(5),3065(4))]. 3125 x v ((c_0' v (x v c_0)') v c_0) = c_0. [back_rewrite(2067),rewrite(3063(8),3065(7),3076(9),3106(7),3065(12))]. 3177 c_0'' = c_0. [back_rewrite(1948),rewrite(3065(6))]. 3191 x v ((x v c_0) v ((c_0' v (x v c_0)') v c_0)) = c_0. [back_rewrite(2767),rewrite(3106(9),3106(11),3104(12),5(9),3106(9))]. 3193 ((x v c_0)' v c_0')' = x v c_0. [back_rewrite(3101),rewrite(3120(4),3106(5),3120(11))]. 3877 ((x v (y v c_0))' v ((y v c_0)' v (x v c_0'))')' = x. [para(3193(a,1),19(a,1,1,1,1,2))]. 3887 ((x v c_0)' v ((x v c_0) v ((x v c_0)' v c_0))')' = x v c_0. [para(3193(a,1),21(a,1,1,2,1,2,1)),rewrite(5(11),3193(21))]. 3895 ((x v c_0)' v ((x v c_0)' v c_0)')' = c_0. [para(3193(a,1),28(a,1,1,1,1,2)),rewrite(3120(4))]. 3924 x v (y v ((c_0' v (x v c_0)') v c_0)) = y v c_0. [para(3125(a,1),5(a,1,2)),flip(a)]. 3935 (((x v ((c_0' v (x v c_0)') v c_0)')' v c_0)' v x)' = (x v ((c_0' v (x v c_0)') v c_0)')'. [para(3125(a,1),22(a,1,1,1,1,2,1,1)),rewrite(3177(14))]. 3948 (x v c_0) v c_0 = c_0. [back_rewrite(3191),rewrite(3924(12))]. 4065 (x v c_0) v (y v c_0) = y v c_0. [para(3948(a,1),5(a,1,2)),flip(a)]. 4082 x v c_0 = c_0. [back_rewrite(3887),rewrite(4065(11),3895(11)),flip(a)]. 4114 (c_0' v x)' = (x v c_0')'. [back_rewrite(3935),rewrite(4082(4),4082(7),4082(6),4082(8),4082(11))]. 4127 (c_0' v (c_0' v (x v c_0'))')' = x. [back_rewrite(3877),rewrite(4082(2),4082(2),4082(4))]. 4381 (x v (y v (z v (u v x')))')' = (c_0' v x)'. [back_rewrite(2204),rewrite(4082(9),4082(9),4082(9),3177(10),4082(9)),flip(a)]. 4420 ((x v c_0')' v (y v ((c_0' v (z v z)'')' v (x v z)))')' = x. [back_rewrite(1822),rewrite(4082(2))]. 4488 (c_0' v (c_0' v x)')' = x. [back_rewrite(1519),rewrite(4381(7),4082(6),4082(6),4082(6),4114(8,R))]. 4507 (c_0' v (x v x)'')' v (y v x) = c_0. [back_rewrite(1462),rewrite(4082(11))]. 4833 x v c_0' = x. [back_rewrite(4127),rewrite(4488(11))]. 4856 x'' = x. [back_rewrite(4420),rewrite(4833(3),4507(10),4082(3),4833(4))]. 4857 $F # answer(CC). [resolve(4856,a,10,a)]. ============================== end of proof ========================== % Redundant proof: 5145 $F # answer(CC). [back_rewrite(10),rewrite(4856(3)),xx(a)]. ============================== PROOF ================================= % Proof 2 at 1.11 (+ 0.01) seconds: B1. % Length of proof is 141. % Level of proof is 34. % Maximum clause weight is 86. % Given clauses 112. 2 x v (x ^ y) = x # answer(B1). [goal]. 5 x v (y v z) = y v (x v z) # label(AJ). [assumption]. 6 x ^ y = (x' v y')' # label(DM). [assumption]. 7 x v x' = y v y' # label(ONE). [assumption]. 8 (x v y') ^ (x v y) = x # label(CUT). [assumption]. 9 ((x v y')' v (x v y)')' = x. [copy(8),rewrite(6(4))]. 11 c2 v (c2 ^ c3) != c2 # answer(B1). [deny(2)]. 12 c2 v (c2' v c3')' != c2 # answer(B1). [copy(11),rewrite(6(4))]. 17 x v x' = c_0. [new_symbol(7)]. 18 x v (y v (z v u)) = z v (x v (y v u)). [para(5(a,1),5(a,1,2))]. 19 ((x v (y v z)')' v (y v (x v z))')' = x. [para(5(a,1),9(a,1,1,2,1))]. 20 ((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))]. 21 (x v (x v ((x v y')' v y))')' = (x v y')'. [para(9(a,1),9(a,1,1,1)),rewrite(5(5))]. 22 (((x v y')' v (x v y)'')' v x)' = (x v y')'. [para(9(a,1),9(a,1,1,2))]. 23 x v (y v x') = y v c_0. [para(17(a,1),5(a,1,2)),flip(a)]. 24 (c_0' v (x v x)')' = x. [para(17(a,1),9(a,1,1,1,1))]. 25 ((x v x'')' v c_0')' = x. [para(17(a,1),9(a,1,1,2,1))]. 26 ((x v y')' v (x v y)') v x = c_0. [para(9(a,1),17(a,1,2))]. 27 x v (y v (z v x')) = y v (z v c_0). [para(23(a,1),5(a,1,2)),flip(a)]. 28 ((x v (y v x')')' v (y v c_0)')' = x. [para(23(a,1),9(a,1,1,2,1))]. 30 (c_0' v (x v ((x v y) v y))')' = x v y. [para(5(a,1),24(a,1,1,2,1))]. 31 ((x v y)' v (x v (c_0' v (y v y)'))')' = x. [para(24(a,1),9(a,1,1,1,1,2))]. 32 (x v (c_0' v (x v x))')' = c_0'. [para(24(a,1),9(a,1,1,1))]. 33 ((c_0' v (x v x)'')' v x)' = c_0'. [para(24(a,1),9(a,1,1,2))]. 34 (c_0' v (x v x)') v x = c_0. [para(24(a,1),17(a,1,2))]. 35 (c_0' v (x v x)') v (y v x) = y v c_0. [para(24(a,1),23(a,1,2,2))]. 36 x v (y v (z v (u v v))) = z v (x v (u v (y v v))). [para(18(a,1),5(a,1,2))]. 40 ((x v (y v (z v u))')' v (z v (x v (y v u)))')' = x. [para(18(a,1),9(a,1,1,2,1))]. 41 ((x v (y v (z v u))')' v (y v (z v (x v u)))')' = x. [para(18(a,2),9(a,1,1,2,1))]. 42 x v (y v (z v (u v x'))) = y v (z v (u v c_0)). [para(23(a,1),18(a,1,2,2)),flip(a)]. 43 (c_0' v (x v (y v ((y v (x v z)) v z)))')' = y v (x v z). [para(18(a,1),24(a,1,1,2,1)),rewrite(5(6))]. 56 (c_0' v (x' v x')') v c_0 = x v c_0. [para(34(a,1),23(a,1,2)),flip(a)]. 65 (x v ((x v x'')' v c_0)')' = (x v x'')'. [para(25(a,1),9(a,1,1,1))]. 66 (((x v x'')' v c_0'')' v x)' = (x v x'')'. [para(25(a,1),9(a,1,1,2))]. 68 ((x v x'')' v c_0') v x = c_0. [para(25(a,1),17(a,1,2))]. 72 (x v (x v (c_0' v x))')' = c_0'. [para(5(a,1),32(a,1,1,2,1))]. 74 (c_0' v (x v (c_0' v (x v x)))')' = x. [para(32(a,1),9(a,1,1,1))]. 76 (x v (c_0' v (x v x))') v c_0' = c_0. [para(32(a,1),17(a,1,2))]. 85 (c_0' v (((x' v x''')' v c_0') v x)')' = (x' v x''')' v c_0'. [para(68(a,1),9(a,1,1,1,1))]. 118 (c_0' v (c_0' v (x v (x v x)))')' = x. [para(32(a,1),19(a,1,1,1))]. 126 (c_0' v (x v (x v (c_0' v x)))')' = x. [para(72(a,1),9(a,1,1,1))]. 144 ((c_0' v (x v x)'')' v x) v c_0' = c_0. [para(24(a,1),26(a,1,1,2))]. 158 (c_0' v (x v (c_0' v (x v x)))') v x = c_0. [para(32(a,1),26(a,1,1,1))]. 169 (c_0' v (x v (x v (c_0' v x)))') v x = c_0. [para(72(a,1),26(a,1,1,1))]. 183 (c_0' v ((x v (c_0' v (x v x))') v c_0)')' = x v (c_0' v (x v x))'. [para(76(a,1),9(a,1,1,1,1))]. 184 (x v (c_0' v (x v x))') v c_0 = c_0 v c_0. [para(76(a,1),23(a,1,2)),flip(a)]. 193 x v (c_0' v (x v x))' = c_0. [back_rewrite(183),rewrite(184(10),24(8)),flip(a)]. 251 x v (y v (c_0' v (x v x))') = y v c_0. [para(193(a,1),5(a,1,2)),flip(a)]. 254 (c_0' v (x v x)) v c_0 = x v c_0. [para(193(a,1),23(a,1,2))]. 255 c_0'' v (c_0'' v c_0)' = c_0. [para(23(a,1),193(a,1,2,1))]. 280 (c_0'' v c_0) v c_0 = c_0'' v c_0. [para(23(a,1),254(a,1,1))]. 294 (c_0' v (c_0'' v (c_0'' v c_0))')' = c_0''. [para(255(a,1),9(a,1,1,1,1))]. 300 (c_0'' v c_0) v (x v c_0) = x v (c_0'' v c_0). [para(255(a,1),27(a,1,2,2))]. 480 (((x v c_0')' v ((c_0' v (y v y)') v (x v y))'')' v x)' = (x v c_0')'. [para(35(a,2),22(a,1,1,1,1,2,1,1))]. 540 ((c_0' v (x v x)'')' v x) v c_0 = c_0 v c_0. [para(33(a,1),56(a,1,1,2,1,1)),rewrite(33(13),56(11)),flip(a)]. 545 (c_0' v ((x v y) v (c_0' v (x v ((x v y) v y))))')' = x v y. [para(5(a,1),74(a,1,1,2,1,2,2))]. 606 ((x v (x' v y')')' v (((x' v y')' v (x' v y)'')' v c_0)')' = x. [para(22(a,1),28(a,1,1,1,1,2))]. 614 (c_0' v (c_0' v (x v ((x v y) v ((x v y) v y))))')' = x v y. [para(5(a,1),118(a,1,1,2,1,2,2)),rewrite(5(9))]. 676 (c_0' v (x v x)) v (y v c_0) = x v (y v c_0). [para(251(a,1),27(a,1,2))]. 812 (c_0' v c_0''')' v c_0' = (c_0' v c_0''')'. [para(68(a,1),30(a,1,1,2,1,2)),rewrite(65(15)),flip(a)]. 821 c_0'' v c_0 = c_0''. [para(280(a,1),30(a,1,1,2,1,2,1)),rewrite(280(14),5(13),280(12),294(14),280(10)),flip(a)]. 851 c_0'' v (x v c_0) = x v c_0''. [back_rewrite(300),rewrite(821(5),821(11))]. 853 (c_0' v (c_0 v c_0)') v c_0'' = c_0''. [para(821(a,1),35(a,1,2)),rewrite(821(16))]. 858 c_0' v (c_0'' v (x v c_0)) = x v c_0. [para(851(a,2),23(a,1,2))]. 907 c_0'' v (x v (c_0' v c_0)) = x v c_0. [para(858(a,1),18(a,2))]. 995 (c_0' v (c_0' v ((c_0' v c_0) v c_0))') v c_0 = c_0''. [para(34(a,1),907(a,1,2)),rewrite(821(5),5(14)),flip(a)]. 1002 x v ((c_0' v (x v (c_0' v ((x v (c_0' v c_0)) v c_0)))') v c_0) = c_0''. [para(907(a,1),35(a,1,2)),rewrite(5(13),5(12),5(18),821(23))]. 1019 (c_0' v c_0''')'' = c_0'. [para(853(a,1),28(a,1,1,1,1,2,1)),rewrite(34(17),812(11))]. 1024 (c_0' v c_0''')' = c_0. [para(1019(a,1),17(a,1,2)),rewrite(812(11))]. 1029 ((c_0' v c_0'''')' v c_0)' = c_0'. [para(1024(a,1),9(a,1,1,2))]. 1224 ((((c_0' v c_0'''')' v c_0) v c_0'')' v c_0')' = (c_0' v c_0'''')' v c_0. [para(1029(a,1),25(a,1,1,1,1,2,1))]. 1447 (c_0' v (x v x)'')' v x = c_0. [para(144(a,1),9(a,1,1,1,1)),rewrite(540(12),24(8)),flip(a)]. 1462 (c_0' v (x v x)'')' v (y v x) = y v c_0. [para(1447(a,1),5(a,1,2)),flip(a)]. 1519 ((x v (y v (z v (u v x')))')' v (z v (y v (u v c_0)))')' = x. [para(27(a,1),40(a,1,1,2,1,2))]. 1642 (((c_0' v (c_0' v ((x v y')' v (((x v y')' v (x v y)') v (((x v y')' v (x v y)') v (x v y)'))))') v x)' v c_0')' = c_0' v (c_0' v ((x v y')' v (((x v y')' v (x v y)') v (((x v y')' v (x v y)') v (x v y)'))))'. [para(158(a,1),20(a,1,1,2,1)),rewrite(5(23),5(25),5(24),5(56),5(58),5(57))]. 1656 (((c_0' v (c_0' v (c_0' v ((c_0' v (x v x)') v ((c_0' v (x v x)') v (x v x)'))))') v x)' v c_0')' = c_0' v (c_0' v (c_0' v ((c_0' v (x v x)') v ((c_0' v (x v x)') v (x v x)'))))'. [para(158(a,1),31(a,1,1,2,1)),rewrite(5(20),5(22),5(21),5(50),5(52),5(51))]. 1822 ((x v (y v c_0)')' v (y v ((c_0' v (z v z)'')' v (x v z)))')' = x. [para(1447(a,1),41(a,1,1,1,1,2,1,2))]. 1916 c_0 v (c_0' v c_0) = c_0. [para(676(a,1),30(a,1,1,2,1,2)),rewrite(5(10),5(9),126(13),5(7)),flip(a)]. 1943 c_0 v (c_0' v (x v c_0)) = x v c_0. [para(1916(a,1),18(a,2,2))]. 1948 c_0'' = c_0 v c_0. [para(1916(a,1),35(a,1,2)),rewrite(5(11),995(15))]. 2028 ((c_0 v (c_0 v c_0))' v c_0')' = c_0. [back_rewrite(1224),rewrite(1948(5),1447(11),1948(4),1948(15),1447(21))]. 2067 x v ((c_0' v (x v (c_0' v ((x v (c_0' v c_0)) v c_0)))') v c_0) = c_0 v c_0. [back_rewrite(1002),rewrite(1948(21))]. 2074 (c_0' v (c_0' v ((c_0' v c_0) v c_0))') v c_0 = c_0 v c_0. [back_rewrite(995),rewrite(1948(18))]. 2096 (c_0 v c_0) v (x v (c_0' v c_0)) = x v c_0. [back_rewrite(907),rewrite(1948(3))]. 2158 ((c_0 v ((x v x'')' v c_0))' v x)' = (x v x'')'. [back_rewrite(66),rewrite(1948(7),5(8))]. 2204 (((x v (y v (z v (u v x')))')' v (y v (z v (u v c_0)))'')' v x)' = (x v (y v (z v (u v x')))')'. [para(42(a,1),22(a,1,1,1,1,2,1,1))]. 2316 c_0' v (x v ((x v c_0) v c_0)) = x v c_0. [para(676(a,1),43(a,1,1,2,1,2,2)),rewrite(5(11),545(16),5(9)),flip(a)]. 2318 (c_0' v (c_0 v (x v c_0))')' = x v c_0. [para(1943(a,1),43(a,1,1,2,1,2,2,1)),rewrite(5(10),5(12),2316(11),1943(16))]. 2742 x v ((x v c_0) v (c_0' v c_0)) = x v c_0. [para(2316(a,1),18(a,2))]. 2759 x v (y v ((x v c_0) v (c_0' v c_0))) = y v (x v c_0). [para(2316(a,1),36(a,1,2)),flip(a)]. 2767 x v ((x v c_0) v ((c_0' v (x v ((x v ((x v c_0) v c_0)) v ((x v ((x v c_0) v c_0)) v c_0)))') v c_0)) = c_0. [para(2316(a,1),169(a,1,1,2,1,2,2)),rewrite(5(15),5(16),5(24),5(23))]. 2793 (c_0' v (x v ((x v c_0) v c_0))') v c_0 = (c_0' v (c_0 v (x v c_0))') v c_0. [para(2318(a,1),56(a,1,1,2,1,1)),rewrite(2318(13),5(7))]. 2795 ((x v ((c_0 v (x v c_0)) v c_0))' v (c_0' v c_0)')' = c_0 v (x v c_0). [para(2318(a,1),28(a,1,1,1,1,2)),rewrite(5(7))]. 2800 (c_0' v c_0')' = c_0' v c_0. [para(1916(a,1),2318(a,1,1,2,1))]. 2803 (c_0' v c_0') v c_0 = c_0 v c_0. [back_rewrite(2074),rewrite(2793(15),1916(8))]. 2840 (c_0' v (c_0' v c_0))' = c_0'. [para(2800(a,1),9(a,1,1,2)),rewrite(1948(5),5(6),1916(6))]. 2854 (c_0' v (c_0' v c_0)) v c_0 = c_0 v c_0. [para(2800(a,1),56(a,1,1,2))]. 3052 c_0' v (c_0' v c_0) = c_0. [para(2840(a,1),25(a,1,1,1,1,2,1)),rewrite(1948(10),5(11),2854(10),2028(10)),flip(a)]. 3057 c_0' v (x v (c_0' v c_0)) = x v c_0. [para(3052(a,1),5(a,1,2)),flip(a)]. 3063 c_0' v c_0 = c_0 v c_0. [para(3052(a,1),35(a,1,2)),rewrite(5(11),2793(15),1916(8),2803(7)),flip(a)]. 3064 c_0 v (c_0 v c_0) = c_0. [para(35(a,2),3052(a,1,2)),rewrite(5(11),34(10),3063(6),5(6),3063(5))]. 3065 c_0 v c_0 = c_0. [para(3052(a,1),22(a,1,1,1,1,2,1,1)),rewrite(3063(6),24(8),1948(4),3064(5),2800(6),3063(4),3063(9),24(11))]. 3076 c_0' v (x v c_0) = x v c_0. [back_rewrite(3057),rewrite(3063(6),3065(5))]. 3101 ((x v ((c_0 v (x v c_0)) v c_0))' v c_0')' = c_0 v (x v c_0). [back_rewrite(2795),rewrite(3063(12),3065(11))]. 3104 x v (y v ((x v c_0) v c_0)) = y v (x v c_0). [back_rewrite(2759),rewrite(3063(6),3065(5))]. 3106 x v ((x v c_0) v c_0) = x v c_0. [back_rewrite(2742),rewrite(3063(6),3065(5))]. 3120 c_0 v (x v c_0) = x v c_0. [back_rewrite(2096),rewrite(3065(3),3063(5),3065(4))]. 3125 x v ((c_0' v (x v c_0)') v c_0) = c_0. [back_rewrite(2067),rewrite(3063(8),3065(7),3076(9),3106(7),3065(12))]. 3177 c_0'' = c_0. [back_rewrite(1948),rewrite(3065(6))]. 3191 x v ((x v c_0) v ((c_0' v (x v c_0)') v c_0)) = c_0. [back_rewrite(2767),rewrite(3106(9),3106(11),3104(12),5(9),3106(9))]. 3193 ((x v c_0)' v c_0')' = x v c_0. [back_rewrite(3101),rewrite(3120(4),3106(5),3120(11))]. 3215 (((x v x'')' v c_0)' v x)' = (x v x'')'. [back_rewrite(2158),rewrite(3120(8))]. 3877 ((x v (y v c_0))' v ((y v c_0)' v (x v c_0'))')' = x. [para(3193(a,1),19(a,1,1,1,1,2))]. 3887 ((x v c_0)' v ((x v c_0) v ((x v c_0)' v c_0))')' = x v c_0. [para(3193(a,1),21(a,1,1,2,1,2,1)),rewrite(5(11),3193(21))]. 3895 ((x v c_0)' v ((x v c_0)' v c_0)')' = c_0. [para(3193(a,1),28(a,1,1,1,1,2)),rewrite(3120(4))]. 3924 x v (y v ((c_0' v (x v c_0)') v c_0)) = y v c_0. [para(3125(a,1),5(a,1,2)),flip(a)]. 3935 (((x v ((c_0' v (x v c_0)') v c_0)')' v c_0)' v x)' = (x v ((c_0' v (x v c_0)') v c_0)')'. [para(3125(a,1),22(a,1,1,1,1,2,1,1)),rewrite(3177(14))]. 3948 (x v c_0) v c_0 = c_0. [back_rewrite(3191),rewrite(3924(12))]. 4065 (x v c_0) v (y v c_0) = y v c_0. [para(3948(a,1),5(a,1,2)),flip(a)]. 4082 x v c_0 = c_0. [back_rewrite(3887),rewrite(4065(11),3895(11)),flip(a)]. 4114 (c_0' v x)' = (x v c_0')'. [back_rewrite(3935),rewrite(4082(4),4082(7),4082(6),4082(8),4082(11))]. 4127 (c_0' v (c_0' v (x v c_0'))')' = x. [back_rewrite(3877),rewrite(4082(2),4082(2),4082(4))]. 4279 (x v x'')' = (c_0' v x)'. [back_rewrite(3215),rewrite(4082(6)),flip(a)]. 4381 (x v (y v (z v (u v x')))')' = (c_0' v x)'. [back_rewrite(2204),rewrite(4082(9),4082(9),4082(9),3177(10),4082(9)),flip(a)]. 4420 ((x v c_0')' v (y v ((c_0' v (z v z)'')' v (x v z)))')' = x. [back_rewrite(1822),rewrite(4082(2))]. 4488 (c_0' v (c_0' v x)')' = x. [back_rewrite(1519),rewrite(4381(7),4082(6),4082(6),4082(6),4114(8,R))]. 4507 (c_0' v (x v x)'')' v (y v x) = c_0. [back_rewrite(1462),rewrite(4082(11))]. 4655 (c_0' v (x v (x' v y')')')' = x. [back_rewrite(606),rewrite(4082(18),4114(10,R))]. 4724 (c_0' v (x v x)') v (y v x) = c_0. [back_rewrite(35),rewrite(4082(9))]. 4750 (c_0' v ((c_0' v (c_0' v (c_0' v ((c_0' v (x v x)') v ((c_0' v (x v x)') v (x v x)'))))') v x)')' = c_0' v (c_0' v (c_0' v ((c_0' v (x v x)') v ((c_0' v (x v x)') v (x v x)'))))'. [back_rewrite(1656),rewrite(4114(30,R))]. 4751 (c_0' v ((c_0' v (c_0' v ((x v y')' v (((x v y')' v (x v y)') v (((x v y')' v (x v y)') v (x v y)'))))') v x)')' = c_0' v (c_0' v ((x v y')' v (((x v y')' v (x v y)') v (((x v y')' v (x v y)') v (x v y)'))))'. [back_rewrite(1642),rewrite(4114(33,R))]. 4830 (c_0' v (((c_0' v x')' v c_0') v x)')' = (c_0' v x')' v c_0'. [back_rewrite(85),rewrite(4279(8),4279(20))]. 4833 x v c_0' = x. [back_rewrite(4127),rewrite(4488(11))]. 4853 x v ((x v y) v ((x v y) v y)) = x v y. [back_rewrite(614),rewrite(4488(13))]. 4856 x'' = x. [back_rewrite(4420),rewrite(4833(3),4507(10),4082(3),4833(4))]. 4884 (c_0' v x)' = x'. [back_rewrite(480),rewrite(4833(3),4724(8),4856(4),4082(3),4833(7))]. 4892 x v x = x. [back_rewrite(4830),rewrite(4884(7),4856(4),4833(5),4884(6),4856(3),4884(6),4856(3),4833(4))]. 5007 (c_0' v x) v x = c_0' v x. [back_rewrite(4751),rewrite(4853(26),4884(14),9(11),4884(9),4856(6),4853(28),4884(16),9(13))]. 5008 c_0' v x = x. [back_rewrite(4750),rewrite(4892(11),4892(15),4892(17),5007(18),4892(17),4884(15),4884(12),4884(9),4856(6),5007(6),4884(6),4884(5),4856(2),4892(9),4892(13),4892(15),5007(16),4892(15),4884(13),4884(10),4884(7),4856(4)),flip(a)]. 5164 x v (x' v y')' = x. [back_rewrite(4655),rewrite(5008(9),4856(7))]. 5165 $F # answer(B1). [resolve(5164,a,12,a)]. ============================== end of proof ========================== % Redundant proof: 5360 $F # answer(B1). [back_rewrite(12),rewrite(5164(8)),xx(a)]. % Disable descendants: 11x 12x 10x given #113 (F,wt=5): 4082 x v c_0 = c_0. [back_rewrite(3887),rewrite(4065(11),3895(11)),flip(a)]. given #114 (T,wt=5): 4856 x'' = x. [back_rewrite(4420),rewrite(4833(3),4507(10),4082(3),4833(4))]. given #115 (T,wt=5): 4892 x v x = x. [back_rewrite(4830),rewrite(4884(7),4856(4),4833(5),4884(6),4856(3),4884(6),4856(3),4833(4))]. given #116 (A,wt=23): 51 x v (y v (z v (u v (v v w)))) = z v (x v (u v (v v (y v w)))). [para(18(a,2),18(a,2,2,2))]. given #117 (F,wt=5): 4938 c_0 v x = c_0. [back_rewrite(4588),rewrite(4892(5),4884(8),253(6),4833(4))]. given #118 (F,wt=6): 4833 x v c_0' = x. [back_rewrite(4127),rewrite(4488(11))]. % Operation v is commutative; C redundancy checks enabled. given #119 (T,wt=6): 5008 c_0' v x = x. [back_rewrite(4750),rewrite(4892(11),4892(15),4892(17),5007(18),4892(17),4884(15),4884(12),4884(9),4856(6),5007(6),4884(6),4884(5),4856(2),4892(9),4892(13),4892(15),5007(16),4892(15),4884(13),4884(10),4884(7),4856(4)),flip(a)]. given #120 (T,wt=7): 5510 x v y = y v x. [para(4833(a,1),5(a,1,2)),rewrite(4833(4))]. given #121 (A,wt=19): 52 x v (y v (z v (u v v))) = u v (y v (x v (z v v))). [para(18(a,2),18(a,2,2)),flip(a)]. given #122 (F,wt=8): 4727 x v (y v x') = c_0. [back_rewrite(23),rewrite(4082(5))]. given #123 (F,wt=8): 5658 x v (x' v y) = c_0. [back_rewrite(5017),rewrite(5510(9),5369(9),5510(8),5534(8),5510(10),5363(10),5511(3))]. given #124 (T,wt=9): 5369 x v (y v x')' = x. [back_rewrite(5156),rewrite(5361(10))]. given #125 (T,wt=9): 5382 x v (y v x) = y v x. [para(4892(a,1),5(a,1,2)),flip(a)]. given #126 (A,wt=25): 105 ((x v (y v (z v (u v v)))')' v (z v (x v (u v (y v v))))')' = x. [para(18(a,1),19(a,1,1,1,1,2,1))]. given #127 (F,wt=9): 5589 x v (x v y) = x v y. [back_rewrite(5157),rewrite(5510(2))]. given #128 (F,wt=9): 5964 x v (x' v y)' = x. [para(5510(a,1),5369(a,1,2,1))]. given #129 (T,wt=10): 4726 x v (y v (z v x')) = c_0. [back_rewrite(27),rewrite(4082(6),4082(6))]. given #130 (T,wt=10): 4932 x' v (y v x)' = x'. [back_rewrite(4717),rewrite(4884(6),4833(6),4884(9),4856(6),4884(8),4833(8))]. given #131 (A,wt=25): 106 ((x v (y v (z v (u v v)))')' v (y v (u v (x v (z v v))))')' = x. [para(18(a,1),19(a,1,1,2,1,2))]. given #132 (F,wt=8): 6152 (x v y) v y' = c_0. [para(4932(a,1),4727(a,1,2))]. given #133 (F,wt=8): 6275 (x v y) v x' = c_0. [para(5510(a,1),6152(a,1,1))]. given #134 (T,wt=10): 4933 x' v (y v (z v x)) = c_0. [back_rewrite(4681),rewrite(4884(4),4833(4))]. given #135 (T,wt=10): 5688 x v (y v (x v y)') = c_0. [back_rewrite(4891),rewrite(5510(3))]. given #136 (A,wt=21): 107 ((x v (y v (z v u))')' v (z v (y v (x v u)))')' = x. [para(18(a,1),19(a,1,1,2,1))]. given #137 (F,wt=10): 5953 x v (y v (x' v z)) = c_0. [para(5658(a,1),5(a,1,2)),rewrite(4082(2)),flip(a)]. given #138 (F,wt=10): 5955 x' v (y v (x v z)) = c_0. [para(5658(a,1),18(a,1,2)),rewrite(4082(2)),flip(a)]. given #139 (T,wt=10): 6123 x' v (x v y)' = x'. [para(4856(a,1),5964(a,1,2,1,1))]. given #140 (T,wt=10): 6124 x v ((y v x') v z) = c_0. [para(5510(a,1),4726(a,1,2))]. given #141 (A,wt=25): 108 ((x v (y v (z v (u v v)))')' v (u v (x v (y v (z v v))))')' = x. [para(18(a,2),19(a,1,1,1,1,2,1))]. given #142 (F,wt=10): 6125 x v ((x' v y) v z) = c_0. [para(5964(a,1),4726(a,1,2,2)),rewrite(5511(4))]. given #143 (F,wt=10): 6153 (x v y) v (z v y') = c_0. [para(4932(a,1),4726(a,1,2,2))]. given #144 (T,wt=10): 6278 (x v y) v (z v x') = c_0. [para(6275(a,1),5(a,1,2)),rewrite(4082(2)),flip(a)]. given #145 (T,wt=10): 6279 (x v (y v z)) v y' = c_0. [para(5(a,1),6275(a,1,1))]. given #146 (A,wt=25): 109 ((x v (y v (z v (u v v)))')' v (y v (z v (u v (x v v))))')' = x. [para(18(a,2),19(a,1,1,2,1,2))]. given #147 (F,wt=10): 6315 (x v (y v z)) v z' = c_0. [para(4933(a,1),5510(a,1)),flip(a)]. given #148 (F,wt=10): 6316 x' v ((y v x) v z) = c_0. [para(5510(a,1),4933(a,1,2))]. given #149 (T,wt=10): 6414 x' v ((x v y) v z) = c_0. [para(5510(a,1),5955(a,1,2))]. given #150 (T,wt=10): 6429 (x v y) v (y' v z) = c_0. [para(4932(a,1),6124(a,1,2,1))]. given #151 (A,wt=25): 124 ((x v y)' v ((y v (z v u)')' v (x v (z v (y v u))'))')' = x. [para(19(a,1),19(a,1,1,1,1,2))]. given #152 (F,wt=10): 6430 (x v y) v (x' v z) = c_0. [para(6123(a,1),6124(a,1,2,1))]. given #153 (F,wt=10): 6546 ((x v y) v z) v y' = c_0. [para(4932(a,1),6278(a,1,2))]. given #154 (T,wt=10): 6547 ((x v y) v z) v x' = c_0. [para(6123(a,1),6278(a,1,2))]. given #155 (T,wt=11): 5368 x v (y v (z v x'))' = x. [back_rewrite(5158),rewrite(5361(12))]. given #156 (A,wt=23): 485 x v (y v (z v (u v (v v w)))) = v v (x v (y v (u v (z v w)))). [para(37(a,1),18(a,1,2,2))]. given #157 (F,wt=11): 5511 x v (y v z) = z v (x v y). [para(4833(a,1),18(a,1,2,2)),rewrite(4833(5))]. % Operation v is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 5511 x v (y v z) = z v (x v y). [para(4833(a,1),18(a,1,2,2)),rewrite(4833(5))]. % back CAC tautology: 485 x v (y v (z v (u v (v v w)))) = v v (x v (y v (u v (z v w)))). [para(37(a,1),18(a,1,2,2))]. % back CAC tautology: 52 x v (y v (z v (u v v))) = u v (y v (x v (z v v))). [para(18(a,2),18(a,2,2)),flip(a)]. % back CAC tautology: 51 x v (y v (z v (u v (v v w)))) = z v (x v (u v (v v (y v w)))). [para(18(a,2),18(a,2,2,2))]. % back CAC tautology: 50 x v (y v (z v (u v v))) = z v (u v (x v (y v v))). [para(18(a,1),18(a,2,2))]. % back CAC tautology: 49 x v (y v (z v (u v (v v w)))) = z v (x v (v v (y v (u v w)))). [para(18(a,1),18(a,2,2,2))]. % back CAC tautology: 48 x v (y v (z v (u v v))) = y v (x v (u v (z v v))). [para(18(a,2),18(a,1,2))]. % back CAC tautology: 47 x v (y v (z v (u v (v v w)))) = v v (x v (y v (z v (u v w)))). [para(18(a,2),18(a,1,2,2))]. % back CAC tautology: 46 x v (y v (z v (u v v))) = u v (x v (z v (y v v))). [para(18(a,1),18(a,1,2))]. % back CAC tautology: 45 x v (y v (z v (u v (v v w)))) = u v (x v (y v (v v (z v w)))). [para(18(a,1),18(a,1,2,2))]. % back CAC tautology: 38 x v (y v (z v (u v v))) = u v (x v (y v (z v v))). [para(18(a,2),5(a,1,2))]. % back CAC tautology: 36 x v (y v (z v (u v v))) = z v (x v (u v (y v v))). [para(18(a,1),5(a,1,2))]. % back CAC tautology: 39 x v (y v (z v u)) = x v (z v (y v u)). [para(18(a,2),5(a,1))]. % back CAC tautology: 37 x v (y v (z v u)) = z v (y v (x v u)). [para(18(a,1),5(a,1))]. % back CAC tautology: 18 x v (y v (z v u)) = z v (x v (y v u)). [para(5(a,1),5(a,1,2))]. % back CAC tautology: 7289 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (u v (v v (w v (v6 v y))))). [para(5511(a,2),51(a,2,2,2,2,2))]. % back CAC tautology: 7285 x v (y v (z v (u v (v v w)))) = z v (x v (u v (w v (v v y)))). [para(5511(a,1),51(a,2,2,2,2))]. % back CAC tautology: 7284 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (u v (v v (v6 v (y v w))))). [para(5511(a,1),51(a,2,2,2,2,2))]. % back CAC tautology: 7280 x v (y v (z v (u v (v v w)))) = z v (x v (w v (u v (y v v)))). [para(5511(a,2),51(a,1,2,2,2))]. % back CAC tautology: 7279 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (u v (v6 v (y v (v v w))))). [para(5511(a,2),51(a,1,2,2,2,2))]. % back CAC tautology: 7275 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (u v (w v (y v (v6 v v))))). [para(5511(a,1),51(a,1,2,2,2,2))]. % back CAC tautology: 7271 x v (y v (z v (u v v))) = v v (z v (x v (y v u))). [para(5511(a,2),50(a,1,2,2))]. % back CAC tautology: 7270 x v (y v (z v (u v (v v w)))) = z v (w v (x v (y v (u v v)))). [para(5511(a,2),50(a,1,2,2,2))]. % back CAC tautology: 7267 x v (y v (z v (u v v))) = u v (v v (x v (y v z))). [para(5511(a,1),50(a,1,2,2))]. % back CAC tautology: 7266 x v (y v (z v (u v (v v w)))) = z v (v v (x v (y v (w v u)))). [para(5511(a,1),50(a,1,2,2,2))]. % back CAC tautology: 7258 x v (y v (z v (u v (v v w)))) = z v (x v (v v (u v (w v y)))). [para(5511(a,2),49(a,2,2,2,2))]. % back CAC tautology: 7257 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (v v (y v (w v (v6 v u))))). [para(5511(a,2),49(a,2,2,2,2,2))]. % back CAC tautology: 7253 x v (y v (z v (u v (v v w)))) = z v (x v (v v (w v (y v u)))). [para(5511(a,1),49(a,2,2,2,2))]. % back CAC tautology: 7252 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (v v (y v (v6 v (u v w))))). [para(5511(a,1),49(a,2,2,2,2,2))]. % back CAC tautology: 7248 x v (y v (z v (u v (v v w)))) = z v (x v (u v (y v (w v v)))). [para(5511(a,2),49(a,1,2,2,2))]. % back CAC tautology: 7247 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (v6 v (y v (u v (v v w))))). [para(5511(a,2),49(a,1,2,2,2,2))]. % back CAC tautology: 7243 x v (y v (z v (u v (v v w)))) = z v (x v (w v (y v (v v u)))). [para(5511(a,1),49(a,1,2,2,2))]. % back CAC tautology: 7242 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (w v (y v (u v (v6 v v))))). [para(5511(a,1),49(a,1,2,2,2,2))]. % back CAC tautology: 7238 x v (y v (z v (u v v))) = y v (x v (z v (v v u))). [para(5511(a,2),48(a,1,2,2))]. % back CAC tautology: 7237 x v (y v (z v (u v (v v w)))) = y v (x v (w v (z v (u v v)))). [para(5511(a,2),48(a,1,2,2,2))]. % back CAC tautology: 7234 x v (y v (z v (u v v))) = y v (x v (v v (u v z))). [para(5511(a,1),48(a,1,2,2))]. % back CAC tautology: 7233 x v (y v (z v (u v (v v w)))) = y v (x v (v v (z v (w v u)))). [para(5511(a,1),48(a,1,2,2,2))]. % back CAC tautology: 7225 x v (y v (z v (u v (v v (w v v6))))) = v v (x v (y v (z v (w v (v6 v u))))). [para(5511(a,2),47(a,2,2,2,2,2))]. % back CAC tautology: 7221 x v (y v (z v (u v (v v (w v v6))))) = v v (x v (y v (z v (v6 v (u v w))))). [para(5511(a,1),47(a,2,2,2,2,2))]. % back CAC tautology: 7218 x v (y v (z v (u v (v v (w v v6))))) = v6 v (x v (y v (z v (u v (v v w))))). [para(5511(a,2),47(a,1,2,2,2,2))]. % back CAC tautology: 7214 x v (y v (z v (u v (v v w)))) = w v (x v (y v (z v (v v u)))). [para(5511(a,1),47(a,1,2,2,2))]. % back CAC tautology: 7213 x v (y v (z v (u v (v v (w v v6))))) = w v (x v (y v (z v (u v (v6 v v))))). [para(5511(a,1),47(a,1,2,2,2,2))]. % back CAC tautology: 7207 x v (y v (z v (u v (v v w)))) = u v (x v (z v (v v (w v y)))). [para(5511(a,2),46(a,2,2,2,2))]. % back CAC tautology: 7204 x v (y v (z v (u v v))) = u v (x v (v v (z v y))). [para(5511(a,1),46(a,2,2,2))]. % back CAC tautology: 7203 x v (y v (z v (u v (v v w)))) = u v (x v (z v (w v (y v v)))). [para(5511(a,1),46(a,2,2,2,2))]. % back CAC tautology: 7201 x v (y v (z v (u v (v v w)))) = w v (x v (z v (y v (u v v)))). [para(5511(a,2),46(a,1,2,2,2))]. % back CAC tautology: 7198 x v (y v (z v (u v v))) = v v (x v (u v (y v z))). [para(5511(a,1),46(a,1,2,2))]. % back CAC tautology: 7197 x v (y v (z v (u v (v v w)))) = v v (x v (z v (y v (w v u)))). [para(5511(a,1),46(a,1,2,2,2))]. % back CAC tautology: 7189 x v (y v (z v (u v (v v w)))) = u v (x v (y v (z v (w v v)))). [para(5511(a,2),45(a,2,2,2,2))]. % back CAC tautology: 7188 x v (y v (z v (u v (v v (w v v6))))) = u v (x v (y v (v v (w v (v6 v z))))). [para(5511(a,2),45(a,2,2,2,2,2))]. % back CAC tautology: 7184 x v (y v (z v (u v (v v w)))) = u v (x v (y v (w v (v v z)))). [para(5511(a,1),45(a,2,2,2,2))]. % back CAC tautology: 7183 x v (y v (z v (u v (v v (w v v6))))) = u v (x v (y v (v v (v6 v (z v w))))). [para(5511(a,1),45(a,2,2,2,2,2))]. % back CAC tautology: 7179 x v (y v (z v (u v (v v (w v v6))))) = u v (x v (y v (v6 v (z v (v v w))))). [para(5511(a,2),45(a,1,2,2,2,2))]. % back CAC tautology: 7175 x v (y v (z v (u v (v v w)))) = v v (x v (y v (w v (z v u)))). [para(5511(a,1),45(a,1,2,2,2))]. % back CAC tautology: 7174 x v (y v (z v (u v (v v (w v v6))))) = u v (x v (y v (w v (z v (v6 v v))))). [para(5511(a,1),45(a,1,2,2,2,2))]. % back CAC tautology: 7163 x v (y v (z v (u v v))) = z v (x v (y v (v v u))). [para(5511(a,2),36(a,2,2,2))]. % back CAC tautology: 7160 x v (y v (z v (u v v))) = z v (x v (v v (u v y))). [para(5511(a,1),36(a,2,2,2))]. % back CAC tautology: 7157 x v (y v (z v (u v v))) = u v (x v (v v (y v z))). [para(5511(a,1),36(a,1,2,2))]. % back CAC tautology: 7155 x v (y v (z v (u v v))) = x v (v v (y v (z v u))). [para(5511(a,2),39(a,1,2,2))]. % back CAC tautology: 7154 x v (y v (z v u)) = x v (u v (z v y)). [para(5511(a,1),39(a,1,2))]. % back CAC tautology: 7153 x v (y v (z v (u v v))) = x v (u v (y v (v v z))). [para(5511(a,1),39(a,1,2,2))]. % back CAC tautology: 7150 x v (y v (z v u)) = u v (z v (x v y)). [para(5511(a,1),37(a,1,2))]. % back CAC tautology: 7144 x v (y v (z v (u v (v v (w v v6))))) = w v (y v (v v (z v (x v (u v v6))))). [para(485(a,2),485(a,2,2)),flip(a)]. % back CAC tautology: 7143 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (u v (z v (v6 v (w v (y v v7)))))). [para(485(a,2),485(a,2,2,2))]. % back CAC tautology: 7142 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (u v (w v (v6 v (v8 v (v7 v (z v v9)))))))). [para(485(a,2),485(a,2,2,2,2,2))]. % back CAC tautology: 7141 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (v6 v (y v (u v (w v (z v v7)))))). [para(485(a,1),485(a,2,2,2))]. % back CAC tautology: 7140 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (v7 v (u v (z v (v6 v (w v v8))))))). [para(485(a,1),485(a,2,2,2,2))]. % back CAC tautology: 7139 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (u v (v8 v (z v (w v (v7 v (v6 v v9)))))))). [para(485(a,1),485(a,2,2,2,2,2))]. % back CAC tautology: 7138 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v8 v (x v (y v (u v (z v (v v (w v (v7 v (v6 v v9)))))))). [para(485(a,2),485(a,1,2,2,2,2))]. % back CAC tautology: 7137 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (y v (v v (u v (w v (z v v7)))))). [para(485(a,1),485(a,1,2,2))]. % back CAC tautology: 7136 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (x v (y v (v v (z v (v7 v (v6 v (u v v8))))))). [para(485(a,1),485(a,1,2,2,2))]. % back CAC tautology: 7135 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = w v (x v (y v (u v (z v (v6 v (v8 v (v7 v (v v v9)))))))). [para(485(a,1),485(a,1,2,2,2,2))]. % back CAC tautology: 7109 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (u v (v6 v (w v (v7 v (z v v8))))))). [para(52(a,2),485(a,2,2,2,2,2))]. % back CAC tautology: 7108 x v (y v (z v (u v (v v (w v v6))))) = v v (x v (w v (u v (y v (z v v6))))). [para(52(a,1),485(a,2,2,2))]. % back CAC tautology: 7107 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (u v (v7 v (w v (z v (v6 v v8))))))). [para(52(a,1),485(a,2,2,2,2,2))]. % back CAC tautology: 7106 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v7 v (x v (y v (u v (z v (w v (v v (v6 v v8))))))). [para(52(a,2),485(a,1,2,2,2,2))]. % back CAC tautology: 7105 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v6 v (x v (y v (u v (z v (w v (v7 v (v v v8))))))). [para(52(a,1),485(a,1,2,2,2,2))]. % back CAC tautology: 7104 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (y v (z v (x v (u v (w v (v v v7)))))). [para(485(a,2),52(a,2,2,2)),flip(a)]. % back CAC tautology: 7103 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (y v (x v (v v (w v (v7 v (v6 v (z v v8))))))). [para(485(a,2),52(a,2,2,2,2))]. % back CAC tautology: 7102 x v (y v (z v (u v (v v (w v v6))))) = u v (w v (y v (x v (v v (z v v6))))). [para(485(a,1),52(a,2,2))]. % back CAC tautology: 7101 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (y v (v6 v (x v (z v (w v (v v v7)))))). [para(485(a,1),52(a,2,2,2))]. % back CAC tautology: 7100 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (y v (x v (v7 v (z v (v v (v6 v (w v v8))))))). [para(485(a,1),52(a,2,2,2,2))]. % back CAC tautology: 7099 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (y v (x v (v6 v (u v (w v (v v v7)))))). [para(485(a,2),52(a,1,2,2))]. % back CAC tautology: 7098 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v7 v (y v (x v (z v (u v (v v (v6 v (w v v8))))))). [para(485(a,2),52(a,1,2,2,2))]. % back CAC tautology: 7097 x v (y v (z v (u v (v v (w v v6))))) = w v (z v (x v (u v (v v (y v v6))))). [para(485(a,1),52(a,1,2))]. % back CAC tautology: 7096 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (y v (x v (u v (v6 v (w v (z v v7)))))). [para(485(a,1),52(a,1,2,2))]. % back CAC tautology: 7095 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (y v (x v (z v (w v (v7 v (v6 v (u v v8))))))). [para(485(a,1),52(a,1,2,2,2))]. % back CAC tautology: 7091 x v (y v (z v (u v (v v w)))) = v v (x v (y v (u v (w v z)))). [para(5510(a,1),485(a,2,2,2,2,2))]. % back CAC tautology: 7087 x v (y v (z v (u v (v v w)))) = w v (x v (y v (u v (z v v)))). [para(5510(a,1),485(a,1,2,2,2,2))]. % back CAC tautology: 7084 x v (y v (z v (u v v))) = v v (x v (y v (u v z))). [para(4833(a,1),485(a,1,2,2,2,2)),rewrite(4833(7))]. % back CAC tautology: 7083 x v (y v (z v (u v (v v (w v v6))))) = v v (y v (w v (x v (u v (z v v6))))). [para(51(a,2),485(a,2,2))]. % back CAC tautology: 7082 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (u v (v6 v (y v (z v (w v v7)))))). [para(51(a,2),485(a,2,2,2))]. % back CAC tautology: 7081 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (u v (w v (v8 v (z v (v6 v (v7 v v9)))))))). [para(51(a,2),485(a,2,2,2,2,2))]. % back CAC tautology: 7080 x v (y v (z v (u v (v v (w v v6))))) = v v (u v (x v (z v (w v (y v v6))))). [para(51(a,1),485(a,2,2))]. % back CAC tautology: 7079 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (w v (u v (v6 v (v7 v (z v v8))))))). [para(51(a,1),485(a,2,2,2,2))]. % back CAC tautology: 7078 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (u v (v6 v (z v (v7 v (v8 v (w v v9)))))))). [para(51(a,1),485(a,2,2,2,2,2))]. % back CAC tautology: 7077 x v (y v (z v (u v (v v (w v v6))))) = w v (x v (u v (v v (y v (z v v6))))). [para(51(a,2),485(a,1,2))]. % back CAC tautology: 7076 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v6 v (x v (y v (u v (z v (v v (v7 v (v8 v (w v v9)))))))). [para(51(a,2),485(a,1,2,2,2,2))]. % back CAC tautology: 7075 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v7 v (x v (y v (v v (z v (u v (w v (v6 v v8))))))). [para(51(a,1),485(a,1,2,2,2))]. % back CAC tautology: 7074 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = w v (x v (y v (u v (z v (v8 v (v v (v6 v (v7 v v9)))))))). [para(51(a,1),485(a,1,2,2,2,2))]. % back CAC tautology: 7073 x v (y v (z v (u v (v v (w v v6))))) = w v (v v (x v (y v (z v (u v v6))))). [para(485(a,2),51(a,2,2)),flip(a)]. % back CAC tautology: 7072 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (y v (w v (v7 v (v6 v (v v v8))))))). [para(485(a,2),51(a,2,2,2,2))]. % back CAC tautology: 7071 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v v (w v (v6 v (v8 v (v7 v (y v v9)))))))). [para(485(a,2),51(a,2,2,2,2,2))]. % back CAC tautology: 7070 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v6 v (u v (v v (w v (y v v7)))))). [para(485(a,1),51(a,2,2,2))]. % back CAC tautology: 7069 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v7 v (v v (y v (v6 v (w v v8))))))). [para(485(a,1),51(a,2,2,2,2))]. % back CAC tautology: 7068 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v v (v8 v (y v (w v (v7 v (v6 v v9)))))))). [para(485(a,1),51(a,2,2,2,2,2))]. % back CAC tautology: 7067 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (z v (u v (y v (w v (v v v7)))))). [para(485(a,2),51(a,1,2,2))]. % back CAC tautology: 7066 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v7 v (u v (y v (v v (v6 v (w v v8))))))). [para(485(a,2),51(a,1,2,2,2))]. % back CAC tautology: 7065 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v8 v (y v (v v (w v (v7 v (v6 v v9)))))))). [para(485(a,2),51(a,1,2,2,2,2))]. % back CAC tautology: 7064 x v (y v (z v (u v (v v (w v v6))))) = u v (x v (w v (v v (z v (y v v6))))). [para(485(a,1),51(a,1,2))]. % back CAC tautology: 7063 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (v v (v6 v (y v (w v (z v v7)))))). [para(485(a,1),51(a,1,2,2))]. % back CAC tautology: 7062 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (w v (y v (v7 v (v6 v (u v v8))))))). [para(485(a,1),51(a,1,2,2,2))]. % back CAC tautology: 7061 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (w v (y v (v6 v (v8 v (v7 v (v v v9)))))))). [para(485(a,1),51(a,1,2,2,2,2))]. % back CAC tautology: 7059 x v (y v (z v (u v (v v w)))) = v v (u v (z v (x v (y v w)))). [para(50(a,1),485(a,2,2))]. % back CAC tautology: 7058 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (y v (w v (v6 v (u v (z v v7)))))). [para(50(a,1),485(a,2,2,2,2))]. % back CAC tautology: 7057 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (u v (v6 v (v7 v (z v (w v v8))))))). [para(50(a,1),485(a,2,2,2,2,2))]. % back CAC tautology: 7056 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (y v (w v (z v (u v (v v v7)))))). [para(50(a,1),485(a,1,2,2,2))]. % back CAC tautology: 7055 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v6 v (x v (y v (u v (z v (v7 v (v v (w v v8))))))). [para(50(a,1),485(a,1,2,2,2,2))]. % back CAC tautology: 7054 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (z v (x v (y v (u v (w v (v v v7)))))). [para(485(a,2),50(a,1,2,2))]. % back CAC tautology: 7053 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (v7 v (x v (y v (u v (v v (v6 v (w v v8))))))). [para(485(a,2),50(a,1,2,2,2))]. % back CAC tautology: 7052 x v (y v (z v (u v (v v w)))) = v v (u v (y v (z v (x v w)))). [para(485(a,1),50(a,1))]. % back CAC tautology: 7051 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (v v (x v (y v (v6 v (w v (z v v7)))))). [para(485(a,1),50(a,1,2,2))]. % back CAC tautology: 7050 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (v v (x v (y v (w v (v7 v (v6 v (u v v8))))))). [para(485(a,1),50(a,1,2,2,2))]. % back CAC tautology: 7049 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (u v (w v (y v (v6 v (z v v7)))))). [para(49(a,2),485(a,2,2,2))]. % back CAC tautology: 7048 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (u v (w v (v7 v (z v (v8 v (v6 v v9)))))))). [para(49(a,2),485(a,2,2,2,2,2))]. % back CAC tautology: 7047 x v (y v (z v (u v (v v (w v v6))))) = v v (u v (x v (w v (y v (z v v6))))). [para(49(a,1),485(a,2,2))]. % back CAC tautology: 7046 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (w v (u v (v7 v (z v (v6 v v8))))))). [para(49(a,1),485(a,2,2,2,2))]. % back CAC tautology: 7045 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (u v (v6 v (z v (v8 v (w v (v7 v v9)))))))). [para(49(a,1),485(a,2,2,2,2,2))]. % back CAC tautology: 7044 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v6 v (x v (y v (u v (z v (v v (v8 v (w v (v7 v v9)))))))). [para(49(a,2),485(a,1,2,2,2,2))]. % back CAC tautology: 7043 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v6 v (x v (y v (v v (z v (u v (v7 v (w v v8))))))). [para(49(a,1),485(a,1,2,2,2))]. % back CAC tautology: 7042 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = w v (x v (y v (u v (z v (v7 v (v v (v8 v (v6 v v9)))))))). [para(49(a,1),485(a,1,2,2,2,2))]. % back CAC tautology: 7041 x v (y v (z v (u v (v v (w v v6))))) = w v (z v (x v (v v (y v (u v v6))))). [para(485(a,2),49(a,2,2)),flip(a)]. % back CAC tautology: 7040 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (u v (w v (v7 v (v6 v (y v v8))))))). [para(485(a,2),49(a,2,2,2,2))]. % back CAC tautology: 7039 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v v (y v (w v (v6 v (v8 v (v7 v (u v v9)))))))). [para(485(a,2),49(a,2,2,2,2,2))]. % back CAC tautology: 7038 x v (y v (z v (u v (v v (w v v6))))) = z v (w v (x v (v v (u v (y v v6))))). [para(485(a,1),49(a,2,2))]. % back CAC tautology: 7037 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v6 v (v v (y v (w v (u v v7)))))). [para(485(a,1),49(a,2,2,2))]. % back CAC tautology: 7036 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (v7 v (y v (u v (v6 v (w v v8))))))). [para(485(a,1),49(a,2,2,2,2))]. % back CAC tautology: 7035 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v v (y v (v8 v (u v (w v (v7 v (v6 v v9)))))))). [para(485(a,1),49(a,2,2,2,2,2))]. % back CAC tautology: 7034 x v (y v (z v (u v (v v (w v v6))))) = y v (x v (v v (w v (z v (u v v6))))). [para(485(a,2),49(a,1,2))]. % back CAC tautology: 7033 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (u v (y v (z v (w v (v v v7)))))). [para(485(a,2),49(a,1,2,2))]. % back CAC tautology: 7032 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (y v (v7 v (v v (v6 v (w v v8))))))). [para(485(a,2),49(a,1,2,2,2))]. % back CAC tautology: 7031 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v8 v (y v (u v (v v (w v (v7 v (v6 v v9)))))))). [para(485(a,2),49(a,1,2,2,2,2))]. % back CAC tautology: 7030 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (w v (y v (v v (v7 v (v6 v (u v v8))))))). [para(485(a,1),49(a,1,2,2,2))]. % back CAC tautology: 7029 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (w v (y v (u v (v6 v (v8 v (v7 v (v v v9)))))))). [para(485(a,1),49(a,1,2,2,2,2))]. % back CAC tautology: 7028 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (u v (w v (z v (v7 v (v6 v v8))))))). [para(48(a,1),485(a,2,2,2,2,2))]. % back CAC tautology: 7027 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (x v (y v (u v (z v (v v (v7 v (v6 v v8))))))). [para(48(a,1),485(a,1,2,2,2,2))]. % back CAC tautology: 7026 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = y v (x v (z v (v6 v (u v (w v (v v v7)))))). [para(485(a,2),48(a,1,2,2))]. % back CAC tautology: 7025 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = y v (x v (v7 v (z v (u v (v v (v6 v (w v v8))))))). [para(485(a,2),48(a,1,2,2,2))]. % back CAC tautology: 7024 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = y v (x v (v6 v (u v (z v (w v (v v v7)))))). [para(485(a,1),48(a,1,2,2)),flip(a)]. % back CAC tautology: 7023 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = y v (x v (v v (z v (w v (v7 v (v6 v (u v v8))))))). [para(485(a,1),48(a,1,2,2,2))]. % back CAC tautology: 7022 x v (y v (z v (u v (v v (w v v6))))) = w v (y v (u v (z v (x v (v v v6))))). [para(47(a,2),485(a,2,2)),flip(a)]. % back CAC tautology: 7021 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (u v (z v (w v (v6 v (y v v7)))))). [para(47(a,2),485(a,2,2,2))]. % back CAC tautology: 7020 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (u v (w v (v6 v (v7 v (v8 v (z v v9)))))))). [para(47(a,2),485(a,2,2,2,2,2))]. % back CAC tautology: 7019 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (v6 v (y v (u v (z v (w v v7)))))). [para(47(a,1),485(a,2,2,2))]. % back CAC tautology: 7018 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (v7 v (u v (z v (w v (v6 v v8))))))). [para(47(a,1),485(a,2,2,2,2))]. % back CAC tautology: 7017 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (u v (v8 v (z v (w v (v6 v (v7 v v9)))))))). [para(47(a,1),485(a,2,2,2,2,2))]. % back CAC tautology: 7016 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v8 v (x v (y v (u v (z v (v v (w v (v6 v (v7 v v9)))))))). [para(47(a,2),485(a,1,2,2,2,2))]. % back CAC tautology: 7015 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (x v (y v (v v (u v (v6 v (z v v7)))))). [para(47(a,1),485(a,1,2,2))]. % back CAC tautology: 7014 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (x v (y v (v v (z v (v6 v (v7 v (u v v8))))))). [para(47(a,1),485(a,1,2,2,2))]. % back CAC tautology: 7013 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = w v (x v (y v (u v (z v (v6 v (v7 v (v8 v (v v v9)))))))). [para(47(a,1),485(a,1,2,2,2,2))]. % back CAC tautology: 7012 x v (y v (z v (u v (v v (w v v6))))) = w v (y v (z v (v v (x v (u v v6))))). [para(485(a,2),47(a,2,2)),flip(a)]. % back CAC tautology: 7011 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (z v (u v (v6 v (w v (y v v7)))))). [para(485(a,2),47(a,2,2,2))]. % back CAC tautology: 7010 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (z v (w v (v6 v (v8 v (v7 v (u v v9)))))))). [para(485(a,2),47(a,2,2,2,2,2))]. % back CAC tautology: 7009 x v (y v (z v (u v (v v (w v v6))))) = v v (w v (x v (y v (u v (z v v6))))). [para(485(a,1),47(a,2,2))]. % back CAC tautology: 7008 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (v6 v (y v (z v (w v (u v v7)))))). [para(485(a,1),47(a,2,2,2))]. % back CAC tautology: 7007 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (v7 v (z v (u v (v6 v (w v v8))))))). [para(485(a,1),47(a,2,2,2,2))]. % back CAC tautology: 7006 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (z v (v8 v (u v (w v (v7 v (v6 v v9)))))))). [para(485(a,1),47(a,2,2,2,2,2))]. % back CAC tautology: 7005 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (y v (z v (v7 v (v v (v6 v (w v v8))))))). [para(485(a,2),47(a,1,2,2,2))]. % back CAC tautology: 7004 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v8 v (x v (y v (z v (u v (v v (w v (v7 v (v6 v v9)))))))). [para(485(a,2),47(a,1,2,2,2,2))]. % back CAC tautology: 7003 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (y v (u v (v v (w v (z v v7)))))). [para(485(a,1),47(a,1,2,2))]. % back CAC tautology: 7002 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (x v (y v (z v (v v (v7 v (v6 v (u v v8))))))). [para(485(a,1),47(a,1,2,2,2))]. % back CAC tautology: 7001 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = w v (x v (y v (z v (u v (v6 v (v8 v (v7 v (v v v9)))))))). [para(485(a,1),47(a,1,2,2,2,2))]. % back CAC tautology: 7000 x v (y v (z v (u v (v v (w v v6))))) = v v (x v (u v (w v (z v (y v v6))))). [para(46(a,2),485(a,2,2,2))]. % back CAC tautology: 6999 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (u v (w v (v7 v (v6 v (z v v8))))))). [para(46(a,2),485(a,2,2,2,2,2))]. % back CAC tautology: 6998 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (u v (v7 v (z v (v6 v (w v v8))))))). [para(46(a,1),485(a,2,2,2,2,2))]. % back CAC tautology: 6997 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (y v (v v (z v (w v (u v v7)))))). [para(46(a,1),485(a,1,2,2,2))]. % back CAC tautology: 6996 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (x v (y v (u v (z v (v7 v (v6 v (v v v8))))))). [para(46(a,1),485(a,1,2,2,2,2))]. % back CAC tautology: 6995 x v (y v (z v (u v (v v (w v v6))))) = w v (z v (y v (x v (v v (u v v6))))). [para(485(a,2),46(a,2,2)),flip(a)]. % back CAC tautology: 6994 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (z v (v v (w v (v7 v (v6 v (y v v8))))))). [para(485(a,2),46(a,2,2,2,2))]. % back CAC tautology: 6993 x v (y v (z v (u v (v v (w v v6))))) = u v (w v (x v (z v (v v (y v v6))))). [para(485(a,1),46(a,2,2))]. % back CAC tautology: 6992 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (v6 v (z v (y v (w v (v v v7)))))). [para(485(a,1),46(a,2,2,2))]. % back CAC tautology: 6991 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (z v (v7 v (y v (v v (v6 v (w v v8))))))). [para(485(a,1),46(a,2,2,2,2))]. % back CAC tautology: 6990 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v7 v (x v (z v (y v (u v (v v (v6 v (w v v8))))))). [para(485(a,2),46(a,1,2,2,2))]. % back CAC tautology: 6989 x v (y v (z v (u v (v v (w v v6))))) = w v (x v (u v (z v (v v (y v v6))))). [para(485(a,1),46(a,1,2))]. % back CAC tautology: 6988 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (u v (y v (v6 v (w v (z v v7)))))). [para(485(a,1),46(a,1,2,2))]. % back CAC tautology: 6987 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (z v (y v (w v (v7 v (v6 v (u v v8))))))). [para(485(a,1),46(a,1,2,2,2))]. % back CAC tautology: 6986 x v (y v (z v (u v (v v (w v v6))))) = v v (y v (w v (z v (x v (u v v6))))). [para(45(a,2),485(a,2,2)),flip(a)]. % back CAC tautology: 6985 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (u v (z v (v6 v (y v (w v v7)))))). [para(45(a,2),485(a,2,2,2))]. % back CAC tautology: 6984 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (u v (w v (v6 v (v8 v (z v (v7 v v9)))))))). [para(45(a,2),485(a,2,2,2,2,2))]. % back CAC tautology: 6983 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (w v (y v (u v (v6 v (z v v7)))))). [para(45(a,1),485(a,2,2,2))]. % back CAC tautology: 6982 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (v6 v (u v (z v (v7 v (w v v8))))))). [para(45(a,1),485(a,2,2,2,2))]. % back CAC tautology: 6981 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (u v (v7 v (z v (w v (v8 v (v6 v v9)))))))). [para(45(a,1),485(a,2,2,2,2,2))]. % back CAC tautology: 6980 x v (y v (z v (u v (v v (w v v6))))) = w v (x v (v v (z v (y v (u v v6))))). [para(45(a,2),485(a,1,2))]. % back CAC tautology: 6979 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v7 v (x v (y v (u v (z v (v v (w v (v8 v (v6 v v9)))))))). [para(45(a,2),485(a,1,2,2,2,2))]. % back CAC tautology: 6978 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (y v (v v (u v (z v (w v v7)))))). [para(45(a,1),485(a,1,2,2))]. % back CAC tautology: 6977 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (x v (y v (v v (z v (v7 v (u v (v6 v v8))))))). [para(45(a,1),485(a,1,2,2,2))]. % back CAC tautology: 6976 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = w v (x v (y v (u v (z v (v6 v (v8 v (v v (v7 v v9)))))))). [para(45(a,1),485(a,1,2,2,2,2))]. % back CAC tautology: 6975 x v (y v (z v (u v (v v (w v v6))))) = w v (y v (v v (x v (z v (u v v6))))). [para(485(a,2),45(a,2,2)),flip(a)]. % back CAC tautology: 6974 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (v v (z v (v6 v (w v (y v v7)))))). [para(485(a,2),45(a,2,2,2))]. % back CAC tautology: 6973 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (y v (z v (w v (v7 v (v6 v (v v v8))))))). [para(485(a,2),45(a,2,2,2,2))]. % back CAC tautology: 6972 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = u v (x v (y v (v v (w v (v6 v (v8 v (v7 v (z v v9)))))))). [para(485(a,2),45(a,2,2,2,2,2))]. % back CAC tautology: 6971 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (v6 v (y v (v v (w v (z v v7)))))). [para(485(a,1),45(a,2,2,2))]. % back CAC tautology: 6970 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (y v (v7 v (v v (z v (v6 v (w v v8))))))). [para(485(a,1),45(a,2,2,2,2))]. % back CAC tautology: 6969 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = u v (x v (y v (v v (v8 v (z v (w v (v7 v (v6 v v9)))))))). [para(485(a,1),45(a,2,2,2,2,2))]. % back CAC tautology: 6968 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (y v (u v (v6 v (w v (v v v7)))))). [para(485(a,2),45(a,1,2,2))]. % back CAC tautology: 6967 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v7 v (x v (y v (u v (z v (v v (v6 v (w v v8))))))). [para(485(a,2),45(a,1,2,2,2))]. % back CAC tautology: 6966 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = u v (x v (y v (v8 v (z v (v v (w v (v7 v (v6 v v9)))))))). [para(485(a,2),45(a,1,2,2,2,2))]. % back CAC tautology: 6965 x v (y v (z v (u v (v v (w v v6))))) = w v (x v (z v (v v (u v (y v v6))))). [para(485(a,1),45(a,1,2))]. % back CAC tautology: 6964 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (y v (v6 v (u v (w v (z v v7)))))). [para(485(a,1),45(a,1,2,2))]. % back CAC tautology: 6963 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (w v (z v (v7 v (v6 v (u v v8))))))). [para(485(a,1),45(a,1,2,2,2))]. % back CAC tautology: 6962 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = u v (x v (y v (w v (z v (v6 v (v8 v (v7 v (v v v9)))))))). [para(485(a,1),45(a,1,2,2,2,2))]. % back CAC tautology: 6961 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (v6 v (y v (z v (w v (v v v7)))))). [para(485(a,1),38(a,2,2,2))]. % back CAC tautology: 6960 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (y v (v6 v (u v (w v (v v v7)))))). [para(485(a,2),38(a,1,2,2))]. % back CAC tautology: 6959 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (y v (v v (v6 v (w v (u v v7)))))). [para(485(a,2),36(a,2,2,2))]. % back CAC tautology: 6958 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (v v (y v (v6 v (w v (z v v7)))))). [para(485(a,1),36(a,1,2,2))]. % back CAC tautology: 6957 x v (y v (z v (u v (v v (w v v6))))) = x v (y v (w v (z v (v v (u v v6))))). [para(485(a,2),39(a,1,2))]. % back CAC tautology: 6956 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = x v (v6 v (y v (z v (u v (w v (v v v7)))))). [para(485(a,2),39(a,1,2,2))]. % back CAC tautology: 6955 x v (y v (z v (u v (v v (w v v6))))) = x v (w v (z v (y v (v v (u v v6))))). [para(485(a,1),39(a,1,2)),flip(a)]. % back CAC tautology: 6954 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = x v (u v (y v (v v (v6 v (w v (z v v7)))))). [para(485(a,1),39(a,1,2,2))]. % back CAC tautology: 6953 x v (y v (z v (u v (v v (w v v6))))) = u v (z v (x v (w v (v v (y v v6))))). [para(485(a,1),37(a,1,2))]. % back CAC tautology: 5952 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (y v (x v (w v (v v (v6 v (z v v7)))))). [para(52(a,2),52(a,2,2,2,2))]. % back CAC tautology: 5951 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (y v (x v (v6 v (v v (z v (w v v7)))))). [para(52(a,1),52(a,2,2,2,2))]. % back CAC tautology: 5950 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (y v (x v (z v (v v (u v (w v v7)))))). [para(52(a,2),52(a,1,2,2,2))]. % back CAC tautology: 5949 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (y v (x v (z v (v v (v6 v (u v v7)))))). [para(52(a,1),52(a,1,2,2,2))]. % back CAC tautology: 5946 x v (y v (z v (u v v))) = u v (y v (x v (v v z))). [para(5510(a,1),52(a,2,2,2,2))]. % back CAC tautology: 5943 x v (y v (z v (u v v))) = v v (y v (x v (z v u))). [para(5510(a,1),52(a,1,2,2,2))]. % back CAC tautology: 5940 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (y v (z v (x v (w v (v6 v (u v v7)))))). [para(51(a,2),52(a,2,2,2)),flip(a)]. % back CAC tautology: 5939 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (y v (x v (v v (v7 v (z v (w v (v6 v v8))))))). [para(51(a,2),52(a,2,2,2,2))]. % back CAC tautology: 5938 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (y v (x v (w v (z v (v6 v (v7 v (v v v8))))))). [para(51(a,1),52(a,2,2,2,2))]. % back CAC tautology: 5937 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (y v (x v (z v (u v (v6 v (v7 v (v v v8))))))). [para(51(a,2),52(a,1,2,2,2))]. % back CAC tautology: 5936 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (y v (x v (u v (z v (v v (w v v7)))))). [para(51(a,1),52(a,1,2,2))]. % back CAC tautology: 5935 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (y v (x v (z v (v7 v (u v (w v (v6 v v8))))))). [para(51(a,1),52(a,1,2,2,2))]. % back CAC tautology: 5934 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v v (v6 v (w v (v7 v (y v v8))))))). [para(52(a,2),51(a,2,2,2,2,2))]. % back CAC tautology: 5933 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v v (v7 v (w v (y v (v6 v v8))))))). [para(52(a,1),51(a,2,2,2,2,2))]. % back CAC tautology: 5932 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v7 v (y v (w v (v v (v6 v v8))))))). [para(52(a,2),51(a,1,2,2,2,2))]. % back CAC tautology: 5931 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v6 v (y v (w v (v7 v (v v v8))))))). [para(52(a,1),51(a,1,2,2,2,2))]. % back CAC tautology: 5929 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (y v (x v (w v (v6 v (z v (v v v7)))))). [para(50(a,1),52(a,2,2,2,2))]. % back CAC tautology: 5928 x v (y v (z v (u v (v v (w v v6))))) = w v (y v (x v (v v (z v (u v v6))))). [para(50(a,1),52(a,1,2,2))]. % back CAC tautology: 5927 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (y v (x v (z v (v6 v (u v (v v v7)))))). [para(50(a,1),52(a,1,2,2,2))]. % back CAC tautology: 5926 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (v6 v (x v (y v (v v (u v (w v v7)))))). [para(52(a,2),50(a,1,2,2,2))]. % back CAC tautology: 5925 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (w v (x v (y v (v v (v6 v (u v v7)))))). [para(52(a,1),50(a,1,2,2,2))]. % back CAC tautology: 5924 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (y v (z v (x v (v6 v (u v (w v v7)))))). [para(49(a,2),52(a,2,2,2)),flip(a)]. % back CAC tautology: 5923 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (y v (x v (v v (v6 v (z v (v7 v (w v v8))))))). [para(49(a,2),52(a,2,2,2,2))]. % back CAC tautology: 5922 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (y v (x v (w v (z v (v7 v (v v (v6 v v8))))))). [para(49(a,1),52(a,2,2,2,2))]. % back CAC tautology: 5921 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (y v (x v (z v (u v (v7 v (v v (v6 v v8))))))). [para(49(a,2),52(a,1,2,2,2))]. % back CAC tautology: 5920 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (y v (x v (u v (z v (v6 v (v v v7)))))). [para(49(a,1),52(a,1,2,2))]. % back CAC tautology: 5919 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (y v (x v (z v (v6 v (u v (v7 v (w v v8))))))). [para(49(a,1),52(a,1,2,2,2))]. % back CAC tautology: 5918 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (y v (v6 v (w v (v7 v (u v v8))))))). [para(52(a,2),49(a,2,2,2,2,2))]. % back CAC tautology: 5917 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (y v (v7 v (w v (u v (v6 v v8))))))). [para(52(a,1),49(a,2,2,2,2,2))]. % back CAC tautology: 5916 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v7 v (y v (u v (w v (v v (v6 v v8))))))). [para(52(a,2),49(a,1,2,2,2,2))]. % back CAC tautology: 5915 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v6 v (y v (u v (w v (v7 v (v v v8))))))). [para(52(a,1),49(a,1,2,2,2,2))]. % back CAC tautology: 5914 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (y v (x v (v v (z v (v6 v (w v v7)))))). [para(48(a,1),52(a,2,2,2,2))]. % back CAC tautology: 5913 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (y v (x v (z v (u v (v6 v (w v v7)))))). [para(48(a,1),52(a,1,2,2,2))]. % back CAC tautology: 5912 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = y v (x v (v6 v (z v (v v (u v (w v v7)))))). [para(52(a,2),48(a,1,2,2,2))]. % back CAC tautology: 5911 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = y v (x v (w v (z v (v v (v6 v (u v v7)))))). [para(52(a,1),48(a,1,2,2,2))]. % back CAC tautology: 5910 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (y v (z v (x v (u v (v v (w v v7)))))). [para(47(a,2),52(a,2,2,2)),flip(a)]. % back CAC tautology: 5909 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (y v (x v (v v (w v (v6 v (v7 v (z v v8))))))). [para(47(a,2),52(a,2,2,2,2))]. % back CAC tautology: 5908 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (y v (v6 v (x v (z v (v v (w v v7)))))). [para(47(a,1),52(a,2,2,2))]. % back CAC tautology: 5907 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (y v (x v (v7 v (z v (v v (w v (v6 v v8))))))). [para(47(a,1),52(a,2,2,2,2))]. % back CAC tautology: 5906 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (y v (x v (v6 v (u v (v v (w v v7)))))). [para(47(a,2),52(a,1,2,2))]. % back CAC tautology: 5905 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v7 v (y v (x v (z v (u v (v v (w v (v6 v v8))))))). [para(47(a,2),52(a,1,2,2,2))]. % back CAC tautology: 5904 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (y v (x v (u v (w v (v6 v (z v v7)))))). [para(47(a,1),52(a,1,2,2))]. % back CAC tautology: 5903 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (y v (x v (z v (w v (v6 v (v7 v (u v v8))))))). [para(47(a,1),52(a,1,2,2,2))]. % back CAC tautology: 5902 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (z v (v6 v (w v (v7 v (u v v8))))))). [para(52(a,2),47(a,2,2,2,2,2))]. % back CAC tautology: 5901 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (z v (v7 v (w v (u v (v6 v v8))))))). [para(52(a,1),47(a,2,2,2,2,2))]. % back CAC tautology: 5900 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v7 v (x v (y v (z v (u v (w v (v v (v6 v v8))))))). [para(52(a,2),47(a,1,2,2,2,2))]. % back CAC tautology: 5899 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v6 v (x v (y v (z v (u v (w v (v7 v (v v v8))))))). [para(52(a,1),47(a,1,2,2,2,2))]. % back CAC tautology: 5898 x v (y v (z v (u v (v v (w v v6))))) = w v (y v (z v (x v (v v (u v v6))))). [para(46(a,2),52(a,2,2,2)),flip(a)]. % back CAC tautology: 5897 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (y v (x v (v v (v6 v (w v (z v v7)))))). [para(46(a,2),52(a,2,2,2,2))]. % back CAC tautology: 5896 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (y v (x v (v6 v (z v (w v (v v v7)))))). [para(46(a,1),52(a,2,2,2,2))]. % back CAC tautology: 5895 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (y v (x v (z v (u v (w v (v v v7)))))). [para(46(a,2),52(a,1,2,2,2))]. % back CAC tautology: 5894 x v (y v (z v (u v (v v (w v v6))))) = w v (y v (x v (u v (v v (z v v6))))). [para(46(a,1),52(a,1,2,2))]. % back CAC tautology: 5893 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (y v (x v (z v (v6 v (w v (u v v7)))))). [para(46(a,1),52(a,1,2,2,2))]. % back CAC tautology: 5892 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (z v (w v (v v (v6 v (y v v7)))))). [para(52(a,2),46(a,2,2,2,2))]. % back CAC tautology: 5891 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (z v (v6 v (v v (y v (w v v7)))))). [para(52(a,1),46(a,2,2,2,2))]. % back CAC tautology: 5890 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (z v (y v (v v (u v (w v v7)))))). [para(52(a,2),46(a,1,2,2,2))]. % back CAC tautology: 5889 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (x v (z v (y v (v v (v6 v (u v v7)))))). [para(52(a,1),46(a,1,2,2,2))]. % back CAC tautology: 5888 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (y v (z v (x v (u v (v6 v (v v v7)))))). [para(45(a,2),52(a,2,2,2)),flip(a)]. % back CAC tautology: 5887 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (y v (x v (v v (w v (v7 v (z v (v6 v v8))))))). [para(45(a,2),52(a,2,2,2,2))]. % back CAC tautology: 5886 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (y v (w v (x v (z v (v6 v (v v v7)))))). [para(45(a,1),52(a,2,2,2))]. % back CAC tautology: 5885 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (y v (x v (v6 v (z v (v v (v7 v (w v v8))))))). [para(45(a,1),52(a,2,2,2,2))]. % back CAC tautology: 5884 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (y v (x v (w v (u v (v6 v (v v v7)))))). [para(45(a,2),52(a,1,2,2))]. % back CAC tautology: 5883 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v6 v (y v (x v (z v (u v (v v (v7 v (w v v8))))))). [para(45(a,2),52(a,1,2,2,2))]. % back CAC tautology: 5882 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (y v (x v (u v (v6 v (z v (w v v7)))))). [para(45(a,1),52(a,1,2,2))]. % back CAC tautology: 5881 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (y v (x v (z v (w v (v7 v (u v (v6 v v8))))))). [para(45(a,1),52(a,1,2,2,2))]. % back CAC tautology: 5880 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (y v (v v (v6 v (w v (v7 v (z v v8))))))). [para(52(a,2),45(a,2,2,2,2,2))]. % back CAC tautology: 5879 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (y v (v v (v7 v (w v (z v (v6 v v8))))))). [para(52(a,1),45(a,2,2,2,2,2))]. % back CAC tautology: 5878 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (y v (v7 v (z v (w v (v v (v6 v v8))))))). [para(52(a,2),45(a,1,2,2,2,2))]. % back CAC tautology: 5877 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (y v (v6 v (z v (w v (v7 v (v v v8))))))). [para(52(a,1),45(a,1,2,2,2,2))]. % back CAC tautology: 5876 x v (y v (z v (u v (v v (w v v6))))) = x v (w v (y v (u v (z v (v v v6))))). [para(52(a,2),39(a,1,2,2))]. % back CAC tautology: 5875 x v (y v (z v (u v (v v (w v v6))))) = x v (v v (y v (u v (w v (z v v6))))). [para(52(a,1),39(a,1,2,2))]. % back CAC tautology: 5874 x v (y v (z v (u v (v v (w v v6))))) = w v (y v (x v (u v (z v (v v v6))))). [para(52(a,2),37(a,1,2,2))]. % back CAC tautology: 5873 x v (y v (z v (u v (v v (w v v6))))) = v v (y v (x v (u v (w v (z v v6))))). [para(52(a,1),37(a,1,2,2))]. % back CAC tautology: 5868 x v (y v (z v (u v (v v w)))) = z v (x v (u v (v v (w v y)))). [para(5510(a,1),51(a,2,2,2,2,2))]. % back CAC tautology: 5863 x v (y v (z v (u v (v v w)))) = z v (x v (u v (w v (y v v)))). [para(5510(a,1),51(a,1,2,2,2,2))]. % back CAC tautology: 5859 x v (y v (z v (u v v))) = z v (v v (x v (y v u))). [para(5510(a,1),50(a,1,2,2,2))]. % back CAC tautology: 5854 x v (y v (z v (u v (v v w)))) = z v (x v (v v (y v (w v u)))). [para(5510(a,1),49(a,2,2,2,2,2))]. % back CAC tautology: 5849 x v (y v (z v (u v (v v w)))) = z v (x v (w v (y v (u v v)))). [para(5510(a,1),49(a,1,2,2,2,2))]. % back CAC tautology: 5845 x v (y v (z v (u v v))) = y v (x v (v v (z v u))). [para(5510(a,1),48(a,1,2,2,2))]. % back CAC tautology: 5840 x v (y v (z v (u v (v v w)))) = v v (x v (y v (z v (w v u)))). [para(5510(a,1),47(a,2,2,2,2,2))]. % back CAC tautology: 5835 x v (y v (z v (u v (v v w)))) = w v (x v (y v (z v (u v v)))). [para(5510(a,1),47(a,1,2,2,2,2))]. % back CAC tautology: 5831 x v (y v (z v (u v v))) = u v (x v (z v (v v y))). [para(5510(a,1),46(a,2,2,2,2))]. % back CAC tautology: 5827 x v (y v (z v (u v v))) = v v (x v (z v (y v u))). [para(5510(a,1),46(a,1,2,2,2))]. % back CAC tautology: 5822 x v (y v (z v (u v (v v w)))) = u v (x v (y v (v v (w v z)))). [para(5510(a,1),45(a,2,2,2,2,2))]. % back CAC tautology: 5817 x v (y v (z v (u v (v v w)))) = u v (x v (y v (w v (z v v)))). [para(5510(a,1),45(a,1,2,2,2,2))]. % back CAC tautology: 5802 x v (y v (z v u)) = x v (u v (y v z)). [para(5510(a,1),39(a,1,2,2))]. % back CAC tautology: 5799 x v (y v (z v u)) = u v (y v (x v z)). [para(5510(a,1),37(a,1,2,2))]. % back CAC tautology: 5521 x v (y v (z v (u v v))) = z v (x v (u v (v v y))). [para(4833(a,1),51(a,1,2,2,2,2)),rewrite(4833(7))]. % back CAC tautology: 5520 x v (y v (z v u)) = z v (u v (x v y)). [para(4833(a,1),50(a,1,2,2,2)),rewrite(4833(6))]. % back CAC tautology: 5519 x v (y v (z v (u v v))) = z v (x v (v v (y v u))). [para(4833(a,1),49(a,1,2,2,2,2)),rewrite(4833(7))]. % back CAC tautology: 5518 x v (y v (z v u)) = y v (x v (u v z)). [para(4833(a,1),48(a,1,2,2,2)),rewrite(4833(6))]. % back CAC tautology: 5517 x v (y v (z v (u v v))) = v v (x v (y v (z v u))). [para(4833(a,1),47(a,1,2,2,2,2)),rewrite(4833(7))]. % back CAC tautology: 5516 x v (y v (z v u)) = u v (x v (z v y)). [para(4833(a,1),46(a,1,2,2,2)),rewrite(4833(6))]. % back CAC tautology: 5515 x v (y v (z v (u v v))) = u v (x v (y v (v v z))). [para(4833(a,1),45(a,1,2,2,2,2)),rewrite(4833(7))]. % back CAC tautology: 5514 x v (y v (z v u)) = u v (x v (y v z)). [para(4833(a,1),38(a,1,2,2,2)),rewrite(4833(6))]. % back CAC tautology: 5513 x v (y v (z v u)) = z v (x v (u v y)). [para(4833(a,1),36(a,1,2,2,2)),rewrite(4833(6))]. % back CAC tautology: 5512 x v (y v z) = z v (y v x). [para(4833(a,1),37(a,1,2,2)),rewrite(4833(5))]. % back CAC tautology: 5509 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v v (v6 v (u v (y v (w v v7)))))). [para(51(a,2),51(a,2,2,2))]. % back CAC tautology: 5508 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v v (w v (v8 v (y v (v6 v (v7 v v9)))))))). [para(51(a,2),51(a,2,2,2,2,2))]. % back CAC tautology: 5507 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (w v (v v (v6 v (v7 v (y v v8))))))). [para(51(a,1),51(a,2,2,2,2))]. % back CAC tautology: 5506 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v v (v6 v (y v (v7 v (v8 v (w v v9)))))))). [para(51(a,1),51(a,2,2,2,2,2))]. % back CAC tautology: 5505 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (w v (u v (y v (v6 v (v7 v (v v v8))))))). [para(51(a,2),51(a,1,2,2,2))]. % back CAC tautology: 5504 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v6 v (y v (v v (v7 v (v8 v (w v v9)))))))). [para(51(a,2),51(a,1,2,2,2,2))]. % back CAC tautology: 5503 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (w v (y v (v8 v (v v (v6 v (v7 v v9)))))))). [para(51(a,1),51(a,1,2,2,2,2))]. % back CAC tautology: 5498 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (u v (w v (v6 v (v v (y v v7)))))). [para(50(a,1),51(a,2,2,2,2))]. % back CAC tautology: 5497 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v v (v6 v (v7 v (y v (w v v8))))))). [para(50(a,1),51(a,2,2,2,2,2))]. % back CAC tautology: 5496 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (w v (v6 v (y v (u v (v v v7)))))). [para(50(a,1),51(a,1,2,2,2))]. % back CAC tautology: 5495 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v6 v (y v (v7 v (v v (w v v8))))))). [para(50(a,1),51(a,1,2,2,2,2))]. % back CAC tautology: 5494 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (z v (x v (y v (w v (v6 v (u v v7)))))). [para(51(a,2),50(a,1,2,2))]. % back CAC tautology: 5493 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (w v (x v (y v (u v (v6 v (v7 v (v v v8))))))). [para(51(a,2),50(a,1,2,2,2))]. % back CAC tautology: 5492 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (v6 v (x v (y v (z v (v v (w v v7)))))). [para(51(a,1),50(a,1,2,2))]. % back CAC tautology: 5491 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (v v (x v (y v (v7 v (u v (w v (v6 v v8))))))). [para(51(a,1),50(a,1,2,2,2))]. % back CAC tautology: 5490 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v v (w v (u v (v6 v (y v v7)))))). [para(49(a,2),51(a,2,2,2))]. % back CAC tautology: 5489 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v v (w v (v7 v (y v (v8 v (v6 v v9)))))))). [para(49(a,2),51(a,2,2,2,2,2))]. % back CAC tautology: 5488 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (w v (v v (v7 v (y v (v6 v v8))))))). [para(49(a,1),51(a,2,2,2,2))]. % back CAC tautology: 5487 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v v (v6 v (y v (v8 v (w v (v7 v v9)))))))). [para(49(a,1),51(a,2,2,2,2,2))]. % back CAC tautology: 5486 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (w v (u v (y v (v7 v (v v (v6 v v8))))))). [para(49(a,2),51(a,1,2,2,2))]. % back CAC tautology: 5485 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v6 v (y v (v v (v8 v (w v (v7 v v9)))))))). [para(49(a,2),51(a,1,2,2,2,2))]. % back CAC tautology: 5484 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (w v (y v (v7 v (v v (v8 v (v6 v v9)))))))). [para(49(a,1),51(a,1,2,2,2,2))]. % back CAC tautology: 5483 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (u v (v7 v (y v (w v (v6 v v8))))))). [para(51(a,2),49(a,2,2,2,2))]. % back CAC tautology: 5482 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v v (y v (w v (v8 v (u v (v6 v (v7 v v9)))))))). [para(51(a,2),49(a,2,2,2,2,2))]. % back CAC tautology: 5481 x v (y v (z v (u v (v v w)))) = v v (z v (y v (u v (x v w)))). [para(51(a,1),49(a,2))]. % back CAC tautology: 5480 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v v (y v (v6 v (u v (v7 v (v8 v (w v v9)))))))). [para(51(a,1),49(a,2,2,2,2,2))]. % back CAC tautology: 5479 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v6 v (y v (u v (v v (v7 v (v8 v (w v v9)))))))). [para(51(a,2),49(a,1,2,2,2,2))]. % back CAC tautology: 5478 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v7 v (y v (v v (u v (w v (v6 v v8))))))). [para(51(a,1),49(a,1,2,2,2))]. % back CAC tautology: 5477 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (w v (y v (u v (v8 v (v v (v6 v (v7 v v9)))))))). [para(51(a,1),49(a,1,2,2,2,2))]. % back CAC tautology: 5476 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v v (w v (y v (v7 v (v6 v v8))))))). [para(48(a,1),51(a,2,2,2,2,2))]. % back CAC tautology: 5475 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (w v (y v (v v (v7 v (v6 v v8))))))). [para(48(a,1),51(a,1,2,2,2,2))]. % back CAC tautology: 5474 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = y v (x v (w v (z v (u v (v6 v (v7 v (v v v8))))))). [para(51(a,2),48(a,1,2,2,2))]. % back CAC tautology: 5473 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = y v (x v (v v (z v (v7 v (u v (w v (v6 v v8))))))). [para(51(a,1),48(a,1,2,2,2))]. % back CAC tautology: 5472 x v (y v (z v (u v (v v (w v v6))))) = w v (u v (x v (y v (z v (v v v6))))). [para(47(a,2),51(a,2,2)),flip(a)]. % back CAC tautology: 5471 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (y v (w v (v6 v (v7 v (v v v8))))))). [para(47(a,2),51(a,2,2,2,2))]. % back CAC tautology: 5470 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v v (w v (v6 v (v7 v (v8 v (y v v9)))))))). [para(47(a,2),51(a,2,2,2,2,2))]. % back CAC tautology: 5469 x v (y v (z v (u v (v v (w v v6))))) = z v (w v (x v (u v (v v (y v v6))))). [para(47(a,1),51(a,2,2))]. % back CAC tautology: 5468 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v6 v (u v (v v (y v (w v v7)))))). [para(47(a,1),51(a,2,2,2))]. % back CAC tautology: 5467 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v7 v (v v (y v (w v (v6 v v8))))))). [para(47(a,1),51(a,2,2,2,2))]. % back CAC tautology: 5466 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v v (v8 v (y v (w v (v6 v (v7 v v9)))))))). [para(47(a,1),51(a,2,2,2,2,2))]. % back CAC tautology: 5465 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (z v (u v (y v (v v (w v v7)))))). [para(47(a,2),51(a,1,2,2))]. % back CAC tautology: 5464 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v7 v (u v (y v (v v (w v (v6 v v8))))))). [para(47(a,2),51(a,1,2,2,2))]. % back CAC tautology: 5463 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v8 v (y v (v v (w v (v6 v (v7 v v9)))))))). [para(47(a,2),51(a,1,2,2,2,2))]. % back CAC tautology: 5462 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (w v (y v (v6 v (v7 v (u v v8))))))). [para(47(a,1),51(a,1,2,2,2))]. % back CAC tautology: 5461 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (w v (y v (v6 v (v7 v (v8 v (v v v9)))))))). [para(47(a,1),51(a,1,2,2,2,2))]. % back CAC tautology: 5460 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (z v (v6 v (y v (u v (w v v7)))))). [para(51(a,2),47(a,2,2,2))]. % back CAC tautology: 5459 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (u v (v7 v (z v (w v (v6 v v8))))))). [para(51(a,2),47(a,2,2,2,2))]. % back CAC tautology: 5458 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (z v (w v (v8 v (u v (v6 v (v7 v v9)))))))). [para(51(a,2),47(a,2,2,2,2,2))]. % back CAC tautology: 5457 x v (y v (z v (u v (v v (w v v6))))) = v v (z v (x v (u v (w v (y v v6))))). [para(51(a,1),47(a,2,2))]. % back CAC tautology: 5456 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (z v (v6 v (u v (v7 v (v8 v (w v v9)))))))). [para(51(a,1),47(a,2,2,2,2,2))]. % back CAC tautology: 5455 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (x v (y v (v v (z v (v6 v (u v v7)))))). [para(51(a,2),47(a,1,2,2))]. % back CAC tautology: 5454 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v6 v (x v (y v (z v (u v (v v (v7 v (v8 v (w v v9)))))))). [para(51(a,2),47(a,1,2,2,2,2))]. % back CAC tautology: 5453 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v7 v (x v (y v (z v (v v (u v (w v (v6 v v8))))))). [para(51(a,1),47(a,1,2,2,2))]. % back CAC tautology: 5452 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = w v (x v (y v (z v (u v (v8 v (v v (v6 v (v7 v v9)))))))). [para(51(a,1),47(a,1,2,2,2,2))]. % back CAC tautology: 5451 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v v (w v (v7 v (v6 v (y v v8))))))). [para(46(a,2),51(a,2,2,2,2,2))]. % back CAC tautology: 5450 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (u v (v6 v (v v (w v (y v v7)))))). [para(46(a,1),51(a,2,2,2,2))]. % back CAC tautology: 5449 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v v (v7 v (y v (v6 v (w v v8))))))). [para(46(a,1),51(a,2,2,2,2,2))]. % back CAC tautology: 5448 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v6 v (u v (y v (w v (v v v7)))))). [para(46(a,2),51(a,1,2,2,2))]. % back CAC tautology: 5447 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v7 v (y v (v v (v6 v (w v v8))))))). [para(46(a,2),51(a,1,2,2,2,2))]. % back CAC tautology: 5446 x v (y v (z v (u v (v v (w v v6))))) = u v (x v (w v (v v (y v (z v v6))))). [para(46(a,1),51(a,1,2,2))]. % back CAC tautology: 5445 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (w v (y v (v7 v (v6 v (v v v8))))))). [para(46(a,1),51(a,1,2,2,2,2))]. % back CAC tautology: 5444 x v (y v (z v (u v (v v (w v v6))))) = u v (v v (y v (x v (w v (z v v6))))). [para(51(a,2),46(a,2,2)),flip(a)]. % back CAC tautology: 5443 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (z v (v v (v7 v (y v (w v (v6 v v8))))))). [para(51(a,2),46(a,2,2,2,2))]. % back CAC tautology: 5442 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (z v (w v (y v (v6 v (v7 v (v v v8))))))). [para(51(a,1),46(a,2,2,2,2))]. % back CAC tautology: 5441 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (x v (z v (y v (u v (v6 v (v7 v (v v v8))))))). [para(51(a,2),46(a,1,2,2,2))]. % back CAC tautology: 5440 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (z v (y v (v7 v (u v (w v (v6 v v8))))))). [para(51(a,1),46(a,1,2,2,2))]. % back CAC tautology: 5439 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v v (w v (v6 v (v8 v (y v (v7 v v9)))))))). [para(45(a,2),51(a,2,2,2,2,2))]. % back CAC tautology: 5438 x v (y v (z v (u v (v v (w v v6))))) = z v (y v (x v (u v (w v (v v v6))))). [para(45(a,1),51(a,2,2))]. % back CAC tautology: 5437 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (w v (u v (v v (v6 v (y v v7)))))). [para(45(a,1),51(a,2,2,2))]. % back CAC tautology: 5436 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v6 v (v v (y v (v7 v (w v v8))))))). [para(45(a,1),51(a,2,2,2,2))]. % back CAC tautology: 5435 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v v (v7 v (y v (w v (v8 v (v6 v v9)))))))). [para(45(a,1),51(a,2,2,2,2,2))]. % back CAC tautology: 5434 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (x v (z v (u v (y v (v6 v (v v v7)))))). [para(45(a,2),51(a,1,2,2))]. % back CAC tautology: 5433 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v6 v (u v (y v (v v (v7 v (w v v8))))))). [para(45(a,2),51(a,1,2,2,2))]. % back CAC tautology: 5432 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (v7 v (y v (v v (w v (v8 v (v6 v v9)))))))). [para(45(a,2),51(a,1,2,2,2,2))]. % back CAC tautology: 5431 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (u v (w v (y v (v6 v (v8 v (v v (v7 v v9)))))))). [para(45(a,1),51(a,1,2,2,2,2))]. % back CAC tautology: 5430 x v (y v (z v (u v (v v (w v v6))))) = u v (y v (w v (x v (v v (z v v6))))). [para(51(a,2),45(a,2,2))]. % back CAC tautology: 5429 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (v v (v6 v (y v (z v (w v v7)))))). [para(51(a,2),45(a,2,2,2))]. % back CAC tautology: 5428 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = u v (x v (y v (v v (w v (v8 v (z v (v6 v (v7 v v9)))))))). [para(51(a,2),45(a,2,2,2,2,2))]. % back CAC tautology: 5427 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (y v (w v (v v (v6 v (v7 v (z v v8))))))). [para(51(a,1),45(a,2,2,2,2))]. % back CAC tautology: 5426 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = u v (x v (y v (v v (v6 v (z v (v7 v (v8 v (w v v9)))))))). [para(51(a,1),45(a,2,2,2,2,2))]. % back CAC tautology: 5425 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (x v (y v (u v (z v (v6 v (v7 v (v v v8))))))). [para(51(a,2),45(a,1,2,2,2))]. % back CAC tautology: 5424 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = u v (x v (y v (v6 v (z v (v v (v7 v (v8 v (w v v9)))))))). [para(51(a,2),45(a,1,2,2,2,2))]. % back CAC tautology: 5423 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = u v (x v (y v (w v (z v (v8 v (v v (v6 v (v7 v v9)))))))). [para(51(a,1),45(a,1,2,2,2,2))]. % back CAC tautology: 5422 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (u v (v6 v (v v (y v (w v v7)))))). [para(38(a,1),51(a,2,2,2,2))]. % back CAC tautology: 5421 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (u v (w v (v v (v6 v (y v v7)))))). [para(36(a,1),51(a,2,2,2,2))]. % back CAC tautology: 5420 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v v (v7 v (y v (w v (v6 v v8))))))). [para(51(a,2),36(a,2,2,2,2))]. % back CAC tautology: 5419 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (w v (y v (v6 v (v7 v (v v v8))))))). [para(51(a,1),36(a,2,2,2,2))]. % back CAC tautology: 5418 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = x v (v v (y v (z v (w v (v6 v (u v v7)))))). [para(51(a,2),39(a,1,2,2))]. % back CAC tautology: 5417 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = x v (u v (y v (v6 v (z v (v v (w v v7)))))). [para(51(a,1),39(a,1,2,2))]. % back CAC tautology: 5416 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (y v (x v (z v (w v (v6 v (u v v7)))))). [para(51(a,2),37(a,1,2,2))]. % back CAC tautology: 5415 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (y v (x v (v6 v (z v (v v (w v v7)))))). [para(51(a,1),37(a,1,2,2))]. % back CAC tautology: 4064 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (w v (x v (y v (v6 v (u v (v v v7)))))). [para(50(a,1),50(a,1,2,2,2))]. % back CAC tautology: 4062 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (z v (x v (y v (v6 v (u v (w v v7)))))). [para(49(a,2),50(a,1,2,2))]. % back CAC tautology: 4061 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (w v (x v (y v (u v (v7 v (v v (v6 v v8))))))). [para(49(a,2),50(a,1,2,2,2))]. % back CAC tautology: 4060 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (w v (x v (y v (z v (v6 v (v v v7)))))). [para(49(a,1),50(a,1,2,2))]. % back CAC tautology: 4059 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (v v (x v (y v (v6 v (u v (v7 v (w v v8))))))). [para(49(a,1),50(a,1,2,2,2))]. % back CAC tautology: 4058 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v v (w v (v6 v (y v (u v v7)))))). [para(50(a,1),49(a,2,2,2,2))]. % back CAC tautology: 4057 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (y v (v6 v (v7 v (u v (w v v8))))))). [para(50(a,1),49(a,2,2,2,2,2))]. % back CAC tautology: 4056 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v6 v (y v (w v (u v (v v v7)))))). [para(50(a,1),49(a,1,2,2,2))]. % back CAC tautology: 4055 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v6 v (y v (u v (v7 v (v v (w v v8))))))). [para(50(a,1),49(a,1,2,2,2,2))]. % back CAC tautology: 4054 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (v v (x v (y v (u v (v6 v (w v v7)))))). [para(48(a,1),50(a,1,2,2,2))]. % back CAC tautology: 4053 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = y v (x v (w v (z v (v6 v (u v (v v v7)))))). [para(50(a,1),48(a,1,2,2,2))]. % back CAC tautology: 4052 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (z v (x v (y v (u v (v v (w v v7)))))). [para(47(a,2),50(a,1,2,2))]. % back CAC tautology: 4051 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (v7 v (x v (y v (u v (v v (w v (v6 v v8))))))). [para(47(a,2),50(a,1,2,2,2))]. % back CAC tautology: 4050 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (v v (x v (y v (w v (v6 v (z v v7)))))). [para(47(a,1),50(a,1,2,2))]. % back CAC tautology: 4049 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (v v (x v (y v (w v (v6 v (v7 v (u v v8))))))). [para(47(a,1),50(a,1,2,2,2))]. % back CAC tautology: 4048 x v (y v (z v (u v (v v (w v v6))))) = v v (x v (u v (w v (y v (z v v6))))). [para(50(a,1),47(a,2,2,2))]. % back CAC tautology: 4047 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (y v (w v (v6 v (z v (u v v7)))))). [para(50(a,1),47(a,2,2,2,2))]. % back CAC tautology: 4046 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (z v (v6 v (v7 v (u v (w v v8))))))). [para(50(a,1),47(a,2,2,2,2,2))]. % back CAC tautology: 4045 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (y v (z v (w v (u v (v v v7)))))). [para(50(a,1),47(a,1,2,2,2))]. % back CAC tautology: 4044 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v6 v (x v (y v (z v (u v (v7 v (v v (w v v8))))))). [para(50(a,1),47(a,1,2,2,2,2))]. % back CAC tautology: 4043 x v (y v (z v (u v (v v (w v v6))))) = w v (z v (x v (y v (v v (u v v6))))). [para(46(a,2),50(a,1,2,2))]. % back CAC tautology: 4042 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (v6 v (x v (y v (u v (w v (v v v7)))))). [para(46(a,2),50(a,1,2,2,2))]. % back CAC tautology: 4041 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (v v (x v (y v (v6 v (w v (u v v7)))))). [para(46(a,1),50(a,1,2,2,2))]. % back CAC tautology: 4040 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (z v (w v (v6 v (y v (v v v7)))))). [para(50(a,1),46(a,2,2,2,2))]. % back CAC tautology: 4039 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (x v (z v (y v (v6 v (u v (v v v7)))))). [para(50(a,1),46(a,1,2,2,2))]. % back CAC tautology: 4038 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (z v (x v (y v (u v (v6 v (v v v7)))))). [para(45(a,2),50(a,1,2,2))]. % back CAC tautology: 4037 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (v6 v (x v (y v (u v (v v (v7 v (w v v8))))))). [para(45(a,2),50(a,1,2,2,2))]. % back CAC tautology: 4036 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (v v (x v (y v (v6 v (z v (w v v7)))))). [para(45(a,1),50(a,1,2,2))]. % back CAC tautology: 4035 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (v v (x v (y v (w v (v7 v (u v (v6 v v8))))))). [para(45(a,1),50(a,1,2,2,2))]. % back CAC tautology: 4034 x v (y v (z v (u v (v v w)))) = u v (v v (z v (x v (y v w)))). [para(50(a,1),45(a,2,2))]. % back CAC tautology: 4033 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (y v (w v (v6 v (v v (z v v7)))))). [para(50(a,1),45(a,2,2,2,2))]. % back CAC tautology: 4032 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (y v (v v (v6 v (v7 v (z v (w v v8))))))). [para(50(a,1),45(a,2,2,2,2,2))]. % back CAC tautology: 4031 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (x v (y v (v6 v (z v (u v (v v v7)))))). [para(50(a,1),45(a,1,2,2,2))]. % back CAC tautology: 4030 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (y v (v6 v (z v (v7 v (v v (w v v8))))))). [para(50(a,1),45(a,1,2,2,2,2))]. % back CAC tautology: 4001 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (v6 v (x v (y v (u v (v v (w v v7)))))). [para(38(a,2),50(a,1,2,2,2))]. % back CAC tautology: 4000 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (v v (x v (y v (w v (v6 v (u v v7)))))). [para(38(a,1),50(a,1,2,2,2))]. % back CAC tautology: 3999 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (y v (w v (v6 v (z v (v v v7)))))). [para(50(a,1),38(a,2,2,2,2))]. % back CAC tautology: 3998 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (x v (y v (z v (v6 v (u v (v v v7)))))). [para(50(a,1),38(a,1,2,2,2))]. % back CAC tautology: 3997 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (w v (x v (y v (u v (v6 v (v v v7)))))). [para(36(a,2),50(a,1,2,2,2))]. % back CAC tautology: 3996 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (v v (x v (y v (v6 v (u v (w v v7)))))). [para(36(a,1),50(a,1,2,2,2))]. % back CAC tautology: 3995 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (u v (w v (v6 v (y v (v v v7)))))). [para(50(a,1),36(a,2,2,2,2))]. % back CAC tautology: 3994 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (w v (y v (v6 v (u v (v v v7)))))). [para(50(a,1),36(a,1,2,2,2))]. % back CAC tautology: 3981 x v (y v (z v (u v (v v (w v v6))))) = z v (u v (x v (y v (w v (v v v6))))). [para(39(a,1),50(a,1,2,2,2))]. % back CAC tautology: 3980 x v (y v (z v (u v (v v (w v v6))))) = x v (v v (y v (w v (z v (u v v6))))). [para(50(a,1),39(a,1,2,2))]. % back CAC tautology: 3979 x v (y v (z v (u v (v v (w v v6))))) = z v (w v (x v (y v (v v (u v v6))))). [para(37(a,1),50(a,1,2,2,2))]. % back CAC tautology: 3978 x v (y v (z v (u v (v v (w v v6))))) = v v (y v (x v (w v (z v (u v v6))))). [para(50(a,1),37(a,1,2,2))]. % back CAC tautology: 3869 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (y v (w v (v v (v6 v (u v v7)))))). [para(49(a,2),49(a,2,2,2))]. % back CAC tautology: 3868 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (u v (v6 v (y v (v7 v (w v v8))))))). [para(49(a,2),49(a,2,2,2,2))]. % back CAC tautology: 3867 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v v (y v (w v (v7 v (u v (v8 v (v6 v v9)))))))). [para(49(a,2),49(a,2,2,2,2,2))]. % back CAC tautology: 3866 x v (y v (z v (u v (v v (w v v6))))) = z v (y v (x v (w v (v v (u v v6))))). [para(49(a,1),49(a,2,2))]. % back CAC tautology: 3865 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (w v (y v (v7 v (u v (v6 v v8))))))). [para(49(a,1),49(a,2,2,2,2))]. % back CAC tautology: 3864 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v v (y v (v6 v (u v (v8 v (w v (v7 v v9)))))))). [para(49(a,1),49(a,2,2,2,2,2))]. % back CAC tautology: 3863 x v (y v (z v (u v (v v w)))) = v v (z v (u v (x v (y v w)))). [para(49(a,2),49(a,1))]. % back CAC tautology: 3862 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (y v (w v (v7 v (v v (v6 v v8))))))). [para(49(a,2),49(a,1,2,2,2))]. % back CAC tautology: 3861 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v6 v (y v (u v (v v (v8 v (w v (v7 v v9)))))))). [para(49(a,2),49(a,1,2,2,2,2))]. % back CAC tautology: 3860 x v (y v (z v (u v (v v (w v v6))))) = v v (x v (w v (z v (y v (u v v6))))). [para(49(a,1),49(a,1,2))]. % back CAC tautology: 3859 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (z v (y v (w v (v6 v (v v v7)))))). [para(49(a,1),49(a,1,2,2))]. % back CAC tautology: 3858 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v6 v (y v (v v (u v (v7 v (w v v8))))))). [para(49(a,1),49(a,1,2,2,2))]. % back CAC tautology: 3857 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (w v (y v (u v (v7 v (v v (v8 v (v6 v v9)))))))). [para(49(a,1),49(a,1,2,2,2,2))]. % back CAC tautology: 3855 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v v (u v (y v (v6 v (w v v7)))))). [para(48(a,1),49(a,2,2,2,2))]. % back CAC tautology: 3854 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (y v (w v (u v (v7 v (v6 v v8))))))). [para(48(a,1),49(a,2,2,2,2,2))]. % back CAC tautology: 3853 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (u v (y v (v v (v6 v (w v v7)))))). [para(48(a,1),49(a,1,2,2,2))]. % back CAC tautology: 3852 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (w v (y v (u v (v v (v7 v (v6 v v8))))))). [para(48(a,1),49(a,1,2,2,2,2))]. % back CAC tautology: 3851 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = y v (x v (w v (z v (u v (v7 v (v v (v6 v v8))))))). [para(49(a,2),48(a,1,2,2,2))]. % back CAC tautology: 3850 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = y v (x v (v v (z v (v6 v (u v (v7 v (w v v8))))))). [para(49(a,1),48(a,1,2,2,2))]. % back CAC tautology: 3849 x v (y v (z v (u v (v v (w v v6))))) = w v (z v (x v (u v (y v (v v v6))))). [para(47(a,2),49(a,2,2)),flip(a)]. % back CAC tautology: 3848 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (u v (w v (v6 v (v7 v (y v v8))))))). [para(47(a,2),49(a,2,2,2,2))]. % back CAC tautology: 3847 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v v (y v (w v (v6 v (v7 v (v8 v (u v v9)))))))). [para(47(a,2),49(a,2,2,2,2,2))]. % back CAC tautology: 3846 x v (y v (z v (u v (v v (w v v6))))) = z v (w v (x v (v v (y v (u v v6))))). [para(47(a,1),49(a,2,2))]. % back CAC tautology: 3845 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v6 v (v v (y v (u v (w v v7)))))). [para(47(a,1),49(a,2,2,2))]. % back CAC tautology: 3844 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (v7 v (y v (u v (w v (v6 v v8))))))). [para(47(a,1),49(a,2,2,2,2))]. % back CAC tautology: 3843 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v v (y v (v8 v (u v (w v (v6 v (v7 v v9)))))))). [para(47(a,1),49(a,2,2,2,2,2))]. % back CAC tautology: 3842 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (u v (y v (z v (v v (w v v7)))))). [para(47(a,2),49(a,1,2,2))]. % back CAC tautology: 3841 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (y v (v7 v (v v (w v (v6 v v8))))))). [para(47(a,2),49(a,1,2,2,2))]. % back CAC tautology: 3840 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v8 v (y v (u v (v v (w v (v6 v (v7 v v9)))))))). [para(47(a,2),49(a,1,2,2,2,2))]. % back CAC tautology: 3839 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (w v (y v (v v (v6 v (v7 v (u v v8))))))). [para(47(a,1),49(a,1,2,2,2))]. % back CAC tautology: 3838 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (w v (y v (u v (v6 v (v7 v (v8 v (v v v9)))))))). [para(47(a,1),49(a,1,2,2,2,2))]. % back CAC tautology: 3837 x v (y v (z v (u v (v v (w v v6))))) = v v (y v (u v (x v (w v (z v v6))))). [para(49(a,2),47(a,2,2))]. % back CAC tautology: 3836 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (z v (w v (y v (v6 v (u v v7)))))). [para(49(a,2),47(a,2,2,2))]. % back CAC tautology: 3835 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (u v (v6 v (z v (v7 v (w v v8))))))). [para(49(a,2),47(a,2,2,2,2))]. % back CAC tautology: 3834 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (z v (w v (v7 v (u v (v8 v (v6 v v9)))))))). [para(49(a,2),47(a,2,2,2,2,2))]. % back CAC tautology: 3833 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v v (x v (y v (z v (v6 v (u v (v8 v (w v (v7 v v9)))))))). [para(49(a,1),47(a,2,2,2,2,2))]. % back CAC tautology: 3832 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (y v (v v (z v (u v (w v v7)))))). [para(49(a,2),47(a,1,2,2))]. % back CAC tautology: 3831 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = v6 v (x v (y v (z v (u v (v v (v8 v (w v (v7 v v9)))))))). [para(49(a,2),47(a,1,2,2,2,2))]. % back CAC tautology: 3830 x v (y v (z v (u v (v v (w v v6))))) = w v (x v (z v (v v (y v (u v v6))))). [para(49(a,1),47(a,1,2))]. % back CAC tautology: 3829 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v6 v (x v (y v (z v (v v (u v (v7 v (w v v8))))))). [para(49(a,1),47(a,1,2,2,2))]. % back CAC tautology: 3828 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = w v (x v (y v (z v (u v (v7 v (v v (v8 v (v6 v v9)))))))). [para(49(a,1),47(a,1,2,2,2,2))]. % back CAC tautology: 3827 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v v (u v (v6 v (w v (y v v7)))))). [para(46(a,2),49(a,2,2,2,2))]. % back CAC tautology: 3826 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (y v (w v (v7 v (v6 v (u v v8))))))). [para(46(a,2),49(a,2,2,2,2,2))]. % back CAC tautology: 3825 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (w v (v v (u v (y v v6))))). [para(46(a,1),49(a,2,2,2))]. % back CAC tautology: 3824 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v v (v6 v (y v (w v (u v v7)))))). [para(46(a,1),49(a,2,2,2,2))]. % back CAC tautology: 3823 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (y v (v7 v (u v (v6 v (w v v8))))))). [para(46(a,1),49(a,2,2,2,2,2))]. % back CAC tautology: 3822 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (u v (y v (v6 v (w v (v v v7)))))). [para(46(a,2),49(a,1,2,2,2))]. % back CAC tautology: 3821 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v7 v (y v (u v (v v (v6 v (w v v8))))))). [para(46(a,2),49(a,1,2,2,2,2))]. % back CAC tautology: 3820 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v6 v (y v (v v (w v (u v v7)))))). [para(46(a,1),49(a,1,2,2,2))]. % back CAC tautology: 3819 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (w v (y v (u v (v7 v (v6 v (v v v8))))))). [para(46(a,1),49(a,1,2,2,2,2))]. % back CAC tautology: 3818 x v (y v (z v (u v (v v (w v v6))))) = u v (w v (y v (x v (z v (v v v6))))). [para(49(a,2),46(a,2,2)),flip(a)]. % back CAC tautology: 3817 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (z v (v v (v6 v (y v (v7 v (w v v8))))))). [para(49(a,2),46(a,2,2,2,2))]. % back CAC tautology: 3816 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (z v (w v (y v (v7 v (v v (v6 v v8))))))). [para(49(a,1),46(a,2,2,2,2))]. % back CAC tautology: 3815 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (x v (z v (y v (u v (v7 v (v v (v6 v v8))))))). [para(49(a,2),46(a,1,2,2,2))]. % back CAC tautology: 3814 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (z v (y v (v6 v (u v (v7 v (w v v8))))))). [para(49(a,1),46(a,1,2,2,2))]. % back CAC tautology: 3813 x v (y v (z v (u v (v v (w v v6))))) = v v (z v (x v (w v (y v (u v v6))))). [para(45(a,2),49(a,2,2)),flip(a)]. % back CAC tautology: 3812 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (u v (w v (v7 v (y v (v6 v v8))))))). [para(45(a,2),49(a,2,2,2,2))]. % back CAC tautology: 3811 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v v (y v (w v (v6 v (v8 v (u v (v7 v v9)))))))). [para(45(a,2),49(a,2,2,2,2,2))]. % back CAC tautology: 3810 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (w v (v v (y v (v6 v (u v v7)))))). [para(45(a,1),49(a,2,2,2))]. % back CAC tautology: 3809 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (v6 v (y v (u v (v7 v (w v v8))))))). [para(45(a,1),49(a,2,2,2,2))]. % back CAC tautology: 3808 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v v (y v (v7 v (u v (w v (v8 v (v6 v v9)))))))). [para(45(a,1),49(a,2,2,2,2,2))]. % back CAC tautology: 3807 x v (y v (z v (u v (v v (w v v6))))) = y v (x v (w v (v v (z v (u v v6))))). [para(45(a,2),49(a,1,2))]. % back CAC tautology: 3806 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (x v (u v (y v (z v (v6 v (v v v7)))))). [para(45(a,2),49(a,1,2,2))]. % back CAC tautology: 3805 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (y v (v6 v (v v (v7 v (w v v8))))))). [para(45(a,2),49(a,1,2,2,2))]. % back CAC tautology: 3804 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (v7 v (y v (u v (v v (w v (v8 v (v6 v v9)))))))). [para(45(a,2),49(a,1,2,2,2,2))]. % back CAC tautology: 3803 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (w v (y v (v v (v7 v (u v (v6 v v8))))))). [para(45(a,1),49(a,1,2,2,2))]. % back CAC tautology: 3802 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = z v (x v (w v (y v (u v (v6 v (v8 v (v v (v7 v v9)))))))). [para(45(a,1),49(a,1,2,2,2,2))]. % back CAC tautology: 3801 x v (y v (z v (u v (v v (w v v6))))) = u v (y v (z v (x v (w v (v v v6))))). [para(49(a,2),45(a,2,2))]. % back CAC tautology: 3800 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (v v (w v (y v (v6 v (z v v7)))))). [para(49(a,2),45(a,2,2,2))]. % back CAC tautology: 3799 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = u v (x v (y v (v v (w v (v7 v (z v (v8 v (v6 v v9)))))))). [para(49(a,2),45(a,2,2,2,2,2))]. % back CAC tautology: 3798 x v (y v (z v (u v (v v (w v v6))))) = u v (v v (x v (w v (y v (z v v6))))). [para(49(a,1),45(a,2,2))]. % back CAC tautology: 3797 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (z v (y v (v6 v (v v (w v v7)))))). [para(49(a,1),45(a,2,2,2))]. % back CAC tautology: 3796 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = u v (x v (y v (w v (v v (v7 v (z v (v6 v v8))))))). [para(49(a,1),45(a,2,2,2,2))]. % back CAC tautology: 3795 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = u v (x v (y v (v v (v6 v (z v (v8 v (w v (v7 v v9)))))))). [para(49(a,1),45(a,2,2,2,2,2))]. % back CAC tautology: 3794 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (y v (v6 v (v v (u v (w v v7)))))). [para(49(a,2),45(a,1,2,2))]. % back CAC tautology: 3793 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (x v (y v (u v (z v (v7 v (v v (v6 v v8))))))). [para(49(a,2),45(a,1,2,2,2))]. % back CAC tautology: 3792 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = u v (x v (y v (v6 v (z v (v v (v8 v (w v (v7 v v9)))))))). [para(49(a,2),45(a,1,2,2,2,2))]. % back CAC tautology: 3791 x v (y v (z v (u v (v v (w v (v6 v (v7 v (v8 v v9)))))))) = u v (x v (y v (w v (z v (v7 v (v v (v8 v (v6 v v9)))))))). [para(49(a,1),45(a,1,2,2,2,2))]. % back CAC tautology: 3786 x v (y v (z v (u v (v v (w v v6))))) = x v (w v (z v (v v (u v (y v v6))))). [para(49(a,1),43(a,2,2)),rewrite(5(13),5(12),5(11),5(10),2709(18))]. % back CAC tautology: 3717 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v v (u v (w v (v6 v (y v v7)))))). [para(38(a,2),49(a,2,2,2,2))]. % back CAC tautology: 3716 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (w v (v v (y v (u v v6))))). [para(38(a,1),49(a,2,2,2))]. % back CAC tautology: 3715 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v v (v6 v (y v (u v (w v v7)))))). [para(38(a,1),49(a,2,2,2,2))]. % back CAC tautology: 3714 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (y v (v7 v (u v (w v (v6 v v8))))))). [para(38(a,1),49(a,2,2,2,2,2))]. % back CAC tautology: 3713 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (u v (y v (v6 v (v v (w v v7)))))). [para(38(a,2),49(a,1,2,2,2))]. % back CAC tautology: 3712 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (w v (y v (v v (v6 v (u v v7)))))). [para(38(a,1),49(a,1,2,2,2))]. % back CAC tautology: 3711 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (w v (y v (u v (v6 v (v7 v (v v v8))))))). [para(38(a,1),49(a,1,2,2,2,2))]. % back CAC tautology: 3710 x v (y v (z v (u v (v v (w v v6))))) = u v (y v (w v (x v (z v (v v v6))))). [para(49(a,2),38(a,2,2)),flip(a)]. % back CAC tautology: 3709 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v v (w v (y v (v6 v (u v v7)))))). [para(36(a,1),49(a,2,2,2,2))]. % back CAC tautology: 3708 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (u v (y v (w v (v6 v (v v v7)))))). [para(36(a,2),49(a,1,2,2,2))]. % back CAC tautology: 3707 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v6 v (y v (v v (u v (w v v7)))))). [para(36(a,1),49(a,1,2,2,2))]. % back CAC tautology: 3706 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (v v (v6 v (y v (v7 v (w v v8))))))). [para(49(a,2),36(a,2,2,2,2))]. % back CAC tautology: 3705 x v (y v (z v (u v (v v (w v v6))))) = z v (y v (x v (w v (u v (v v v6))))). [para(49(a,1),36(a,2,2))]. % back CAC tautology: 3704 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v v (u v (v6 v (y v (w v v7)))))). [para(49(a,1),36(a,2,2,2))]. % back CAC tautology: 3703 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (u v (w v (y v (v7 v (v v (v6 v v8))))))). [para(49(a,1),36(a,2,2,2,2))]. % back CAC tautology: 3702 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (w v (y v (u v (v7 v (v v (v6 v v8))))))). [para(49(a,2),36(a,1,2,2,2))]. % back CAC tautology: 3701 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v v (y v (v6 v (u v (v7 v (w v v8))))))). [para(49(a,1),36(a,1,2,2,2))]. % back CAC tautology: 3672 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = x v (v v (y v (z v (v6 v (u v (w v v7)))))). [para(49(a,2),39(a,1,2,2))]. % back CAC tautology: 3671 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = x v (u v (y v (w v (z v (v6 v (v v v7)))))). [para(49(a,1),39(a,1,2,2))]. % back CAC tautology: 3670 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (v v (w v (u v (y v v6))))). [para(37(a,1),49(a,2,2,2,2))]. % back CAC tautology: 3669 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (y v (x v (z v (v6 v (u v (w v v7)))))). [para(49(a,2),37(a,1,2,2))]. % back CAC tautology: 3668 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (y v (x v (w v (z v (v6 v (v v v7)))))). [para(49(a,1),37(a,1,2,2))]. % back CAC tautology: 3580 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = y v (x v (v v (z v (u v (v6 v (w v v7)))))). [para(48(a,1),48(a,1,2,2,2))]. % back CAC tautology: 3579 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = y v (x v (z v (v6 v (u v (v v (w v v7)))))). [para(47(a,2),48(a,1,2,2))]. % back CAC tautology: 3578 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = y v (x v (v7 v (z v (u v (v v (w v (v6 v v8))))))). [para(47(a,2),48(a,1,2,2,2))]. % back CAC tautology: 3577 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = y v (x v (v6 v (u v (z v (v v (w v v7)))))). [para(47(a,1),48(a,1,2,2)),flip(a)]. % back CAC tautology: 3576 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = y v (x v (v v (z v (w v (v6 v (v7 v (u v v8))))))). [para(47(a,1),48(a,1,2,2,2))]. % back CAC tautology: 3575 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = v v (x v (y v (z v (w v (u v (v7 v (v6 v v8))))))). [para(48(a,1),47(a,2,2,2,2,2))]. % back CAC tautology: 3574 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = w v (x v (y v (z v (u v (v v (v7 v (v6 v v8))))))). [para(48(a,1),47(a,1,2,2,2,2))]. % back CAC tautology: 3573 x v (y v (z v (u v (v v (w v v6))))) = y v (x v (z v (w v (v v (u v v6))))). [para(46(a,2),48(a,1,2,2))]. % back CAC tautology: 3572 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = y v (x v (v6 v (z v (u v (w v (v v v7)))))). [para(46(a,2),48(a,1,2,2,2))]. % back CAC tautology: 3571 x v (y v (z v (u v (v v (w v v6))))) = y v (x v (w v (u v (v v (z v v6))))). [para(46(a,1),48(a,1,2,2))]. % back CAC tautology: 3570 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = y v (x v (v v (z v (v6 v (w v (u v v7)))))). [para(46(a,1),48(a,1,2,2,2))]. % back CAC tautology: 3569 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (z v (v v (y v (v6 v (w v v7)))))). [para(48(a,1),46(a,2,2,2,2))]. % back CAC tautology: 3568 x v (y v (z v (u v (v v (w v (v6