============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 27046 was started by mccune on cleo, Fri Apr 13 09:19:39 2007 The command was "/home/mccune/bin/prover9 -f ba-4basis.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file ba-4basis.in assign(max_seconds,30). 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) # label(goal). [goal]. 2 x v (x ^ y) = x # answer(B1) # label(goal). [goal]. 3 x ^ (y v z) = (x ^ y) v (x ^ z) # answer(DIST1) # label(goal). [goal]. 4 x v (y ^ (x v z)) = x v (z ^ (x v y)) # answer(MOD) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x v (y v z) = y v (x v z) # 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 (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 #10 (T,wt=10): 23 x v (y v x') = y v c_0. [para(17(a,1),5(a,1,2)),flip(a)]. given #11 (T,wt=10): 24 (c_0' v (x v x)')' = x. [para(17(a,1),9(a,1,1,1,1))]. given #12 (T,wt=11): 49 (c_0' v (x v x)') v x = c_0. [para(24(a,1),17(a,1,2))]. given #13 (T,wt=12): 25 ((x v x'')' v c_0')' = x. [para(17(a,1),9(a,1,1,2,1))]. given #14 (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 #15 (T,wt=13): 47 (x v (c_0' v (x v x))')' = c_0'. [para(24(a,1),9(a,1,1,1))]. given #16 (T,wt=13): 68 ((x v x'')' v c_0') v x = c_0. [para(25(a,1),17(a,1,2))]. given #17 (T,wt=13): 85 (x v (x v (c_0' v x))')' = c_0'. [para(24(a,1),19(a,1,1,1))]. given #18 (T,wt=14): 26 ((x v y')' v (x v y)') v x = c_0. [para(9(a,1),17(a,1,2))]. given #19 (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 #20 (T,wt=14): 33 x v (y v (z v x')) = y v (z v c_0). [para(17(a,1),18(a,1,2,2)),flip(a)]. given #21 (T,wt=14): 97 (x v (c_0' v (x v x))') v c_0' = c_0. [para(47(a,1),17(a,1,2))]. given #22 (T,wt=11): 256 x v (c_0' v (x v x))' = c_0. [back_rewrite(243),rewrite(248(10),24(8)),flip(a)]. given #23 (T,wt=11): 260 x v (x v (c_0' v x))' = c_0. [para(5(a,1),256(a,1,2,1))]. given #24 (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 #25 (T,wt=12): 266 (c_0' v (x v x)) v c_0 = x v c_0. [para(256(a,1),23(a,1,2))]. given #26 (T,wt=12): 267 c_0'' v (c_0'' v c_0)' = c_0. [para(23(a,1),256(a,1,2,1))]. given #27 (T,wt=12): 277 (x v (c_0' v x)) v c_0 = x v c_0. [para(260(a,1),23(a,1,2))]. given #28 (T,wt=13): 322 (c_0'' v c_0) v c_0 = c_0'' v c_0. [para(23(a,1),266(a,1,1))]. given #29 (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 #30 (T,wt=15): 28 x v (y v (z v u)) = z v (y v (x v u)). [para(18(a,1),5(a,1))]. given #31 (T,wt=15): 30 x v (y v (z v u)) = x v (z v (y v u)). [para(18(a,2),5(a,1))]. given #32 (T,wt=15): 48 ((c_0' v (x v x)'')' v x)' = c_0'. [para(24(a,1),9(a,1,1,2))]. given #33 (T,wt=15): 52 (c_0' v (x v x)') v (y v x) = y v c_0. [para(24(a,1),23(a,1,2,2))]. given #34 (A,wt=19): 27 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 #35 (T,wt=15): 63 (c_0' v (x' v x')') v c_0 = x v c_0. [para(49(a,1),23(a,1,2)),flip(a)]. given #36 (T,wt=15): 95 (c_0' v (x v (c_0' v (x v x)))')' = x. [para(47(a,1),9(a,1,1,1))]. given #37 (T,wt=15): 106 (c_0' v (c_0' v (x v (x v x)))')' = x. [para(47(a,1),19(a,1,1,1))]. given #38 (T,wt=15): 126 (c_0' v (x v (x v (c_0' v x)))')' = x. [para(85(a,1),9(a,1,1,1))]. given #39 (A,wt=19): 29 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 #40 (T,wt=15): 258 x v (y v (c_0' v (x v x))') = y v c_0. [para(256(a,1),5(a,1,2)),flip(a)]. given #41 (T,wt=15): 273 x v (y v (x v (c_0' v x))') = y v c_0. [para(260(a,1),5(a,1,2)),flip(a)]. given #42 (T,wt=16): 42 ((x v (y v x')')' v (y v c_0)')' = x. [para(23(a,1),9(a,1,1,2,1))]. given #43 (T,wt=16): 45 (c_0' v (x v ((x v y) v y))')' = x v y. [para(5(a,1),24(a,1,1,2,1))]. given #44 (A,wt=21): 31 ((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 #45 (T,wt=9): 963 c_0'' v c_0 = c_0''. [para(322(a,1),45(a,1,1,2,1,2,1)),rewrite(322(14),5(13),322(12),330(14),322(10)),flip(a)]. given #46 (T,wt=13): 999 c_0'' v (x v c_0) = x v c_0''. [back_rewrite(339),rewrite(963(5),963(11))]. given #47 (T,wt=14): 1083 c_0' v (c_0'' v (x v c_0)) = x v c_0. [para(999(a,2),23(a,1,2))]. given #48 (T,wt=14): 1137 c_0'' v (x v (c_0' v c_0)) = x v c_0. [para(1083(a,1),18(a,2))]. given #49 (A,wt=21): 32 ((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 #50 (T,wt=15): 1078 (c_0' v (c_0 v c_0)') v c_0'' = c_0''. [para(963(a,1),52(a,1,2)),rewrite(963(16))]. given #51 (T,wt=12): 1263 (c_0' v c_0''')'' = c_0'. [para(1078(a,1),42(a,1,1,1,1,2,1)),rewrite(49(17),955(11))]. given #52 (T,wt=10): 1266 (c_0' v c_0''')' = c_0. [para(1263(a,1),17(a,1,2)),rewrite(955(11))]. given #53 (T,wt=11): 1272 (c_0' v c_0''') v c_0 = c_0. [para(1266(a,1),17(a,1,2))]. given #54 (A,wt=23): 34 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 #55 (T,wt=15): 1100 (c_0'' v (x v c_0))' = (x v c_0'')'. [para(999(a,2),21(a,2,1)),rewrite(21(12)),flip(a)]. given #56 (T,wt=15): 1271 ((c_0' v c_0'''')' v c_0)' = c_0'. [para(1266(a,1),9(a,1,1,2))]. given #57 (T,wt=15): 1273 (c_0' v c_0''') v (x v c_0) = x v c_0. [para(1266(a,1),23(a,1,2,2))]. given #58 (T,wt=15): 1284 (c_0''' v (c_0' v c_0)')' = c_0''. [para(1266(a,1),42(a,1,1,1,1,2)),rewrite(963(5))]. given #59 (A,wt=19): 35 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 #60 (T,wt=15): 1291 (c_0' v c_0''') v c_0'' = c_0''. [para(1272(a,1),999(a,1,2)),rewrite(963(5)),flip(a)]. given #61 (T,wt=16): 152 ((c_0' v (x v x)'')' v x) v c_0' = c_0. [para(24(a,1),26(a,1,1,2))]. given #62 (T,wt=13): 1707 (c_0' v (x v x)'')' v x = c_0. [para(152(a,1),9(a,1,1,1,1)),rewrite(651(12),24(8)),flip(a)]. given #63 (T,wt=13): 1719 (c_0' v (c_0' v c_0')'')' = c_0. [para(152(a,1),45(a,1,1,2,1,2)),rewrite(463(18),1707(25))]. given #64 (A,wt=23): 36 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 #65 (T,wt=14): 1787 (c_0' v (c_0' v c_0')'') v c_0 = c_0. [para(1719(a,1),17(a,1,2))]. given #66 (T,wt=16): 165 (c_0' v (x v (c_0' v (x v x)))') v x = c_0. [para(47(a,1),26(a,1,1,1))]. given #67 (T,wt=16): 169 (c_0' v (x v (x v (c_0' v x)))') v x = c_0. [para(85(a,1),26(a,1,1,1))]. given #68 (T,wt=16): 687 (c_0' v (c_0' v (x v (x v x)))') v x = c_0. [para(106(a,1),17(a,1,2))]. given #69 (A,wt=19): 37 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 #70 (T,wt=16): 869 (c_0' v (x v x)) v (y v c_0) = x v (y v c_0). [para(258(a,1),33(a,1,2))]. given #71 (T,wt=8): 2392 c_0 v (c_0' v c_0) = c_0. [para(869(a,1),45(a,1,1,2,1,2)),rewrite(5(10),5(9),126(13),5(7)),flip(a)]. given #72 (T,wt=7): 2430 c_0'' = c_0 v c_0. [para(2392(a,1),52(a,1,2)),rewrite(5(11),1157(15))]. given #73 (T,wt=9): 2435 (c_0 v c_0) v c_0 = c_0 v c_0. [para(2392(a,1),1137(a,1,2)),rewrite(2430(3))]. given #74 (A,wt=23): 38 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 #75 (T,wt=12): 2420 c_0 v (x v (c_0' v c_0)) = x v c_0. [para(2392(a,1),5(a,1,2)),flip(a)]. given #76 (T,wt=12): 2423 c_0' v (x v (c_0 v c_0)) = x v c_0. [para(2392(a,1),18(a,1,2)),flip(a)]. given #77 (T,wt=12): 2424 c_0 v (c_0' v (x v c_0)) = x v c_0. [para(2392(a,1),18(a,2,2))]. given #78 (T,wt=12): 2499 ((c_0 v (c_0 v c_0))' v c_0')' = c_0. [back_rewrite(1519),rewrite(2430(5),1707(11),2430(4),2430(15),1707(21))]. given #79 (A,wt=19): 39 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 #80 (T,wt=13): 2498 ((c_0 v (c_0 v c_0))' v c_0') v c_0 = c_0. [back_rewrite(1521),rewrite(2430(5),2430(14),1707(20),2430(13),5(21),1707(20))]. given #81 (T,wt=13): 2588 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0). [back_rewrite(1119),rewrite(2430(3),2430(16),5(17),63(16))]. given #82 (T,wt=13): 2598 (c_0 v (x v c_0))' = (x v (c_0 v c_0))'. [back_rewrite(1100),rewrite(2430(3),2588(6),2430(8))]. given #83 (T,wt=14): 2421 ((c_0 v (c_0' v c_0)')' v c_0')' = c_0. [para(2392(a,1),9(a,1,1,2,1))]. given #84 (A,wt=23): 40 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 #85 (T,wt=14): 2520 (x v (c_0 v c_0)) v (c_0 v (x v c_0))' = c_0. [back_rewrite(1491),rewrite(2430(3),2430(7),2502(11))]. given #86 (T,wt=14): 2570 (c_0 v c_0) v (x v (c_0' v c_0)) = x v c_0. [back_rewrite(1137),rewrite(2430(3))]. given #87 (T,wt=14): 2655 (c_0 v (x v c_0)) v (x v (c_0 v c_0))' = c_0. [back_rewrite(2521),rewrite(2588(6))]. given #88 (T,wt=14): 2674 (c_0' v (c_0 v (c_0 v c_0))')' = c_0 v c_0. [para(2435(a,1),45(a,1,1,2,1,2,1)),rewrite(2435(10),5(9),2435(8),2435(15))]. given #89 (A,wt=19): 41 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 #90 (T,wt=14): 3388 (c_0 v c_0) v (c_0' v (x v c_0)) = x v c_0. [para(5(a,1),2570(a,1,2))]. given #91 (T,wt=15): 2426 ((c_0 v (c_0' v c_0)')' v c_0') v c_0 = c_0. [para(2392(a,1),26(a,1,1,2,1))]. given #92 (T,wt=15): 2531 ((c_0 v c_0)' v (c_0' v c_0)')' = c_0 v c_0. [back_rewrite(1284),rewrite(2430(3),2430(14))]. given #93 (T,wt=15): 2607 ((c_0 v (x v c_0))' v (x v c_0')')' = x. [back_rewrite(1082),rewrite(2430(3),2588(6))]. given #94 (A,wt=18): 43 ((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 #95 (T,wt=11): 3585 c_0' v (c_0' v c_0')' = c_0. [para(49(a,1),2607(a,1,1,2,1)),rewrite(63(12),2499(10)),flip(a)]. given #96 (T,wt=12): 3844 (c_0' v c_0') v c_0 = c_0' v c_0. [para(3585(a,1),23(a,1,2))]. given #97 (T,wt=14): 3594 (c_0' v x')' v (c_0' v x)' = c_0. [para(26(a,1),2607(a,1,1,2,1)),rewrite(149(13),2499(10)),flip(a)]. given #98 (T,wt=15): 2662 (c_0 v (x v c_0)) v c_0 = (x v (c_0 v c_0)) v c_0. [back_rewrite(2503),rewrite(2588(6))]. given #99 (A,wt=18): 44 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 #100 (T,wt=15): 2668 ((x v (c_0 v c_0))' v (x v c_0')')' = x. [para(2430(a,1),9(a,1,1,1,1,2))]. given #101 (T,wt=15): 3842 c_0' v (x v (c_0' v c_0')') = x v c_0. [para(3585(a,1),5(a,1,2)),flip(a)]. given #102 (T,wt=15): 3896 (c_0' v x')' v c_0 = (c_0' v x) v c_0. [para(3594(a,1),23(a,1,2)),flip(a)]. given #103 (T,wt=9): 4245 c_0' v (c_0' v c_0) = c_0. [back_rewrite(3953),rewrite(4153(21),5(20),4126(19))]. given #104 (A,wt=18): 46 ((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 #105 (T,wt=5): 4403 c_0 v c_0 = c_0. [back_rewrite(2426),rewrite(4281(5),4385(5),17(4),4324(7))]. given #106 (T,wt=5): 4538 c_0'' = c_0. [back_rewrite(2430),rewrite(4403(6))]. given #107 (T,wt=6): 4455 c_0' v c_0 = c_0. [back_rewrite(4281),rewrite(4403(7))]. given #108 (T,wt=8): 4452 (c_0' v c_0')' = c_0. [back_rewrite(4294),rewrite(4403(9))]. given #109 (A,wt=22): 50 (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 #110 (T,wt=9): 4406 c_0 v (x v c_0) = x v c_0. [back_rewrite(2420),rewrite(4281(5),4403(4))]. given #111 (T,wt=9): 4450 (c_0' v c_0') v c_0 = c_0. [back_rewrite(4324),rewrite(4403(10))]. given #112 (T,wt=10): 4422 c_0' v (x v c_0) = x v c_0. [back_rewrite(3094),rewrite(4403(6),4403(5),4403(8),4117(8))]. given #113 (T,wt=11): 4718 x v ((x v c_0) v c_0) = x v c_0. [para(869(a,1),50(a,1,1,2,1,2,2)),rewrite(5(11),4535(12),5(10),4531(13),5(9),4535(10)),flip(a)]. given #114 (A,wt=22): 51 (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 #115 (T,wt=12): 4744 (c_0' v (x v c_0)')' = x v c_0. [para(3594(a,1),50(a,1,1,2,1,2,2,1,2)),rewrite(3893(16),4718(7),3594(17))]. given #116 (T,wt=12): 4864 ((x v c_0)' v c_0')' = x v c_0. [para(4744(a,1),42(a,1,1,1,1,2)),rewrite(5(5),4718(5),4455(7))]. given #117 (T,wt=13): 4405 c_0 v (x v (y v c_0)) = x v (y v c_0). [back_rewrite(2422),rewrite(4281(5),4403(4))]. given #118 (T,wt=13): 4526 ((x v c_0)' v (x v c_0')')' = x. [back_rewrite(2668),rewrite(4403(3))]. given #119 (A,wt=17): 53 x v ((c_0' v (x v ((x v y) v y))') v y) = c_0. [para(49(a,1),5(a,1)),rewrite(5(6)),flip(a)]. given #120 (T,wt=13): 4557 (c_0' v c_0') v (x v c_0) = x v c_0. [back_rewrite(4117),rewrite(4422(13))]. given #121 (T,wt=13): 4750 x v ((c_0' v (x v c_0)') v c_0) = c_0. [para(4406(a,1),52(a,1,2)),rewrite(5(7),4718(7),5(9),4403(12))]. given #122 (T,wt=7): 5030 (x v c_0) v c_0 = c_0. [back_rewrite(4996),rewrite(5007(12))]. ============================== PROOF ================================= % Proof 1 at 1.28 (+ 0.02) seconds: CC. % Length of proof is 129. % Level of proof is 37. % Maximum clause weight is 39. % Given clauses 122. 1 x'' = x # answer(CC) # label(goal). [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))]. 29 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))]. 31 ((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))]. 33 x v (y v (z v x')) = y v (z v c_0). [para(17(a,1),18(a,1,2,2)),flip(a)]. 42 ((x v (y v x')')' v (y v c_0)')' = x. [para(23(a,1),9(a,1,1,2,1))]. 44 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)]. 45 (c_0' v (x v ((x v y) v y))')' = x v y. [para(5(a,1),24(a,1,1,2,1))]. 47 (x v (c_0' v (x v x))')' = c_0'. [para(24(a,1),9(a,1,1,1))]. 48 ((c_0' v (x v x)'')' v x)' = c_0'. [para(24(a,1),9(a,1,1,2))]. 49 (c_0' v (x v x)') v x = c_0. [para(24(a,1),17(a,1,2))]. 50 (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))]. 52 (c_0' v (x v x)') v (y v x) = y v c_0. [para(24(a,1),23(a,1,2,2))]. 53 x v ((c_0' v (x v ((x v y) v y))') v y) = c_0. [para(49(a,1),5(a,1)),rewrite(5(6)),flip(a)]. 63 (c_0' v (x' v x')') v c_0 = x v c_0. [para(49(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))]. 85 (x v (x v (c_0' v x))')' = c_0'. [para(24(a,1),19(a,1,1,1))]. 95 (c_0' v (x v (c_0' v (x v x)))')' = x. [para(47(a,1),9(a,1,1,1))]. 97 (x v (c_0' v (x v x))') v c_0' = c_0. [para(47(a,1),17(a,1,2))]. 126 (c_0' v (x v (x v (c_0' v x)))')' = x. [para(85(a,1),9(a,1,1,1))]. 149 ((x' v y')' v (x' v y)') v c_0 = x v c_0. [para(26(a,1),23(a,1,2)),flip(a)]. 152 ((c_0' v (x v x)'')' v x) v c_0' = c_0. [para(24(a,1),26(a,1,1,2))]. 165 (c_0' v (x v (c_0' v (x v x)))') v x = c_0. [para(47(a,1),26(a,1,1,1))]. 169 (c_0' v (x v (x v (c_0' v x)))') v x = c_0. [para(85(a,1),26(a,1,1,1))]. 243 (c_0' v ((x v (c_0' v (x v x))') v c_0)')' = x v (c_0' v (x v x))'. [para(97(a,1),9(a,1,1,1,1))]. 248 (x v (c_0' v (x v x))') v c_0 = c_0 v c_0. [para(97(a,1),23(a,1,2)),flip(a)]. 256 x v (c_0' v (x v x))' = c_0. [back_rewrite(243),rewrite(248(10),24(8)),flip(a)]. 258 x v (y v (c_0' v (x v x))') = y v c_0. [para(256(a,1),5(a,1,2)),flip(a)]. 266 (c_0' v (x v x)) v c_0 = x v c_0. [para(256(a,1),23(a,1,2))]. 267 c_0'' v (c_0'' v c_0)' = c_0. [para(23(a,1),256(a,1,2,1))]. 322 (c_0'' v c_0) v c_0 = c_0'' v c_0. [para(23(a,1),266(a,1,1))]. 330 (c_0' v (c_0'' v (c_0'' v c_0))')' = c_0''. [para(267(a,1),9(a,1,1,1,1))]. 339 (c_0'' v c_0) v (x v c_0) = x v (c_0'' v c_0). [para(267(a,1),33(a,1,2,2))]. 651 ((c_0' v (x v x)'')' v x) v c_0 = c_0 v c_0. [para(48(a,1),63(a,1,1,2,1,1)),rewrite(48(13),63(11)),flip(a)]. 672 (c_0' v (x v ((x v c_0'') v ((x v c_0'') v c_0)))')' = x v c_0''. [para(33(a,1),95(a,1,1,2,1,2)),rewrite(5(13),5(14))]. 712 (c_0' v (x v (x v (c_0' v x)))') v (y v x) = y v c_0. [para(126(a,1),23(a,1,2,2))]. 869 (c_0' v (x v x)) v (y v c_0) = x v (y v c_0). [para(258(a,1),33(a,1,2))]. 955 (c_0' v c_0''')' v c_0' = (c_0' v c_0''')'. [para(68(a,1),45(a,1,1,2,1,2)),rewrite(65(15)),flip(a)]. 963 c_0'' v c_0 = c_0''. [para(322(a,1),45(a,1,1,2,1,2,1)),rewrite(322(14),5(13),322(12),330(14),322(10)),flip(a)]. 999 c_0'' v (x v c_0) = x v c_0''. [back_rewrite(339),rewrite(963(5),963(11))]. 1028 ((x v (y v (z v (u v x')))')' v (z v (y v (u v c_0)))')' = x. [para(33(a,1),31(a,1,1,2,1,2))]. 1078 (c_0' v (c_0 v c_0)') v c_0'' = c_0''. [para(963(a,1),52(a,1,2)),rewrite(963(16))]. 1082 ((c_0'' v (x v c_0))' v (x v c_0')')' = x. [para(999(a,2),9(a,1,1,1,1))]. 1083 c_0' v (c_0'' v (x v c_0)) = x v c_0. [para(999(a,2),23(a,1,2))]. 1119 c_0'' v (x v c_0) = (c_0' v (x' v x')') v c_0''. [para(63(a,1),999(a,1,2))]. 1136 c_0' v (c_0'' v (x v (y v c_0))) = x v (y v c_0). [para(1083(a,1),18(a,2,2))]. 1137 c_0'' v (x v (c_0' v c_0)) = x v c_0. [para(1083(a,1),18(a,2))]. 1157 (c_0' v (c_0' v ((c_0' v c_0) v c_0))') v c_0 = c_0''. [para(49(a,1),1137(a,1,2)),rewrite(963(5),5(14)),flip(a)]. 1263 (c_0' v c_0''')'' = c_0'. [para(1078(a,1),42(a,1,1,1,1,2,1)),rewrite(49(17),955(11))]. 1266 (c_0' v c_0''')' = c_0. [para(1263(a,1),17(a,1,2)),rewrite(955(11))]. 1271 ((c_0' v c_0'''')' v c_0)' = c_0'. [para(1266(a,1),9(a,1,1,2))]. 1284 (c_0''' v (c_0' v c_0)')' = c_0''. [para(1266(a,1),42(a,1,1,1,1,2)),rewrite(963(5))]. 1519 ((((c_0' v c_0'''')' v c_0) v c_0'')' v c_0')' = (c_0' v c_0'''')' v c_0. [para(1271(a,1),25(a,1,1,1,1,2,1))]. 1546 ((c_0''' v (c_0' v c_0)'')' v c_0'')' = c_0'''. [para(1284(a,1),9(a,1,1,2))]. 1707 (c_0' v (x v x)'')' v x = c_0. [para(152(a,1),9(a,1,1,1,1)),rewrite(651(12),24(8)),flip(a)]. 2143 ((x v c_0')' v ((c_0' v (y v (y v (c_0' v y)))') v (x v y))')' = x. [para(169(a,1),19(a,1,1,1,1,2,1))]. 2392 c_0 v (c_0' v c_0) = c_0. [para(869(a,1),45(a,1,1,2,1,2)),rewrite(5(10),5(9),126(13),5(7)),flip(a)]. 2420 c_0 v (x v (c_0' v c_0)) = x v c_0. [para(2392(a,1),5(a,1,2)),flip(a)]. 2426 ((c_0 v (c_0' v c_0)')' v c_0') v c_0 = c_0. [para(2392(a,1),26(a,1,1,2,1))]. 2430 c_0'' = c_0 v c_0. [para(2392(a,1),52(a,1,2)),rewrite(5(11),1157(15))]. 2432 c_0 v (x v (y v (z v (c_0' v c_0)))) = x v (y v (z v c_0)). [para(2392(a,1),29(a,1,2,2,2)),flip(a)]. 2494 (c_0 v (((c_0 v c_0)' v (c_0' v c_0)'')' v c_0))' = (c_0 v c_0)'. [back_rewrite(1546),rewrite(2430(3),2430(15),5(16),2430(20))]. 2499 ((c_0 v (c_0 v c_0))' v c_0')' = c_0. [back_rewrite(1519),rewrite(2430(5),1707(11),2430(4),2430(15),1707(21))]. 2550 (c_0' v (c_0' v ((c_0' v c_0) v c_0))') v c_0 = c_0 v c_0. [back_rewrite(1157),rewrite(2430(18))]. 2571 (c_0 v c_0) v (c_0' v (x v (y v c_0))) = x v (y v c_0). [back_rewrite(1136),rewrite(2430(5),5(10))]. 2588 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0). [back_rewrite(1119),rewrite(2430(3),2430(16),5(17),63(16))]. 2607 ((c_0 v (x v c_0))' v (x v c_0')')' = x. [back_rewrite(1082),rewrite(2430(3),2588(6))]. 2625 (c_0' v (x v ((x v (c_0 v c_0)) v ((x v (c_0 v c_0)) v c_0)))')' = x v (c_0 v c_0). [back_rewrite(672),rewrite(2430(5),2430(9),2430(20))]. 3585 c_0' v (c_0' v c_0')' = c_0. [para(49(a,1),2607(a,1,1,2,1)),rewrite(63(12),2499(10)),flip(a)]. 3594 (c_0' v x')' v (c_0' v x)' = c_0. [para(26(a,1),2607(a,1,1,2,1)),rewrite(149(13),2499(10)),flip(a)]. 3842 c_0' v (x v (c_0' v c_0')') = x v c_0. [para(3585(a,1),5(a,1,2)),flip(a)]. 3844 (c_0' v c_0') v c_0 = c_0' v c_0. [para(3585(a,1),23(a,1,2))]. 3854 (c_0' v ((c_0' v c_0')' v ((c_0' v c_0')' v c_0))') v (c_0' v c_0')' = c_0. [para(3585(a,1),169(a,1,1,2,1,2,2))]. 3893 (c_0' v x')' v (y v (z v (c_0' v x)')) = y v (z v c_0). [para(3594(a,1),18(a,1,2,2)),flip(a)]. 3896 (c_0' v x')' v c_0 = (c_0' v x) v c_0. [para(3594(a,1),23(a,1,2)),flip(a)]. 3953 (c_0' v ((c_0' v c_0) v ((c_0' v c_0) v c_0))') v (c_0' v c_0')' = c_0. [back_rewrite(3854),rewrite(3896(16),5(15),3896(14))]. 4055 (((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(44(a,1),22(a,1,1,1,1,2,1,1))]. 4126 (c_0' v ((c_0' v c_0) v ((c_0' v c_0) v c_0))') v c_0 = c_0' v c_0. [para(165(a,1),3842(a,1,2)),rewrite(3842(28),3896(20),5(19),3896(18)),flip(a)]. 4153 (c_0' v c_0')' = c_0' v c_0. [para(3896(a,1),21(a,1,1,2,1,2)),rewrite(45(14)),flip(a)]. 4245 c_0' v (c_0' v c_0) = c_0. [back_rewrite(3953),rewrite(4153(21),5(20),4126(19))]. 4281 c_0' v c_0 = c_0 v c_0. [para(4245(a,1),52(a,1,2)),rewrite(5(11),2550(15)),flip(a)]. 4282 c_0 v (c_0 v c_0) = c_0. [para(52(a,2),4245(a,1,2)),rewrite(5(11),49(10),4281(6),5(6),4281(5))]. 4324 (c_0' v c_0') v c_0 = c_0 v c_0. [back_rewrite(3844),rewrite(4281(11))]. 4385 (c_0 v c_0)' = c_0'. [back_rewrite(2494),rewrite(4281(9),17(11),4281(5),4282(5)),flip(a)]. 4400 c_0 v (x v (y v (z v (c_0 v c_0)))) = x v (y v (z v c_0)). [back_rewrite(2432),rewrite(4281(5))]. 4403 c_0 v c_0 = c_0. [back_rewrite(2426),rewrite(4281(5),4385(5),17(4),4324(7))]. 4406 c_0 v (x v c_0) = x v c_0. [back_rewrite(2420),rewrite(4281(5),4403(4))]. 4439 c_0 v (x v (y v (z v c_0))) = x v (y v (z v c_0)). [back_rewrite(4400),rewrite(4403(4))]. 4455 c_0' v c_0 = c_0. [back_rewrite(4281),rewrite(4403(7))]. 4531 (c_0' v (x v ((x v c_0) v ((x v c_0) v c_0)))')' = x v c_0. [back_rewrite(2625),rewrite(4403(5),4403(7),4403(16))]. 4535 c_0' v (x v (y v c_0)) = x v (y v c_0). [back_rewrite(2571),rewrite(4403(3),4439(8))]. 4538 c_0'' = c_0. [back_rewrite(2430),rewrite(4403(6))]. 4718 x v ((x v c_0) v c_0) = x v c_0. [para(869(a,1),50(a,1,1,2,1,2,2)),rewrite(5(11),4535(12),5(10),4531(13),5(9),4535(10)),flip(a)]. 4744 (c_0' v (x v c_0)')' = x v c_0. [para(3594(a,1),50(a,1,1,2,1,2,2,1,2)),rewrite(3893(16),4718(7),3594(17))]. 4750 x v ((c_0' v (x v c_0)') v c_0) = c_0. [para(4406(a,1),52(a,1,2)),rewrite(5(7),4718(7),5(9),4403(12))]. 4755 x v (y v ((x v c_0) v c_0)) = y v (x v c_0). [para(4718(a,1),5(a,1,2)),flip(a)]. 4864 ((x v c_0)' v c_0')' = x v c_0. [para(4744(a,1),42(a,1,1,1,1,2)),rewrite(5(5),4718(5),4455(7))]. 4877 ((x v (y v c_0))' v ((y v c_0)' v (x v c_0'))')' = x. [para(4864(a,1),19(a,1,1,1,1,2))]. 4887 ((x v c_0)' v ((x v c_0) v ((x v c_0)' v c_0))')' = x v c_0. [para(4864(a,1),21(a,1,1,2,1,2,1)),rewrite(5(11),4864(21))]. 4895 ((x v c_0)' v ((x v c_0)' v c_0)')' = c_0. [para(4864(a,1),42(a,1,1,1,1,2)),rewrite(4406(4))]. 4996 x v ((x v c_0) v ((c_0' v (x v c_0)') v c_0)) = c_0. [para(4718(a,1),53(a,1,2,1,2,1,2,1)),rewrite(4755(10),5(7),4718(7),5(11))]. 5007 x v (y v ((c_0' v (x v c_0)') v c_0)) = y v c_0. [para(4750(a,1),5(a,1,2)),flip(a)]. 5015 (((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(4750(a,1),22(a,1,1,1,1,2,1,1)),rewrite(4538(14))]. 5030 (x v c_0) v c_0 = c_0. [back_rewrite(4996),rewrite(5007(12))]. 5048 (x v c_0) v (y v c_0) = y v c_0. [para(5030(a,1),5(a,1,2)),flip(a)]. 5064 x v c_0 = c_0. [back_rewrite(4887),rewrite(5048(11),4895(11)),flip(a)]. 5068 (c_0' v x)' = (x v c_0')'. [back_rewrite(5015),rewrite(5064(4),5064(7),5064(6),5064(8),5064(11))]. 5097 (c_0' v (c_0' v (x v c_0'))')' = x. [back_rewrite(4877),rewrite(5064(2),5064(2),5064(4))]. 5194 (x v (y v (z v (u v x')))')' = (c_0' v x)'. [back_rewrite(4055),rewrite(5064(9),5064(9),5064(9),4538(10),5064(9)),flip(a)]. 5645 (c_0' v (c_0' v x)')' = x. [back_rewrite(1028),rewrite(5194(7),5064(6),5064(6),5064(6),5068(8,R))]. 5725 (c_0' v (x v (x v (c_0' v x)))') v (y v x) = c_0. [back_rewrite(712),rewrite(5064(13))]. 5895 x v c_0' = x. [back_rewrite(5097),rewrite(5645(11))]. 5925 x'' = x. [back_rewrite(2143),rewrite(5895(3),5725(12),5895(4))]. 5926 $F # answer(CC). [resolve(5925,a,10,a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 2 at 1.37 (+ 0.02) seconds: B1. % Length of proof is 154. % Level of proof is 41. % Maximum clause weight is 86. % Given clauses 122. 2 x v (x ^ y) = x # answer(B1) # label(goal). [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 (u v v))) = z v (x v (u v (y v v))). [para(18(a,1),5(a,1,2))]. 29 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))]. 31 ((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))]. 33 x v (y v (z v x')) = y v (z v c_0). [para(17(a,1),18(a,1,2,2)),flip(a)]. 42 ((x v (y v x')')' v (y v c_0)')' = x. [para(23(a,1),9(a,1,1,2,1))]. 44 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)]. 45 (c_0' v (x v ((x v y) v y))')' = x v y. [para(5(a,1),24(a,1,1,2,1))]. 46 ((x v y)' v (x v (c_0' v (y v y)'))')' = x. [para(24(a,1),9(a,1,1,1,1,2))]. 47 (x v (c_0' v (x v x))')' = c_0'. [para(24(a,1),9(a,1,1,1))]. 48 ((c_0' v (x v x)'')' v x)' = c_0'. [para(24(a,1),9(a,1,1,2))]. 49 (c_0' v (x v x)') v x = c_0. [para(24(a,1),17(a,1,2))]. 50 (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))]. 52 (c_0' v (x v x)') v (y v x) = y v c_0. [para(24(a,1),23(a,1,2,2))]. 53 x v ((c_0' v (x v ((x v y) v y))') v y) = c_0. [para(49(a,1),5(a,1)),rewrite(5(6)),flip(a)]. 63 (c_0' v (x' v x')') v c_0 = x v c_0. [para(49(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))]. 85 (x v (x v (c_0' v x))')' = c_0'. [para(24(a,1),19(a,1,1,1))]. 95 (c_0' v (x v (c_0' v (x v x)))')' = x. [para(47(a,1),9(a,1,1,1))]. 97 (x v (c_0' v (x v x))') v c_0' = c_0. [para(47(a,1),17(a,1,2))]. 108 (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))]. 126 (c_0' v (x v (x v (c_0' v x)))')' = x. [para(85(a,1),9(a,1,1,1))]. 149 ((x' v y')' v (x' v y)') v c_0 = x v c_0. [para(26(a,1),23(a,1,2)),flip(a)]. 152 ((c_0' v (x v x)'')' v x) v c_0' = c_0. [para(24(a,1),26(a,1,1,2))]. 165 (c_0' v (x v (c_0' v (x v x)))') v x = c_0. [para(47(a,1),26(a,1,1,1))]. 169 (c_0' v (x v (x v (c_0' v x)))') v x = c_0. [para(85(a,1),26(a,1,1,1))]. 243 (c_0' v ((x v (c_0' v (x v x))') v c_0)')' = x v (c_0' v (x v x))'. [para(97(a,1),9(a,1,1,1,1))]. 248 (x v (c_0' v (x v x))') v c_0 = c_0 v c_0. [para(97(a,1),23(a,1,2)),flip(a)]. 256 x v (c_0' v (x v x))' = c_0. [back_rewrite(243),rewrite(248(10),24(8)),flip(a)]. 258 x v (y v (c_0' v (x v x))') = y v c_0. [para(256(a,1),5(a,1,2)),flip(a)]. 266 (c_0' v (x v x)) v c_0 = x v c_0. [para(256(a,1),23(a,1,2))]. 267 c_0'' v (c_0'' v c_0)' = c_0. [para(23(a,1),256(a,1,2,1))]. 322 (c_0'' v c_0) v c_0 = c_0'' v c_0. [para(23(a,1),266(a,1,1))]. 330 (c_0' v (c_0'' v (c_0'' v c_0))')' = c_0''. [para(267(a,1),9(a,1,1,1,1))]. 339 (c_0'' v c_0) v (x v c_0) = x v (c_0'' v c_0). [para(267(a,1),33(a,1,2,2))]. 523 (((x v c_0')' v ((c_0' v (y v y)') v (x v y))'')' v x)' = (x v c_0')'. [para(52(a,2),22(a,1,1,1,1,2,1,1))]. 651 ((c_0' v (x v x)'')' v x) v c_0 = c_0 v c_0. [para(48(a,1),63(a,1,1,2,1,1)),rewrite(48(13),63(11)),flip(a)]. 672 (c_0' v (x v ((x v c_0'') v ((x v c_0'') v c_0)))')' = x v c_0''. [para(33(a,1),95(a,1,1,2,1,2)),rewrite(5(13),5(14))]. 682 (c_0' v (c_0' v (x v ((x v y) v ((x v y) v y))))')' = x v y. [para(27(a,2),95(a,1,1,2,1))]. 712 (c_0' v (x v (x v (c_0' v x)))') v (y v x) = y v c_0. [para(126(a,1),23(a,1,2,2))]. 869 (c_0' v (x v x)) v (y v c_0) = x v (y v c_0). [para(258(a,1),33(a,1,2))]. 935 ((x v (x' v y')')' v (((x' v y')' v (x' v y)'')' v c_0)')' = x. [para(22(a,1),42(a,1,1,1,1,2))]. 955 (c_0' v c_0''')' v c_0' = (c_0' v c_0''')'. [para(68(a,1),45(a,1,1,2,1,2)),rewrite(65(15)),flip(a)]. 963 c_0'' v c_0 = c_0''. [para(322(a,1),45(a,1,1,2,1,2,1)),rewrite(322(14),5(13),322(12),330(14),322(10)),flip(a)]. 999 c_0'' v (x v c_0) = x v c_0''. [back_rewrite(339),rewrite(963(5),963(11))]. 1028 ((x v (y v (z v (u v x')))')' v (z v (y v (u v c_0)))')' = x. [para(33(a,1),31(a,1,1,2,1,2))]. 1078 (c_0' v (c_0 v c_0)') v c_0'' = c_0''. [para(963(a,1),52(a,1,2)),rewrite(963(16))]. 1082 ((c_0'' v (x v c_0))' v (x v c_0')')' = x. [para(999(a,2),9(a,1,1,1,1))]. 1083 c_0' v (c_0'' v (x v c_0)) = x v c_0. [para(999(a,2),23(a,1,2))]. 1119 c_0'' v (x v c_0) = (c_0' v (x' v x')') v c_0''. [para(63(a,1),999(a,1,2))]. 1136 c_0' v (c_0'' v (x v (y v c_0))) = x v (y v c_0). [para(1083(a,1),18(a,2,2))]. 1137 c_0'' v (x v (c_0' v c_0)) = x v c_0. [para(1083(a,1),18(a,2))]. 1157 (c_0' v (c_0' v ((c_0' v c_0) v c_0))') v c_0 = c_0''. [para(49(a,1),1137(a,1,2)),rewrite(963(5),5(14)),flip(a)]. 1263 (c_0' v c_0''')'' = c_0'. [para(1078(a,1),42(a,1,1,1,1,2,1)),rewrite(49(17),955(11))]. 1266 (c_0' v c_0''')' = c_0. [para(1263(a,1),17(a,1,2)),rewrite(955(11))]. 1271 ((c_0' v c_0'''')' v c_0)' = c_0'. [para(1266(a,1),9(a,1,1,2))]. 1284 (c_0''' v (c_0' v c_0)')' = c_0''. [para(1266(a,1),42(a,1,1,1,1,2)),rewrite(963(5))]. 1519 ((((c_0' v c_0'''')' v c_0) v c_0'')' v c_0')' = (c_0' v c_0'''')' v c_0. [para(1271(a,1),25(a,1,1,1,1,2,1))]. 1546 ((c_0''' v (c_0' v c_0)'')' v c_0'')' = c_0'''. [para(1284(a,1),9(a,1,1,2))]. 1707 (c_0' v (x v x)'')' v x = c_0. [para(152(a,1),9(a,1,1,1,1)),rewrite(651(12),24(8)),flip(a)]. 2055 (((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(165(a,1),20(a,1,1,2,1)),rewrite(5(23),5(25),5(24),5(56),5(58),5(57))]. 2143 ((x v c_0')' v ((c_0' v (y v (y v (c_0' v y)))') v (x v y))')' = x. [para(169(a,1),19(a,1,1,1,1,2,1))]. 2392 c_0 v (c_0' v c_0) = c_0. [para(869(a,1),45(a,1,1,2,1,2)),rewrite(5(10),5(9),126(13),5(7)),flip(a)]. 2420 c_0 v (x v (c_0' v c_0)) = x v c_0. [para(2392(a,1),5(a,1,2)),flip(a)]. 2426 ((c_0 v (c_0' v c_0)')' v c_0') v c_0 = c_0. [para(2392(a,1),26(a,1,1,2,1))]. 2430 c_0'' = c_0 v c_0. [para(2392(a,1),52(a,1,2)),rewrite(5(11),1157(15))]. 2432 c_0 v (x v (y v (z v (c_0' v c_0)))) = x v (y v (z v c_0)). [para(2392(a,1),29(a,1,2,2,2)),flip(a)]. 2494 (c_0 v (((c_0 v c_0)' v (c_0' v c_0)'')' v c_0))' = (c_0 v c_0)'. [back_rewrite(1546),rewrite(2430(3),2430(15),5(16),2430(20))]. 2499 ((c_0 v (c_0 v c_0))' v c_0')' = c_0. [back_rewrite(1519),rewrite(2430(5),1707(11),2430(4),2430(15),1707(21))]. 2550 (c_0' v (c_0' v ((c_0' v c_0) v c_0))') v c_0 = c_0 v c_0. [back_rewrite(1157),rewrite(2430(18))]. 2571 (c_0 v c_0) v (c_0' v (x v (y v c_0))) = x v (y v c_0). [back_rewrite(1136),rewrite(2430(5),5(10))]. 2588 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0). [back_rewrite(1119),rewrite(2430(3),2430(16),5(17),63(16))]. 2607 ((c_0 v (x v c_0))' v (x v c_0')')' = x. [back_rewrite(1082),rewrite(2430(3),2588(6))]. 2625 (c_0' v (x v ((x v (c_0 v c_0)) v ((x v (c_0 v c_0)) v c_0)))')' = x v (c_0 v c_0). [back_rewrite(672),rewrite(2430(5),2430(9),2430(20))]. 2640 ((c_0 v ((x v x'')' v c_0))' v x)' = (x v x'')'. [back_rewrite(66),rewrite(2430(7),5(8))]. 3585 c_0' v (c_0' v c_0')' = c_0. [para(49(a,1),2607(a,1,1,2,1)),rewrite(63(12),2499(10)),flip(a)]. 3594 (c_0' v x')' v (c_0' v x)' = c_0. [para(26(a,1),2607(a,1,1,2,1)),rewrite(149(13),2499(10)),flip(a)]. 3842 c_0' v (x v (c_0' v c_0')') = x v c_0. [para(3585(a,1),5(a,1,2)),flip(a)]. 3844 (c_0' v c_0') v c_0 = c_0' v c_0. [para(3585(a,1),23(a,1,2))]. 3854 (c_0' v ((c_0' v c_0')' v ((c_0' v c_0')' v c_0))') v (c_0' v c_0')' = c_0. [para(3585(a,1),169(a,1,1,2,1,2,2))]. 3893 (c_0' v x')' v (y v (z v (c_0' v x)')) = y v (z v c_0). [para(3594(a,1),18(a,1,2,2)),flip(a)]. 3896 (c_0' v x')' v c_0 = (c_0' v x) v c_0. [para(3594(a,1),23(a,1,2)),flip(a)]. 3953 (c_0' v ((c_0' v c_0) v ((c_0' v c_0) v c_0))') v (c_0' v c_0')' = c_0. [back_rewrite(3854),rewrite(3896(16),5(15),3896(14))]. 4055 (((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(44(a,1),22(a,1,1,1,1,2,1,1))]. 4126 (c_0' v ((c_0' v c_0) v ((c_0' v c_0) v c_0))') v c_0 = c_0' v c_0. [para(165(a,1),3842(a,1,2)),rewrite(3842(28),3896(20),5(19),3896(18)),flip(a)]. 4153 (c_0' v c_0')' = c_0' v c_0. [para(3896(a,1),21(a,1,1,2,1,2)),rewrite(45(14)),flip(a)]. 4245 c_0' v (c_0' v c_0) = c_0. [back_rewrite(3953),rewrite(4153(21),5(20),4126(19))]. 4281 c_0' v c_0 = c_0 v c_0. [para(4245(a,1),52(a,1,2)),rewrite(5(11),2550(15)),flip(a)]. 4282 c_0 v (c_0 v c_0) = c_0. [para(52(a,2),4245(a,1,2)),rewrite(5(11),49(10),4281(6),5(6),4281(5))]. 4324 (c_0' v c_0') v c_0 = c_0 v c_0. [back_rewrite(3844),rewrite(4281(11))]. 4385 (c_0 v c_0)' = c_0'. [back_rewrite(2494),rewrite(4281(9),17(11),4281(5),4282(5)),flip(a)]. 4400 c_0 v (x v (y v (z v (c_0 v c_0)))) = x v (y v (z v c_0)). [back_rewrite(2432),rewrite(4281(5))]. 4403 c_0 v c_0 = c_0. [back_rewrite(2426),rewrite(4281(5),4385(5),17(4),4324(7))]. 4406 c_0 v (x v c_0) = x v c_0. [back_rewrite(2420),rewrite(4281(5),4403(4))]. 4439 c_0 v (x v (y v (z v c_0))) = x v (y v (z v c_0)). [back_rewrite(4400),rewrite(4403(4))]. 4455 c_0' v c_0 = c_0. [back_rewrite(4281),rewrite(4403(7))]. 4531 (c_0' v (x v ((x v c_0) v ((x v c_0) v c_0)))')' = x v c_0. [back_rewrite(2625),rewrite(4403(5),4403(7),4403(16))]. 4535 c_0' v (x v (y v c_0)) = x v (y v c_0). [back_rewrite(2571),rewrite(4403(3),4439(8))]. 4538 c_0'' = c_0. [back_rewrite(2430),rewrite(4403(6))]. 4544 (((x v x'')' v c_0)' v x)' = (x v x'')'. [back_rewrite(2640),rewrite(4406(8))]. 4638 (((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(165(a,1),46(a,1,1,2,1)),rewrite(5(20),5(22),5(21),5(50),5(52),5(51))]. 4718 x v ((x v c_0) v c_0) = x v c_0. [para(869(a,1),50(a,1,1,2,1,2,2)),rewrite(5(11),4535(12),5(10),4531(13),5(9),4535(10)),flip(a)]. 4744 (c_0' v (x v c_0)')' = x v c_0. [para(3594(a,1),50(a,1,1,2,1,2,2,1,2)),rewrite(3893(16),4718(7),3594(17))]. 4750 x v ((c_0' v (x v c_0)') v c_0) = c_0. [para(4406(a,1),52(a,1,2)),rewrite(5(7),4718(7),5(9),4403(12))]. 4755 x v (y v ((x v c_0) v c_0)) = y v (x v c_0). [para(4718(a,1),5(a,1,2)),flip(a)]. 4864 ((x v c_0)' v c_0')' = x v c_0. [para(4744(a,1),42(a,1,1,1,1,2)),rewrite(5(5),4718(5),4455(7))]. 4877 ((x v (y v c_0))' v ((y v c_0)' v (x v c_0'))')' = x. [para(4864(a,1),19(a,1,1,1,1,2))]. 4887 ((x v c_0)' v ((x v c_0) v ((x v c_0)' v c_0))')' = x v c_0. [para(4864(a,1),21(a,1,1,2,1,2,1)),rewrite(5(11),4864(21))]. 4895 ((x v c_0)' v ((x v c_0)' v c_0)')' = c_0. [para(4864(a,1),42(a,1,1,1,1,2)),rewrite(4406(4))]. 4996 x v ((x v c_0) v ((c_0' v (x v c_0)') v c_0)) = c_0. [para(4718(a,1),53(a,1,2,1,2,1,2,1)),rewrite(4755(10),5(7),4718(7),5(11))]. 5007 x v (y v ((c_0' v (x v c_0)') v c_0)) = y v c_0. [para(4750(a,1),5(a,1,2)),flip(a)]. 5015 (((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(4750(a,1),22(a,1,1,1,1,2,1,1)),rewrite(4538(14))]. 5030 (x v c_0) v c_0 = c_0. [back_rewrite(4996),rewrite(5007(12))]. 5048 (x v c_0) v (y v c_0) = y v c_0. [para(5030(a,1),5(a,1,2)),flip(a)]. 5064 x v c_0 = c_0. [back_rewrite(4887),rewrite(5048(11),4895(11)),flip(a)]. 5068 (c_0' v x)' = (x v c_0')'. [back_rewrite(5015),rewrite(5064(4),5064(7),5064(6),5064(8),5064(11))]. 5097 (c_0' v (c_0' v (x v c_0'))')' = x. [back_rewrite(4877),rewrite(5064(2),5064(2),5064(4))]. 5147 (x v x'')' = (c_0' v x)'. [back_rewrite(4544),rewrite(5064(6)),flip(a)]. 5194 (x v (y v (z v (u v x')))')' = (c_0' v x)'. [back_rewrite(4055),rewrite(5064(9),5064(9),5064(9),4538(10),5064(9)),flip(a)]. 5645 (c_0' v (c_0' v x)')' = x. [back_rewrite(1028),rewrite(5194(7),5064(6),5064(6),5064(6),5068(8,R))]. 5662 (c_0' v (x v (x' v y')')')' = x. [back_rewrite(935),rewrite(5064(18),5068(10,R))]. 5725 (c_0' v (x v (x v (c_0' v x)))') v (y v x) = c_0. [back_rewrite(712),rewrite(5064(13))]. 5787 (c_0' v (x v x)') v (y v x) = c_0. [back_rewrite(52),rewrite(5064(9))]. 5801 (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(4638),rewrite(5068(30,R))]. 5818 (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(2055),rewrite(5068(33,R))]. 5888 (c_0' v (((c_0' v x')' v c_0') v x)')' = (c_0' v x')' v c_0'. [back_rewrite(108),rewrite(5147(8),5147(20))]. 5895 x v c_0' = x. [back_rewrite(5097),rewrite(5645(11))]. 5918 x v ((x v y) v ((x v y) v y)) = x v y. [back_rewrite(682),rewrite(5645(13))]. 5925 x'' = x. [back_rewrite(2143),rewrite(5895(3),5725(12),5895(4))]. 5934 (c_0' v x)' = x'. [back_rewrite(523),rewrite(5895(3),5787(8),5925(4),5064(3),5895(7))]. 5943 x v x = x. [back_rewrite(5888),rewrite(5934(7),5925(4),5895(5),5934(6),5925(3),5934(6),5925(3),5895(4))]. 6069 (c_0' v x) v x = c_0' v x. [back_rewrite(5818),rewrite(5918(26),5934(14),9(11),5934(9),5925(6),5918(28),5934(16),9(13))]. 6071 c_0' v x = x. [back_rewrite(5801),rewrite(5943(11),5943(15),5943(17),6069(18),5943(17),5934(15),5934(12),5934(9),5925(6),6069(6),5934(6),5934(5),5925(2),5943(9),5943(13),5943(15),6069(16),5943(15),5934(13),5934(10),5934(7),5925(4)),flip(a)]. 6094 x v (x' v y')' = x. [back_rewrite(5662),rewrite(6071(9),5925(7))]. 6095 $F # answer(B1). [resolve(6094,a,12,a)]. ============================== end of proof ========================== % Redundant proof: 6385 $F # answer(CC). [back_rewrite(10),rewrite(5925(3)),xx(a)]. % Redundant proof: 6491 $F # answer(B1). [back_rewrite(12),rewrite(6094(8)),xx(a)]. % Disable descendants (x means already disabled): 11x 12x 10x given #123 (T,wt=5): 5064 x v c_0 = c_0. [back_rewrite(4887),rewrite(5048(11),4895(11)),flip(a)]. given #124 (A,wt=25): 71 ((x v y)' v (x v ((y v (z v u)')' v (z v (y v u))'))')' = x. [para(19(a,1),9(a,1,1,1,1,2))]. given #125 (T,wt=5): 5925 x'' = x. [back_rewrite(2143),rewrite(5895(3),5725(12),5895(4))]. given #126 (T,wt=5): 5943 x v x = x. [back_rewrite(5888),rewrite(5934(7),5925(4),5895(5),5934(6),5925(3),5934(6),5925(3),5895(4))]. given #127 (T,wt=5): 6013 c_0 v x = c_0. [back_rewrite(5175),rewrite(5895(5),5925(4),5934(4),5937(2),5895(4))]. given #128 (T,wt=6): 5895 x v c_0' = x. [back_rewrite(5097),rewrite(5645(11))]. % Operation v is commutative; C redundancy checks enabled. given #129 (A,wt=25): 76 ((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 #130 (T,wt=6): 6071 c_0' v x = x. [back_rewrite(5801),rewrite(5943(11),5943(15),5943(17),6069(18),5943(17),5934(15),5934(12),5934(9),5925(6),6069(6),5934(6),5934(5),5925(2),5943(9),5943(13),5943(15),6069(16),5943(15),5934(13),5934(10),5934(7),5925(4)),flip(a)]. given #131 (T,wt=7): 6650 x v y = y v x. [para(5895(a,1),5(a,1,2)),rewrite(5895(4))]. given #132 (T,wt=8): 5791 x v (y v x') = c_0. [back_rewrite(23),rewrite(5064(5))]. given #133 (T,wt=8): 6789 x v (x' v y) = c_0. [back_rewrite(6277),rewrite(6650(9),6595(9),6650(8),6675(8),6650(10),6588(10),6651(3))]. given #134 (A,wt=25): 77 ((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 #135 (T,wt=9): 6595 x v (y v x')' = x. [back_rewrite(6085),rewrite(6586(10))]. given #136 (T,wt=9): 6612 x v (y v x) = y v x. [para(5943(a,1),5(a,1,2)),flip(a)]. given #137 (T,wt=9): 6844 x v (x v y) = x v y. [back_rewrite(6086),rewrite(6650(2))]. given #138 (T,wt=9): 7281 x v (x' v y)' = x. [para(6650(a,1),6595(a,1,2,1))]. given #139 (A,wt=21): 78 ((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 #140 (T,wt=10): 5790 x v (y v (z v x')) = c_0. [back_rewrite(33),rewrite(5064(6),5064(6))]. given #141 (T,wt=10): 5974 x' v (y v x)' = x'. [back_rewrite(5781),rewrite(5934(6),5895(6),5934(9),5925(6),5934(8),5895(8))]. given #142 (T,wt=8): 7414 (x v y) v y' = c_0. [para(5974(a,1),5791(a,1,2))]. given #143 (T,wt=8): 7442 (x v y) v x' = c_0. [para(6650(a,1),7414(a,1,1))]. given #144 (A,wt=25): 79 ((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 #145 (T,wt=10): 5975 x' v (y v (z v x)) = c_0. [back_rewrite(5758),rewrite(5934(4),5895(4))]. given #146 (T,wt=10): 6877 x v (y v (x v y)') = c_0. [back_rewrite(5942),rewrite(6650(3))]. given #147 (T,wt=10): 7181 x v (y v (x' v z)) = c_0. [para(6789(a,1),5(a,1,2)),rewrite(5064(2)),flip(a)]. given #148 (T,wt=10): 7183 x' v (y v (x v z)) = c_0. [para(6789(a,1),18(a,1,2)),rewrite(5064(2)),flip(a)]. given #149 (A,wt=25): 80 ((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 #150 (T,wt=10): 7334 x' v (x v y)' = x'. [para(5925(a,1),7281(a,1,2,1,1))]. given #151 (T,wt=10): 7386 x v ((y v x') v z) = c_0. [para(6650(a,1),5790(a,1,2))]. given #152 (T,wt=10): 7387 x v ((x' v y) v z) = c_0. [para(7281(a,1),5790(a,1,2,2)),rewrite(6651(4))]. given #153 (T,wt=10): 7415 (x v y) v (z v y') = c_0. [para(5974(a,1),5790(a,1,2,2))]. given #154 (A,wt=25): 92 ((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 #155 (T,wt=10): 7443 (x v y) v (z v x') = c_0. [para(7442(a,1),5(a,1,2)),rewrite(5064(2)),flip(a)]. given #156 (T,wt=10): 7444 (x v (y v z)) v y' = c_0. [para(5(a,1),7442(a,1,1))]. given #157 (T,wt=10): 7549 (x v (y v z)) v z' = c_0. [para(5975(a,1),6650(a,1)),flip(a)]. given #158 (T,wt=10): 7550 x' v ((y v x) v z) = c_0. [para(6650(a,1),5975(a,1,2))]. given #159 (A,wt=23): 420 x v (y v (z v (u v (v v w)))) = v v (x v (y v (u v (z v w)))). [para(28(a,1),18(a,1,2,2))]. given #160 (T,wt=10): 7583 x' v ((x v y) v z) = c_0. [para(6650(a,1),7183(a,1,2))]. given #161 (T,wt=10): 7676 (x v y) v (y' v z) = c_0. [para(5974(a,1),7386(a,1,2,1))]. given #162 (T,wt=10): 7677 (x v y) v (x' v z) = c_0. [para(7334(a,1),7386(a,1,2,1))]. given #163 (T,wt=10): 7847 ((x v y) v z) v y' = c_0. [para(5974(a,1),7443(a,1,2))]. given #164 (A,wt=23): 421 x v (y v (z v (u v (v v w)))) = z v (x v (v v (u v (y v w)))). [para(28(a,1),18(a,2,2,2))]. given #165 (T,wt=10): 7848 ((x v y) v z) v x' = c_0. [para(7334(a,1),7443(a,1,2))]. given #166 (T,wt=11): 6594 x v (y v (z v x'))' = x. [back_rewrite(6087),rewrite(6586(12))]. given #167 (T,wt=11): 6651 x v (y v z) = z v (x v y). [para(5895(a,1),18(a,1,2,2)),rewrite(5895(5))]. % Operation v is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 6651 x v (y v z) = z v (x v y). [para(5895(a,1),18(a,1,2,2)),rewrite(5895(5))]. % back CAC tautology: 421 x v (y v (z v (u v (v v w)))) = z v (x v (v v (u v (y v w)))). [para(28(a,1),18(a,2,2,2))]. % back CAC tautology: 420 x v (y v (z v (u v (v v w)))) = v v (x v (y v (u v (z v w)))). [para(28(a,1),18(a,1,2,2))]. % back CAC tautology: 41 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: 40 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: 39 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: 38 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: 37 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: 36 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: 35 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: 34 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: 29 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: 27 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: 30 x v (y v (z v u)) = x v (z v (y v u)). [para(18(a,2),5(a,1))]. % back CAC tautology: 28 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: 8518 x v (y v (z v (u v v))) = v v (y v (z v (x v u))). [para(6651(a,2),41(a,2,2,2)),flip(a)]. % back CAC tautology: 8517 x v (y v (z v (u v (v v w)))) = u v (y v (x v (v v (w v z)))). [para(6651(a,2),41(a,2,2,2,2))]. % back CAC tautology: 8514 x v (y v (z v (u v v))) = u v (y v (v v (x v z))). [para(6651(a,1),41(a,2,2,2))]. % back CAC tautology: 8513 x v (y v (z v (u v (v v w)))) = u v (y v (x v (w v (z v v)))). [para(6651(a,1),41(a,2,2,2,2))]. % back CAC tautology: 8511 x v (y v (z v (u v v))) = z v (y v (x v (v v u))). [para(6651(a,2),41(a,1,2,2))]. % back CAC tautology: 8510 x v (y v (z v (u v (v v w)))) = w v (y v (x v (z v (u v v)))). [para(6651(a,2),41(a,1,2,2,2))]. % back CAC tautology: 8507 x v (y v (z v (u v v))) = v v (y v (x v (u v z))). [para(6651(a,1),41(a,1,2,2))]. % back CAC tautology: 8506 x v (y v (z v (u v (v v w)))) = v v (y v (x v (z v (w v u)))). [para(6651(a,1),41(a,1,2,2,2))]. % back CAC tautology: 8499 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(6651(a,2),40(a,2,2,2,2,2))]. % back CAC tautology: 8495 x v (y v (z v (u v (v v w)))) = z v (x v (u v (w v (v v y)))). [para(6651(a,1),40(a,2,2,2,2))]. % back CAC tautology: 8494 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(6651(a,1),40(a,2,2,2,2,2))]. % back CAC tautology: 8490 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(6651(a,2),40(a,1,2,2,2,2))]. % back CAC tautology: 8486 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(6651(a,1),40(a,1,2,2,2,2))]. % back CAC tautology: 8482 x v (y v (z v (u v v))) = v v (z v (x v (y v u))). [para(6651(a,2),39(a,1,2,2))]. % back CAC tautology: 8481 x v (y v (z v (u v (v v w)))) = z v (w v (x v (y v (u v v)))). [para(6651(a,2),39(a,1,2,2,2))]. % back CAC tautology: 8478 x v (y v (z v (u v v))) = u v (v v (x v (y v z))). [para(6651(a,1),39(a,1,2,2))]. % back CAC tautology: 8477 x v (y v (z v (u v (v v w)))) = z v (v v (x v (y v (w v u)))). [para(6651(a,1),39(a,1,2,2,2))]. % back CAC tautology: 8469 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(6651(a,2),38(a,2,2,2,2,2))]. % back CAC tautology: 8465 x v (y v (z v (u v (v v w)))) = z v (x v (v v (w v (y v u)))). [para(6651(a,1),38(a,2,2,2,2))]. % back CAC tautology: 8464 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(6651(a,1),38(a,2,2,2,2,2))]. % back CAC tautology: 8460 x v (y v (z v (u v (v v w)))) = z v (x v (u v (y v (w v v)))). [para(6651(a,2),38(a,1,2,2,2))]. % back CAC tautology: 8459 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(6651(a,2),38(a,1,2,2,2,2))]. % back CAC tautology: 8455 x v (y v (z v (u v (v v w)))) = z v (x v (w v (y v (v v u)))). [para(6651(a,1),38(a,1,2,2,2))]. % back CAC tautology: 8454 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(6651(a,1),38(a,1,2,2,2,2))]. % back CAC tautology: 8450 x v (y v (z v (u v v))) = y v (x v (z v (v v u))). [para(6651(a,2),37(a,1,2,2))]. % back CAC tautology: 8449 x v (y v (z v (u v (v v w)))) = y v (x v (w v (z v (u v v)))). [para(6651(a,2),37(a,1,2,2,2))]. % back CAC tautology: 8446 x v (y v (z v (u v v))) = y v (x v (v v (u v z))). [para(6651(a,1),37(a,1,2,2))]. % back CAC tautology: 8445 x v (y v (z v (u v (v v w)))) = y v (x v (v v (z v (w v u)))). [para(6651(a,1),37(a,1,2,2,2))]. % back CAC tautology: 8437 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(6651(a,2),36(a,2,2,2,2,2))]. % back CAC tautology: 8433 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(6651(a,1),36(a,2,2,2,2,2))]. % back CAC tautology: 8430 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(6651(a,2),36(a,1,2,2,2,2))]. % back CAC tautology: 8426 x v (y v (z v (u v (v v w)))) = w v (x v (y v (z v (v v u)))). [para(6651(a,1),36(a,1,2,2,2))]. % back CAC tautology: 8425 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(6651(a,1),36(a,1,2,2,2,2))]. % back CAC tautology: 8420 x v (y v (z v (u v (v v w)))) = u v (x v (z v (v v (w v y)))). [para(6651(a,2),35(a,2,2,2,2))]. % back CAC tautology: 8417 x v (y v (z v (u v v))) = u v (x v (v v (z v y))). [para(6651(a,1),35(a,2,2,2))]. % back CAC tautology: 8416 x v (y v (z v (u v (v v w)))) = u v (x v (z v (w v (y v v)))). [para(6651(a,1),35(a,2,2,2,2))]. % back CAC tautology: 8414 x v (y v (z v (u v (v v w)))) = w v (x v (z v (y v (u v v)))). [para(6651(a,2),35(a,1,2,2,2))]. % back CAC tautology: 8411 x v (y v (z v (u v v))) = v v (x v (u v (y v z))). [para(6651(a,1),35(a,1,2,2))]. % back CAC tautology: 8410 x v (y v (z v (u v (v v w)))) = v v (x v (z v (y v (w v u)))). [para(6651(a,1),35(a,1,2,2,2))]. % back CAC tautology: 8402 x v (y v (z v (u v (v v w)))) = u v (x v (y v (z v (w v v)))). [para(6651(a,2),34(a,2,2,2,2))]. % back CAC tautology: 8401 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(6651(a,2),34(a,2,2,2,2,2))]. % back CAC tautology: 8397 x v (y v (z v (u v (v v w)))) = u v (x v (y v (w v (v v z)))). [para(6651(a,1),34(a,2,2,2,2))]. % back CAC tautology: 8396 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(6651(a,1),34(a,2,2,2,2,2))]. % back CAC tautology: 8392 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(6651(a,2),34(a,1,2,2,2,2))]. % back CAC tautology: 8388 x v (y v (z v (u v (v v w)))) = v v (x v (y v (w v (z v u)))). [para(6651(a,1),34(a,1,2,2,2))]. % back CAC tautology: 8387 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(6651(a,1),34(a,1,2,2,2,2))]. % back CAC tautology: 8376 x v (y v (z v (u v v))) = z v (x v (y v (v v u))). [para(6651(a,2),27(a,2,2,2))]. % back CAC tautology: 8371 x v (y v (z v (u v v))) = u v (x v (v v (y v z))). [para(6651(a,1),27(a,1,2,2))]. % back CAC tautology: 8369 x v (y v (z v (u v v))) = x v (v v (y v (z v u))). [para(6651(a,2),30(a,1,2,2))]. % back CAC tautology: 8368 x v (y v (z v u)) = x v (u v (z v y)). [para(6651(a,1),30(a,1,2))]. % back CAC tautology: 8367 x v (y v (z v (u v v))) = x v (u v (y v (v v z))). [para(6651(a,1),30(a,1,2,2))]. % back CAC tautology: 8364 x v (y v (z v u)) = u v (z v (x v y)). [para(6651(a,1),28(a,1,2))]. % back CAC tautology: 8336 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 (u v (w v (v8 v (y v (v7 v (v6 v v9)))))))). [para(421(a,2),421(a,2,2,2,2,2))]. % back CAC tautology: 8335 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 (u v (v7 v (v6 v (y v v8))))))). [para(421(a,1),421(a,2,2,2,2))]. % back CAC tautology: 8334 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 (u v (v6 v (y v (v8 v (v7 v (w v v9)))))))). [para(421(a,1),421(a,2,2,2,2,2))]. % back CAC tautology: 8333 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (v6 v (z v (y v (w v (u v v7)))))). [para(421(a,2),421(a,1,2,2))]. % back CAC tautology: 8332 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 (u v (y v (v v (v8 v (v7 v (w v v9)))))))). [para(421(a,2),421(a,1,2,2,2,2))]. % back CAC tautology: 8331 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v7 v (v v (y v (u v (v6 v (w v v8))))))). [para(421(a,1),421(a,1,2,2,2))]. % back CAC tautology: 8330 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 (u v (y v (v8 v (v v (v7 v (v6 v v9)))))))). [para(421(a,1),421(a,1,2,2,2,2))]. % back CAC tautology: 8325 x v (y v (z v (u v (v v (w v v6))))) = w v (v v (x v (z v (y v (u v v6))))). [para(420(a,2),421(a,2,2)),flip(a)]. % back CAC tautology: 8324 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 (u v (w v (v6 v (v8 v (v7 v (y v v9)))))))). [para(420(a,2),421(a,2,2,2,2,2))]. % back CAC tautology: 8323 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v6 v (v v (u v (w v (y v v7)))))). [para(420(a,1),421(a,2,2,2))]. % back CAC tautology: 8322 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 (u v (y v (v6 v (w v v8))))))). [para(420(a,1),421(a,2,2,2,2))]. % back CAC tautology: 8321 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 (u v (v8 v (y v (w v (v7 v (v6 v v9)))))))). [para(420(a,1),421(a,2,2,2,2,2))]. % back CAC tautology: 8320 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (u v (z v (y v (w v (v v v7)))))). [para(420(a,2),421(a,1,2,2))]. % back CAC tautology: 8319 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 (u v (y v (v v (w v (v7 v (v6 v v9)))))))). [para(420(a,2),421(a,1,2,2,2,2))]. % back CAC tautology: 8318 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (v6 v (v v (y v (w v (z v v7)))))). [para(420(a,1),421(a,1,2,2))]. % back CAC tautology: 8317 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (w v (v v (y v (v7 v (v6 v (u v v8))))))). [para(420(a,1),421(a,1,2,2,2))]. % back CAC tautology: 8316 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 (u v (y v (v6 v (v8 v (v7 v (v v v9)))))))). [para(420(a,1),421(a,1,2,2,2,2))]. % back CAC tautology: 8315 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 (w v (z v v7)))))). [para(421(a,2),420(a,2,2,2))]. % back CAC tautology: 8314 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 (v7 v (v6 v v9)))))))). [para(421(a,2),420(a,2,2,2,2,2))]. % back CAC tautology: 8313 x v (y v (z v (u v (v v (w v v6))))) = v v (u v (x v (w v (z v (y v v6))))). [para(421(a,1),420(a,2,2))]. % back CAC tautology: 8312 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 (v6 v (z v v8))))))). [para(421(a,1),420(a,2,2,2,2))]. % back CAC tautology: 8311 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 (v7 v (w v v9)))))))). [para(421(a,1),420(a,2,2,2,2,2))]. % back CAC tautology: 8310 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 (v7 v (w v v9)))))))). [para(421(a,2),420(a,1,2,2,2,2))]. % back CAC tautology: 8309 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 (v6 v (w v v8))))))). [para(421(a,1),420(a,1,2,2,2))]. % back CAC tautology: 8308 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 (v7 v (v6 v v9)))))))). [para(421(a,1),420(a,1,2,2,2,2))]. % back CAC tautology: 8285 x v (y v (z v (u v (v v w)))) = z v (x v (v v (u v (w v y)))). [para(6650(a,1),421(a,2,2,2,2,2))]. % back CAC tautology: 8281 x v (y v (z v (u v (v v w)))) = z v (x v (w v (u v (y v v)))). [para(6650(a,1),421(a,1,2,2,2,2))]. % back CAC tautology: 8278 x v (y v (z v (u v v))) = z v (x v (v v (u v y))). [para(5895(a,1),421(a,1,2,2,2,2)),rewrite(5895(7))]. % back CAC tautology: 8275 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 (w v (v7 v (y v v8))))))). [para(41(a,2),421(a,2,2,2,2,2))]. % back CAC tautology: 8274 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 (w v (y v (v6 v v8))))))). [para(41(a,1),421(a,2,2,2,2,2))]. % back CAC tautology: 8273 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 (w v (v v (v6 v v8))))))). [para(41(a,2),421(a,1,2,2,2,2))]. % back CAC tautology: 8272 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 (w v (v7 v (v v v8))))))). [para(41(a,1),421(a,1,2,2,2,2))]. % back CAC tautology: 8271 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 (w v (u v v7)))))). [para(421(a,2),41(a,2,2,2)),flip(a)]. % back CAC tautology: 8270 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 (v6 v (w v v8))))))). [para(421(a,2),41(a,2,2,2,2))]. % back CAC tautology: 8269 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 (v6 v (v v v8))))))). [para(421(a,1),41(a,2,2,2,2))]. % back CAC tautology: 8268 x v (y v (z v (u v (v v (w v v6))))) = w v (u v (x v (y v (v v (z v v6))))). [para(421(a,2),41(a,1,2))]. % back CAC tautology: 8267 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 (v6 v (v v v8))))))). [para(421(a,2),41(a,1,2,2,2))]. % back CAC tautology: 8266 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 (w v (v v v7)))))). [para(421(a,1),41(a,1,2,2))]. % back CAC tautology: 8265 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 (v6 v (w v v8))))))). [para(421(a,1),41(a,1,2,2,2))]. % back CAC tautology: 8264 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 (u v (w v (v8 v (y v (v6 v (v7 v v9)))))))). [para(40(a,2),421(a,2,2,2,2,2))]. % back CAC tautology: 8263 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 (u v (v6 v (v7 v (y v v8))))))). [para(40(a,1),421(a,2,2,2,2))]. % back CAC tautology: 8262 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 (u v (v6 v (y v (v7 v (v8 v (w v v9)))))))). [para(40(a,1),421(a,2,2,2,2,2))]. % back CAC tautology: 8261 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (w v (z v (y v (v6 v (u v v7)))))). [para(40(a,2),421(a,1,2,2))]. % back CAC tautology: 8260 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 (u v (y v (v v (v7 v (v8 v (w v v9)))))))). [para(40(a,2),421(a,1,2,2,2,2))]. % back CAC tautology: 8259 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v7 v (v v (y v (u v (w v (v6 v v8))))))). [para(40(a,1),421(a,1,2,2,2))]. % back CAC tautology: 8258 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 (u v (y v (v8 v (v v (v6 v (v7 v v9)))))))). [para(40(a,1),421(a,1,2,2,2,2))]. % back CAC tautology: 8257 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 (v7 v (v6 v v9)))))))). [para(421(a,2),40(a,2,2,2,2,2))]. % back CAC tautology: 8256 x v (y v (z v (u v (v v (w v v6))))) = z v (v v (x v (w v (y v (u v v6))))). [para(421(a,1),40(a,2,2))]. % back CAC tautology: 8255 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 (v6 v (y v v8))))))). [para(421(a,1),40(a,2,2,2,2))]. % back CAC tautology: 8254 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 (v7 v (w v v9)))))))). [para(421(a,1),40(a,2,2,2,2,2))]. % back CAC tautology: 8253 x v (y v (z v (u v (v v (w v v6))))) = y v (x v (w v (v v (u v (z v v6))))). [para(421(a,2),40(a,1,2))]. % back CAC tautology: 8252 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 (v7 v (w v v9)))))))). [para(421(a,2),40(a,1,2,2,2,2))]. % back CAC tautology: 8251 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 (v7 v (v6 v v9)))))))). [para(421(a,1),40(a,1,2,2,2,2))]. % back CAC tautology: 8250 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 (u v (y v v7)))))). [para(39(a,1),421(a,2,2,2,2))]. % back CAC tautology: 8249 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 (v7 v (y v (w v v8))))))). [para(39(a,1),421(a,2,2,2,2,2))]. % back CAC tautology: 8248 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v6 v (w v (y v (u v (v v v7)))))). [para(39(a,1),421(a,1,2,2,2))]. % back CAC tautology: 8247 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 (v7 v (v v (w v v8))))))). [para(39(a,1),421(a,1,2,2,2,2))]. % back CAC tautology: 8246 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 (w v (u v v7)))))). [para(421(a,2),39(a,1,2,2))]. % back CAC tautology: 8245 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 (v6 v (v v v8))))))). [para(421(a,2),39(a,1,2,2,2))]. % back CAC tautology: 8244 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 (w v (v v v7)))))). [para(421(a,1),39(a,1,2,2))]. % back CAC tautology: 8243 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 (v6 v (w v v8))))))). [para(421(a,1),39(a,1,2,2,2))]. % back CAC tautology: 8242 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 (u v (w v (v7 v (y v (v8 v (v6 v v9)))))))). [para(38(a,2),421(a,2,2,2,2,2))]. % back CAC tautology: 8241 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 (u v (v7 v (y v (v6 v v8))))))). [para(38(a,1),421(a,2,2,2,2))]. % back CAC tautology: 8240 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 (u v (v6 v (y v (v8 v (w v (v7 v v9)))))))). [para(38(a,1),421(a,2,2,2,2,2))]. % back CAC tautology: 8239 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v v (x v (v6 v (z v (y v (u v (w v v7)))))). [para(38(a,2),421(a,1,2,2))]. % back CAC tautology: 8238 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 (u v (y v (v v (v8 v (w v (v7 v v9)))))))). [para(38(a,2),421(a,1,2,2,2,2))]. % back CAC tautology: 8237 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (v6 v (v v (y v (u v (v7 v (w v v8))))))). [para(38(a,1),421(a,1,2,2,2))]. % back CAC tautology: 8236 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 (u v (y v (v7 v (v v (v8 v (v6 v v9)))))))). [para(38(a,1),421(a,1,2,2,2,2))]. % back CAC tautology: 8235 x v (y v (z v (u v (v v (w v v6))))) = u v (w v (x v (v v (y v (z v v6))))). [para(421(a,2),38(a,2,2)),flip(a)]. % back CAC tautology: 8234 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 (v7 v (v6 v v9)))))))). [para(421(a,2),38(a,2,2,2,2,2))]. % back CAC tautology: 8233 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 (v7 v (w v v9)))))))). [para(421(a,1),38(a,2,2,2,2,2))]. % back CAC tautology: 8232 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 (v7 v (w v v9)))))))). [para(421(a,2),38(a,1,2,2,2,2))]. % back CAC tautology: 8231 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 (v6 v (w v v8))))))). [para(421(a,1),38(a,1,2,2,2))]. % back CAC tautology: 8230 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 (v7 v (v6 v v9)))))))). [para(421(a,1),38(a,1,2,2,2,2))]. % back CAC tautology: 8229 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 (y v (v7 v (v6 v v8))))))). [para(37(a,1),421(a,2,2,2,2,2))]. % back CAC tautology: 8228 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 (v v (v7 v (v6 v v8))))))). [para(37(a,1),421(a,1,2,2,2,2))]. % back CAC tautology: 8227 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 (v6 v (v v v8))))))). [para(421(a,2),37(a,1,2,2,2))]. % back CAC tautology: 8226 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 (v6 v (w v v8))))))). [para(421(a,1),37(a,1,2,2,2))]. % back CAC tautology: 8225 x v (y v (z v (u v (v v (w v v6))))) = w v (u v (x v (z v (y v (v v v6))))). [para(36(a,2),421(a,2,2)),flip(a)]. % back CAC tautology: 8224 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 (u v (w v (v6 v (v7 v (v8 v (y v v9)))))))). [para(36(a,2),421(a,2,2,2,2,2))]. % back CAC tautology: 8223 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (v6 v (v v (u v (y v (w v v7)))))). [para(36(a,1),421(a,2,2,2))]. % back CAC tautology: 8222 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 (u v (y v (w v (v6 v v8))))))). [para(36(a,1),421(a,2,2,2,2))]. % back CAC tautology: 8221 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 (u v (v8 v (y v (w v (v6 v (v7 v v9)))))))). [para(36(a,1),421(a,2,2,2,2,2))]. % back CAC tautology: 8220 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = v6 v (x v (u v (z v (y v (v v (w v v7)))))). [para(36(a,2),421(a,1,2,2))]. % back CAC tautology: 8219 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 (u v (y v (v v (w v (v6 v (v7 v v9)))))))). [para(36(a,2),421(a,1,2,2,2,2))]. % back CAC tautology: 8218 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (w v (v v (y v (v6 v (z v v7)))))). [para(36(a,1),421(a,1,2,2))]. % back CAC tautology: 8217 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (w v (v v (y v (v6 v (v7 v (u v v8))))))). [para(36(a,1),421(a,1,2,2,2))]. % back CAC tautology: 8216 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 (u v (y v (v6 v (v7 v (v8 v (v v v9)))))))). [para(36(a,1),421(a,1,2,2,2,2))]. % back CAC tautology: 8215 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 (w v (u v v7)))))). [para(421(a,2),36(a,2,2,2))]. % back CAC tautology: 8214 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 (v7 v (v6 v v9)))))))). [para(421(a,2),36(a,2,2,2,2,2))]. % back CAC tautology: 8213 x v (y v (z v (u v (v v (w v v6))))) = v v (z v (x v (w v (u v (y v v6))))). [para(421(a,1),36(a,2,2))]. % back CAC tautology: 8212 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 (v7 v (w v v9)))))))). [para(421(a,1),36(a,2,2,2,2,2))]. % back CAC tautology: 8211 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 (v7 v (w v v9)))))))). [para(421(a,2),36(a,1,2,2,2,2))]. % back CAC tautology: 8210 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 (v6 v (w v v8))))))). [para(421(a,1),36(a,1,2,2,2))]. % back CAC tautology: 8209 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 (v7 v (v6 v v9)))))))). [para(421(a,1),36(a,1,2,2,2,2))]. % back CAC tautology: 8208 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 (w v (y v v7)))))). [para(35(a,1),421(a,2,2,2,2))]. % back CAC tautology: 8207 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 (v6 v (w v v8))))))). [para(35(a,1),421(a,2,2,2,2,2))]. % back CAC tautology: 8206 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 (v6 v (v v v8))))))). [para(35(a,1),421(a,1,2,2,2,2))]. % back CAC tautology: 8205 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 (v6 v (w v v8))))))). [para(421(a,2),35(a,2,2,2,2))]. % back CAC tautology: 8204 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 (v6 v (v v v8))))))). [para(421(a,1),35(a,2,2,2,2))]. % back CAC tautology: 8203 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 (v6 v (v v v8))))))). [para(421(a,2),35(a,1,2,2,2))]. % back CAC tautology: 8202 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 (v6 v (w v v8))))))). [para(421(a,1),35(a,1,2,2,2))]. % back CAC tautology: 8201 x v (y v (z v (u v (v v (w v v6))))) = v v (w v (x v (z v (y v (u v v6))))). [para(34(a,2),421(a,2,2)),flip(a)]. % back CAC tautology: 8200 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 (u v (w v (v6 v (v8 v (y v (v7 v v9)))))))). [para(34(a,2),421(a,2,2,2,2,2))]. % back CAC tautology: 8199 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = z v (x v (w v (v v (u v (v6 v (y v v7)))))). [para(34(a,1),421(a,2,2,2))]. % back CAC tautology: 8198 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 (u v (y v (v7 v (w v v8))))))). [para(34(a,1),421(a,2,2,2,2))]. % back CAC tautology: 8197 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 (u v (v7 v (y v (w v (v8 v (v6 v v9)))))))). [para(34(a,1),421(a,2,2,2,2,2))]. % back CAC tautology: 8196 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = w v (x v (u v (z v (y v (v6 v (v v v7)))))). [para(34(a,2),421(a,1,2,2))]. % back CAC tautology: 8195 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 (u v (y v (v v (w v (v8 v (v6 v v9)))))))). [para(34(a,2),421(a,1,2,2,2,2))]. % back CAC tautology: 8194 x v (y v (z v (u v (v v (w v (v6 v v7)))))) = u v (x v (v6 v (v v (y v (z v (w v v7)))))). [para(34(a,1),421(a,1,2,2))]. % back CAC tautology: 8193 x v (y v (z v (u v (v v (w v (v6 v (v7 v v8))))))) = z v (x v (w v (v v (y v (v7 v (u v (v6 v v8))))))). [para(34(a,1),421(a,1,2,2,2))]. % back CAC tautology: 8192 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 (u v (y v (v6 v (v8 v (v v (v7 v v9)))))))). [para(34(a,1),421(a,1,2,2,2,2))]. % back CAC tautology: 8191 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 (v7 v (v6 v v9)))))))). [para(421(a,2),34(a,2,2,2,2,2))]. % back CAC tautology: 8190 x v (y v (z v (u v (v v (w v v6))))) = u v (v v (x v (w v (z v (y v v6))))). [para(421(a,1),34(a,2,2))]. % back CAC tautology: 8189 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 (w v (v v v7)))))). [para(421(a,1),34(a,2,2,2))]. % back CAC tautology: 8188 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 (v6 v (z v v8))))))). [para(421(a,1),34(a,2,2,2,2))]. % back CAC tautology: 8187 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 (v7 v (w v v9)))))))). [para(421(a,1),34(a,2,2,2,2,2))]. % back CAC tautology: 8186 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 (w v (u v v7)))))). [para(421(a,2),34(a,1,2,2))]. % back CAC tautology: 8185 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 (v7 v (w v v9)))))))). [para(421(a,2),34(a,1,2,2,2,2))]. % back CAC tautology: 8184 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 (v7 v (v6 v v9)))))))). [para(421(a,1),34(a,1,2,2,2,2))]. % back CAC tautology: 8183 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 (w v (u v v7)))))). [para(421(a,2),30(a,1,2,2))]. % back CAC tautology: 8182 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 (w v (v v v7)))))). [para(421(a,1),30(a,1,2,2))]. % back CAC tautology: 8106 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(420(a,2),420(a,2,2)),flip(a)]. % back CAC tautology: 8105 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(420(a,2),420(a,2,2,2))]. % back CAC tautology: 8104 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(420(a,2),420(a,2,2,2,2,2))]. % back CAC tautology: 8103 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(420(a,1),420(a,2,2,2))]. % back CAC tautology: 8102 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(420(a,1),420(a,2,2,2,2))]. % back CAC tautology: 8101 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(420(a,1),420(a,2,2,2,2,2))]. % back CAC tautology: 8100 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(420(a,2),420(a,1,2,2,2,2))]. % back CAC tautology: 8099 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(420(a,1),420(a,1,2,2))]. % back CAC tautology: 8098 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(420(a,1),420(a,1,2,2,2))]. % back CAC tautology: 8097 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(420(a,1),420(a,1,2,2,2,2))]. % back CAC tautology: 8072 x v (y v (z v (u v (v v w)))) = v v (x v (y v (u v (w v z)))). [para(6650(a,1),420(a,2,2,2,2,2))]. % back CAC tautology: 8068 x v (y v (z v (u v (v v w)))) = w v (x v (y v (u v (z v v)))). [para(6650(a,1),420(a,1,2,2,2,2))]. % back CAC tautology: 8065 x v (y v (z v (u v v))) = v v (x v (y v (u v z))). [para(5895(a,1),420(a,1,2,2,2,2)),rewrite(5895(7))]. % back CAC tautology: 8062 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(41(a,2),420(a,2,2,2,2,2))]. % back CAC tautology: 8061 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(41(a,1),420(a,2,2,2))]. % back CAC tautology: 8060 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(41(a,1),420(a,2,2,2,2,2))]. % back CAC tautology: 8059 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(41(a,2),420(a,1,2,2,2,2))]. % back CAC tautology: 8058 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(41(a,1),420(a,1,2,2,2,2))]. % back CAC tautology: 8057 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(420(a,2),41(a,2,2,2)),flip(a)]. % back CAC tautology: 8056 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(420(a,2),41(a,2,2,2,2))]. % back CAC tautology: 8055 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(420(a,1),41(a,2,2))]. % back CAC tautology: 8054 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(420(a,1),41(a,2,2,2))]. % back CAC tautology: 8053 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(420(a,1),41(a,2,2,2,2))]. % back CAC tautology: 8052 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(420(a,2),41(a,1,2,2))]. % back CAC tautology: 8051 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(420(a,2),41(a,1,2,2,2))]. % back CAC tautology: 8050 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(420(a,1),41(a,1,2))]. % back CAC tautology: 8049 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(420(a,1),41(a,1,2,2))]. % back CAC tautology: 8048 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(420(a,1),41(a,1,2,2,2))]. % back CAC tautology: 8047 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(40(a,2),420(a,2,2))]. % back CAC tautology: 8046 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(40(a,2),420(a,2,2,2))]. % back CAC tautology: 8045 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(40(a,2),420(a,2,2,2,2,2))]. % back CAC tautology: 8044 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(40(a,1),420(a,2,2))]. % back CAC tautology: 8043 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(40(a,1),420(a,2,2,2,2))]. % back CAC tautology: 8042 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(40(a,1),420(a,2,2,2,2,2))]. % back CAC tautology: 8041 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(40(a,2),420(a,1,2))]. % back CAC tautology: 8040 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(40(a,2),420(a,1,2,2,2,2))]. % back CAC tautology: 8039 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(40(a,1),420(a,1,2,2,2))]. % back CAC tautology: 8038 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(40(a,1),420(a,1,2,2,2,2))]. % back CAC tautology: 8037 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(420(a,2),40(a,2,2)),flip(a)]. % back CAC tautology: 8036 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(420(a,2),40(a,2,2,2,2))]. % back CAC tautology: 8035 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(420(a,2),40(a,2,2,2,2,2))]. % back CAC tautology: 8034 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(420(a,1),40(a,2,2,2))]. % back CAC tautology: 8033 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(420(a,1),40(a,2,2,2,2))]. % back CAC tautology: 8032 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(420(a,1),40(a,2,2,2,2,2))]. % back CAC tautology: 8031 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(420(a,2),40(a,1,2,2))]. % back CAC tautology: 8030 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(420(a,2),40(a,1,2,2,2))]. % back CAC tautology: 8029 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(420(a,2),40(a,1,2,2,2,2))]. % back CAC tautology: 8028 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(420(a,1),40(a,1,2))]. % back CAC tautology: 8027 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(420(a,1),40(a,1,2,2))]. % back CAC tautology: 8026 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(420(a,1),40(a,1,2,2,2))]. % back CAC tautology: 8025 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(420(a,1),40(a,1,2,2,2,2))]. % back CAC tautology: 8024 x v (y v (z v (u v (v v w)))) = v v (u v (z v (x v (y v w)))). [para(39(a,1),420(a,2,2))]. % back CAC tautology: 8023 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(39(a,1),420(a,2,2,2,2))]. % back CAC tautology: 8022 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(39(a,1),420(a,2,2,2,2,2))]. % back CAC tautology: 8021 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(39(a,1),420(a,1,2,2,2))]. % back CAC tautology: 8020 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(39(a,1),420(a,1,2,2,2,2))]. % back CAC tautology: 8019 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(420(a,2),39(a,1,2,2))]. % back CAC tautology: 8018 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(420(a,2),39(a,1,2,2,2))]. % back CAC tautology: 8017 x v (y v (z v (u v (v v w)))) = v v (u v (y v (z v (x v w)))). [para(420(a,1),39(a,1))]. % back CAC tautology: 8016 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(420(a,1),39(a,1,2,2))]. % back CAC tautology: 8015 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(420(a,1),39(a,1,2,2,2))]. % back CAC tautology: 8014 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(38(a,2),420(a,2,2,2))]. % back CAC tautology: 8013 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(38(a,2),420(a,2,2,2,2,2))]. % back CAC tautology: 8012 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(38(a,1),420(a,2,2))]. % back CAC tautology: 8011 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(38(a,1),420(a,2,2,2,2))]. % back CAC tautology: 8010 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(38(a,1),420(a,2,2,2,2,2))]. % back CAC tautology: 8009 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(38(a,2),420(a,1,2,2,2,2))]. % back CAC tautology: 8008 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(38(a,1),420(a,1,2,2,2))]. % back CAC tautology: 8007 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(38(a,1),420(a,1,2,2,2,2))]. % back CAC tautology: 8006 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(420(a,2),38(a,2,2)),flip(a)]. % back CAC tautology: 8005 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(420(a,2),38(a,2,2,2,2))]. % back CAC tautology: 8004 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(420(a,2),38(a,2,2,2,2,2))]. % back CAC tautology: 8003 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(420(a,1),38(a,2,2))]. % back CAC tautology: 8002 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(420(a,1),38(a,2,2,2))]. % back CAC tautology: 8001 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(420(a,1),38(a,2,2,2,2))]. % back CAC tautology: 8000 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(420(a,1),38(a,2,2,2,2,2))]. % back CAC tautology: 7999 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(420(a,2),38(a,1,2))]. % back CAC tautology: 7998 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(420(a,2),38(a,1,2,2))]. % back CAC tautology: 7997 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(420(a,2),38(a,1,2,2,2))]. % back CAC tautology: 7996 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(420(a,2),38(a,1,2,2,2,2))]. % back CAC tautology: 7995 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(420(a,1),38(a,1,2,2,2))]. % back CAC tautology: 7994 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(420(a,1),38(a,1,2,2,2,2))]. % back CAC tautology: 7993 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(37(a,1),420(a,2,2,2,2,2))]. % back CAC tautology: 7992 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(37(a,1),420(a,1,2,2,2,2))]. % back CAC tautology: 7991 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(420(a,2),37(a,1,2,2))]. % back CAC tautology: 7990 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(420(a,2),37(a,1,2,2,2))]. % back CAC tautology: 7989 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(420(a,1),37(a,1,2,2)),flip(a)]. % back CAC tautology: 7988 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(420(a,1),37(a,1,2,2,2))]. % back CAC tautology: 7987 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(36(a,2),420(a,2,2)),flip(a)]. % back CAC tautology: 7986 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(36(a,2),420(a,2,2,2))]. % back CAC tautology: 7985 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(36(a,2),420(a,2,2,2,2,2))]. % back CAC tautology: 7984 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(36(a,1),420(a,2,2,2))]. % back CAC tautology: 7983 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(36(a,1),420(a,2,2,2,2))]. % back CAC tautology: 7982 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(36(a,1),420(a,2,2,2,2,2))]. % back CAC tautology: 7981 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(36(a,2),420(a,1,2,2,2,2))]. % back CAC tautology: 7980 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(36(a,1),420(a,1,2,2))]. % back CAC tautology: 7979 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(36(a,1),420(a,1,2,2,2))]. % back CAC tautology: 7978 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(36(a,1),420(a,1,2,2,2,2))]. % back CAC tautology: 7977 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(420(a,2),36(a,2,2)),flip(a)]. % back CAC tautology: 7976 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(420(a,2),36(a,2,2,2))]. % back CAC tautology: 7975 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(420(a,2),36(a,2,2,2,2,2))]. % back CAC tautology: 7974 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(420(a,1),36(a,2,2))]. % back CAC tautology: 7973 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(420(a,1),36(a,2,2,2))]. % back CAC tautology: 7972 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(420(a,1),36(a,2,2,2,2))]. % back CAC tautology: 7971 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(420(a,1),36(a,2,2,2,2,2))]. % back CAC tautology: 7970 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(420(a,2),36(a,1,2,2,2))]. % back CAC tautology: 7969 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(420(a,2),36(a,1,2,2,2,2))]. % back CAC tautology: 7968 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(420(a,1),36(a,1,2,2))]. % back CAC tautology: 7967 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(420(a,1),36(a,1,2,2,2))]. % back CAC tautology: 7966 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(420(a,1),36(a,1,2,2,2,2))]. % back CAC tautology: 7965 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(35(a,2),420(a,2,2,2))]. % back CAC tautology: 7964 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(35(a,2),420(a,2,2,2,2,2))]. % back CAC tautology: 7963 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(35(a,1),420(a,2,2,2,2,2))]. % back CAC tautology: 7962 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(35(a,1),420(a,1,2,2,2))]. % back CAC tautology: 7961 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(35(a,1),420(a,1,2,2,2,2))]. % back CAC tautology: 7960 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(420(a,2),35(a,2,2)),flip(a)]. % back CAC tautology: 7959 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(420(a,2),35(a,2,2,2,2))]. % back CAC tautology: 7958 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(420(a,1),35(a,2,2))]. % back CAC tautology: 7957 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(420(a,1),35(a,2,2,2))]. % back CAC tautology: 7956 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(420(a,1),35(a,2,2,2,2))]. % back CAC tautology: 7955 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(420(a,2),35(a,1,2,2,2))]. % back CAC tautology: 7954 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(420(a,1),35(a,1,2))]. % back CAC tautology: 7953 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(420(a,1),35(a,1,2,2))]. % back CAC tautology: 7952 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(420(a,1),35(a,1,2,2,2))]. % back CAC tautology: 7951 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(34(a,2),420(a,2,2)),flip(a)]. % back CAC tautology: 7950 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(34(a,2),420(a,2,2,2))]. % back CAC tautology: 7949 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(34(a,2),420(a,2,2,2,2,2))]. % back CAC tautology: 7948 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(34(a,1),420(a,2,2,2))]. % back CAC tautology: 7947 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(34(a,1),420(a,2,2,2,2))]. % back CAC tautology: 7946 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(34(a,1),420(a,2,2,2,2,2))]. % back CAC tautology: 7945 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(34(a,2),420(a,1,2))]. % back CAC tautology: 7944 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(34(a,2),420(a,1,2,2,2,2))]. % back CAC tautology: 7943 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(34(a,1),420(a,1,2,2))]. % back CAC tautology: 7942 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(34(a,1),420(a,1,2,2,2))]. % back CAC tautology: 7941 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(34(a,1),420(a,1,2,2,2,2))]. % back CAC tautology: 7940 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(420(a,2),34(a,2,2)),flip(a)]. % back CAC tautology: 7939 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(420(a,2),34(a,2,2,2))]. % back CAC tautology: 7938 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(420(a,2),34(a,2,2,2,2))]. % back CAC tautology: 7937 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(420(a,2),34(a,2,2,2,2,2))]. % back CAC tautology: 7936 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(420(a,1),34(a,2,2,2))]. % back CAC tautology: 7935 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(420(a,1),34(a,2,2,2,2))]. % back CAC tautology: 7934 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(420(a,1),34(a,2,2,2,2,2))]. % back CAC tautology: 7933 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(420(a,2),34(a,1,2,2))]. % back CAC tautology: 7932 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(420(a,2),34(a,1,2,2,2))]. % back CAC tautology: 7931 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(420(a,2),34(a,1,2,2,2,2))]. % back CAC tautology: 7930 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(420(a,1),34(a,1,2))]. % back CAC tautology: 7929 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(420(a,1),34(a,1,2,2))]. % back CAC tautology: 7928 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(420(a,1),34(a,1,2,2,2))]. % back CAC tautology: 7927 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(420(a,1),34(a,1,2,2,2,2))]. % back CAC tautology: 7926 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(420(a,1),29(a,2,2,2))]. % back CAC tautology: 7925 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(420(a,2),29(a,1,2,2))]. % back CAC tautology: 7924 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(420(a,2),27(a,2,2,2))]. % back CAC tautology: 7923 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(420(a,1),27(a,1,2,2))]. % back CAC tautology: 7922 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(420(a,2),30(a,1,2))]. % back CAC tautology: 7921 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(420(a,2),30(a,1,2,2))]. % back CAC tautology: 7920 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(420(a,1),30(a,1,2,2))]. % back CAC tautology: 7919 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(420(a,1),28(a,1,2))]. % back CAC tautology: 7177 x v (y v (z v (u v v))) = u v (y v (x v (v v z))). [para(6650(a,1),41(a,2,2,2,2))]. % back CAC tautology: 7173 x v (y v (z v (u v v))) = v v (y v (x v (z v u))). [para(6650(a,1),41(a,1,2,2,2))]. % back CAC tautology: 7168 x v (y v (z v (u v (v v w)))) = z v (x v (u v (v v (w v y)))). [para(6650(a,1),40(a,2,2,2,2,2))]. % back CAC tautology: 7163 x v (y v (z v (u v (v v w)))) = z v (x v (u v (w v (y v v)))). [para(6650(a,1),40(a,1,2,2,2,2))]. % back CAC tautology: 7159 x v (y v (z v (u v v))) = z v (v v (x v (y v u))). [para(6650(a,1),39(a,1,2,2,2))]. % back CAC tautology: 7154 x v (y v (z v (u v (v v w)))) = z v (x v (v v (y v (w v u)))). [para(6650(a,1),38(a,2,2,2,2,2))]. % back CAC tautology: 7149 x v (y v (z v (u v (v v w)))) = z v (x v (w v (y v (u v v)))). [para(6650(a,1),38(a,1,2,2,2,2))]. % back CAC tautology: 7145 x v (y v (z v (u v v))) = y v (x v (v v (z v u))). [para(6650(a,1),37(a,1,2,2,2))]. % back CAC tautology: 7140 x v (y v (z v (u v (v v w)))) = v v (x v (y v (z v (w v u)))). [para(6650(a,1),36(a,2,2,2,2,2))]. % back CAC tautology: 7135 x v (y v (z v (u v (v v w)))) = w v (x v (y v (z v (u v v)))). [para(6650(a,1),36(a,1,2,2,2,2))]. % back CAC tautology: 7131 x v (y v (z v (u v v))) = u v (x v (z v (v v y))). [para(6650(a,1),35(a,2,2,2,2))]. % back CAC tautology: 7127 x v (y v (z v (u v v))) = v v (x v (z v (y v u))). [para(6650(a,1),35(a,1,2,2,2))]. % back CAC tautology: 7122 x v (y v (z v (u v (v v w)))) = u v (x v (y v (v v (w v z)))). [para(6650(a,1),34(a,2,2,2,2,2))]. % back CAC tautology: 7117 x v (y v (z v (u v (v v w)))) = u v (x v (y v (w v (z v v)))). [para(6650(a,1),34(a,1,2,2,2,2))]. % back CAC tautology: 7102 x v (y v (z v u)) = x v (u v (y v z)). [para(6650(a,1),30(a,1,2,2))]. % back CAC tautology: 6662 x v (y v (z v u)) = u v (y v (x v z)). [para(5895(a,1),41(a,1,2,2,2)),rewrite(5895(6))]. % back CAC tautology: 6661 x v (y v (z v (u v v))) = z v (x v (u v (v v y))). [para(5895(a,1),40(a,1,2,2,2,2)),rewrite(5895(7))]. % back CAC tautology: 6660 x v (y v (z v u)) = z v (u v (x v y)). [para(5895(a,1),39(a,1,2,2,2)),rewrite(5895(6))]. % back CAC tautology: 6659 x v (y v (z v (u v v))) = z v (x v (v v (y v u))). [para(5895(a,1),38(a,1,2,2,2,2)),rewrite(5895(7))]. % back CAC tautology: 6658 x v (y v (z v u)) = y v (x v (u v z)). [para(5895(a,1),37(a,1,2,2,2)),rewrite(5895(6))]. % back CAC tautology: 6657 x v (y v (z v (u v v))) = v v (x v (y v (z v u))). [para(5895(a,1),36(a,1,2,2,2,2)),rewrite(5895(7))]. % back CAC tautology: 6656 x v (y v (z v u)) = u v (x v (z v y)). [para(5895(a,1),35(a,1,2,2,2)),rewrite(5895(6))]. % back CAC tautology: 6655 x v (y v (z v (u v v))) = u v (x v (y v (v v z))). [para(5895(a,1),34(a,1,2,2,2,2)),rewrite(5895(7))]. % back CAC tautology: 6654 x v (y v (z v u)) = u v (x v (y v z)). [para(5895(a,1),29(a,1,2,2,2)),rewrite(5895(6))]. % back CAC tautology: 6653 x v (y v (z v u)) = z v (x v (u v y)). [para(5895(a,1),27(a,1,2,2,2)),rewrite(5895(6))]. % back CAC tautology: 6652 x v (y v z) = z v (y v x). [para(5895(a,1),28(a,1,2,2)),rewrite(5895(5))]. % back CAC tautology: 4735 x v (y v (z v (u v (v v (w v v6))))) = x v (w v (u v (y v (z v (v v v6))))). [para(40(a,2),50(a,2,2)),rewrite(5(13),5(12),5(11),5(10),4700(18)),flip(a)]. % back CAC tautology: 4734 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(40(a,1),50(a,2,2)),rewrite(5(13),5(12),5(11),5(10),4700(18))]. % back CAC tautology: 4725 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(38(a,1),50(a,2,2)),rewrite(5(13),5(12),5(11),5(10),4700(18))]. % back CAC tautology: 4712 x v (y v (z v (u v (v v (w v v6))))) = x v (u v (w v (y v (v v (z v v6))))). [para(36(a,2),50(a,2,2)),rewrite(5(13),5(12),5(11),5(10),4700(18))]. % back CAC tautology: 4711 x v (y v (z v (u v (v v (w v v6))))) = x v (w v (z v (u v (y v (v v v6))))). [para(36(a,1),50(a,2,2)),rewrite(5(13),5(12),5(11),5(10),4700(18)),flip(a)]. % back CAC tautology: 4701 x v (y v (z v (u v (v v (w v v6))))) = x v (w v (v v (y v (u v (z v v6))))). [para(34(a,2),50(a,2,2)),rewrite(5(13),5(12),5(11),5(10),4700(18)),flip(a)]. % back CAC tautology: 3566 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(41(a,2),41(a,2,2,2,2))]. % back CAC tautology: 3565 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(41(a,1),41(a,2,2,2,2))]. % back CAC tautology: 3564 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(41(a,2),41(a,1,2,2,2))]. % back CAC tautology: 3563 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(41(a,1),41(a,1,2,2,2))]. % back CAC tautology: 3562 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(40(a,2),41(a,2,2,2)),flip(a)]. % back CAC tautology: 3561 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(40(a,2),41(a,2,2,2,2))]. % back CAC tautology: 3560 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(40(a,1),41(a,2,2,2,2))]. % back CAC tautology: 3559 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(40(a,2),41(a,1,2,2,2))]. % back CAC tautology: 3558 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(40(a,1),41(a,1,2,2))]. % back CAC tautology: 3557 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(40(a,1),41(a,1,2,2,2))]. % back CAC tautology: 3556 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(41(a,2),40(a,2,2,2,2,2))]. % back CAC tautology: 3555 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(41(a,1),40(a,2,2,2,2,2))]. % back CAC tautology: 3554 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(41(a,2),40(a,1,2,2,2,2))]. % back CAC tautology: 3553 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(41(a,1),40(a,1,2,2,2,2))]. % back CAC tautology: 3549 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(39(a,1),41(a,2,2,2,2))]. % back CAC tautology: 3548 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(39(a,1),41(a,1,2,2))]. % back CAC tautology: 3547 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(39(a,1),41(a,1,2,2,2))]. % back CAC tautology: 3546 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(41(a,2),39(a,1,2,2,2))]. % back CAC tautology: 3545 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(41(a,1),39(a,1,2,2,2))]. % back CAC tautology: 3544 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(38(a,2),41(a,2,2,2)),flip(a)]. % back CAC tautology: 3543 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(38(a,2),41(a,2,2,2,2))]. % back CAC tautology: 3542 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(38(a,1),41(a,2,2,2,2))]. % back CAC tautology: 3541 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(38(a,2),41(a,1,2,2,2))]. % back CAC tautology: 3540 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(38(a,1),41(a,1,2,2))]. % back CAC tautology: 3539 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(38(a,1),41(a,1,2,2,2))]. % back CAC tautology: 3538 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(41(a,2),38(a,2,2,2,2,2))]. % back CAC tautology: 3537 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(41(a,1),38(a,2,2,2,2,2))]. % back CAC tautology: 3536 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(41(a,2),38(a,1,2,2,2,2))]. % back CAC tautology: 3535 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(41(a,1),38(a,1,2,2,2,2))]. % back CAC tautology: 3530 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(37(a,1),41(a,2,2,2,2))]. % back CAC tautology: 3529 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(37(a,1),41(a,1,2,2,2))]. % back CAC tautology: 3528 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(41(a,2),37(a,1,2,2,2))]. % back CAC tautology: 3527 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(41(a,1),37(a,1,2,2,2))]. % back CAC tautology: 3510 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(36(a,2),41(a,2,2,2)),flip(a)]. % back CAC tautology: 3509 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(36(a,2),41(a,2,2,2,2))]. % back CAC tautology: 3508 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(36(a,1),41(a,2,2,2))]. % back CAC tautology: 3507 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(36(a,1),41(a,2,2,2,2))]. % back CAC tautology: 3506 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(36(a,2),41(a,1,2,2))]. % back CAC tautology: 3505 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(36(a,2),41(a,1,2,2,2))]. % back CAC tautology: 3504 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(36(a,1),41(a,1,2,2))]. % back CAC tautology: 3503 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(36(a,1),41(a,1,2,2,2))]. % back CAC tautology: 3502 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(41(a,2),36(a,2,2,2,2,2))]. % back CAC tautology: 3501 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(41(a,1),36(a,2,2,2,2,2))]. % back CAC tautology: 3500 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(41(a,2),36(a,1,2,2,2,2))]. % back CAC tautology: 3499 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(41(a,1),36(a,1,2,2,2,2))]. % back CAC tautology: 3493 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(35(a,2),41(a,2,2,2)),flip(a)]. % back CAC tautology: 3492 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(35(a,2),41(a,2,2,2,2))]. % back CAC tautology: 3491 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(35(a,1),41(a,2,2,2,2))]. % back CAC tautology: 3490 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(35(a,2),41(a,1,2,2,2))]. % back CAC tautology: 3489 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(35(a,1),41(a,1,2,2))]. % back CAC tautology: 3488 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(35(a,1),41(a,1,2,2,2))]. % back CAC tautology: 3487 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(41(a,2),35(a,2,2,2,2))]. % back CAC tautology: 3486 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(41(a,1),35(a,2,2,2,2))]. % back CAC tautology: 3485 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(41(a,2),35(a,1,2,2,2))]. % back CAC tautology: 3484 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(41(a,1),35(a,1,2,2,2))]. % back CAC tautology: 3483 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(34(a,2),41(a,2,2,2)),flip(a)]. % back CAC tautology: 3482 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(34(a,2),41(a,2,2,2,2))]. % back CAC tautology: 3481 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(34(a,1),41(a,2,2,2))]. % back CAC tautology: 3480 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(34(a,1),41(a,2,2,2,2))]. % back CAC tautology: 3479 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(34(a,2),41(a,1,2,2))]. % back CAC tautology: 3478 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(34(a,2),41(a,1,2,2,2))]. % back CAC tautology: 3477 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(34(a,1),41(a,1,2,2))]. % back CAC tautology: 3476 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(34(a,1),41(a,1,2,2,2))]. % back CAC tautology: 3475 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(41(a,2),34(a,2,2,2,2,2))]. % back CAC tautology: 3474 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(41(a,1),34(a,2,2,2,2,2))]. % back CAC tautology: 3473 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(41(a,2),34(a,1,2,2,2,2))]. % back CAC tautology: 3472 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(41(a,1),34(a,1,2,2,2,2))]. % back CAC tautology: 3444 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(41(a,2),30(a,1,2,2))]. % back CAC tautology: 3443 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(41(a,1),30(a,1,2,2))]. % back CAC tautology: 3442 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(41(a,2),28(a,1,2,2))]. % back CAC tautology: 3441 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(41(a,1),28(a,1,2,2))]. % back CAC tautology: 3377 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(40(a,2),40(a,2,2,2))]. % back CAC tautology: 3376 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(40(a,2),40(a,2,2,2,2,2))]. % back CAC tautology: 3375 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(40(a,1),40(a,2,2,2,2))]. % back CAC tautology: 3374 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(40(a,1),40(a,2,2,2,2,2))]. % back CAC tautology: 3373 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(40(a,2),40(a,1,2,2,2))]. % back CAC tautology: 3372 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(40(a,2),40(a,1,2,2,2,2))]. % back CAC tautology: 3371 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(40(a,1),40(a,1,2,2,2,2))]. % back CAC tautology: 3367 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(39(a,1),40(a,2,2,2,2))]. % back CAC tautology: 3366 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(39(a,1),40(a,2,2,2,2,2))]. % back CAC tautology: 3365 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(39(a,1),40(a,1,2,2,2))]. % back CAC tautology: 3364 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(39(a,1),40(a,1,2,2,2,2))]. % back CAC tautology: 3363 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(40(a,2),39(a,1,2,2))]. % back CAC tautology: 3362 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(40(a,2),39(a,1,2,2,2))]. % back CAC tautology: 3361 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(40(a,1),39(a,1,2,2))]. % back CAC tautology: 3360 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(40(a,1),39(a,1,2,2,2))]. % back CAC tautology: 3359 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(38(a,2),40(a,2,2,2))]. % back CAC tautology: 3358 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(38(a,2),40(a,2,2,2,2,2))]. % back CAC tautology: 3357 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(38(a,1),40(a,2,2,2,2))]. % back CAC tautology: 3356 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(38(a,1),40(a,2,2,2,2,2))]. % back CAC tautology: 3355 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(38(a,2),40(a,1,2,2,2))]. % back CAC tautology: 3354 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(38(a,2),40(a,1,2,2,2,2))]. % back CAC tautology: 3353 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(38(a,1),40(a,1,2,2,2,2))]. % back CAC tautology: 3352 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(40(a,2),38(a,2,2,2,2))]. % back CAC tautology: 3351 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(40(a,2),38(a,2,2,2,2,2))]. % back CAC tautology: 3350 x v (y v (z v (u v (v v w)))) = v v (z v (y v (u v (x v w)))). [para(40(a,1),38(a,2))]. % back CAC tautology: 3349 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(40(a,1),38(a,2,2,2,2,2))]. % back CAC tautology: 3348 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(40(a,2),38(a,1,2,2,2,2))]. % back CAC tautology: 3347 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(40(a,1),38(a,1,2,2,2))]. % back CAC tautology: 3346 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(40(a,1),38(a,1,2,2,2,2))]. % back CAC tautology: 3338 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(37(a,1),40(a,2,2,2,2,2))]. % back CAC tautology: 3337 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(37(a,1),40(a,1,2,2,2,2))]. % back CAC tautology: 3336 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(40(a,2),37(a,1,2,2,2))]. % back CAC tautology: 3335 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(40(a,1),37(a,1,2,2,2))]. % back CAC tautology: 3303 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(36(a,2),40(a,2,2)),flip(a)]. % back CAC tautology: 3302 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(36(a,2),40(a,2,2,2,2))]. % back CAC tautology: 3301 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(36(a,2),40(a,2,2,2,2,2))]. % back CAC tautology: 3300 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(36(a,1),40(a,2,2))]. % back CAC tautology: 3299 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(36(a,1),40(a,2,2,2))]. % back CAC tautology: 3298 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(36(a,1),40(a,2,2,2,2))]. % back CAC tautology: 3297 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(36(a,1),40(a,2,2,2,2,2))]. % back CAC tautology: 3296 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(36(a,2),40(a,1,2,2))]. % back CAC tautology: 3295 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(36(a,2),40(a,1,2,2,2))]. % back CAC tautology: 3294 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(36(a,2),40(a,1,2,2,2,2))]. % back CAC tautology: 3293 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(36(a,1),40(a,1,2,2,2))]. % back CAC tautology: 3292 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(36(a,1),40(a,1,2,2,2,2))]. % back CAC tautology: 3291 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(40(a,2),36(a,2,2,2))]. % back CAC tautology: 3290 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(40(a,2),36(a,2,2,2,2))]. % back CAC tautology: 3289 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(40(a,2),36(a,2,2,2,2,2))]. % back CAC tautology: 3288 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(40(a,1),36(a,2,2))]. % back CAC tautology: 3287 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(40(a,1),36(a,2,2,2,2,2))]. % back CAC tautology: 3286 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(40(a,2),36(a,1,2,2))]. % back CAC tautology: 3285 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(40(a,2),36(a,1,2,2,2,2))]. % back CAC tautology: 3284 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(40(a,1),36(a,1,2,2,2))]. % back CAC tautology: 3283 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(40(a,1),36(a,1,2,2,2,2))]. % back CAC tautology: 3272 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(35(a,2),40(a,2,2,2,2,2))]. % back CAC tautology: 3271 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(35(a,1),40(a,2,2,2,2))]. % back CAC tautology: 3270 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(35(a,1),40(a,2,2,2,2,2))]. % back CAC tautology: 3269 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(35(a,2),40(a,1,2,2,2))]. % back CAC tautology: 3268 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(35(a,2),40(a,1,2,2,2,2))]. % back CAC tautology: 3267 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(35(a,1),40(a,1,2,2))]. % back CAC tautology: 3266 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(35(a,1),40(a,1,2,2,2,2))]. % back CAC tautology: 3265 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(40(a,2),35(a,2,2)),flip(a)]. % back CAC tautology: 3264 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(40(a,2),35(a,2,2,2,2))]. % back CAC tautology: 3263 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(40(a,1),35(a,2,2,2,2))]. % back CAC tautology: 3262 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(40(a,2),35(a,1,2,2,2))]. % back CAC tautology: 3261 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(40(a,1),35(a,1,2,2,2))]. % back CAC tautology: 3260 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(34(a,2),40(a,2,2,2,2,2))]. % back CAC tautology: 3259 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(34(a,1),40(a,2,2))]. % back CAC tautology: 3258 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(34(a,1),40(a,2,2,2))]. % back CAC tautology: 3257 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(34(a,1),40(a,2,2,2,2))]. % back CAC tautology: 3256 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(34(a,1),40(a,2,2,2,2,2))]. % back CAC tautology: 3255 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(34(a,2),40(a,1,2,2))]. % back CAC tautology: 3254 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(34(a,2),40(a,1,2,2,2))]. % back CAC tautology: 3253 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(34(a,2),40(a,1,2,2,2,2))]. % back CAC tautology: 3252 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(34(a,1),40(a,1,2,2,2,2))]. % back CAC tautology: 3251 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(40(a,2),34(a,2,2))]. % back CAC tautology: 3250 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(40(a,2),34(a,2,2,2))]. % back CAC tautology: 3249 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(40(a,2),34(a,2,2,2,2,2))]. % back CAC tautology: 3248 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(40(a,1),34(a,2,2,2,2))]. % back CAC tautology: 3247 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(40(a,1),34(a,2,2,2,2,2))]. % back CAC tautology: 3246 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(40(a,2),34(a,1,2,2,2))]. % back CAC tautology: 3245 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(40(a,2),34(a,1,2,2,2,2))]. % back CAC tautology: 3244 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(40(a,1),34(a,1,2,2,2,2))]. % back CAC tautology: 3219 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(29(a,1),40(a,2,2,2,2))]. % back CAC tautology: 3210 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(27(a,1),40(a,2,2,2,2))]. % back CAC tautology: 3209 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(40(a,2),27(a,2,2,2,2))]. % back CAC tautology: 3208 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(40(a,1),27(a,2,2,2,2))]. % back CAC t