============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13586 was started by mccune on cleo.thornwood, Mon Jun 19 16:43:06 2006 The command was "/home/mccune/bin/prover9 -f ba-4basis.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file ba-4basis.in assign(new_constants,1). clauses(sos). x v (y v z) = y v (x v z) # label(AJ). x ^ y = c(c(x) v c(y)) # label(DM). x v c(x) = y v c(y) # label(ONE). (x v c(y)) ^ (x v y) = x # label(CUT). end_of_list. clauses(goals). c(c(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 GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). c(c(c1)) != c1 # answer(CC). c2 v (c2 ^ c3) != c2 # answer(B1). (c4 ^ c5) v (c4 ^ c6) != c4 ^ (c5 v c6) # answer(DIST1). c7 v (c9 ^ (c7 v c8)) != c7 v (c8 ^ (c7 v c9)) # answer(MOD). end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x v (y v z) = y v (x v z) # label(AJ). [input]. 2 x ^ y = c(c(x) v c(y)) # label(DM). [input]. 3 x v c(x) = y v c(y) # label(ONE). [input]. 4 (x v c(y)) ^ (x v y) = x # label(CUT). [input]. 5 c(c(c1)) != c1 # answer(CC). [clausify]. 6 c2 v (c2 ^ c3) != c2 # answer(B1). [clausify]. 7 (c4 ^ c5) v (c4 ^ c6) != c4 ^ (c5 v c6) # answer(DIST1). [clausify]. 8 c7 v (c9 ^ (c7 v c8)) != c7 v (c8 ^ (c7 v c9)) # answer(MOD). [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: % assign(max_proofs, 4). % (Horn set with more than one neg. clause) % assign(max_proofs, 4) -> set(restrict_denials). % Restrict denials; moving clauses to denials list: clauses(denials). 5 c(c(c1)) != c1 # answer(CC). [clausify]. 6 c2 v (c2 ^ c3) != c2 # answer(B1). [clausify]. 7 (c4 ^ c5) v (c4 ^ c6) != c4 ^ (c5 v c6) # answer(DIST1). [clausify]. 8 c7 v (c9 ^ (c7 v c8)) != c7 v (c8 ^ (c7 v c9)) # answer(MOD). [clausify]. end_of_list. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, v, ^, c ]). After inverse_order: Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, v, ^, c ]). Unfolding symbols: ^/2. Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: no changes. NOTE: New constant: 0 x v c(x) = c_0. [new_symbol(11)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c_0, v, ^, c ]). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 9 x v (y v z) = y v (x v z) # label(AJ). [input]. 10 x ^ y = c(c(x) v c(y)) # label(DM). [input]. 12 c(c(x v c(y)) v c(x v y)) = x # label(CUT). [copy(4),demod(10(4))]. 13 x v c(x) = c_0. [new_symbol(11)]. end_of_list. clauses(demodulators). 9 x v (y v z) = y v (x v z) # label(AJ). [input]. % (lex-dep) 10 x ^ y = c(c(x) v c(y)) # label(DM). [input]. 12 c(c(x v c(y)) v c(x v y)) = x # label(CUT). [copy(4),demod(10(4))]. 13 x v c(x) = c_0. [new_symbol(11)]. end_of_list. clauses(denials). 14 c(c(c1)) != c1 # answer(CC). [clausify]. 15 c2 v c(c(c2) v c(c3)) != c2 # answer(B1). [copy(6),demod(10(4))]. 16 c(c(c4) v c(c5 v c6)) != c(c(c4) v c(c5)) v c(c(c4) v c(c6)) # answer(DIST1). [copy(7),demod(10(3),10(9),10(18)),flip(a)]. 17 c7 v c(c(c8) v c(c7 v c9)) != c7 v c(c(c9) v c(c7 v c8)) # answer(MOD). [copy(8),demod(10(6),10(16)),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 9 x v (y v z) = y v (x v z) # label(AJ). [input]. given #2 (I,wt=10): 10 x ^ y = c(c(x) v c(y)) # label(DM). [input]. given #3 (I,wt=13): 12 c(c(x v c(y)) v c(x v y)) = x # label(CUT). [copy(4),demod(10(4))]. given #4 (I,wt=6): 13 x v c(x) = c_0. [new_symbol(11)]. given #5 (T,wt=10): 23 x v (y v c(x)) = y v c_0. [para(13(a,1),9(a,1,2)),flip(a)]. given #6 (A,wt=15): 18 x v (y v (z v u)) = z v (x v (y v u)). [para(9(a,1),9(a,1,2))]. given #7 (F,wt=10): 24 c(c(c_0) v c(x v x)) = x. [para(13(a,1),12(a,1,1,1,1))]. given #8 (F,wt=11): 49 (c(c_0) v c(x v x)) v x = c_0. [para(24(a,1),13(a,1,2))]. given #9 (T,wt=12): 25 c(c(x v c(c(x))) v c(c_0)) = x. [para(13(a,1),12(a,1,1,2,1))]. given #10 (T,wt=13): 47 c(x v c(c(c_0) v (x v x))) = c(c_0). [para(24(a,1),12(a,1,1,1))]. given #11 (A,wt=17): 19 c(c(x v c(y v z)) v c(y v (x v z))) = x. [para(9(a,1),12(a,1,1,2,1))]. given #12 (F,wt=13): 68 (c(x v c(c(x))) v c(c_0)) v x = c_0. [para(25(a,1),13(a,1,2))]. given #13 (F,wt=13): 72 c(x v c(x v (c(c_0) v x))) = c(c_0). [para(9(a,1),47(a,1,1,2,1))]. given #14 (T,wt=14): 26 (c(x v c(y)) v c(x v y)) v x = c_0. [para(12(a,1),13(a,1,2))]. given #15 (T,wt=14): 27 x v (y v (z v c(x))) = y v (z v c_0). [para(23(a,1),9(a,1,2)),flip(a)]. given #16 (A,wt=21): 20 c(c(x v y) v c(x v (c(y v c(z)) v c(y v z)))) = x. [para(12(a,1),12(a,1,1,1,1,2))]. given #17 (F,wt=14): 76 (x v c(c(c_0) v (x v x))) v c(c_0) = c_0. [para(47(a,1),13(a,1,2))]. given #18 (F,wt=11): 256 x v c(c(c_0) v (x v x)) = c_0. [back_demod(243),demod(244(10),24(8)),flip(a)]. given #19 (T,wt=11): 260 x v c(x v (c(c_0) v x)) = c_0. [para(9(a,1),256(a,1,2,1))]. given #20 (T,wt=12): 261 (c(c_0) v (x v x)) v c_0 = x v c_0. [para(256(a,1),23(a,1,2))]. given #21 (A,wt=19): 21 c(x v c(x v (c(x v c(y)) v y))) = c(x v c(y)). [para(12(a,1),12(a,1,1,1)),demod(9(5))]. given #22 (F,wt=12): 262 c(c(c_0)) v c(c(c(c_0)) v c_0) = c_0. [para(23(a,1),256(a,1,2,1))]. given #23 (F,wt=12): 274 (x v (c(c_0) v x)) v c_0 = x v c_0. [para(260(a,1),23(a,1,2))]. given #24 (T,wt=13): 284 (c(c(c_0)) v c_0) v c_0 = c(c(c_0)) v c_0. [para(23(a,1),261(a,1,1))]. given #25 (T,wt=15): 31 x v (y v (z v u)) = z v (y v (x v u)). [para(18(a,1),9(a,1))]. given #26 (A,wt=21): 22 c(c(c(x v c(y)) v c(c(x v y))) v x) = c(x v c(y)). [para(12(a,1),12(a,1,1,2))]. given #27 (F,wt=15): 33 x v (y v (z v u)) = x v (z v (y v u)). [para(18(a,2),9(a,1))]. given #28 (F,wt=15): 48 c(c(c(c_0) v c(c(x v x))) v x) = c(c_0). [para(24(a,1),12(a,1,1,2))]. given #29 (T,wt=15): 50 (c(c_0) v c(x v x)) v (y v x) = y v c_0. [para(24(a,1),23(a,1,2,2))]. given #30 (T,wt=15): 56 (c(c_0) v c(c(x) v c(x))) v c_0 = x v c_0. [para(49(a,1),23(a,1,2)),flip(a)]. given #31 (A,wt=16): 28 c(c(x v c(y v c(x))) v c(y v c_0)) = x. [para(23(a,1),12(a,1,1,2,1))]. given #32 (F,wt=15): 74 c(c(c_0) v c(x v (c(c_0) v (x v x)))) = x. [para(47(a,1),12(a,1,1,1))]. given #33 (F,wt=15): 105 c(c(c_0) v c(c(c_0) v (x v (x v x)))) = x. [para(47(a,1),19(a,1,1,1))]. given #34 (T,wt=15): 126 c(c(c_0) v c(x v (x v (c(c_0) v x)))) = x. [para(72(a,1),12(a,1,1,1))]. given #35 (T,wt=15): 258 x v (y v c(c(c_0) v (x v x))) = y v c_0. [para(256(a,1),9(a,1,2)),flip(a)]. given #36 (A,wt=18): 29 (c(x v c(y)) v c(x v y)) v (z v x) = z v c_0. [para(12(a,1),23(a,1,2,2))]. given #37 (F,wt=15): 273 x v (y v c(x v (c(c_0) v x))) = y v c_0. [para(260(a,1),9(a,1,2)),flip(a)]. given #38 (F,wt=16): 45 c(c(c_0) v c(x v ((x v y) v y))) = x v y. [para(9(a,1),24(a,1,1,2,1))]. given #39 (T,wt=9): 825 c(c(c_0)) v c_0 = c(c(c_0)). [para(284(a,1),45(a,1,1,2,1,2,1)),demod(284(14),9(13),284(12),330(14),284(10)),flip(a)]. given #40 (T,wt=13): 855 c(c(c_0)) v (x v c_0) = x v c(c(c_0)). [back_demod(336),demod(825(5),825(11))]. given #41 (A,wt=19): 30 x v (y v (z v (u v v))) = z v (x v (u v (y v v))). [para(18(a,1),9(a,1,2))]. given #42 (F,wt=14): 862 c(c_0) v (c(c(c_0)) v (x v c_0)) = x v c_0. [para(855(a,2),23(a,1,2))]. given #43 (F,wt=14): 1040 c(c(c_0)) v (x v (c(c_0) v c_0)) = x v c_0. [para(862(a,1),18(a,2))]. given #44 (T,wt=15): 858 (c(c_0) v c(c_0 v c_0)) v c(c(c_0)) = c(c(c_0)). [para(825(a,1),50(a,1,2)),demod(825(16))]. given #45 (T,wt=12): 1083 c(c(c(c_0) v c(c(c(c_0))))) = c(c_0). [para(858(a,1),28(a,1,1,1,1,2,1)),demod(49(17),817(11))]. given #46 (A,wt=19): 32 x v (y v (z v (u v v))) = u v (x v (y v (z v v))). [para(18(a,2),9(a,1,2))]. given #47 (F,wt=10): 1087 c(c(c_0) v c(c(c(c_0)))) = c_0. [para(1083(a,1),13(a,1,2)),demod(817(11))]. given #48 (F,wt=11): 1235 (c(c_0) v c(c(c(c_0)))) v c_0 = c_0. [para(1087(a,1),13(a,1,2))]. given #49 (T,wt=15): 885 c(c(c(c_0)) v (x v c_0)) = c(x v c(c(c_0))). [para(855(a,2),21(a,2,1)),demod(21(12)),flip(a)]. given #50 (T,wt=15): 1234 c(c(c(c_0) v c(c(c(c(c_0))))) v c_0) = c(c_0). [para(1087(a,1),12(a,1,1,2))]. given #51 (A,wt=21): 34 c(c(x v c(y v (z v u))) v c(z v (x v (y v u)))) = x. [para(18(a,1),12(a,1,1,2,1))]. given #52 (F,wt=15): 1236 (c(c_0) v c(c(c(c_0)))) v (x v c_0) = x v c_0. [para(1087(a,1),23(a,1,2,2))]. given #53 (F,wt=15): 1247 c(c(c(c(c_0))) v c(c(c_0) v c_0)) = c(c(c_0)). [para(1087(a,1),28(a,1,1,1,1,2)),demod(825(5))]. given #54 (T,wt=15): 1257 (c(c_0) v c(c(c(c_0)))) v c(c(c_0)) = c(c(c_0)). [para(1235(a,1),855(a,1,2)),demod(825(5)),flip(a)]. given #55 (T,wt=16): 152 (c(c(c_0) v c(c(x v x))) v x) v c(c_0) = c_0. [para(24(a,1),26(a,1,1,2))]. given #56 (A,wt=21): 35 c(c(x v c(y v (z v u))) v c(y v (z v (x v u)))) = x. [para(18(a,2),12(a,1,1,2,1))]. given #57 (F,wt=13): 1455 c(c(c_0) v c(c(x v x))) v x = c_0. [para(152(a,1),12(a,1,1,1,1)),demod(547(12),24(8)),flip(a)]. given #58 (F,wt=13): 1461 c(c(c_0) v c(c(c(c_0) v c(c_0)))) = c_0. [para(152(a,1),45(a,1,1,2,1,2)),demod(463(18),1455(25))]. given #59 (T,wt=14): 1605 (c(c_0) v c(c(c(c_0) v c(c_0)))) v c_0 = c_0. [para(1461(a,1),13(a,1,2))]. given #60 (T,wt=16): 158 (c(c_0) v c(x v (c(c_0) v (x v x)))) v x = c_0. [para(47(a,1),26(a,1,1,1))]. given #61 (A,wt=18): 36 x v (y v (z v (u v c(x)))) = y v (z v (u v c_0)). [para(23(a,1),18(a,1,2,2)),flip(a)]. given #62 (F,wt=16): 169 (c(c_0) v c(x v (x v (c(c_0) v x)))) v x = c_0. [para(72(a,1),26(a,1,1,1))]. given #63 (F,wt=16): 622 (c(c_0) v c(c(c_0) v (x v (x v x)))) v x = c_0. [para(105(a,1),13(a,1,2))]. given #64 (T,wt=16): 680 (c(c_0) v (x v x)) v (y v c_0) = x v (y v c_0). [para(258(a,1),27(a,1,2))]. given #65 (T,wt=8): 1864 c_0 v (c(c_0) v c_0) = c_0. [para(680(a,1),45(a,1,1,2,1,2)),demod(9(10),9(9),126(13),9(7)),flip(a)]. given #66 (A,wt=23): 37 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 #67 (F,wt=7): 1897 c(c(c_0)) = c_0 v c_0. [para(1864(a,1),50(a,1,2)),demod(9(11),1060(15))]. given #68 (F,wt=9): 1900 (c_0 v c_0) v c_0 = c_0 v c_0. [para(1864(a,1),1040(a,1,2)),demod(1897(3))]. given #69 (T,wt=12): 1887 c_0 v (x v (c(c_0) v c_0)) = x v c_0. [para(1864(a,1),9(a,1,2)),flip(a)]. given #70 (T,wt=12): 1890 c(c_0) v (x v (c_0 v c_0)) = x v c_0. [para(1864(a,1),18(a,1,2)),flip(a)]. given #71 (A,wt=19): 38 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 #72 (F,wt=12): 1891 c_0 v (c(c_0) v (x v c_0)) = x v c_0. [para(1864(a,1),18(a,2,2))]. given #73 (F,wt=12): 1975 c(c(c_0 v (c_0 v c_0)) v c(c_0)) = c_0. [back_demod(1294),demod(1897(5),1455(11),1897(4),1897(15),1455(21))]. given #74 (T,wt=13): 1974 (c(c_0 v (c_0 v c_0)) v c(c_0)) v c_0 = c_0. [back_demod(1296),demod(1897(5),1897(14),1455(20),1897(13),9(21),1455(20))]. given #75 (T,wt=13): 2058 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0). [back_demod(898),demod(1897(3),1897(16),9(17),56(16))]. given #76 (A,wt=23): 39 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 #77 (F,wt=13): 2064 c(c_0 v (x v c_0)) = c(x v (c_0 v c_0)). [back_demod(885),demod(1897(3),2058(6),1897(8))]. given #78 (F,wt=14): 1888 c(c(c_0 v c(c(c_0) v c_0)) v c(c_0)) = c_0. [para(1864(a,1),12(a,1,1,2,1))]. given #79 (T,wt=14): 1999 (x v (c_0 v c_0)) v c(c_0 v (x v c_0)) = c_0. [back_demod(1264),demod(1897(3),1897(7),1981(11))]. given #80 (T,wt=14): 2042 (c_0 v c_0) v (x v (c(c_0) v c_0)) = x v c_0. [back_demod(1040),demod(1897(3))]. given #81 (A,wt=19): 40 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 #82 (F,wt=14): 2125 (c_0 v (x v c_0)) v c(x v (c_0 v c_0)) = c_0. [back_demod(2000),demod(2058(6))]. given #83 (F,wt=14): 2387 c(c(c_0) v c(c_0 v (c_0 v c_0))) = c_0 v c_0. [para(1900(a,1),45(a,1,1,2,1,2,1)),demod(1900(10),9(9),1900(8),1900(15))]. given #84 (T,wt=14): 2954 (c_0 v c_0) v (c(c_0) v (x v c_0)) = x v c_0. [para(9(a,1),2042(a,1,2))]. given #85 (T,wt=15): 1893 (c(c_0 v c(c(c_0) v c_0)) v c(c_0)) v c_0 = c_0. [para(1864(a,1),26(a,1,1,2,1))]. given #86 (A,wt=23): 41 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 #87 (F,wt=15): 2004 c(c(c_0 v c_0) v c(c(c_0) v c_0)) = c_0 v c_0. [back_demod(1247),demod(1897(3),1897(14))]. given #88 (F,wt=15): 2078 c(c(c_0 v (x v c_0)) v c(x v c(c_0))) = x. [back_demod(861),demod(1897(3),2058(6))]. given #89 (T,wt=11): 3326 c(c_0) v c(c(c_0) v c(c_0)) = c_0. [para(49(a,1),2078(a,1,1,2,1)),demod(56(12),1975(10)),flip(a)]. given #90 (T,wt=12): 3365 (c(c_0) v c(c_0)) v c_0 = c(c_0) v c_0. [para(3326(a,1),23(a,1,2))]. given #91 (A,wt=19): 42 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 #92 (F,wt=14): 3335 c(c(c_0) v c(x)) v c(c(c_0) v x) = c_0. [para(26(a,1),2078(a,1,1,2,1)),demod(141(13),1975(10)),flip(a)]. given #93 (F,wt=15): 2132 (c_0 v (x v c_0)) v c_0 = (x v (c_0 v c_0)) v c_0. [back_demod(1982),demod(2058(6))]. given #94 (T,wt=15): 2379 c(c(x v (c_0 v c_0)) v c(x v c(c_0))) = x. [para(1897(a,1),12(a,1,1,1,1,2))]. given #95 (T,wt=15): 3364 c(c_0) v (x v c(c(c_0) v c(c_0))) = x v c_0. [para(3326(a,1),9(a,1,2)),flip(a)]. given #96 (A,wt=23): 43 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 #97 (F,wt=15): 3521 c(c(c_0) v c(x)) v c_0 = (c(c_0) v x) v c_0. [para(3335(a,1),23(a,1,2)),flip(a)]. given #98 (F,wt=9): 4071 c(c_0) v (c(c_0) v c_0) = c_0. [back_demod(3579),demod(3983(21),9(20),3705(19))]. given #99 (T,wt=5): 4228 c_0 v c_0 = c_0. [back_demod(1893),demod(4107(5),4208(5),13(4),4148(7))]. given #100 (T,wt=5): 4362 c(c(c_0)) = c_0. [back_demod(1897),demod(4228(6))]. given #101 (A,wt=19): 44 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 #102 (F,wt=6): 4284 c(c_0) v c_0 = c_0. [back_demod(4107),demod(4228(7))]. given #103 (F,wt=8): 4282 c(c(c_0) v c(c_0)) = c_0. [back_demod(4120),demod(4228(9))]. given #104 (T,wt=9): 4231 c_0 v (x v c_0) = x v c_0. [back_demod(1887),demod(4107(5),4228(4))]. given #105 (T,wt=9): 4280 (c(c_0) v c(c_0)) v c_0 = c_0. [back_demod(4148),demod(4228(10))]. given #106 (A,wt=18): 46 c(c(x v y) v c(x v (c(c_0) v c(y v y)))) = x. [para(24(a,1),12(a,1,1,1,1,2))]. given #107 (F,wt=10): 4225 c(c_0) v (x v c_0) = x v c_0. [back_demod(1898),demod(4107(5),4208(5),13(4),3694(8))]. given #108 (F,wt=13): 4230 c_0 v (x v (y v c_0)) = x v (y v c_0). [back_demod(1889),demod(4107(5),4228(4))]. given #109 (T,wt=13): 4268 (c(c_0) v c(c_0)) v (x v c_0) = x v c_0. [back_demod(3694),demod(4225(13))]. given #110 (T,wt=13): 4345 c(c(x v c_0) v c(x v c(c_0))) = x. [back_demod(2379),demod(4228(3))]. given #111 (A,wt=22): 51 c(c(c_0) v c(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)),demod(9(6))]. given #112 (F,wt=11): 4719 x v ((x v c_0) v c_0) = x v c_0. [para(680(a,1),51(a,1,1,2,1,2,2)),demod(9(11),4267(12),9(10),4350(13),9(9),4267(10)),flip(a)]. given #113 (F,wt=12): 4749 c(c(c_0) v c(x v c_0)) = x v c_0. [para(3335(a,1),51(a,1,1,2,1,2,2,1,2)),demod(3523(16),4719(7),3335(17))]. given #114 (T,wt=12): 4820 c(c(x v c_0) v c(c_0)) = x v c_0. [para(4749(a,1),28(a,1,1,1,1,2)),demod(9(5),4719(5),4284(7))]. given #115 (T,wt=13): 4804 x v ((c(c_0) v c(x v c_0)) v c_0) = c_0. [back_demod(4264),demod(4768(10),9(7),4719(7))]. given #116 (A,wt=22): 52 c(c(c_0) v c(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 #117 (F,wt=14): 4236 c(c((x v x) v x) v c(c_0)) = x v x. [back_demod(550),demod(4107(7),4228(6))]. given #118 (F,wt=14): 4254 c(c(x v c(c_0 v c(x))) v c(c_0)) = x. [back_demod(2087),demod(4228(3),4228(9))]. given #119 (T,wt=14): 4267 c(c_0) v (x v (y v c_0)) = x v (y v c_0). [back_demod(4109),demod(4225(7))]. given #120 (T,wt=14): 4344 (c(x v c_0) v c(x v c(c_0))) v x = c_0. [back_demod(2380),demod(4228(3))]. given #121 (A,wt=17): 53 x v ((c(c_0) v c(x v ((x v y) v y))) v y) = c_0. [para(49(a,1),9(a,1)),demod(9(6)),flip(a)]. given #122 (F,wt=7): 5250 (x v c_0) v c_0 = c_0. [para(4719(a,1),53(a,1,2,1,2,1,2,1)),demod(4768(10),9(7),4719(7),9(11),4859(12))]. ============================== PROOF ================================= % Proof 1 at 1.39 (+ 0.01) seconds: CC. % Length of proof is 149. % Level of proof is 40. % Maximum clause weight is 39. % Given clauses 122. 3 x v c(x) = y v c(y) # label(ONE). [input]. 4 (x v c(y)) ^ (x v y) = x # label(CUT). [input]. 9 x v (y v z) = y v (x v z) # label(AJ). [input]. 10 x ^ y = c(c(x) v c(y)) # label(DM). [input]. 11 x v c(x) = y v c(y) # label(ONE). [copy(3)]. 12 c(c(x v c(y)) v c(x v y)) = x # label(CUT). [copy(4),demod(10(4))]. 13 x v c(x) = c_0. [new_symbol(11)]. 14 c(c(c1)) != c1 # answer(CC). [clausify]. 18 x v (y v (z v u)) = z v (x v (y v u)). [para(9(a,1),9(a,1,2))]. 19 c(c(x v c(y v z)) v c(y v (x v z))) = x. [para(9(a,1),12(a,1,1,2,1))]. 21 c(x v c(x v (c(x v c(y)) v y))) = c(x v c(y)). [para(12(a,1),12(a,1,1,1)),demod(9(5))]. 22 c(c(c(x v c(y)) v c(c(x v y))) v x) = c(x v c(y)). [para(12(a,1),12(a,1,1,2))]. 23 x v (y v c(x)) = y v c_0. [para(13(a,1),9(a,1,2)),flip(a)]. 24 c(c(c_0) v c(x v x)) = x. [para(13(a,1),12(a,1,1,1,1))]. 25 c(c(x v c(c(x))) v c(c_0)) = x. [para(13(a,1),12(a,1,1,2,1))]. 26 (c(x v c(y)) v c(x v y)) v x = c_0. [para(12(a,1),13(a,1,2))]. 27 x v (y v (z v c(x))) = y v (z v c_0). [para(23(a,1),9(a,1,2)),flip(a)]. 28 c(c(x v c(y v c(x))) v c(y v c_0)) = x. [para(23(a,1),12(a,1,1,2,1))]. 29 (c(x v c(y)) v c(x v y)) v (z v x) = z v c_0. [para(12(a,1),23(a,1,2,2))]. 30 x v (y v (z v (u v v))) = z v (x v (u v (y v v))). [para(18(a,1),9(a,1,2))]. 34 c(c(x v c(y v (z v u))) v c(z v (x v (y v u)))) = x. [para(18(a,1),12(a,1,1,2,1))]. 35 c(c(x v c(y v (z v u))) v c(y v (z v (x v u)))) = x. [para(18(a,2),12(a,1,1,2,1))]. 36 x v (y v (z v (u v c(x)))) = y v (z v (u v c_0)). [para(23(a,1),18(a,1,2,2)),flip(a)]. 45 c(c(c_0) v c(x v ((x v y) v y))) = x v y. [para(9(a,1),24(a,1,1,2,1))]. 47 c(x v c(c(c_0) v (x v x))) = c(c_0). [para(24(a,1),12(a,1,1,1))]. 48 c(c(c(c_0) v c(c(x v x))) v x) = c(c_0). [para(24(a,1),12(a,1,1,2))]. 49 (c(c_0) v c(x v x)) v x = c_0. [para(24(a,1),13(a,1,2))]. 50 (c(c_0) v c(x v x)) v (y v x) = y v c_0. [para(24(a,1),23(a,1,2,2))]. 51 c(c(c_0) v c(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)),demod(9(6))]. 53 x v ((c(c_0) v c(x v ((x v y) v y))) v y) = c_0. [para(49(a,1),9(a,1)),demod(9(6)),flip(a)]. 56 (c(c_0) v c(c(x) v c(x))) v c_0 = x v c_0. [para(49(a,1),23(a,1,2)),flip(a)]. 65 c(x v c(c(x v c(c(x))) v c_0)) = c(x v c(c(x))). [para(25(a,1),12(a,1,1,1))]. 66 c(c(c(x v c(c(x))) v c(c(c_0))) v x) = c(x v c(c(x))). [para(25(a,1),12(a,1,1,2))]. 68 (c(x v c(c(x))) v c(c_0)) v x = c_0. [para(25(a,1),13(a,1,2))]. 72 c(x v c(x v (c(c_0) v x))) = c(c_0). [para(9(a,1),47(a,1,1,2,1))]. 74 c(c(c_0) v c(x v (c(c_0) v (x v x)))) = x. [para(47(a,1),12(a,1,1,1))]. 76 (x v c(c(c_0) v (x v x))) v c(c_0) = c_0. [para(47(a,1),13(a,1,2))]. 126 c(c(c_0) v c(x v (x v (c(c_0) v x)))) = x. [para(72(a,1),12(a,1,1,1))]. 141 (c(c(x) v c(y)) v c(c(x) v y)) v c_0 = x v c_0. [para(26(a,1),23(a,1,2)),flip(a)]. 152 (c(c(c_0) v c(c(x v x))) v x) v c(c_0) = c_0. [para(24(a,1),26(a,1,1,2))]. 158 (c(c_0) v c(x v (c(c_0) v (x v x)))) v x = c_0. [para(47(a,1),26(a,1,1,1))]. 169 (c(c_0) v c(x v (x v (c(c_0) v x)))) v x = c_0. [para(72(a,1),26(a,1,1,1))]. 243 c(c(c_0) v c((x v c(c(c_0) v (x v x))) v c_0)) = x v c(c(c_0) v (x v x)). [para(76(a,1),12(a,1,1,1,1))]. 244 (x v c(c(c_0) v (x v x))) v c_0 = c_0 v c_0. [para(76(a,1),23(a,1,2)),flip(a)]. 256 x v c(c(c_0) v (x v x)) = c_0. [back_demod(243),demod(244(10),24(8)),flip(a)]. 258 x v (y v c(c(c_0) v (x v x))) = y v c_0. [para(256(a,1),9(a,1,2)),flip(a)]. 260 x v c(x v (c(c_0) v x)) = c_0. [para(9(a,1),256(a,1,2,1))]. 261 (c(c_0) v (x v x)) v c_0 = x v c_0. [para(256(a,1),23(a,1,2))]. 262 c(c(c_0)) v c(c(c(c_0)) v c_0) = c_0. [para(23(a,1),256(a,1,2,1))]. 273 x v (y v c(x v (c(c_0) v x))) = y v c_0. [para(260(a,1),9(a,1,2)),flip(a)]. 284 (c(c(c_0)) v c_0) v c_0 = c(c(c_0)) v c_0. [para(23(a,1),261(a,1,1))]. 330 c(c(c_0) v c(c(c(c_0)) v (c(c(c_0)) v c_0))) = c(c(c_0)). [para(262(a,1),12(a,1,1,1,1))]. 336 (c(c(c_0)) v c_0) v (x v c_0) = x v (c(c(c_0)) v c_0). [para(262(a,1),27(a,1,2,2))]. 547 (c(c(c_0) v c(c(x v x))) v x) v c_0 = c_0 v c_0. [para(48(a,1),56(a,1,1,2,1,1)),demod(48(13),56(11)),flip(a)]. 576 c(c(x v c((c(c(c_0)) v c_0) v c(x))) v c(c(c(c_0)) v c_0)) = x. [para(284(a,1),28(a,1,1,2,1))]. 605 c(c(c_0) v c(x v ((x v c(c(c_0))) v ((x v c(c(c_0))) v c_0)))) = x v c(c(c_0)). [para(27(a,1),74(a,1,1,2,1,2)),demod(9(13),9(14))]. 680 (c(c_0) v (x v x)) v (y v c_0) = x v (y v c_0). [para(258(a,1),27(a,1,2))]. 805 c(c(c(x v c(y v c(x v (c(c_0) v x)))) v c(c(y v c_0))) v x) = c(x v c(y v c(x v (c(c_0) v x)))). [para(273(a,1),22(a,1,1,1,1,2,1,1))]. 808 (c(x v c(y v c(x v (c(c_0) v x)))) v c(y v c_0)) v (z v x) = z v c_0. [para(273(a,1),29(a,1,1,2,1))]. 817 c(c(c_0) v c(c(c(c_0)))) v c(c_0) = c(c(c_0) v c(c(c(c_0)))). [para(68(a,1),45(a,1,1,2,1,2)),demod(65(15)),flip(a)]. 825 c(c(c_0)) v c_0 = c(c(c_0)). [para(284(a,1),45(a,1,1,2,1,2,1)),demod(284(14),9(13),284(12),330(14),284(10)),flip(a)]. 842 c(c(x v c(c(c(c_0)) v c(x))) v c(c(c(c_0)))) = x. [back_demod(576),demod(825(5),825(13))]. 855 c(c(c_0)) v (x v c_0) = x v c(c(c_0)). [back_demod(336),demod(825(5),825(11))]. 858 (c(c_0) v c(c_0 v c_0)) v c(c(c_0)) = c(c(c_0)). [para(825(a,1),50(a,1,2)),demod(825(16))]. 861 c(c(c(c(c_0)) v (x v c_0)) v c(x v c(c_0))) = x. [para(855(a,2),12(a,1,1,1,1))]. 862 c(c_0) v (c(c(c_0)) v (x v c_0)) = x v c_0. [para(855(a,2),23(a,1,2))]. 898 c(c(c_0)) v (x v c_0) = (c(c_0) v c(c(x) v c(x))) v c(c(c_0)). [para(56(a,1),855(a,1,2))]. 1040 c(c(c_0)) v (x v (c(c_0) v c_0)) = x v c_0. [para(862(a,1),18(a,2))]. 1060 (c(c_0) v c(c(c_0) v ((c(c_0) v c_0) v c_0))) v c_0 = c(c(c_0)). [para(49(a,1),1040(a,1,2)),demod(825(5),9(14)),flip(a)]. 1083 c(c(c(c_0) v c(c(c(c_0))))) = c(c_0). [para(858(a,1),28(a,1,1,1,1,2,1)),demod(49(17),817(11))]. 1087 c(c(c_0) v c(c(c(c_0)))) = c_0. [para(1083(a,1),13(a,1,2)),demod(817(11))]. 1234 c(c(c(c_0) v c(c(c(c(c_0))))) v c_0) = c(c_0). [para(1087(a,1),12(a,1,1,2))]. 1247 c(c(c(c(c_0))) v c(c(c_0) v c_0)) = c(c(c_0)). [para(1087(a,1),28(a,1,1,1,1,2)),demod(825(5))]. 1294 c(c((c(c(c_0) v c(c(c(c(c_0))))) v c_0) v c(c(c_0))) v c(c_0)) = c(c(c_0) v c(c(c(c(c_0))))) v c_0. [para(1234(a,1),25(a,1,1,1,1,2,1))]. 1333 c(c(x v c(y v (z v (u v c(x))))) v c(z v (y v (u v c_0)))) = x. [para(27(a,1),34(a,1,1,2,1,2))]. 1414 c(c(c(c(c(c_0))) v c(c(c(c_0) v c_0))) v c(c(c_0))) = c(c(c(c_0))). [para(1247(a,1),12(a,1,1,2))]. 1455 c(c(c_0) v c(c(x v x))) v x = c_0. [para(152(a,1),12(a,1,1,1,1)),demod(547(12),24(8)),flip(a)]. 1477 c(c(x v c(y v c_0)) v c(y v ((c(z v c(c(z))) v c(c_0)) v (x v z)))) = x. [para(68(a,1),35(a,1,1,1,1,2,1,2))]. 1710 c(c(c(x v c(y v (z v (u v c(x))))) v c(c(y v (z v (u v c_0))))) v x) = c(x v c(y v (z v (u v c(x))))). [para(36(a,1),22(a,1,1,1,1,2,1,1))]. 1864 c_0 v (c(c_0) v c_0) = c_0. [para(680(a,1),45(a,1,1,2,1,2)),demod(9(10),9(9),126(13),9(7)),flip(a)]. 1887 c_0 v (x v (c(c_0) v c_0)) = x v c_0. [para(1864(a,1),9(a,1,2)),flip(a)]. 1893 (c(c_0 v c(c(c_0) v c_0)) v c(c_0)) v c_0 = c_0. [para(1864(a,1),26(a,1,1,2,1))]. 1897 c(c(c_0)) = c_0 v c_0. [para(1864(a,1),50(a,1,2)),demod(9(11),1060(15))]. 1898 (c(c_0 v c(c(c_0) v c_0)) v c(c_0)) v (x v c_0) = x v c_0. [para(1864(a,1),29(a,1,1,2,1))]. 1963 c(c_0 v (c(c(c_0 v c_0) v c(c(c(c_0) v c_0))) v c_0)) = c(c_0 v c_0). [back_demod(1414),demod(1897(3),1897(15),9(16),1897(20))]. 1975 c(c(c_0 v (c_0 v c_0)) v c(c_0)) = c_0. [back_demod(1294),demod(1897(5),1455(11),1897(4),1897(15),1455(21))]. 2022 (c(c_0) v c(c(c_0) v ((c(c_0) v c_0) v c_0))) v c_0 = c_0 v c_0. [back_demod(1060),demod(1897(18))]. 2058 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0). [back_demod(898),demod(1897(3),1897(16),9(17),56(16))]. 2078 c(c(c_0 v (x v c_0)) v c(x v c(c_0))) = x. [back_demod(861),demod(1897(3),2058(6))]. 2087 c(c(x v c((c_0 v c_0) v c(x))) v c(c_0 v c_0)) = x. [back_demod(842),demod(1897(3),1897(11))]. 2093 c(c(c_0) v c(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_demod(605),demod(1897(5),1897(9),1897(20))]. 2109 c(c(c_0 v (c(x v c(c(x))) v c_0)) v x) = c(x v c(c(x))). [back_demod(66),demod(1897(7),9(8))]. 3326 c(c_0) v c(c(c_0) v c(c_0)) = c_0. [para(49(a,1),2078(a,1,1,2,1)),demod(56(12),1975(10)),flip(a)]. 3335 c(c(c_0) v c(x)) v c(c(c_0) v x) = c_0. [para(26(a,1),2078(a,1,1,2,1)),demod(141(13),1975(10)),flip(a)]. 3364 c(c_0) v (x v c(c(c_0) v c(c_0))) = x v c_0. [para(3326(a,1),9(a,1,2)),flip(a)]. 3365 (c(c_0) v c(c_0)) v c_0 = c(c_0) v c_0. [para(3326(a,1),23(a,1,2))]. 3376 (c(c_0) v c(c(c(c_0) v c(c_0)) v (c(c(c_0) v c(c_0)) v c_0))) v c(c(c_0) v c(c_0)) = c_0. [para(3326(a,1),169(a,1,1,2,1,2,2))]. 3521 c(c(c_0) v c(x)) v c_0 = (c(c_0) v x) v c_0. [para(3335(a,1),23(a,1,2)),flip(a)]. 3523 c(c(c_0) v c(x)) v (y v (z v c(c(c_0) v x))) = y v (z v c_0). [para(3335(a,1),18(a,1,2,2)),flip(a)]. 3579 (c(c_0) v c((c(c_0) v c_0) v ((c(c_0) v c_0) v c_0))) v c(c(c_0) v c(c_0)) = c_0. [back_demod(3376),demod(3521(16),9(15),3521(14))]. 3694 (c(c_0) v c(c_0)) v (x v c_0) = c(c_0) v (x v c_0). [para(3364(a,1),27(a,1,2))]. 3705 (c(c_0) v c((c(c_0) v c_0) v ((c(c_0) v c_0) v c_0))) v c_0 = c(c_0) v c_0. [para(158(a,1),3364(a,1,2)),demod(3364(28),3521(20),9(19),3521(18)),flip(a)]. 3707 x v ((c(c_0) v c(x v ((x v c(c(c_0) v c(c_0))) v ((x v c(c(c_0) v c(c_0))) v c_0)))) v c(c(c_0) v c(c_0))) = c_0. [para(3364(a,1),169(a,1,1,2,1,2,2)),demod(9(19),9(20),9(30))]. 3983 c(c(c_0) v c(c_0)) = c(c_0) v c_0. [para(3521(a,1),21(a,1,1,2,1,2)),demod(45(14)),flip(a)]. 4058 x v (c(c_0) v ((c(c_0) v c(x v ((x v (c(c_0) v c_0)) v ((x v (c(c_0) v c_0)) v c_0)))) v c_0)) = c_0. [back_demod(3707),demod(3983(8),3983(13),3983(24),9(23))]. 4071 c(c_0) v (c(c_0) v c_0) = c_0. [back_demod(3579),demod(3983(21),9(20),3705(19))]. 4107 c(c_0) v c_0 = c_0 v c_0. [para(4071(a,1),50(a,1,2)),demod(9(11),2022(15)),flip(a)]. 4108 c_0 v (c_0 v c_0) = c_0. [para(50(a,2),4071(a,1,2)),demod(9(11),49(10),4107(6),9(6),4107(5))]. 4109 c(c_0) v (x v (c(c_0) v (y v c_0))) = x v (y v c_0). [para(4071(a,1),30(a,1,2,2)),flip(a)]. 4117 x v (c(c_0) v ((c(c_0) v c(x v ((x v (c_0 v c_0)) v ((x v (c_0 v c_0)) v c_0)))) v c_0)) = c_0. [back_demod(4058),demod(4107(8),4107(12))]. 4148 (c(c_0) v c(c_0)) v c_0 = c_0 v c_0. [back_demod(3365),demod(4107(11))]. 4208 c(c_0 v c_0) = c(c_0). [back_demod(1963),demod(4107(9),13(11),4107(5),4108(5)),flip(a)]. 4225 c(c_0) v (x v c_0) = x v c_0. [back_demod(1898),demod(4107(5),4208(5),13(4),3694(8))]. 4228 c_0 v c_0 = c_0. [back_demod(1893),demod(4107(5),4208(5),13(4),4148(7))]. 4231 c_0 v (x v c_0) = x v c_0. [back_demod(1887),demod(4107(5),4228(4))]. 4254 c(c(x v c(c_0 v c(x))) v c(c_0)) = x. [back_demod(2087),demod(4228(3),4228(9))]. 4264 x v ((c(c_0) v c(x v ((x v c_0) v ((x v c_0) v c_0)))) v c_0) = c_0. [back_demod(4117),demod(4228(7),4228(9),4225(17))]. 4267 c(c_0) v (x v (y v c_0)) = x v (y v c_0). [back_demod(4109),demod(4225(7))]. 4284 c(c_0) v c_0 = c_0. [back_demod(4107),demod(4228(7))]. 4350 c(c(c_0) v c(x v ((x v c_0) v ((x v c_0) v c_0)))) = x v c_0. [back_demod(2093),demod(4228(5),4228(7),4228(16))]. 4362 c(c(c_0)) = c_0. [back_demod(1897),demod(4228(6))]. 4367 c(c(c(x v c(c(x))) v c_0) v x) = c(x v c(c(x))). [back_demod(2109),demod(4231(8))]. 4719 x v ((x v c_0) v c_0) = x v c_0. [para(680(a,1),51(a,1,1,2,1,2,2)),demod(9(11),4267(12),9(10),4350(13),9(9),4267(10)),flip(a)]. 4749 c(c(c_0) v c(x v c_0)) = x v c_0. [para(3335(a,1),51(a,1,1,2,1,2,2,1,2)),demod(3523(16),4719(7),3335(17))]. 4768 x v (y v ((x v c_0) v c_0)) = y v (x v c_0). [para(4719(a,1),9(a,1,2)),flip(a)]. 4804 x v ((c(c_0) v c(x v c_0)) v c_0) = c_0. [back_demod(4264),demod(4768(10),9(7),4719(7))]. 4820 c(c(x v c_0) v c(c_0)) = x v c_0. [para(4749(a,1),28(a,1,1,1,1,2)),demod(9(5),4719(5),4284(7))]. 4833 c(c(x v (y v c_0)) v c(c(y v c_0) v (x v c(c_0)))) = x. [para(4820(a,1),19(a,1,1,1,1,2))]. 4843 c(c(x v c_0) v c((x v c_0) v (c(x v c_0) v c_0))) = x v c_0. [para(4820(a,1),21(a,1,1,2,1,2,1)),demod(9(11),4820(21))]. 4851 c(c(x v c_0) v c(c(x v c_0) v c_0)) = c_0. [para(4820(a,1),28(a,1,1,1,1,2)),demod(4231(4))]. 4859 x v (y v ((c(c_0) v c(x v c_0)) v c_0)) = y v c_0. [para(4804(a,1),9(a,1,2)),flip(a)]. 5006 c(x v c(c(x v c(c_0 v c(x))) v c_0)) = c(x v c(c_0 v c(x))). [para(4254(a,1),12(a,1,1,1))]. 5007 c(c(c(x v c(c_0 v c(x))) v c_0) v x) = c(x v c(c_0 v c(x))). [para(4254(a,1),12(a,1,1,2)),demod(4362(9))]. 5250 (x v c_0) v c_0 = c_0. [para(4719(a,1),53(a,1,2,1,2,1,2,1)),demod(4768(10),9(7),4719(7),9(11),4859(12))]. 5268 (x v c_0) v (y v c_0) = y v c_0. [para(5250(a,1),9(a,1,2)),flip(a)]. 5285 x v c_0 = c_0. [back_demod(4843),demod(5268(11),4851(11)),flip(a)]. 5408 c(x v c(c_0 v c(x))) = c(c(c_0) v x). [back_demod(5007),demod(5285(8)),flip(a)]. 5409 c(c(c_0) v x) = c(x v c(c_0)). [back_demod(5006),demod(5408(6),5285(6),5408(10)),flip(a)]. 5443 c(c(c_0) v c(c(c_0) v (x v c(c_0)))) = x. [back_demod(4833),demod(5285(2),5285(2),5285(4))]. 5525 c(x v c(c(x))) = c(c(c_0) v x). [back_demod(4367),demod(5285(6)),flip(a)]. 5860 c(x v c(y v (z v (u v c(x))))) = c(c(c_0) v x). [back_demod(1710),demod(5285(9),5285(9),5285(9),4362(10),5285(9)),flip(a)]. 5923 c(c(x v c(c_0)) v c(y v ((c(c(c_0) v z) v c(c_0)) v (x v z)))) = x. [back_demod(1477),demod(5285(2),5525(8))]. 5936 c(c(c_0) v c(c(c_0) v x)) = x. [back_demod(1333),demod(5860(7),5285(6),5285(6),5285(6),5409(8,R))]. 5995 (c(x v c(y v c(x v (c(c_0) v x)))) v c(c_0)) v (z v x) = c_0. [back_demod(808),demod(5285(11),5285(16))]. 5997 c(x v c(y v c(x v (c(c_0) v x)))) = c(c(c_0) v x). [back_demod(805),demod(5285(11),4362(12),5285(11)),flip(a)]. 6292 x v c(c_0) = x. [back_demod(5443),demod(5936(11))]. 6322 c(c(c_0) v x) v (y v x) = c_0. [back_demod(5995),demod(5997(9),6292(7))]. 6324 c(c(x)) = x. [back_demod(5923),demod(6292(3),6292(8),6322(7),5285(3),6292(4))]. 6325 $F # answer(CC). [resolve(6324,a,14,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 14. ============================== PROOF ================================= % Proof 2 at 1.51 (+ 0.01) seconds: B1. % Length of proof is 168. % Level of proof is 44. % Maximum clause weight is 86. % Given clauses 122. 3 x v c(x) = y v c(y) # label(ONE). [input]. 4 (x v c(y)) ^ (x v y) = x # label(CUT). [input]. 6 c2 v (c2 ^ c3) != c2 # answer(B1). [clausify]. 9 x v (y v z) = y v (x v z) # label(AJ). [input]. 10 x ^ y = c(c(x) v c(y)) # label(DM). [input]. 11 x v c(x) = y v c(y) # label(ONE). [copy(3)]. 12 c(c(x v c(y)) v c(x v y)) = x # label(CUT). [copy(4),demod(10(4))]. 13 x v c(x) = c_0. [new_symbol(11)]. 15 c2 v c(c(c2) v c(c3)) != c2 # answer(B1). [copy(6),demod(10(4))]. 18 x v (y v (z v u)) = z v (x v (y v u)). [para(9(a,1),9(a,1,2))]. 19 c(c(x v c(y v z)) v c(y v (x v z))) = x. [para(9(a,1),12(a,1,1,2,1))]. 20 c(c(x v y) v c(x v (c(y v c(z)) v c(y v z)))) = x. [para(12(a,1),12(a,1,1,1,1,2))]. 21 c(x v c(x v (c(x v c(y)) v y))) = c(x v c(y)). [para(12(a,1),12(a,1,1,1)),demod(9(5))]. 22 c(c(c(x v c(y)) v c(c(x v y))) v x) = c(x v c(y)). [para(12(a,1),12(a,1,1,2))]. 23 x v (y v c(x)) = y v c_0. [para(13(a,1),9(a,1,2)),flip(a)]. 24 c(c(c_0) v c(x v x)) = x. [para(13(a,1),12(a,1,1,1,1))]. 25 c(c(x v c(c(x))) v c(c_0)) = x. [para(13(a,1),12(a,1,1,2,1))]. 26 (c(x v c(y)) v c(x v y)) v x = c_0. [para(12(a,1),13(a,1,2))]. 27 x v (y v (z v c(x))) = y v (z v c_0). [para(23(a,1),9(a,1,2)),flip(a)]. 28 c(c(x v c(y v c(x))) v c(y v c_0)) = x. [para(23(a,1),12(a,1,1,2,1))]. 29 (c(x v c(y)) v c(x v y)) v (z v x) = z v c_0. [para(12(a,1),23(a,1,2,2))]. 30 x v (y v (z v (u v v))) = z v (x v (u v (y v v))). [para(18(a,1),9(a,1,2))]. 34 c(c(x v c(y v (z v u))) v c(z v (x v (y v u)))) = x. [para(18(a,1),12(a,1,1,2,1))]. 35 c(c(x v c(y v (z v u))) v c(y v (z v (x v u)))) = x. [para(18(a,2),12(a,1,1,2,1))]. 36 x v (y v (z v (u v c(x)))) = y v (z v (u v c_0)). [para(23(a,1),18(a,1,2,2)),flip(a)]. 45 c(c(c_0) v c(x v ((x v y) v y))) = x v y. [para(9(a,1),24(a,1,1,2,1))]. 47 c(x v c(c(c_0) v (x v x))) = c(c_0). [para(24(a,1),12(a,1,1,1))]. 48 c(c(c(c_0) v c(c(x v x))) v x) = c(c_0). [para(24(a,1),12(a,1,1,2))]. 49 (c(c_0) v c(x v x)) v x = c_0. [para(24(a,1),13(a,1,2))]. 50 (c(c_0) v c(x v x)) v (y v x) = y v c_0. [para(24(a,1),23(a,1,2,2))]. 51 c(c(c_0) v c(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)),demod(9(6))]. 53 x v ((c(c_0) v c(x v ((x v y) v y))) v y) = c_0. [para(49(a,1),9(a,1)),demod(9(6)),flip(a)]. 56 (c(c_0) v c(c(x) v c(x))) v c_0 = x v c_0. [para(49(a,1),23(a,1,2)),flip(a)]. 65 c(x v c(c(x v c(c(x))) v c_0)) = c(x v c(c(x))). [para(25(a,1),12(a,1,1,1))]. 66 c(c(c(x v c(c(x))) v c(c(c_0))) v x) = c(x v c(c(x))). [para(25(a,1),12(a,1,1,2))]. 68 (c(x v c(c(x))) v c(c_0)) v x = c_0. [para(25(a,1),13(a,1,2))]. 72 c(x v c(x v (c(c_0) v x))) = c(c_0). [para(9(a,1),47(a,1,1,2,1))]. 74 c(c(c_0) v c(x v (c(c_0) v (x v x)))) = x. [para(47(a,1),12(a,1,1,1))]. 76 (x v c(c(c_0) v (x v x))) v c(c_0) = c_0. [para(47(a,1),13(a,1,2))]. 105 c(c(c_0) v c(c(c_0) v (x v (x v x)))) = x. [para(47(a,1),19(a,1,1,1))]. 126 c(c(c_0) v c(x v (x v (c(c_0) v x)))) = x. [para(72(a,1),12(a,1,1,1))]. 141 (c(c(x) v c(y)) v c(c(x) v y)) v c_0 = x v c_0. [para(26(a,1),23(a,1,2)),flip(a)]. 152 (c(c(c_0) v c(c(x v x))) v x) v c(c_0) = c_0. [para(24(a,1),26(a,1,1,2))]. 158 (c(c_0) v c(x v (c(c_0) v (x v x)))) v x = c_0. [para(47(a,1),26(a,1,1,1))]. 169 (c(c_0) v c(x v (x v (c(c_0) v x)))) v x = c_0. [para(72(a,1),26(a,1,1,1))]. 243 c(c(c_0) v c((x v c(c(c_0) v (x v x))) v c_0)) = x v c(c(c_0) v (x v x)). [para(76(a,1),12(a,1,1,1,1))]. 244 (x v c(c(c_0) v (x v x))) v c_0 = c_0 v c_0. [para(76(a,1),23(a,1,2)),flip(a)]. 256 x v c(c(c_0) v (x v x)) = c_0. [back_demod(243),demod(244(10),24(8)),flip(a)]. 258 x v (y v c(c(c_0) v (x v x))) = y v c_0. [para(256(a,1),9(a,1,2)),flip(a)]. 260 x v c(x v (c(c_0) v x)) = c_0. [para(9(a,1),256(a,1,2,1))]. 261 (c(c_0) v (x v x)) v c_0 = x v c_0. [para(256(a,1),23(a,1,2))]. 262 c(c(c_0)) v c(c(c(c_0)) v c_0) = c_0. [para(23(a,1),256(a,1,2,1))]. 273 x v (y v c(x v (c(c_0) v x))) = y v c_0. [para(260(a,1),9(a,1,2)),flip(a)]. 284 (c(c(c_0)) v c_0) v c_0 = c(c(c_0)) v c_0. [para(23(a,1),261(a,1,1))]. 330 c(c(c_0) v c(c(c(c_0)) v (c(c(c_0)) v c_0))) = c(c(c_0)). [para(262(a,1),12(a,1,1,1,1))]. 336 (c(c(c_0)) v c_0) v (x v c_0) = x v (c(c(c_0)) v c_0). [para(262(a,1),27(a,1,2,2))]. 526 c(c(c(x v c(c_0)) v c(c((c(c_0) v c(y v y)) v (x v y)))) v x) = c(x v c(c_0)). [para(50(a,2),22(a,1,1,1,1,2,1,1))]. 547 (c(c(c_0) v c(c(x v x))) v x) v c_0 = c_0 v c_0. [para(48(a,1),56(a,1,1,2,1,1)),demod(48(13),56(11)),flip(a)]. 576 c(c(x v c((c(c(c_0)) v c_0) v c(x))) v c(c(c(c_0)) v c_0)) = x. [para(284(a,1),28(a,1,1,2,1))]. 581 c(c(x v c(c(x) v c(y))) v c(c(c(c(x) v c(y)) v c(c(c(x) v y))) v c_0)) = x. [para(22(a,1),28(a,1,1,1,1,2))]. 605 c(c(c_0) v c(x v ((x v c(c(c_0))) v ((x v c(c(c_0))) v c_0)))) = x v c(c(c_0)). [para(27(a,1),74(a,1,1,2,1,2)),demod(9(13),9(14))]. 618 c(c(c_0) v c(c(c_0) v (x v ((x v y) v ((x v y) v y))))) = x v y. [para(9(a,1),105(a,1,1,2,1,2,2)),demod(9(9))]. 680 (c(c_0) v (x v x)) v (y v c_0) = x v (y v c_0). [para(258(a,1),27(a,1,2))]. 805 c(c(c(x v c(y v c(x v (c(c_0) v x)))) v c(c(y v c_0))) v x) = c(x v c(y v c(x v (c(c_0) v x)))). [para(273(a,1),22(a,1,1,1,1,2,1,1))]. 808 (c(x v c(y v c(x v (c(c_0) v x)))) v c(y v c_0)) v (z v x) = z v c_0. [para(273(a,1),29(a,1,1,2,1))]. 817 c(c(c_0) v c(c(c(c_0)))) v c(c_0) = c(c(c_0) v c(c(c(c_0)))). [para(68(a,1),45(a,1,1,2,1,2)),demod(65(15)),flip(a)]. 825 c(c(c_0)) v c_0 = c(c(c_0)). [para(284(a,1),45(a,1,1,2,1,2,1)),demod(284(14),9(13),284(12),330(14),284(10)),flip(a)]. 842 c(c(x v c(c(c(c_0)) v c(x))) v c(c(c(c_0)))) = x. [back_demod(576),demod(825(5),825(13))]. 855 c(c(c_0)) v (x v c_0) = x v c(c(c_0)). [back_demod(336),demod(825(5),825(11))]. 858 (c(c_0) v c(c_0 v c_0)) v c(c(c_0)) = c(c(c_0)). [para(825(a,1),50(a,1,2)),demod(825(16))]. 861 c(c(c(c(c_0)) v (x v c_0)) v c(x v c(c_0))) = x. [para(855(a,2),12(a,1,1,1,1))]. 862 c(c_0) v (c(c(c_0)) v (x v c_0)) = x v c_0. [para(855(a,2),23(a,1,2))]. 898 c(c(c_0)) v (x v c_0) = (c(c_0) v c(c(x) v c(x))) v c(c(c_0)). [para(56(a,1),855(a,1,2))]. 1040 c(c(c_0)) v (x v (c(c_0) v c_0)) = x v c_0. [para(862(a,1),18(a,2))]. 1060 (c(c_0) v c(c(c_0) v ((c(c_0) v c_0) v c_0))) v c_0 = c(c(c_0)). [para(49(a,1),1040(a,1,2)),demod(825(5),9(14)),flip(a)]. 1083 c(c(c(c_0) v c(c(c(c_0))))) = c(c_0). [para(858(a,1),28(a,1,1,1,1,2,1)),demod(49(17),817(11))]. 1087 c(c(c_0) v c(c(c(c_0)))) = c_0. [para(1083(a,1),13(a,1,2)),demod(817(11))]. 1234 c(c(c(c_0) v c(c(c(c(c_0))))) v c_0) = c(c_0). [para(1087(a,1),12(a,1,1,2))]. 1247 c(c(c(c(c_0))) v c(c(c_0) v c_0)) = c(c(c_0)). [para(1087(a,1),28(a,1,1,1,1,2)),demod(825(5))]. 1294 c(c((c(c(c_0) v c(c(c(c(c_0))))) v c_0) v c(c(c_0))) v c(c_0)) = c(c(c_0) v c(c(c(c(c_0))))) v c_0. [para(1234(a,1),25(a,1,1,1,1,2,1))]. 1333 c(c(x v c(y v (z v (u v c(x))))) v c(z v (y v (u v c_0)))) = x. [para(27(a,1),34(a,1,1,2,1,2))]. 1414 c(c(c(c(c(c_0))) v c(c(c(c_0) v c_0))) v c(c(c_0))) = c(c(c(c_0))). [para(1247(a,1),12(a,1,1,2))]. 1455 c(c(c_0) v c(c(x v x))) v x = c_0. [para(152(a,1),12(a,1,1,1,1)),demod(547(12),24(8)),flip(a)]. 1477 c(c(x v c(y v c_0)) v c(y v ((c(z v c(c(z))) v c(c_0)) v (x v z)))) = x. [para(68(a,1),35(a,1,1,1,1,2,1,2))]. 1653 c(c((c(c_0) v c(c(c_0) v (c(x v c(y)) v ((c(x v c(y)) v c(x v y)) v ((c(x v c(y)) v c(x v y)) v c(x v y)))))) v x) v c(c_0)) = c(c_0) v c(c(c_0) v (c(x v c(y)) v ((c(x v c(y)) v c(x v y)) v ((c(x v c(y)) v c(x v y)) v c(x v y))))). [para(158(a,1),20(a,1,1,2,1)),demod(9(23),9(25),9(24),9(56),9(58),9(57))]. 1710 c(c(c(x v c(y v (z v (u v c(x))))) v c(c(y v (z v (u v c_0))))) v x) = c(x v c(y v (z v (u v c(x))))). [para(36(a,1),22(a,1,1,1,1,2,1,1))]. 1864 c_0 v (c(c_0) v c_0) = c_0. [para(680(a,1),45(a,1,1,2,1,2)),demod(9(10),9(9),126(13),9(7)),flip(a)]. 1887 c_0 v (x v (c(c_0) v c_0)) = x v c_0. [para(1864(a,1),9(a,1,2)),flip(a)]. 1893 (c(c_0 v c(c(c_0) v c_0)) v c(c_0)) v c_0 = c_0. [para(1864(a,1),26(a,1,1,2,1))]. 1897 c(c(c_0)) = c_0 v c_0. [para(1864(a,1),50(a,1,2)),demod(9(11),1060(15))]. 1898 (c(c_0 v c(c(c_0) v c_0)) v c(c_0)) v (x v c_0) = x v c_0. [para(1864(a,1),29(a,1,1,2,1))]. 1963 c(c_0 v (c(c(c_0 v c_0) v c(c(c(c_0) v c_0))) v c_0)) = c(c_0 v c_0). [back_demod(1414),demod(1897(3),1897(15),9(16),1897(20))]. 1975 c(c(c_0 v (c_0 v c_0)) v c(c_0)) = c_0. [back_demod(1294),demod(1897(5),1455(11),1897(4),1897(15),1455(21))]. 2022 (c(c_0) v c(c(c_0) v ((c(c_0) v c_0) v c_0))) v c_0 = c_0 v c_0. [back_demod(1060),demod(1897(18))]. 2058 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0). [back_demod(898),demod(1897(3),1897(16),9(17),56(16))]. 2078 c(c(c_0 v (x v c_0)) v c(x v c(c_0))) = x. [back_demod(861),demod(1897(3),2058(6))]. 2087 c(c(x v c((c_0 v c_0) v c(x))) v c(c_0 v c_0)) = x. [back_demod(842),demod(1897(3),1897(11))]. 2093 c(c(c_0) v c(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_demod(605),demod(1897(5),1897(9),1897(20))]. 2109 c(c(c_0 v (c(x v c(c(x))) v c_0)) v x) = c(x v c(c(x))). [back_demod(66),demod(1897(7),9(8))]. 2380 (c(x v (c_0 v c_0)) v c(x v c(c_0))) v x = c_0. [para(1897(a,1),26(a,1,1,1,1,2))]. 3326 c(c_0) v c(c(c_0) v c(c_0)) = c_0. [para(49(a,1),2078(a,1,1,2,1)),demod(56(12),1975(10)),flip(a)]. 3335 c(c(c_0) v c(x)) v c(c(c_0) v x) = c_0. [para(26(a,1),2078(a,1,1,2,1)),demod(141(13),1975(10)),flip(a)]. 3364 c(c_0) v (x v c(c(c_0) v c(c_0))) = x v c_0. [para(3326(a,1),9(a,1,2)),flip(a)]. 3365 (c(c_0) v c(c_0)) v c_0 = c(c_0) v c_0. [para(3326(a,1),23(a,1,2))]. 3376 (c(c_0) v c(c(c(c_0) v c(c_0)) v (c(c(c_0) v c(c_0)) v c_0))) v c(c(c_0) v c(c_0)) = c_0. [para(3326(a,1),169(a,1,1,2,1,2,2))]. 3521 c(c(c_0) v c(x)) v c_0 = (c(c_0) v x) v c_0. [para(3335(a,1),23(a,1,2)),flip(a)]. 3523 c(c(c_0) v c(x)) v (y v (z v c(c(c_0) v x))) = y v (z v c_0). [para(3335(a,1),18(a,1,2,2)),flip(a)]. 3579 (c(c_0) v c((c(c_0) v c_0) v ((c(c_0) v c_0) v c_0))) v c(c(c_0) v c(c_0)) = c_0. [back_demod(3376),demod(3521(16),9(15),3521(14))]. 3694 (c(c_0) v c(c_0)) v (x v c_0) = c(c_0) v (x v c_0). [para(3364(a,1),27(a,1,2))]. 3705 (c(c_0) v c((c(c_0) v c_0) v ((c(c_0) v c_0) v c_0))) v c_0 = c(c_0) v c_0. [para(158(a,1),3364(a,1,2)),demod(3364(28),3521(20),9(19),3521(18)),flip(a)]. 3707 x v ((c(c_0) v c(x v ((x v c(c(c_0) v c(c_0))) v ((x v c(c(c_0) v c(c_0))) v c_0)))) v c(c(c_0) v c(c_0))) = c_0. [para(3364(a,1),169(a,1,1,2,1,2,2)),demod(9(19),9(20),9(30))]. 3983 c(c(c_0) v c(c_0)) = c(c_0) v c_0. [para(3521(a,1),21(a,1,1,2,1,2)),demod(45(14)),flip(a)]. 4058 x v (c(c_0) v ((c(c_0) v c(x v ((x v (c(c_0) v c_0)) v ((x v (c(c_0) v c_0)) v c_0)))) v c_0)) = c_0. [back_demod(3707),demod(3983(8),3983(13),3983(24),9(23))]. 4071 c(c_0) v (c(c_0) v c_0) = c_0. [back_demod(3579),demod(3983(21),9(20),3705(19))]. 4107 c(c_0) v c_0 = c_0 v c_0. [para(4071(a,1),50(a,1,2)),demod(9(11),2022(15)),flip(a)]. 4108 c_0 v (c_0 v c_0) = c_0. [para(50(a,2),4071(a,1,2)),demod(9(11),49(10),4107(6),9(6),4107(5))]. 4109 c(c_0) v (x v (c(c_0) v (y v c_0))) = x v (y v c_0). [para(4071(a,1),30(a,1,2,2)),flip(a)]. 4117 x v (c(c_0) v ((c(c_0) v c(x v ((x v (c_0 v c_0)) v ((x v (c_0 v c_0)) v c_0)))) v c_0)) = c_0. [back_demod(4058),demod(4107(8),4107(12))]. 4148 (c(c_0) v c(c_0)) v c_0 = c_0 v c_0. [back_demod(3365),demod(4107(11))]. 4208 c(c_0 v c_0) = c(c_0). [back_demod(1963),demod(4107(9),13(11),4107(5),4108(5)),flip(a)]. 4225 c(c_0) v (x v c_0) = x v c_0. [back_demod(1898),demod(4107(5),4208(5),13(4),3694(8))]. 4228 c_0 v c_0 = c_0. [back_demod(1893),demod(4107(5),4208(5),13(4),4148(7))]. 4231 c_0 v (x v c_0) = x v c_0. [back_demod(1887),demod(4107(5),4228(4))]. 4254 c(c(x v c(c_0 v c(x))) v c(c_0)) = x. [back_demod(2087),demod(4228(3),4228(9))]. 4264 x v ((c(c_0) v c(x v ((x v c_0) v ((x v c_0) v c_0)))) v c_0) = c_0. [back_demod(4117),demod(4228(7),4228(9),4225(17))]. 4267 c(c_0) v (x v (y v c_0)) = x v (y v c_0). [back_demod(4109),demod(4225(7))]. 4284 c(c_0) v c_0 = c_0. [back_demod(4107),demod(4228(7))]. 4344 (c(x v c_0) v c(x v c(c_0))) v x = c_0. [back_demod(2380),demod(4228(3))]. 4350 c(c(c_0) v c(x v ((x v c_0) v ((x v c_0) v c_0)))) = x v c_0. [back_demod(2093),demod(4228(5),4228(7),4228(16))]. 4362 c(c(c_0)) = c_0. [back_demod(1897),demod(4228(6))]. 4367 c(c(c(x v c(c(x))) v c_0) v x) = c(x v c(c(x))). [back_demod(2109),demod(4231(8))]. 4719 x v ((x v c_0) v c_0) = x v c_0. [para(680(a,1),51(a,1,1,2,1,2,2)),demod(9(11),4267(12),9(10),4350(13),9(9),4267(10)),flip(a)]. 4749 c(c(c_0) v c(x v c_0)) = x v c_0. [para(3335(a,1),51(a,1,1,2,1,2,2,1,2)),demod(3523(16),4719(7),3335(17))]. 4768 x v (y v ((x v c_0) v c_0)) = y v (x v c_0). [para(4719(a,1),9(a,1,2)),flip(a)]. 4804 x v ((c(c_0) v c(x v c_0)) v c_0) = c_0. [back_demod(4264),demod(4768(10),9(7),4719(7))]. 4820 c(c(x v c_0) v c(c_0)) = x v c_0. [para(4749(a,1),28(a,1,1,1,1,2)),demod(9(5),4719(5),4284(7))]. 4833 c(c(x v (y v c_0)) v c(c(y v c_0) v (x v c(c_0)))) = x. [para(4820(a,1),19(a,1,1,1,1,2))]. 4843 c(c(x v c_0) v c((x v c_0) v (c(x v c_0) v c_0))) = x v c_0. [para(4820(a,1),21(a,1,1,2,1,2,1)),demod(9(11),4820(21))]. 4851 c(c(x v c_0) v c(c(x v c_0) v c_0)) = c_0. [para(4820(a,1),28(a,1,1,1,1,2)),demod(4231(4))]. 4859 x v (y v ((c(c_0) v c(x v c_0)) v c_0)) = y v c_0. [para(4804(a,1),9(a,1,2)),flip(a)]. 5006 c(x v c(c(x v c(c_0 v c(x))) v c_0)) = c(x v c(c_0 v c(x))). [para(4254(a,1),12(a,1,1,1))]. 5007 c(c(c(x v c(c_0 v c(x))) v c_0) v x) = c(x v c(c_0 v c(x))). [para(4254(a,1),12(a,1,1,2)),demod(4362(9))]. 5064 c(c(c_0) v c((c(c(x) v c_0) v c(c(x) v c(c_0))) v x)) = c(c(x) v c_0) v c(c(x) v c(c_0)). [para(4344(a,1),12(a,1,1,1,1))]. 5250 (x v c_0) v c_0 = c_0. [para(4719(a,1),53(a,1,2,1,2,1,2,1)),demod(4768(10),9(7),4719(7),9(11),4859(12))]. 5268 (x v c_0) v (y v c_0) = y v c_0. [para(5250(a,1),9(a,1,2)),flip(a)]. 5285 x v c_0 = c_0. [back_demod(4843),demod(5268(11),4851(11)),flip(a)]. 5388 c(c(c_0) v c((c(c_0) v c(c(x) v c(c_0))) v x)) = c(c_0) v c(c(x) v c(c_0)). [back_demod(5064),demod(5285(5),5285(17))]. 5408 c(x v c(c_0 v c(x))) = c(c(c_0) v x). [back_demod(5007),demod(5285(8)),flip(a)]. 5409 c(c(c_0) v x) = c(x v c(c_0)). [back_demod(5006),demod(5408(6),5285(6),5408(10)),flip(a)]. 5443 c(c(c_0) v c(c(c_0) v (x v c(c_0)))) = x. [back_demod(4833),demod(5285(2),5285(2),5285(4))]. 5525 c(x v c(c(x))) = c(c(c_0) v x). [back_demod(4367),demod(5285(6)),flip(a)]. 5860 c(x v c(y v (z v (u v c(x))))) = c(c(c_0) v x). [back_demod(1710),demod(5285(9),5285(9),5285(9),4362(10),5285(9)),flip(a)]. 5923 c(c(x v c(c_0)) v c(y v ((c(c(c_0) v z) v c(c_0)) v (x v z)))) = x. [back_demod(1477),demod(5285(2),5525(8))]. 5936 c(c(c_0) v c(c(c_0) v x)) = x. [back_demod(1333),demod(5860(7),5285(6),5285(6),5285(6),5409(8,R))]. 5995 (c(x v c(y v c(x v (c(c_0) v x)))) v c(c_0)) v (z v x) = c_0. [back_demod(808),demod(5285(11),5285(16))]. 5997 c(x v c(y v c(x v (c(c_0) v x)))) = c(c(c_0) v x). [back_demod(805),demod(5285(11),4362(12),5285(11)),flip(a)]. 6073 c(c(c_0) v c(x v c(c(x) v c(y)))) = x. [back_demod(581),demod(5285(18),5409(10,R))]. 6142 (c(c_0) v c(x v x)) v (y v x) = c_0. [back_demod(50),demod(5285(9))]. 6214 c(c(c_0) v c((c(c_0) v c(c(c_0) v (c(x v c(y)) v ((c(x v c(y)) v c(x v y)) v ((c(x v c(y)) v c(x v y)) v c(x v y)))))) v x)) = c(c_0) v c(c(c_0) v (c(x v c(y)) v ((c(x v c(y)) v c(x v y)) v ((c(x v c(y)) v c(x v y)) v c(x v y))))). [back_demod(1653),demod(5409(33,R))]. 6292 x v c(c_0) = x. [back_demod(5443),demod(5936(11))]. 6316 x v ((x v y) v ((x v y) v y)) = x v y. [back_demod(618),demod(5936(13))]. 6322 c(c(c_0) v x) v (y v x) = c_0. [back_demod(5995),demod(5997(9),6292(7))]. 6324 c(c(x)) = x. [back_demod(5923),demod(6292(3),6292(8),6322(7),5285(3),6292(4))]. 6334 c(c(c_0) v x) = c(x). [back_demod(526),demod(6292(3),6142(8),6324(4),5285(3),6292(7))]. 6427 (c(c_0) v x) v x = c(c_0) v x. [back_demod(5388),demod(6292(8),6324(6),6334(9),6324(6),6292(10),6324(8))]. 6483 c(c_0) v x = x. [back_demod(6214),demod(6316(26),6334(14),12(11),6427(6),6334(6),6334(5),6324(2),6316(24),6334(12),12(9)),flip(a)]. 6533 x v c(c(x) v c(y)) = x. [back_demod(6073),demod(6483(9),6324(7))]. 6534 $F # answer(B1). [resolve(6533,a,15,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 15. given #123 (F,wt=5): 5285 x v c_0 = c_0. [back_demod(4843),demod(5268(11),4851(11)),flip(a)]. given #124 (T,wt=5): 6324 c(c(x)) = x. [back_demod(5923),demod(6292(3),6292(8),6322(7),5285(3),6292(4))]. given #125 (T,wt=5): 6343 x v x = x. [back_demod(6284),demod(6334(7),6324(4),6292(5),6334(6),6324(3),6334(6),6324(3),6292(4))]. given #126 (A,wt=25): 85 c(x v c(y v (x v (c(x v c(y v z)) v z)))) = c(x v c(y v z)). [para(19(a,1),12(a,1,1,1)),demod(9(7),9(6))]. given #127 (F,wt=5): 6418 c_0 v x = c_0. [back_demod(5551),demod(6292(5),6324(4),6334(4),6337(2),6292(4))]. given #128 (F,wt=6): 6292 x v c(c_0) = x. [back_demod(5443),demod(5936(11))]. % Operation v is associative-commutative; redundancy checks enabled. given #129 (T,wt=6): 6483 c(c_0) v x = x. [back_demod(6214),demod(6316(26),6334(14),12(11),6427(6),6334(6),6334(5),6324(2),6316(24),6334(12),12(9)),flip(a)]. given #130 (T,wt=7): 7060 x v y = y v x. [para(6292(a,1),9(a,1,2)),demod(6292(4))]. given #131 (A,wt=21): 87 c(c(x v y) v c(c(y v c(z)) v (x v c(y v z)))) = x. [para(12(a,1),19(a,1,1,1,1,2))]. given #132 (F,wt=8): 6146 x v (y v c(x)) = c_0. [back_demod(23),demod(5285(5))]. given #133 (F,wt=8): 6331 c(x) v (y v x) = c_0. [back_demod(6015),demod(6292(3),6142(8),6292(4))]. given #134 (T,wt=8): 7402 x v (c(x) v y) = c_0. [para(7060(a,1),6146(a,1,2))]. given #135 (T,wt=8): 7408 (x v y) v c(y) = c_0. [para(6331(a,1),7060(a,1)),flip(a)]. given #136 (A,wt=25): 91 c(c(x v c(y v (z v (u v v)))) v c(z v (x v (u v (y v v))))) = x. [para(18(a,1),19(a,1,1,1,1,2,1))]. given #137 (F,wt=8): 7443 (x v y) v c(x) = c_0. [para(7060(a,1),7408(a,1,1))]. given #138 (F,wt=9): 6941 x v c(y v c(x)) = x. [back_demod(6524),demod(6933(10))]. given #139 (T,wt=9): 6958 x v (y v x) = y v x. [para(6343(a,1),9(a,1,2)),flip(a)]. given #140 (T,wt=9): 7262 x v (x v y) = x v y. [back_demod(6525),demod(7060(2))]. given #141 (A,wt=25): 92 c(c(x v c(y v (z v (u v v)))) v c(y v (u v (x v (z v v))))) = x. [para(18(a,1),19(a,1,1,2,1,2))]. given #142 (F,wt=9): 7561 x v c(c(x) v y) = x. [para(7060(a,1),6941(a,1,2,1))]. given #143 (F,wt=10): 6145 x v (y v (z v c(x))) = c_0. [back_demod(27),demod(5285(6),5285(6))]. given #144 (T,wt=10): 6380 c(x) v c(y v x) = c(x). [back_demod(6136),demod(6334(6),6292(6),6334(9),6324(6),6334(8),6292(8))]. given #145 (T,wt=10): 6381 c(x) v (y v (z v x)) = c_0. [back_demod(6116),demod(6334(4),6292(4))]. given #146 (A,wt=21): 93 c(c(x v c(y v (z v u))) v c(z v (y v (x v u)))) = x. [para(18(a,1),19(a,1,1,2,1))]. given #147 (F,wt=10): 7296 x v (y v c(x v y)) = c_0. [back_demod(6342),demod(7060(3))]. given #148 (F,wt=10): 7409 x v (y v (c(x) v z)) = c_0. [para(7402(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. given #149 (T,wt=10): 7411 c(x) v (y v (x v z)) = c_0. [para(7402(a,1),18(a,1,2)),demod(5285(2)),flip(a)]. given #150 (T,wt=10): 7416 (x v y) v (z v c(y)) = c_0. [para(7408(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. given #151 (A,wt=25): 94 c(c(x v c(y v (z v (u v v)))) v c(u v (x v (y v (z v v))))) = x. [para(18(a,2),19(a,1,1,1,1,2,1))]. given #152 (F,wt=10): 7549 (x v y) v (z v c(x)) = c_0. [para(7443(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. given #153 (F,wt=10): 7550 (x v (y v z)) v c(y) = c_0. [para(9(a,1),7443(a,1,1))]. given #154 (T,wt=10): 7710 c(x) v c(x v y) = c(x). [para(6324(a,1),7561(a,1,2,1,1))]. given #155 (T,wt=10): 7711 x v ((y v c(x)) v z) = c_0. [para(7060(a,1),6145(a,1,2))]. given #156 (A,wt=25): 95 c(c(x v c(y v (z v (u v v)))) v c(y v (z v (u v (x v v))))) = x. [para(18(a,2),19(a,1,1,2,1,2))]. given #157 (F,wt=10): 7712 (x v c(y)) v (z v y) = c_0. [para(6941(a,1),6145(a,1,2,2))]. given #158 (F,wt=10): 7713 (c(x) v y) v (z v x) = c_0. [para(7561(a,1),6145(a,1,2,2))]. given #159 (T,wt=10): 7768 (x v (y v z)) v c(z) = c_0. [para(6381(a,1),7060(a,1)),flip(a)]. given #160 (T,wt=10): 7769 c(x) v ((y v x) v z) = c_0. [para(7060(a,1),6381(a,1,2))]. given #161 (A,wt=25): 106 c(c(x v y) v c(c(y v c(z v u)) v (x v c(z v (y v u))))) = x. [para(19(a,1),19(a,1,1,1,1,2))]. given #162 (F,wt=10): 7856 x v ((c(x) v y) v z) = c_0. [para(7060(a,1),7409(a,1,2))]. given #163 (F,wt=10): 7859 c(x) v ((x v y) v z) = c_0. [para(7060(a,1),7411(a,1,2))]. given #164 (T,wt=10): 7884 (x v y) v (c(y) v z) = c_0. [para(7060(a,1),7416(a,1,2))]. given #165 (T,wt=10): 7959 (x v y) v (c(x) v z) = c_0. [para(7060(a,1),7549(a,1,2))]. given #166 (A,wt=23): 362 x v (y v (z v (u v (v v w)))) = v v (x v (y v (u v (z v w)))). [para(31(a,1),18(a,1,2,2))]. given #167 (F,wt=10): 7960 ((x v y) v z) v c(y) = c_0. [para(6380(a,1),7549(a,1,2))]. given #168 (F,wt=10): 7965 ((x v y) v z) v c(x) = c_0. [para(7060(a,1),7550(a,1,1))]. given #169 (T,wt=11): 6940 x v c(y v (z v c(x))) = x. [back_demod(6526),demod(6933(12))]. given #170 (T,wt=11): 7119 x v c(x v y) = x v c(y). [back_demod(6936),demod(7060(4),6941(4))]. given #171 (A,wt=23): 363 x v (y v (z v (u v (v v w)))) = z v (x v (v v (u v (y v w)))). [para(31(a,1),18(a,2,2,2))]. given #172 (F,wt=11): 7703 x v c(y v (c(x) v z)) = x. [para(9(a,1),7561(a,1,2,1))]. given #173 (F,wt=11): 8328 x v c((y v c(x)) v z) = x. [para(7711(a,1),106(a,1,1,1,1)),demod(9(17),6934(16),6483(9),6324(7))]. given #174 (T,wt=11): 8508 x v c(y v x) = x v c(y). [para(7060(a,1),7119(a,1,2,1))]. given #175 (T,wt=11): 8510 x v c((c(x) v y) v z) = x. [para(7856(a,1),7119(a,1,2,1)),demod(6292(3)),flip(a)]. given #176 (A,wt=19): 364 x v (y v (z v (u v v))) = u v (z v (x v (y v v))). [para(31(a,1),18(a,2,2)),flip(a)]. given #177 (F,wt=12): 6143 x v (y v (z v (u v c(x)))) = c_0. [back_demod(36),demod(5285(7),5285(7),5285(7))]. given #178 (F,wt=12): 6379 x v (c(x v y) v (z v y)) = c_0. [back_demod(6137),demod(6334(5),6292(5))]. given #179 (T,wt=12): 6394 c(x) v c(y v (z v x)) = c(x). [back_demod(5922),demod(6334(6),6292(6),6334(10),6324(7),6334(9),6292(9))]. given #180 (T,wt=12): 6397 c(x) v (y v (z v (u v x))) = c_0. [back_demod(5858),demod(6292(3),6292(4))]. given #181 (A,wt=23): 365 x v (y v (z v (u v (v v w)))) = u v (y v (x v (v v (z v w)))). [para(18(a,1),31(a,1,2,2))]. given #182 (F,wt=12): 7410 x v (y v (z v (c(x) v u))) = c_0. [para(7402(a,1),18(a,1,2,2)),demod(5285(2),5285(2)),flip(a)]. given #183 (F,wt=12): 7412 c(x) v (y v (z v (x v u))) = c_0. [para(7402(a,1),30(a,1,2)),demod(5285(2)),flip(a)]. given #184 (T,wt=12): 7417 (x v (y v z)) v c(x v z) = c_0. [para(9(a,1),7408(a,1,1))]. given #185 (T,wt=12): 7418 (x v y) v (z v (u v c(y))) = c_0. [para(7408(a,1),18(a,1,2,2)),demod(5285(2),5285(2)),flip(a)]. given #186 (A,wt=23): 366 x v (y v (z v (u v (v v w)))) = v v (y v (x v (z v (u v w)))). [para(18(a,2),31(a,1,2,2))]. given #187 (F,wt=12): 7551 (x v y) v (z v (u v c(x))) = c_0. [para(7443(a,1),18(a,1,2,2)),demod(5285(2),5285(2)),flip(a)]. given #188 (F,wt=12): 7552 (x v (y v (z v u))) v c(z) = c_0. [para(18(a,2),7443(a,1,1))]. given #189 (T,wt=12): 7954 (x v (y v z)) v (u v c(y)) = c_0. [para(9(a,1),7549(a,1,1))]. given #190 (T,wt=12): 7967 c(x) v c(y v (x v z)) = c(x). [para(9(a,1),7710(a,1,2,1))]. given #191 (A,wt=25): 368 c(c(x v c(y v (z v (u v v)))) v c(u v (x v (z v (y v v))))) = x. [para(31(a,1),19(a,1,1,1,1,2,1))]. given #192 (F,wt=12): 7973 x v (y v ((z v c(x)) v u)) = c_0. [para(7711(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. given #193 (F,wt=12): 7975 (x v c(y)) v (z v (y v u)) = c_0. [para(7711(a,1),18(a,1,2)),demod(5285(2)),flip(a)]. given #194 (T,wt=12): 8060 (x v c(y)) v (z v (u v y)) = c_0. [para(7712(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. given #195 (T,wt=12): 8109 (c(x) v y) v (z v (u v x)) = c_0. [para(7713(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. given #196 (A,wt=25): 369 c(c(x v c(y v (z v (u v v)))) v c(y v (u v (z v (x v v))))) = x. [para(31(a,1),19(a,1,1,2,1,2))]. given #197 (F,wt=12): 8110 (x v (c(y) v z)) v (u v y) = c_0. [para(9(a,1),7713(a,1,1))]. given #198 (F,wt=12): 8165 (x v (y v z)) v (u v c(z)) = c_0. [para(7768(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. given #199 (T,wt=12): 8201 c(x) v (y v ((z v x) v u)) = c_0. [para(7769(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. given #200 (T,wt=12): 8204 (x v y) v (z v (c(y) v u)) = c_0. [para(7769(a,1),18(a,1,2)),demod(5285(2)),flip(a)]. given #201 (A,wt=23): 380 x v (y v (z v (u v (v v w)))) = v v (y v (x v (u v (z v w)))). [para(31(a,1),31(a,1,2,2))]. given #202 (F,wt=12): 8337 c(x) v c((y v x) v z) = c(x). [para(7769(a,1),106(a,1,1,1,1)),demod(9(16),6934(15),6483(9),6324(7))]. given #203 (F,wt=12): 8357 x v (y v ((c(x) v z) v u)) = c_0. [para(7856(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. given #204 (T,wt=12): 8358 x v ((y v (c(x) v z)) v u) = c_0. [para(9(a,1),7856(a,1,2,1))]. given #205 (T,wt=12): 8360 (c(x) v y) v (z v (x v u)) = c_0. [para(7856(a,1),18(a,1,2)),demod(5285(2)),flip(a)]. given #206 (A,wt=19): 440 x v (y v (z v (u v v))) = x v (u v (y v (z v v))). [para(9(a,1),33(a,1,2,2))]. given #207 (F,wt=12): 8368 c(x) v (y v ((x v z) v u)) = c_0. [para(7859(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. given #208 (F,wt=12): 8369 c(x) v ((y v (x v z)) v u) = c_0. [para(9(a,1),7859(a,1,2,1))]. given #209 (T,wt=12): 8371 (x v y) v (z v (c(x) v u)) = c_0. [para(7859(a,1),18(a,1,2)),demod(5285(2)),flip(a)]. given #210 (T,wt=12): 8403 (x v (y v z)) v (c(y) v u) = c_0. [para(9(a,1),7959(a,1,1))]. given #211 (A,wt=23): 441 x v (y v (z v (u v (v v w)))) = z v (x v (y v (v v (u v w)))). [para(33(a,1),18(a,1,2,2))]. given #212 (F,wt=12): 8444 ((x v y) v z) v (u v c(y)) = c_0. [para(7960(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. given #213 (F,wt=12): 8446 (x v ((y v z) v u)) v c(z) = c_0. [para(9(a,1),7960(a,1,1))]. given #214 (T,wt=12): 8477 ((x v y) v z) v (u v c(x)) = c_0. [para(7965(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. given #215 (T,wt=12): 8478 ((x v (y v z)) v u) v c(y) = c_0. [para(9(a,1),7965(a,1,1,1))]. given #216 (A,wt=23): 442 x v (y v (z v (u v (v v w)))) = x v (u v (y v (v v (z v w)))). [para(18(a,1),33(a,1,2,2))]. given #217 (F,wt=12): 8479 (x v ((y v z) v u)) v c(y) = c_0. [para(9(a,1),7965(a,1,1))]. given #218 (F,wt=12): 8495 (x v (y v c(z))) v (u v z) = c_0. [para(6940(a,1),6145(a,1,2,2))]. given #219 (T,wt=12): 8497 x v ((y v (z v c(x))) v u) = c_0. [para(6940(a,1),7549(a,1,2)),demod(7060(5))]. given #220 (T,wt=12): 8511 c(x) v c((x v y) v z) = c(x). [para(7859(a,1),7119(a,1,2,1)),demod(6292(4)),flip(a)]. given #221 (A,wt=19): 443 x v (y v (z v (u v v))) = x v (u v (z v (y v v))). [para(18(a,1),33(a,1,2))]. given #222 (F,wt=12): 8598 ((x v c(y)) v z) v (u v y) = c_0. [para(8328(a,1),6145(a,1,2,2))]. given #223 (F,wt=12): 8599 x v (((y v c(x)) v z) v u) = c_0. [para(8328(a,1),7549(a,1,2)),demod(7060(5))]. given #224 (T,wt=12): 8600 (x v y) v ((z v c(y)) v u) = c_0. [para(8328(a,1),7768(a,1,1,2)),demod(6324(6))]. given #225 (T,wt=12): 8601 (x v y) v ((z v c(x)) v u) = c_0. [para(8328(a,1),7960(a,1,1,1)),demod(6324(6))]. given #226 (A,wt=23): 444 x v (y v (z v (u v (v v w)))) = x v (v v (y v (z v (u v w)))). [para(18(a,2),33(a,1,2,2))]. given #227 (F,wt=12): 8653 ((c(x) v y) v z) v (u v x) = c_0. [para(8510(a,1),6145(a,1,2,2))]. given #228 (F,wt=12): 8654 x v (((c(x) v y) v z) v u) = c_0. [para(8510(a,1),7549(a,1,2)),demod(7060(5))]. given #229 (T,wt=12): 8655 (x v y) v ((c(y) v z) v u) = c_0. [para(8510(a,1),7768(a,1,1,2)),demod(6324(6))]. given #230 (T,wt=12): 8656 (x v y) v ((c(x) v z) v u) = c_0. [para(8510(a,1),7960(a,1,1,1)),demod(6324(6))]. given #231 (A,wt=19): 445 x v (y v (z v (u v v))) = x v (y v (u v (z v v))). [para(18(a,2),33(a,1,2))]. given #232 (F,wt=12): 8720 x v (c(y v x) v (z v y)) = c_0. [para(7060(a,1),6379(a,1,2,1,1))]. given #233 (F,wt=12): 8721 x v (y v (c(x v y) v z)) = c_0. [para(7060(a,1),6379(a,1,2,2)),demod(9(4))]. given #234 (T,wt=12): 8772 (x v (y v (z v u))) v c(u) = c_0. [para(6394(a,1),7416(a,1,2))]. given #235 (T,wt=12): 8773 ((x v (y v z)) v u) v c(z) = c_0. [para(6394(a,1),7549(a,1,2))]. given #236 (A,wt=25): 447 c(c(x v c(y v (z v (u v v)))) v c(y v (x v (u v (z v v))))) = x. [para(33(a,1),19(a,1,1,1,1,2,1))]. given #237 (F,wt=12): 8774 (x v (y v z)) v (c(z) v u) = c_0. [para(6394(a,1),7711(a,1,2,1))]. given #238 (F,wt=12): 8775 c(x) v ((y v (z v x)) v u) = c_0. [para(6394(a,1),7884(a,1,1)),demod(6324(5))]. given #239 (T,wt=12): 8907 (x v (y v z)) v c(x v y) = c_0. [para(7060(a,1),7417(a,1,1,2))]. given #240 (T,wt=11): 11316 (x v y) v z = x v (y v z). [para(8907(a,1),7119(a,1,2,1)),demod(6292(5),6324(7),7060(6),9(6),9(5),8514(5),8515(5)),flip(a)]. given #241 (A,wt=23): 458 x v (y v (z v (u v (v v w)))) = z v (y v (x v (v v (u v w)))). [para(33(a,1),31(a,1,2,2))]. given #242 (F,wt=12): 10642 c(x v y) v (z v (y v x)) = c_0. [para(8720(a,1),18(a,2))]. given #243 (F,wt=13): 6341 c(c(x v y) v c(c(y) v x)) = x. [back_demod(6286),demod(6334(6),6292(6))]. given #244 (T,wt=13): 6935 c(x v y) v c(x v c(y)) = c(x). [para(20(a,1),6324(a,1,1)),demod(6933(9)),flip(a)]. given #245 (T,wt=13): 6939 x v c(y v (z v (u v c(x)))) = x. [back_demod(6547),demod(6933(14))]. given #246 (A,wt=23): 459 x v (y v (z v (u v (v v w)))) = x v (v v (y v (u v (z v w)))). [para(31(a,1),33(a,1,2,2))]. given #247 (F,wt=13): 6959 x v (y v (z v x)) = y v (z v x). [para(6343(a,1),18(a,1,2,2)),flip(a)]. given #248 (F,wt=13): 7118 x v (y v (x v z)) = y v (x v z). [back_demod(6960),demod(7060(2),6958(2))]. given #249 (T,wt=13): 7542 x v c(y v (z v (c(x) v u))) = x. [para(7402(a,1),91(a,1,1,2,1,2)),demod(5285(9),7060(10),6483(10),6324(8))]. given #250 (T,wt=13): 7557 x v (y v c(z v c(x))) = y v x. [para(6941(a,1),9(a,1,2)),flip(a)]. given #251 (A,wt=23): 461 x v (y v (z v (u v (v v w)))) = x v (z v (y v (v v (u v w)))). [para(33(a,1),33(a,1,2,2))]. given #252 (F,wt=13): 7702 x v (y v c(c(x) v z)) = y v x. [para(7561(a,1),9(a,1,2)),flip(a)]. given #253 (F,wt=13): 8640 c(x v y) v c(y v c(x)) = c(y). [para(8508(a,1),8508(a,1,2,1)),demod(7060(10),6380(10))]. given #254 (T,wt=13): 12281 x v (c(y v c(x)) v z) = x v z. [para(6941(a,1),11316(a,1,1)),flip(a)]. given #255 (T,wt=13): 12283 x v (c(c(x) v y) v z) = x v z. [para(7561(a,1),11316(a,1,1)),flip(a)]. given #256 (A,wt=27): 908 x v (y v (z v (u v (v v (w v v6))))) = u v (x v (y v (w v (z v (v v v6))))). [para(30(a,1),18(a,1,2,2))]. given #257 (F,wt=13): 12465 c(x v y) v c(c(y) v x) = c(x). [para(6341(a,1),6324(a,1,1)),flip(a)]. ============================== PROOF ================================= % Proof 3 at 5.71 (+ 0.04) seconds: MOD. % Length of proof is 201. % Level of proof is 49. % Maximum clause weight is 86. % Given clauses 257. 3 x v c(x) = y v c(y) # label(ONE). [input]. 4 (x v c(y)) ^ (x v y) = x # label(CUT). [input]. 8 c7 v (c9 ^ (c7 v c8)) != c7 v (c8 ^ (c7 v c9)) # answer(MOD). [clausify]. 9 x v (y v z) = y v (x v z) # label(AJ). [input]. 10 x ^ y = c(c(x) v c(y)) # label(DM). [input]. 11 x v c(x) = y v c(y) # label(ONE). [copy(3)]. 12 c(c(x v c(y)) v c(x v y)) = x # label(CUT). [copy(4),demod(10(4))]. 13 x v c(x) = c_0. [new_symbol(11)]. 17 c7 v c(c(c8) v c(c7 v c9)) != c7 v c(c(c9) v c(c7 v c8)) # answer(MOD). [copy(8),demod(10(6),10(16)),flip(a)]. 18 x v (y v (z v u)) = z v (x v (y v u)). [para(9(a,1),9(a,1,2))]. 19 c(c(x v c(y v z)) v c(y v (x v z))) = x. [para(9(a,1),12(a,1,1,2,1))]. 20 c(c(x v y) v c(x v (c(y v c(z)) v c(y v z)))) = x. [para(12(a,1),12(a,1,1,1,1,2))]. 21 c(x v c(x v (c(x v c(y)) v y))) = c(x v c(y)). [para(12(a,1),12(a,1,1,1)),demod(9(5))]. 22 c(c(c(x v c(y)) v c(c(x v y))) v x) = c(x v c(y)). [para(12(a,1),12(a,1,1,2))]. 23 x v (y v c(x)) = y v c_0. [para(13(a,1),9(a,1,2)),flip(a)]. 24 c(c(c_0) v c(x v x)) = x. [para(13(a,1),12(a,1,1,1,1))]. 25 c(c(x v c(c(x))) v c(c_0)) = x. [para(13(a,1),12(a,1,1,2,1))]. 26 (c(x v c(y)) v c(x v y)) v x = c_0. [para(12(a,1),13(a,1,2))]. 27 x v (y v (z v c(x))) = y v (z v c_0). [para(23(a,1),9(a,1,2)),flip(a)]. 28 c(c(x v c(y v c(x))) v c(y v c_0)) = x. [para(23(a,1),12(a,1,1,2,1))]. 29 (c(x v c(y)) v c(x v y)) v (z v x) = z v c_0. [para(12(a,1),23(a,1,2,2))]. 30 x v (y v (z v (u v v))) = z v (x v (u v (y v v))). [para(18(a,1),9(a,1,2))]. 34 c(c(x v c(y v (z v u))) v c(z v (x v (y v u)))) = x. [para(18(a,1),12(a,1,1,2,1))]. 35 c(c(x v c(y v (z v u))) v c(y v (z v (x v u)))) = x. [para(18(a,2),12(a,1,1,2,1))]. 36 x v (y v (z v (u v c(x)))) = y v (z v (u v c_0)). [para(23(a,1),18(a,1,2,2)),flip(a)]. 45 c(c(c_0) v c(x v ((x v y) v y))) = x v y. [para(9(a,1),24(a,1,1,2,1))]. 47 c(x v c(c(c_0) v (x v x))) = c(c_0). [para(24(a,1),12(a,1,1,1))]. 48 c(c(c(c_0) v c(c(x v x))) v x) = c(c_0). [para(24(a,1),12(a,1,1,2))]. 49 (c(c_0) v c(x v x)) v x = c_0. [para(24(a,1),13(a,1,2))]. 50 (c(c_0) v c(x v x)) v (y v x) = y v c_0. [para(24(a,1),23(a,1,2,2))]. 51 c(c(c_0) v c(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)),demod(9(6))]. 53 x v ((c(c_0) v c(x v ((x v y) v y))) v y) = c_0. [para(49(a,1),9(a,1)),demod(9(6)),flip(a)]. 56 (c(c_0) v c(c(x) v c(x))) v c_0 = x v c_0. [para(49(a,1),23(a,1,2)),flip(a)]. 65 c(x v c(c(x v c(c(x))) v c_0)) = c(x v c(c(x))). [para(25(a,1),12(a,1,1,1))]. 66 c(c(c(x v c(c(x))) v c(c(c_0))) v x) = c(x v c(c(x))). [para(25(a,1),12(a,1,1,2))]. 68 (c(x v c(c(x))) v c(c_0)) v x = c_0. [para(25(a,1),13(a,1,2))]. 72 c(x v c(x v (c(c_0) v x))) = c(c_0). [para(9(a,1),47(a,1,1,2,1))]. 74 c(c(c_0) v c(x v (c(c_0) v (x v x)))) = x. [para(47(a,1),12(a,1,1,1))]. 76 (x v c(c(c_0) v (x v x))) v c(c_0) = c_0. [para(47(a,1),13(a,1,2))]. 103 c(c(x v y) v c(c(y v c(c(y))) v (x v c(c_0)))) = x. [para(25(a,1),19(a,1,1,1,1,2))]. 105 c(c(c_0) v c(c(c_0) v (x v (x v x)))) = x. [para(47(a,1),19(a,1,1,1))]. 122 c(c((c(x v c(c(x))) v c(c_0)) v c(y v x)) v c(y v c_0)) = c(x v c(c(x))) v c(c_0). [para(68(a,1),19(a,1,1,2,1,2))]. 126 c(c(c_0) v c(x v (x v (c(c_0) v x)))) = x. [para(72(a,1),12(a,1,1,1))]. 141 (c(c(x) v c(y)) v c(c(x) v y)) v c_0 = x v c_0. [para(26(a,1),23(a,1,2)),flip(a)]. 152 (c(c(c_0) v c(c(x v x))) v x) v c(c_0) = c_0. [para(24(a,1),26(a,1,1,2))]. 158 (c(c_0) v c(x v (c(c_0) v (x v x)))) v x = c_0. [para(47(a,1),26(a,1,1,1))]. 169 (c(c_0) v c(x v (x v (c(c_0) v x)))) v x = c_0. [para(72(a,1),26(a,1,1,1))]. 191 c(c(x v c_0) v c(y v (c((x v c(y)) v c(z)) v c((x v c(y)) v z)))) = y. [para(23(a,1),20(a,1,1,1,1))]. 243 c(c(c_0) v c((x v c(c(c_0) v (x v x))) v c_0)) = x v c(c(c_0) v (x v x)). [para(76(a,1),12(a,1,1,1,1))]. 244 (x v c(c(c_0) v (x v x))) v c_0 = c_0 v c_0. [para(76(a,1),23(a,1,2)),flip(a)]. 256 x v c(c(c_0) v (x v x)) = c_0. [back_demod(243),demod(244(10),24(8)),flip(a)]. 258 x v (y v c(c(c_0) v (x v x))) = y v c_0. [para(256(a,1),9(a,1,2)),flip(a)]. 260 x v c(x v (c(c_0) v x)) = c_0. [para(9(a,1),256(a,1,2,1))]. 261 (c(c_0) v (x v x)) v c_0 = x v c_0. [para(256(a,1),23(a,1,2))]. 262 c(c(c_0)) v c(c(c(c_0)) v c_0) = c_0. [para(23(a,1),256(a,1,2,1))]. 273 x v (y v c(x v (c(c_0) v x))) = y v c_0. [para(260(a,1),9(a,1,2)),flip(a)]. 284 (c(c(c_0)) v c_0) v c_0 = c(c(c_0)) v c_0. [para(23(a,1),261(a,1,1))]. 330 c(c(c_0) v c(c(c(c_0)) v (c(c(c_0)) v c_0))) = c(c(c_0)). [para(262(a,1),12(a,1,1,1,1))]. 336 (c(c(c_0)) v c_0) v (x v c_0) = x v (c(c(c_0)) v c_0). [para(262(a,1),27(a,1,2,2))]. 526 c(c(c(x v c(c_0)) v c(c((c(c_0) v c(y v y)) v (x v y)))) v x) = c(x v c(c_0)). [para(50(a,2),22(a,1,1,1,1,2,1,1))]. 547 (c(c(c_0) v c(c(x v x))) v x) v c_0 = c_0 v c_0. [para(48(a,1),56(a,1,1,2,1,1)),demod(48(13),56(11)),flip(a)]. 576 c(c(x v c((c(c(c_0)) v c_0) v c(x))) v c(c(c(c_0)) v c_0)) = x. [para(284(a,1),28(a,1,1,2,1))]. 605 c(c(c_0) v c(x v ((x v c(c(c_0))) v ((x v c(c(c_0))) v c_0)))) = x v c(c(c_0)). [para(27(a,1),74(a,1,1,2,1,2)),demod(9(13),9(14))]. 618 c(c(c_0) v c(c(c_0) v (x v ((x v y) v ((x v y) v y))))) = x v y. [para(9(a,1),105(a,1,1,2,1,2,2)),demod(9(9))]. 680 (c(c_0) v (x v x)) v (y v c_0) = x v (y v c_0). [para(258(a,1),27(a,1,2))]. 771 (c(x v c(c_0)) v c((c(c_0) v c(y v y)) v (x v y))) v (z v x) = z v c_0. [para(50(a,2),29(a,1,1,2,1))]. 805 c(c(c(x v c(y v c(x v (c(c_0) v x)))) v c(c(y v c_0))) v x) = c(x v c(y v c(x v (c(c_0) v x)))). [para(273(a,1),22(a,1,1,1,1,2,1,1))]. 808 (c(x v c(y v c(x v (c(c_0) v x)))) v c(y v c_0)) v (z v x) = z v c_0. [para(273(a,1),29(a,1,1,2,1))]. 817 c(c(c_0) v c(c(c(c_0)))) v c(c_0) = c(c(c_0) v c(c(c(c_0)))). [para(68(a,1),45(a,1,1,2,1,2)),demod(65(15)),flip(a)]. 825 c(c(c_0)) v c_0 = c(c(c_0)). [para(284(a,1),45(a,1,1,2,1,2,1)),demod(284(14),9(13),284(12),330(14),284(10)),flip(a)]. 842 c(c(x v c(c(c(c_0)) v c(x))) v c(c(c(c_0)))) = x. [back_demod(576),demod(825(5),825(13))]. 855 c(c(c_0)) v (x v c_0) = x v c(c(c_0)). [back_demod(336),demod(825(5),825(11))]. 858 (c(c_0) v c(c_0 v c_0)) v c(c(c_0)) = c(c(c_0)). [para(825(a,1),50(a,1,2)),demod(825(16))]. 861 c(c(c(c(c_0)) v (x v c_0)) v c(x v c(c_0))) = x. [para(855(a,2),12(a,1,1,1,1))]. 862 c(c_0) v (c(c(c_0)) v (x v c_0)) = x v c_0. [para(855(a,2),23(a,1,2))]. 898 c(c(c_0)) v (x v c_0) = (c(c_0) v c(c(x) v c(x))) v c(c(c_0)). [para(56(a,1),855(a,1,2))]. 1040 c(c(c_0)) v (x v (c(c_0) v c_0)) = x v c_0. [para(862(a,1),18(a,2))]. 1060 (c(c_0) v c(c(c_0) v ((c(c_0) v c_0) v c_0))) v c_0 = c(c(c_0)). [para(49(a,1),1040(a,1,2)),demod(825(5),9(14)),flip(a)]. 1083 c(c(c(c_0) v c(c(c(c_0))))) = c(c_0). [para(858(a,1),28(a,1,1,1,1,2,1)),demod(49(17),817(11))]. 1087 c(c(c_0) v c(c(c(c_0)))) = c_0. [para(1083(a,1),13(a,1,2)),demod(817(11))]. 1234 c(c(c(c_0) v c(c(c(c(c_0))))) v c_0) = c(c_0). [para(1087(a,1),12(a,1,1,2))]. 1247 c(c(c(c(c_0))) v c(c(c_0) v c_0)) = c(c(c_0)). [para(1087(a,1),28(a,1,1,1,1,2)),demod(825(5))]. 1294 c(c((c(c(c_0) v c(c(c(c(c_0))))) v c_0) v c(c(c_0))) v c(c_0)) = c(c(c_0) v c(c(c(c(c_0))))) v c_0. [para(1234(a,1),25(a,1,1,1,1,2,1))]. 1333 c(c(x v c(y v (z v (u v c(x))))) v c(z v (y v (u v c_0)))) = x. [para(27(a,1),34(a,1,1,2,1,2))]. 1414 c(c(c(c(c(c_0))) v c(c(c(c_0) v c_0))) v c(c(c_0))) = c(c(c(c_0))). [para(1247(a,1),12(a,1,1,2))]. 1455 c(c(c_0) v c(c(x v x))) v x = c_0. [para(152(a,1),12(a,1,1,1,1)),demod(547(12),24(8)),flip(a)]. 1477 c(c(x v c(y v c_0)) v c(y v ((c(z v c(c(z))) v c(c_0)) v (x v z)))) = x. [para(68(a,1),35(a,1,1,1,1,2,1,2))]. 1653 c(c((c(c_0) v c(c(c_0) v (c(x v c(y)) v ((c(x v c(y)) v c(x v y)) v ((c(x v c(y)) v c(x v y)) v c(x v y)))))) v x) v c(c_0)) = c(c_0) v c(c(c_0) v (c(x v c(y)) v ((c(x v c(y)) v c(x v y)) v ((c(x v c(y)) v c(x v y)) v c(x v y))))). [para(158(a,1),20(a,1,1,2,1)),demod(9(23),9(25),9(24),9(56),9(58),9(57))]. 1710 c(c(c(x v c(y v (z v (u v c(x))))) v c(c(y v (z v (u v c_0))))) v x) = c(x v c(y v (z v (u v c(x))))). [para(36(a,1),22(a,1,1,1,1,2,1,1))]. 1864 c_0 v (c(c_0) v c_0) = c_0. [para(680(a,1),45(a,1,1,2,1,2)),demod(9(10),9(9),126(13),9(7)),flip(a)]. 1887 c_0 v (x v (c(c_0) v c_0)) = x v c_0. [para(1864(a,1),9(a,1,2)),flip(a)]. 1893 (c(c_0 v c(c(c_0) v c_0)) v c(c_0)) v c_0 = c_0. [para(1864(a,1),26(a,1,1,2,1))]. 1897 c(c(c_0)) = c_0 v c_0. [para(1864(a,1),50(a,1,2)),demod(9(11),1060(15))]. 1898 (c(c_0 v c(c(c_0) v c_0)) v c(c_0)) v (x v c_0) = x v c_0. [para(1864(a,1),29(a,1,1,2,1))]. 1963 c(c_0 v (c(c(c_0 v c_0) v c(c(c(c_0) v c_0))) v c_0)) = c(c_0 v c_0). [back_demod(1414),demod(1897(3),1897(15),9(16),1897(20))]. 1975 c(c(c_0 v (c_0 v c_0)) v c(c_0)) = c_0. [back_demod(1294),demod(1897(5),1455(11),1897(4),1897(15),1455(21))]. 2022 (c(c_0) v c(c(c_0) v ((c(c_0) v c_0) v c_0))) v c_0 = c_0 v c_0. [back_demod(1060),demod(1897(18))]. 2058 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0). [back_demod(898),demod(1897(3),1897(16),9(17),56(16))]. 2078 c(c(c_0 v (x v c_0)) v c(x v c(c_0))) = x. [back_demod(861),demod(1897(3),2058(6))]. 2087 c(c(x v c((c_0 v c_0) v c(x))) v c(c_0 v c_0)) = x. [back_demod(842),demod(1897(3),1897(11))]. 2093 c(c(c_0) v c(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_demod(605),demod(1897(5),1897(9),1897(20))]. 2109 c(c(c_0 v (c(x v c(c(x))) v c_0)) v x) = c(x v c(c(x))). [back_demod(66),demod(1897(7),9(8))]. 2380 (c(x v (c_0 v c_0)) v c(x v c(c_0))) v x = c_0. [para(1897(a,1),26(a,1,1,1,1,2))]. 3326 c(c_0) v c(c(c_0) v c(c_0)) = c_0. [para(49(a,1),2078(a,1,1,2,1)),demod(56(12),1975(10)),flip(a)]. 3335 c(c(c_0) v c(x)) v c(c(c_0) v x) = c_0. [para(26(a,1),2078(a,1,1,2,1)),demod(141(13),1975(10)),flip(a)]. 3364 c(c_0) v (x v c(c(c_0) v c(c_0))) = x v c_0. [para(3326(a,1),9(a,1,2)),flip(a)]. 3365 (c(c_0) v c(c_0)) v c_0 = c(c_0) v c_0. [para(3326(a,1),23(a,1,2))]. 3376 (c(c_0) v c(c(c(c_0) v c(c_0)) v (c(c(c_0) v c(c_0)) v c_0))) v c(c(c_0) v c(c_0)) = c_0. [para(3326(a,1),169(a,1,1,2,1,2,2))]. 3521 c(c(c_0) v c(x)) v c_0 = (c(c_0) v x) v c_0. [para(3335(a,1),23(a,1,2)),flip(a)]. 3523 c(c(c_0) v c(x)) v (y v (z v c(c(c_0) v x))) = y v (z v c_0). [para(3335(a,1),18(a,1,2,2)),flip(a)]. 3579 (c(c_0) v c((c(c_0) v c_0) v ((c(c_0) v c_0) v c_0))) v c(c(c_0) v c(c_0)) = c_0. [back_demod(3376),demod(3521(16),9(15),3521(14))]. 3694 (c(c_0) v c(c_0)) v (x v c_0) = c(c_0) v (x v c_0). [para(3364(a,1),27(a,1,2))]. 3705 (c(c_0) v c((c(c_0) v c_0) v ((c(c_0) v c_0) v c_0))) v c_0 = c(c_0) v c_0. [para(158(a,1),3364(a,1,2)),demod(3364(28),3521(20),9(19),3521(18)),flip(a)]. 3707 x v ((c(c_0) v c(x v ((x v c(c(c_0) v c(c_0))) v ((x v c(c(c_0) v c(c_0))) v c_0)))) v c(c(c_0) v c(c_0))) = c_0. [para(3364(a,1),169(a,1,1,2,1,2,2)),demod(9(19),9(20),9(30))]. 3983 c(c(c_0) v c(c_0)) = c(c_0) v c_0. [para(3521(a,1),21(a,1,1,2,1,2)),demod(45(14)),flip(a)]. 4058 x v (c(c_0) v ((c(c_0) v c(x v ((x v (c(c_0) v c_0)) v ((x v (c(c_0) v c_0)) v c_0)))) v c_0)) = c_0. [back_demod(3707),demod(3983(8),3983(13),3983(24),9(23))]. 4071 c(c_0) v (c(c_0) v c_0) = c_0. [back_demod(3579),demod(3983(21),9(20),3705(19))]. 4107 c(c_0) v c_0 = c_0 v c_0. [para(4071(a,1),50(a,1,2)),demod(9(11),2022(15)),flip(a)]. 4108 c_0 v (c_0 v c_0) = c_0. [para(50(a,2),4071(a,1,2)),demod(9(11),49(10),4107(6),9(6),4107(5))]. 4109 c(c_0) v (x v (c(c_0) v (y v c_0))) = x v (y v c_0). [para(4071(a,1),30(a,1,2,2)),flip(a)]. 4117 x v (c(c_0) v ((c(c_0) v c(x v ((x v (c_0 v c_0)) v ((x v (c_0 v c_0)) v c_0)))) v c_0)) = c_0. [back_demod(4058),demod(4107(8),4107(12))]. 4148 (c(c_0) v c(c_0)) v c_0 = c_0 v c_0. [back_demod(3365),demod(4107(11))]. 4208 c(c_0 v c_0) = c(c_0). [back_demod(1963),demod(4107(9),13(11),4107(5),4108(5)),flip(a)]. 4225 c(c_0) v (x v c_0) = x v c_0. [back_demod(1898),demod(4107(5),4208(5),13(4),3694(8))]. 4228 c_0 v c_0 = c_0. [back_demod(1893),demod(4107(5),4208(5),13(4),4148(7))]. 4231 c_0 v (x v c_0) = x v c_0. [back_demod(1887),demod(4107(5),4228(4))]. 4254 c(c(x v c(c_0 v c(x))) v c(c_0)) = x. [back_demod(2087),demod(4228(3),4228(9))]. 4264 x v ((c(c_0) v c(x v ((x v c_0) v ((x v c_0) v c_0)))) v c_0) = c_0. [back_demod(4117),demod(4228(7),4228(9),4225(17))]. 4267 c(c_0) v (x v (y v c_0)) = x v (y v c_0). [back_demod(4109),demod(4225(7))]. 4284 c(c_0) v c_0 = c_0. [back_demod(4107),demod(4228(7))]. 4344 (c(x v c_0) v c(x v c(c_0))) v x = c_0. [back_demod(2380),demod(4228(3))]. 4350 c(c(c_0) v c(x v ((x v c_0) v ((x v c_0) v c_0)))) = x v c_0. [back_demod(2093),demod(4228(5),4228(7),4228(16))]. 4362 c(c(c_0)) = c_0. [back_demod(1897),demod(4228(6))]. 4367 c(c(c(x v c(c(x))) v c_0) v x) = c(x v c(c(x))). [back_demod(2109),demod(4231(8))]. 4719 x v ((x v c_0) v c_0) = x v c_0. [para(680(a,1),51(a,1,1,2,1,2,2)),demod(9(11),4267(12),9(10),4350(13),9(9),4267(10)),flip(a)]. 4749 c(c(c_0) v c(x v c_0)) = x v c_0. [para(3335(a,1),51(a,1,1,2,1,2,2,1,2)),demod(3523(16),4719(7),3335(17))]. 4768 x v (y v ((x v c_0) v c_0)) = y v (x v c_0). [para(4719(a,1),9(a,1,2)),flip(a)]. 4804 x v ((c(c_0) v c(x v c_0)) v c_0) = c_0. [back_demod(4264),demod(4768(10),9(7),4719(7))]. 4820 c(c(x v c_0) v c(c_0)) = x v c_0. [para(4749(a,1),28(a,1,1,1,1,2)),demod(9(5),4719(5),4284(7))]. 4833 c(c(x v (y v c_0)) v c(c(y v c_0) v (x v c(c_0)))) = x. [para(4820(a,1),19(a,1,1,1,1,2))]. 4843 c(c(x v c_0) v c((x v c_0) v (c(x v c_0) v c_0))) = x v c_0. [para(4820(a,1),21(a,1,1,2,1,2,1)),demod(9(11),4820(21))]. 4851 c(c(x v c_0) v c(c(x v c_0) v c_0)) = c_0. [para(4820(a,1),28(a,1,1,1,1,2)),demod(4231(4))]. 4859 x v (y v ((c(c_0) v c(x v c_0)) v c_0)) = y v c_0. [para(4804(a,1),9(a,1,2)),flip(a)]. 5006 c(x v c(c(x v c(c_0 v c(x))) v c_0)) = c(x v c(c_0 v c(x))). [para(4254(a,1),12(a,1,1,1))]. 5007 c(c(c(x v c(c_0 v c(x))) v c_0) v x) = c(x v c(c_0 v c(x))). [para(4254(a,1),12(a,1,1,2)),demod(4362(9))]. 5064 c(c(c_0) v c((c(c(x) v c_0) v c(c(x) v c(c_0))) v x)) = c(c(x) v c_0) v c(c(x) v c(c_0)). [para(4344(a,1),12(a,1,1,1,1))]. 5250 (x v c_0) v c_0 = c_0. [para(4719(a,1),53(a,1,2,1,2,1,2,1)),demod(4768(10),9(7),4719(7),9(11),4859(12))]. 5268 (x v c_0) v (y v c_0) = y v c_0. [para(5250(a,1),9(a,1,2)),flip(a)]. 5285 x v c_0 = c_0. [back_demod(4843),demod(5268(11),4851(11)),flip(a)]. 5388 c(c(c_0) v c((c(c_0) v c(c(x) v c(c_0))) v x)) = c(c_0) v c(c(x) v c(c_0)). [back_demod(5064),demod(5285(5),5285(17))]. 5408 c(x v c(c_0 v c(x))) = c(c(c_0) v x). [back_demod(5007),demod(5285(8)),flip(a)]. 5409 c(c(c_0) v x) = c(x v c(c_0)). [back_demod(5006),demod(5408(6),5285(6),5408(10)),flip(a)]. 5443 c(c(c_0) v c(c(c_0) v (x v c(c_0)))) = x. [back_demod(4833),demod(5285(2),5285(2),5285(4))]. 5525 c(x v c(c(x))) = c(c(c_0) v x). [back_demod(4367),demod(5285(6)),flip(a)]. 5860 c(x v c(y v (z v (u v c(x))))) = c(c(c_0) v x). [back_demod(1710),demod(5285(9),5285(9),5285(9),4362(10),5285(9)),flip(a)]. 5923 c(c(x v c(c_0)) v c(y v ((c(c(c_0) v z) v c(c_0)) v (x v z)))) = x. [back_demod(1477),demod(5285(2),5525(8))]. 5936 c(c(c_0) v c(c(c_0) v x)) = x. [back_demod(1333),demod(5860(7),5285(6),5285(6),5285(6),5409(8,R))]. 5995 (c(x v c(y v c(x v (c(c_0) v x)))) v c(c_0)) v (z v x) = c_0. [back_demod(808),demod(5285(11),5285(16))]. 5997 c(x v c(y v c(x v (c(c_0) v x)))) = c(c(c_0) v x). [back_demod(805),demod(5285(11),4362(12),5285(11)),flip(a)]. 6015 (c(x v c(c_0)) v c((c(c_0) v c(y v y)) v (x v y))) v (z v x) = c_0. [back_demod(771),demod(5285(17))]. 6129 c(c(c_0) v c(x v (c((y v c(x)) v c(z)) v c((y v c(x)) v z)))) = x. [back_demod(191),demod(5285(2))]. 6136 c(c(c_0) v c((c(c(c_0) v x) v c(c_0)) v c(y v x))) = c(c(c_0) v x) v c(c_0). [back_demod(122),demod(5525(4),5285(13),5409(15,R),5525(19))]. 6142 (c(c_0) v c(x v x)) v (y v x) = c_0. [back_demod(50),demod(5285(9))]. 6214 c(c(c_0) v c((c(c_0) v c(c(c_0) v (c(x v c(y)) v ((c(x v c(y)) v c(x v y)) v ((c(x v c(y)) v c(x v y)) v c(x v y)))))) v x)) = c(c_0) v c(c(c_0) v (c(x v c(y)) v ((c(x v c(y)) v c(x v y)) v ((c(x v c(y)) v c(x v y)) v c(x v y))))). [back_demod(1653),demod(5409(33,R))]. 6286 c(c(x v y) v c(c(c(c_0) v y) v (x v c(c_0)))) = x. [back_demod(103),demod(5525(6))]. 6292 x v c(c_0) = x. [back_demod(5443),demod(5936(11))]. 6316 x v ((x v y) v ((x v y) v y)) = x v y. [back_demod(618),demod(5936(13))]. 6322 c(c(c_0) v x) v (y v x) = c_0. [back_demod(5995),demod(5997(9),6292(7))]. 6324 c(c(x)) = x. [back_demod(5923),demod(6292(3),6292(8),6322(7),5285(3),6292(4))]. 6331 c(x) v (y v x) = c_0. [back_demod(6015),demod(6292(3),6142(8),6292(4))]. 6334 c(c(c_0) v x) = c(x). [back_demod(526),demod(6292(3),6142(8),6324(4),5285(3),6292(7))]. 6341 c(c(x v y) v c(c(y) v x)) = x. [back_demod(6286),demod(6334(6),6292(6))]. 6380 c(x) v c(y v x) = c(x). [back_demod(6136),demod(6334(6),6292(6),6334(9),6324(6),6334(8),6292(8))]. 6427 (c(c_0) v x) v x = c(c_0) v x. [back_demod(5388),demod(6292(8),6324(6),6334(9),6324(6),6292(10),6324(8))]. 6483 c(c_0) v x = x. [back_demod(6214),demod(6316(26),6334(14),12(11),6427(6),6334(6),6334(5),6324(2),6316(24),6334(12),12(9)),flip(a)]. 6524 x v (c((y v c(x)) v c(z)) v c((y v c(x)) v z)) = x. [back_demod(6129),demod(6483(15),6324(13))]. 6933 c(x v c(y)) v c(x v y) = c(x). [para(12(a,1),6324(a,1,1)),flip(a)]. 6936 x v c(x v (c(x v c(y)) v y)) = x v c(y). [para(21(a,1),6324(a,1,1)),demod(6324(4)),flip(a)]. 6941 x v c(y v c(x)) = x. [back_demod(6524),demod(6933(10))]. 7060 x v y = y v x. [para(6292(a,1),9(a,1,2)),demod(6292(4))]. 7119 x v c(x v y) = x v c(y). [back_demod(6936),demod(7060(4),6941(4))]. 7408 (x v y) v c(y) = c_0. [para(6331(a,1),7060(a,1)),flip(a)]. 7417 (x v (y v z)) v c(x v z) = c_0. [para(9(a,1),7408(a,1,1))]. 7443 (x v y) v c(x) = c_0. [para(7060(a,1),7408(a,1,1))]. 7549 (x v y) v (z v c(x)) = c_0. [para(7443(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. 7550 (x v (y v z)) v c(y) = c_0. [para(9(a,1),7443(a,1,1))]. 7557 x v (y v c(z v c(x))) = y v x. [para(6941(a,1),9(a,1,2)),flip(a)]. 7561 x v c(c(x) v y) = x. [para(7060(a,1),6941(a,1,2,1))]. 7703 x v c(y v (c(x) v z)) = x. [para(9(a,1),7561(a,1,2,1))]. 7960 ((x v y) v z) v c(y) = c_0. [para(6380(a,1),7549(a,1,2))]. 7965 ((x v y) v z) v c(x) = c_0. [para(7060(a,1),7550(a,1,1))]. 8508 x v c(y v x) = x v c(y). [para(7060(a,1),7119(a,1,2,1))]. 8514 x v ((y v x) v z) = (y v x) v z. [para(7960(a,1),7119(a,1,2,1)),demod(6292(5),6324(6),7060(5)),flip(a)]. 8515 x v ((x v y) v z) = (x v y) v z. [para(7965(a,1),7119(a,1,2,1)),demod(6292(5),6324(6),7060(5)),flip(a)]. 8607 x v (y v c(z v x)) = y v (x v c(z)). [para(8508(a,1),9(a,1,2)),flip(a)]. 8907 (x v (y v z)) v c(x v y) = c_0. [para(7060(a,1),7417(a,1,1,2))]. 11316 (x v y) v z = x v (y v z). [para(8907(a,1),7119(a,1,2,1)),demod(6292(5),6324(7),7060(6),9(6),9(5),8514(5),8515(5)),flip(a)]. 12290 x v (c(y v (c(x) v z)) v u) = x v u. [para(7703(a,1),11316(a,1,1)),flip(a)]. 12465 c(x v y) v c(c(y) v x) = c(x). [para(6341(a,1),6324(a,1,1)),flip(a)]. 13751 c(x v c(y v z)) = c(x v (z v c(y))) v c(x v c(z)). [para(7557(a,1),12465(a,1,2,1)),demod(6324(2),7060(4),8607(4),6324(10)),flip(a)]. 13885 $F # answer(MOD). [back_demod(17),demod(13751(9),7060(8),11316(8),12290(17),13751(17),7060(16),11316(16),7060(22),12290(25)),xx(a)]. ============================== end of proof ========================== given #258 (F,wt=13): 12547 c(x v c(y)) v c(y v x) = c(x). [para(8508(a,1),6935(a,1,1,1)),demod(6324(6),6958(5))]. given #259 (T,wt=13): 12594 c(x v c(y)) v (z v y) = z v y. [para(6941(a,1),6959(a,1,2,2)),demod(6941(9))]. given #260 (T,wt=13): 12595 c(c(x) v y) v (z v x) = z v x. [para(7561(a,1),6959(a,1,2,2)),demod(7561(9))]. given #261 (A,wt=23): 909 x v (y v (z v (u v (v v w)))) = v v (x v (z v (y v (u v w)))). [para(30(a,1),18(a,1,2))]. given #262 (F,wt=13): 12681 c(c(x) v y) v c(y v x) = c(y). [para(6324(a,1),8640(a,1,2,1,2))]. given #263 (F,wt=13): 12682 c(x v y) v c(c(x) v y) = c(y). [para(7060(a,1),8640(a,1,2,1))]. given #264 (T,wt=14): 6132 x v (y v (z v (u v (v v c(x))))) = c_0. [back_demod(172),demod(5285(8),5285(8),5285(8),5285(8))]. given #265 (T,wt=14): 6387 c(x v y) v (z v (x v (u v y))) = c_0. [back_demod(5988),demod(6334(5),6292(5))]. given #266 (A,wt=27): 910 x v (y v (z v (u v (v v (w v v6))))) = v v (x v (y v (z v (w v (u v v6))))). [para(30(a,2),18(a,1,2,2))]. given #267 (F,wt=14): 6404 c(x) v (y v (z v (u v (v v x)))) = c_0. [back_demod(5742),demod(6334(4),6292(4))]. given #268 (F,wt=14): 6541 c(x) v c(y v (z v (u v x))) = c(x). [back_demod(5917),demod(6343(5),6483(6),6483(10),6324(8),6343(9),6483(10))]. given #269 (T,wt=14): 7413 x v (y v (z v (u v (c(x) v v)))) = c_0. [para(7402(a,1),32(a,1,2,2,2)),demod(5285(2),5285(2),5285(2)),flip(a)]. given #270 (T,wt=14): 7414 c(x) v (y v (z v (u v (x v v)))) = c_0. [para(7402(a,1),37(a,1,2,2)),demod(5285(2),5285(2)),flip(a)]. given #271 (A,wt=23): 911 x v (y v (z v (u v (v v w)))) = y v (x v (v v (z v (u v w)))). [para(30(a,2),18(a,1,2)),flip(a)]. given #272 (F,wt=14): 7693 c(x) v c(y v (z v (x v u))) = c(x). [para(7402(a,1),92(a,1,1,2,1,2)),demod(5285(9),7060(10),6483(10),6324(8))]. given #273 (F,wt=14): 7714 c(x) v (y v c(z v x)) = y v c(x). [para(6380(a,1),9(a,1,2)),flip(a)]. given #274 (T,wt=14): 7966 c(x) v (y v c(x v z)) = y v c(x). [para(7710(a,1),9(a,1,2)),flip(a)]. given #275 (T,wt=14): 10640 c(x v y) v (z v (y v (u v x))) = c_0. [para(8720(a,1),18(a,1,2)),demod(5285(2)),flip(a)]. given #276 (A,wt=27): 912 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (v v (y v (w v (u v v6))))). [para(30(a,1),18(a,2,2,2))]. given #277 (F,wt=14): 10653 c(x v y) v (z v (u v (y v x))) = c_0. [para(8720(a,1),30(a,1,2)),demod(5285(2)),flip(a)]. given #278 (F,wt=14): 10779 x v (y v (z v (c(x v y) v u))) = c_0. [para(9(a,1),8721(a,1,2,2))]. given #279 (T,wt=14): 10785 x v (y v (z v (c(y v x) v u))) = c_0. [para(8721(a,1),31(a,1,2)),demod(5285(2)),flip(a)]. given #280 (T,wt=14): 10791 c(x v y) v (z v (x v (y v u))) = c_0. [para(8721(a,1),32(a,1,2)),demod(5285(2)),flip(a)]. given #281 (A,wt=23): 913 x v (y v (z v (u v (v v w)))) = z v (v v (x v (y v (u v w)))). [para(30(a,1),18(a,2,2)),flip(a)]. given #282 (F,wt=14): 10801 c(x v y) v (z v (y v (x v u))) = c_0. [para(8721(a,1),38(a,1,2)),demod(5285(2)),flip(a)]. given #283 (F,wt=14): 12284 c(x) v (c(y v x) v z) = c(x) v z. [para(6380(a,1),11316(a,1,1)),flip(a)]. given #284 (T,wt=14): 12285 c(x) v (c(x v y) v z) = c(x) v z. [para(7710(a,1),11316(a,1,1)),flip(a)]. given #285 (T,wt=14): 12596 c(x v y) v (z v c(y)) = z v c(y). [para(6380(a,1),6959(a,1,2,2)),demod(6380(9))]. given #286 (A,wt=27): 914 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (u v (w v (y v (v v v6))))). [para(30(a,2),18(a,2,2,2))]. given #287 (F,wt=14): 12597 c(x v y) v (z v c(x)) = z v c(x). [para(7710(a,1),6959(a,1,2,2)),demod(7710(9))]. given #288 (F,wt=15): 6548 x v c(y v (z v (u v (v v c(x))))) = x. [back_demod(5854),demod(6483(11),6324(9))]. given #289 (T,wt=15): 7707 x v c(y v (z v (u v (c(x) v v)))) = x. [para(32(a,2),7561(a,1,2,1))]. given #290 (T,wt=15): 8489 x v (y v c(z v (u v c(x)))) = y v x. [para(6940(a,1),9(a,1,2)),flip(a)]. given #291 (A,wt=23): 915 x v (y v (z v (u v (v v w)))) = u v (x v (v v (y v (z v w)))). [para(18(a,1),30(a,1,2,2))]. given #292 (F,wt=15): 8500 x v (y v c(x v z)) = y v (x v c(z)). [para(7119(a,1),9(a,1,2)),flip(a)]. given #293 (F,wt=15): 8501 x v c(y v (x v z)) = x v c(y v z). [para(9(a,1),7119(a,1,2,1))]. given #294 (T,wt=15): 8583 x v (y v c(z v (c(x) v u))) = y v x. [para(7703(a,1),9(a,1,2)),flip(a)]. given #295 (T,wt=15): 8607 x v (y v c(z v x)) = y v (x v c(z)). [para(8508(a,1),9(a,1,2)),flip(a)]. given #296 (A,wt=27): 916 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (w v (y v (u v (v v v6))))). [para(18(a,2),30(a,1,2,2,2))]. given #297 (F,wt=15): 12287 x v (c(y v (z v c(x))) v u) = x v u. [para(6940(a,1),11316(a,1,1)),flip(a)]. given #298 (F,wt=15): 12288 x v (c(x v y) v z) = x v (c(y) v z). [para(7119(a,1),11316(a,1,1)),demod(11316(3)),flip(a)]. given #299 (T,wt=15): 12290 x v (c(y v (c(x) v z)) v u) = x v u. [para(7703(a,1),11316(a,1,1)),flip(a)]. given #300 (T,wt=15): 12291 x v c(y v (z v x)) = x v c(y v z). [para(11316(a,1),8508(a,1,2,1))]. given #301 (A,wt=27): 917 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (u v (v v (w v (y v v6))))). [para(18(a,2),30(a,2,2,2,2))]. given #302 (F,wt=15): 12292 x v (c(y v x) v z) = x v (c(y) v z). [para(8508(a,1),11316(a,1,1)),demod(11316(3)),flip(a)]. given #303 (F,wt=15): 12299 c(x v y) v (z v x) = c(y) v (z v x). [back_demod(10729),demod(12284(6)),flip(a)]. given #304 (T,wt=15): 12300 c(x v y) v (z v y) = c(x) v (z v y). [back_demod(8733),demod(12285(6)),flip(a)]. given #305 (T,wt=15): 12599 c(x v (y v c(z))) v (u v z) = u v z. [para(6940(a,1),6959(a,1,2,2)),demod(6940(11))]. given #306 (A,wt=27): 963 x v (y v (z v (u v (v v (w v v6))))) = u v (y v (x v (w v (z v (v v v6))))). [para(30(a,1),31(a,1,2,2))]. given #307 (F,wt=15): 12603 c(x v (c(y) v z)) v (u v y) = u v y. [para(7703(a,1),6959(a,1,2,2)),demod(7703(11))]. given #308 (F,wt=16): 5961 x v (y v (z v (u v (v v (w v c(x)))))) = c_0. [back_demod(1122),demod(5285(9),5285(9),5285(9),5285(9),5285(9))]. given #309 (T,wt=16): 6393 c(x v y) v c(x v (z v y)) = c(x v y). [back_demod(5939),demod(6334(7),6292(7),6334(11),6324(8),6334(11),6292(11))]. given #310 (T,wt=16): 6834 c(x) v (y v (z v (u v (v v (w v x))))) = c_0. [back_demod(5728),demod(6343(3),6483(4))]. given #311 (A,wt=23): 964 x v (y v (z v (u v (v v w)))) = v v (z v (x v (y v (u v w)))). [para(30(a,1),31(a,1,2))]. given #312 (F,wt=16): 7415 x v (y v (z v (u v (v v (c(x) v w))))) = c_0. [para(7402(a,1),39(a,1,2,2,2,2)),demod(5285(2),5285(2),5285(2),5285(2)),flip(a)]. given #313 (F,wt=16): 7824 c(x) v c(y v (z v (u v (v v x)))) = c(x). [para(6381(a,1),93(a,1,1,2,1,2,2)),demod(5285(10),5285(10),7060(11),6483(11),6324(9))]. given #314 (T,wt=16): 7857 c(x) v (y v (z v (u v (v v (x v w))))) = c_0. [para(7411(a,1),32(a,1,2,2,2)),demod(5285(2),5285(2),5285(2)),flip(a)]. given #315 (T,wt=16): 7970 c(x) v c(y v (z v (u v (x v v)))) = c(x). [para(32(a,2),7710(a,1,2,1))]. given #316 (A,wt=27): 965 x v (y v (z v (u v (v v (w v v6))))) = v v (y v (x v (z v (w v (u v v6))))). [para(30(a,2),31(a,1,2,2))]. given #317 (F,wt=16): 8738 c(x) v (y v c(z v (u v x))) = y v c(x). [para(6394(a,1),9(a,1,2)),flip(a)]. given #318 (F,wt=16): 9043 c(x) v (y v c(z v (x v u))) = y v c(x). [para(7967(a,1),9(a,1,2)),flip(a)]. given #319 (T,wt=16): 11319 c(x v y) v c(x v (y v z)) = c(x v y). [para(8907(a,1),8508(a,1,2,1)),demod(7060(5),6483(5)),flip(a)]. given #320 (T,wt=14): 19112 c(x v y) v c(y v x) = c(x v y). [para(6958(a,1),11319(a,1,2,1))]. given #321 (A,wt=27): 966 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (w v (y v (v v (u v v6))))). [para(31(a,1),30(a,1,2,2,2))]. given #322 (F,wt=16): 12293 c(x) v (c(y v (z v x)) v u) = c(x) v u. [para(6394(a,1),11316(a,1,1)),flip(a)]. given #323 (F,wt=16): 12295 c(x) v (c(y v (x v z)) v u) = c(x) v u. [para(7967(a,1),11316(a,1,1)),flip(a)]. given #324 (T,wt=16): 12369 c(x v y) v c(z v (y v x)) = c(x v y). [para(10642(a,1),7119(a,1,2,1)),demod(7060(5),6483(5)),flip(a)]. given #325 (T,wt=16): 12515 c(x v (y v z)) v c(z v y) = c(z v y). [para(10642(a,1),6341(a,1,1,1,1)),demod(6483(10),6324(8))]. given #326 (A,wt=23): 967 x v (y v (z v (u v (v v w)))) = v v (x v (u v (y v (z v w)))). [para(31(a,1),30(a,1,2,2))]. given #327 (F,wt=16): 12605 c(x v (y v z)) v (u v c(z)) = u v c(z). [para(6394(a,1),6959(a,1,2,2)),demod(6394(11))]. given #328 (F,wt=16): 12608 c(x v (y v z)) v (u v c(y)) = u v c(y). [para(7967(a,1),6959(a,1,2,2)),demod(7967(11))]. given #329 (T,wt=16): 18445 c(x v y) v c(y v (z v x)) = c(y v x). [para(7060(a,1),6393(a,1,1,1))]. given #330 (T,wt=16): 19055 c(x v y) v c(y v (x v z)) = c(x v y). [para(9(a,1),11319(a,1,2,1))]. given #331 (A,wt=27): 968 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (u v (w v (v v (y v v6))))). [para(31(a,1),30(a,2,2,2,2))]. given #332 (F,wt=16): 19425 c(x v (y v z)) v c(y v x) = c(x v y). [para(19112(a,1),12283(a,2)),demod(6324(5),11316(4),19421(9))]. given #333 (F,wt=16): 20137 c(x v (y v z)) v c(z v x) = c(z v x). [para(9(a,1),12515(a,1,1,1))]. given #334 (T,wt=17): 6549 x v c(y v (z v (u v (v v (w v c(x)))))) = x. [back_demod(5852),demod(6483(12),6324(10))]. given #335 (T,wt=17): 6965 x v (y v (z v (u v x))) = y v (z v (u v x)). [para(6343(a,1),32(a,1,2,2,2)),flip(a)]. given #336 (A,wt=27): 973 x v (y v (z v (u v (v v (w v v6))))) = x v (u v (y v (w v (z v (v v v6))))). [para(30(a,1),33(a,1,2,2))]. given #337 (F,wt=17): 7116 x v (y v (z v (x v u))) = y v (z v (x v u)). [back_demod(6966),demod(7060(2),6958(2))]. given #338 (F,wt=17): 7558 x v (y v (z v c(u v c(x)))) = y v (z v x). [para(6941(a,1),18(a,1,2,2)),flip(a)]. given #339 (T,wt=17): 7705 x v (y v (z v c(c(x) v u))) = y v (z v x). [para(7561(a,1),18(a,1,2,2)),flip(a)]. given #340 (T,wt=17): 7709 x v c(y v (z v (u v (v v (c(x) v w))))) = x. [para(39(a,2),7561(a,1,2,1))]. given #341 (A,wt=23): 974 x v (y v (z v (u v (v v w)))) = x v (v v (z v (y v (u v w)))). [para(30(a,1),33(a,1,2))]. given #342 (F,wt=17): 12005 x v (y v c(z v (u v (c(x) v v)))) = x v y. [back_demod(9127),demod(11316(7))]. given #343 (F,wt=17): 12225 x v (y v c(z v (u v (v v c(x))))) = x v y. [back_demod(8041),demod(11316(7))]. given #344 (T,wt=17): 12516 c(x v y) v (z v c(x v c(y))) = z v c(x). [para(6935(a,1),9(a,1,2)),flip(a)]. given #345 (T,wt=17): 12566 c(x v y) v (c(x v c(y)) v z) = c(x) v z. [para(6935(a,1),11316(a,1,1)),flip(a)]. given #346 (A,wt=27): 975 x v (y v (z v (u v (v v (w v v6))))) = x v (v v (y v (z v (w v (u v v6))))). [para(30(a,2),33(a,1,2,2))]. given #347 (F,wt=17): 12571 x v (c(y v (z v (u v c(x)))) v v) = x v v. [para(6939(a,1),11316(a,1,1)),flip(a)]. given #348 (F,wt=17): 12616 c(x v (y v (z v c(u)))) v (v v u) = v v u. [para(6939(a,1),6959(a,1,2,2)),demod(6939(13))]. given #349 (T,wt=17): 12624 x v (c(y v (z v (c(x) v u))) v v) = x v v. [para(7542(a,1),11316(a,1,1)),flip(a)]. given #350 (T,wt=17): 12626 c(x v (y v (c(z) v u))) v (v v z) = v v z. [para(7542(a,1),6959(a,1,2,2)),demod(7542(13))]. given #351 (A,wt=23): 976 x v (y v (z v (u v (v v w)))) = x v (y v (v v (z v (u v w)))). [para(30(a,2),33(a,1,2)),flip(a)]. given #352 (F,wt=17): 12633 x v (y v (c(z v c(x)) v u)) = y v (x v u). [para(7557(a,1),11316(a,1,1)),demod(11316(2),11316(7)),flip(a)]. given #353 (F,wt=17): 12635 c(x v c(y)) v (z v (u v y)) = z v (u v y). [para(7557(a,1),6959(a,1,2,2)),demod(11316(7),7116(7),7557(11))]. given #354 (T,wt=17): 12651 x v (y v (c(c(x) v z) v u)) = y v (x v u). [para(7702(a,1),11316(a,1,1)),demod(11316(2),11316(7)),flip(a)]. given #355 (T,wt=17): 12653 c(c(x) v y) v (z v (u v x)) = z v (u v x). [para(7702(a,1),6959(a,1,2,2)),demod(11316(7),7116(7),7702(11))]. given #356 (A,wt=27): 977 x v (y v (z v (u v (v v (w v v6))))) = z v (x v (u v (y v (w v (v v v6))))). [para(33(a,1),30(a,1,2,2,2))]. given #357 (F,wt=17): 12654 c(x v y) v (z v c(y v c(x))) = z v c(y). [para(8640(a,1),9(a,1,2)),flip(a)]. given #358 (F,wt=17): 12705 c(x v y) v (c(y v c(x)) v z) = c(y) v z. [para(8640(a,1),11316(a,1,1)),flip(a)]. given #359 (T,wt=17): 12914 c(x v c(y)) v (z v (y v u)) = z v (y v u). [para(12281(a,1),18(a,1,2)),flip(a)]. given #360 (T,wt=17): 13602 c(c(x) v y) v (z v (x v u)) = z v (x v u). [para(12283(a,1),18(a,1,2)),flip(a)]. given #361 (A,wt=19): 1021 x v (y v (z v (u v v))) = u v (z v (y v (x v v))). [para(30(a,2),45(a,2)),demod(9(10),9(9),9(8),1020(14))]. given #362 (F,wt=17): 13649 c(x v y) v (z v c(c(y) v x)) = z v c(x). [para(12465(a,1),9(a,1,2)),flip(a)]. ============================== PROOF ================================= % Proof 4 at 16.70 (+ 0.11) seconds: DIST1. % Length of proof is 210. % Level of proof is 53. % Maximum clause weight is 86. % Given clauses 362. 3 x v c(x) = y v c(y) # label(ONE). [input]. 4 (x v c(y)) ^ (x v y) = x # label(CUT). [input]. 7 (c4 ^ c5) v (c4 ^ c6) != c4 ^ (c5 v c6) # answer(DIST1). [clausify]. 9 x v (y v z) = y v (x v z) # label(AJ). [input]. 10 x ^ y = c(c(x) v c(y)) # label(DM). [input]. 11 x v c(x) = y v c(y) # label(ONE). [copy(3)]. 12 c(c(x v c(y)) v c(x v y)) = x # label(CUT). [copy(4),demod(10(4))]. 13 x v c(x) = c_0. [new_symbol(11)]. 16 c(c(c4) v c(c5 v c6)) != c(c(c4) v c(c5)) v c(c(c4) v c(c6)) # answer(DIST1). [copy(7),demod(10(3),10(9),10(18)),flip(a)]. 18 x v (y v (z v u)) = z v (x v (y v u)). [para(9(a,1),9(a,1,2))]. 19 c(c(x v c(y v z)) v c(y v (x v z))) = x. [para(9(a,1),12(a,1,1,2,1))]. 20 c(c(x v y) v c(x v (c(y v c(z)) v c(y v z)))) = x. [para(12(a,1),12(a,1,1,1,1,2))]. 21 c(x v c(x v (c(x v c(y)) v y))) = c(x v c(y)). [para(12(a,1),12(a,1,1,1)),demod(9(5))]. 22 c(c(c(x v c(y)) v c(c(x v y))) v x) = c(x v c(y)). [para(12(a,1),12(a,1,1,2))]. 23 x v (y v c(x)) = y v c_0. [para(13(a,1),9(a,1,2)),flip(a)]. 24 c(c(c_0) v c(x v x)) = x. [para(13(a,1),12(a,1,1,1,1))]. 25 c(c(x v c(c(x))) v c(c_0)) = x. [para(13(a,1),12(a,1,1,2,1))]. 26 (c(x v c(y)) v c(x v y)) v x = c_0. [para(12(a,1),13(a,1,2))]. 27 x v (y v (z v c(x))) = y v (z v c_0). [para(23(a,1),9(a,1,2)),flip(a)]. 28 c(c(x v c(y v c(x))) v c(y v c_0)) = x. [para(23(a,1),12(a,1,1,2,1))]. 29 (c(x v c(y)) v c(x v y)) v (z v x) = z v c_0. [para(12(a,1),23(a,1,2,2))]. 30 x v (y v (z v (u v v))) = z v (x v (u v (y v v))). [para(18(a,1),9(a,1,2))]. 34 c(c(x v c(y v (z v u))) v c(z v (x v (y v u)))) = x. [para(18(a,1),12(a,1,1,2,1))]. 35 c(c(x v c(y v (z v u))) v c(y v (z v (x v u)))) = x. [para(18(a,2),12(a,1,1,2,1))]. 36 x v (y v (z v (u v c(x)))) = y v (z v (u v c_0)). [para(23(a,1),18(a,1,2,2)),flip(a)]. 45 c(c(c_0) v c(x v ((x v y) v y))) = x v y. [para(9(a,1),24(a,1,1,2,1))]. 47 c(x v c(c(c_0) v (x v x))) = c(c_0). [para(24(a,1),12(a,1,1,1))]. 48 c(c(c(c_0) v c(c(x v x))) v x) = c(c_0). [para(24(a,1),12(a,1,1,2))]. 49 (c(c_0) v c(x v x)) v x = c_0. [para(24(a,1),13(a,1,2))]. 50 (c(c_0) v c(x v x)) v (y v x) = y v c_0. [para(24(a,1),23(a,1,2,2))]. 51 c(c(c_0) v c(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)),demod(9(6))]. 53 x v ((c(c_0) v c(x v ((x v y) v y))) v y) = c_0. [para(49(a,1),9(a,1)),demod(9(6)),flip(a)]. 56 (c(c_0) v c(c(x) v c(x))) v c_0 = x v c_0. [para(49(a,1),23(a,1,2)),flip(a)]. 65 c(x v c(c(x v c(c(x))) v c_0)) = c(x v c(c(x))). [para(25(a,1),12(a,1,1,1))]. 66 c(c(c(x v c(c(x))) v c(c(c_0))) v x) = c(x v c(c(x))). [para(25(a,1),12(a,1,1,2))]. 68 (c(x v c(c(x))) v c(c_0)) v x = c_0. [para(25(a,1),13(a,1,2))]. 72 c(x v c(x v (c(c_0) v x))) = c(c_0). [para(9(a,1),47(a,1,1,2,1))]. 74 c(c(c_0) v c(x v (c(c_0) v (x v x)))) = x. [para(47(a,1),12(a,1,1,1))]. 76 (x v c(c(c_0) v (x v x))) v c(c_0) = c_0. [para(47(a,1),13(a,1,2))]. 103 c(c(x v y) v c(c(y v c(c(y))) v (x v c(c_0)))) = x. [para(25(a,1),19(a,1,1,1,1,2))]. 105 c(c(c_0) v c(c(c_0) v (x v (x v x)))) = x. [para(47(a,1),19(a,1,1,1))]. 122 c(c((c(x v c(c(x))) v c(c_0)) v c(y v x)) v c(y v c_0)) = c(x v c(c(x))) v c(c_0). [para(68(a,1),19(a,1,1,2,1,2))]. 126 c(c(c_0) v c(x v (x v (c(c_0) v x)))) = x. [para(72(a,1),12(a,1,1,1))]. 141 (c(c(x) v c(y)) v c(c(x) v y)) v c_0 = x v c_0. [para(26(a,1),23(a,1,2)),flip(a)]. 152 (c(c(c_0) v c(c(x v x))) v x) v c(c_0) = c_0. [para(24(a,1),26(a,1,1,2))]. 158 (c(c_0) v c(x v (c(c_0) v (x v x)))) v x = c_0. [para(47(a,1),26(a,1,1,1))]. 169 (c(c_0) v c(x v (x v (c(c_0) v x)))) v x = c_0. [para(72(a,1),26(a,1,1,1))]. 191 c(c(x v c_0) v c(y v (c((x v c(y)) v c(z)) v c((x v c(y)) v z)))) = y. [para(23(a,1),20(a,1,1,1,1))]. 243 c(c(c_0) v c((x v c(c(c_0) v (x v x))) v c_0)) = x v c(c(c_0) v (x v x)). [para(76(a,1),12(a,1,1,1,1))]. 244 (x v c(c(c_0) v (x v x))) v c_0 = c_0 v c_0. [para(76(a,1),23(a,1,2)),flip(a)]. 256 x v c(c(c_0) v (x v x)) = c_0. [back_demod(243),demod(244(10),24(8)),flip(a)]. 258 x v (y v c(c(c_0) v (x v x))) = y v c_0. [para(256(a,1),9(a,1,2)),flip(a)]. 260 x v c(x v (c(c_0) v x)) = c_0. [para(9(a,1),256(a,1,2,1))]. 261 (c(c_0) v (x v x)) v c_0 = x v c_0. [para(256(a,1),23(a,1,2))]. 262 c(c(c_0)) v c(c(c(c_0)) v c_0) = c_0. [para(23(a,1),256(a,1,2,1))]. 273 x v (y v c(x v (c(c_0) v x))) = y v c_0. [para(260(a,1),9(a,1,2)),flip(a)]. 284 (c(c(c_0)) v c_0) v c_0 = c(c(c_0)) v c_0. [para(23(a,1),261(a,1,1))]. 330 c(c(c_0) v c(c(c(c_0)) v (c(c(c_0)) v c_0))) = c(c(c_0)). [para(262(a,1),12(a,1,1,1,1))]. 336 (c(c(c_0)) v c_0) v (x v c_0) = x v (c(c(c_0)) v c_0). [para(262(a,1),27(a,1,2,2))]. 526 c(c(c(x v c(c_0)) v c(c((c(c_0) v c(y v y)) v (x v y)))) v x) = c(x v c(c_0)). [para(50(a,2),22(a,1,1,1,1,2,1,1))]. 547 (c(c(c_0) v c(c(x v x))) v x) v c_0 = c_0 v c_0. [para(48(a,1),56(a,1,1,2,1,1)),demod(48(13),56(11)),flip(a)]. 576 c(c(x v c((c(c(c_0)) v c_0) v c(x))) v c(c(c(c_0)) v c_0)) = x. [para(284(a,1),28(a,1,1,2,1))]. 605 c(c(c_0) v c(x v ((x v c(c(c_0))) v ((x v c(c(c_0))) v c_0)))) = x v c(c(c_0)). [para(27(a,1),74(a,1,1,2,1,2)),demod(9(13),9(14))]. 618 c(c(c_0) v c(c(c_0) v (x v ((x v y) v ((x v y) v y))))) = x v y. [para(9(a,1),105(a,1,1,2,1,2,2)),demod(9(9))]. 680 (c(c_0) v (x v x)) v (y v c_0) = x v (y v c_0). [para(258(a,1),27(a,1,2))]. 771 (c(x v c(c_0)) v c((c(c_0) v c(y v y)) v (x v y))) v (z v x) = z v c_0. [para(50(a,2),29(a,1,1,2,1))]. 805 c(c(c(x v c(y v c(x v (c(c_0) v x)))) v c(c(y v c_0))) v x) = c(x v c(y v c(x v (c(c_0) v x)))). [para(273(a,1),22(a,1,1,1,1,2,1,1))]. 808 (c(x v c(y v c(x v (c(c_0) v x)))) v c(y v c_0)) v (z v x) = z v c_0. [para(273(a,1),29(a,1,1,2,1))]. 817 c(c(c_0) v c(c(c(c_0)))) v c(c_0) = c(c(c_0) v c(c(c(c_0)))). [para(68(a,1),45(a,1,1,2,1,2)),demod(65(15)),flip(a)]. 825 c(c(c_0)) v c_0 = c(c(c_0)). [para(284(a,1),45(a,1,1,2,1,2,1)),demod(284(14),9(13),284(12),330(14),284(10)),flip(a)]. 842 c(c(x v c(c(c(c_0)) v c(x))) v c(c(c(c_0)))) = x. [back_demod(576),demod(825(5),825(13))]. 855 c(c(c_0)) v (x v c_0) = x v c(c(c_0)). [back_demod(336),demod(825(5),825(11))]. 858 (c(c_0) v c(c_0 v c_0)) v c(c(c_0)) = c(c(c_0)). [para(825(a,1),50(a,1,2)),demod(825(16))]. 861 c(c(c(c(c_0)) v (x v c_0)) v c(x v c(c_0))) = x. [para(855(a,2),12(a,1,1,1,1))]. 862 c(c_0) v (c(c(c_0)) v (x v c_0)) = x v c_0. [para(855(a,2),23(a,1,2))]. 898 c(c(c_0)) v (x v c_0) = (c(c_0) v c(c(x) v c(x))) v c(c(c_0)). [para(56(a,1),855(a,1,2))]. 1040 c(c(c_0)) v (x v (c(c_0) v c_0)) = x v c_0. [para(862(a,1),18(a,2))]. 1060 (c(c_0) v c(c(c_0) v ((c(c_0) v c_0) v c_0))) v c_0 = c(c(c_0)). [para(49(a,1),1040(a,1,2)),demod(825(5),9(14)),flip(a)]. 1083 c(c(c(c_0) v c(c(c(c_0))))) = c(c_0). [para(858(a,1),28(a,1,1,1,1,2,1)),demod(49(17),817(11))]. 1087 c(c(c_0) v c(c(c(c_0)))) = c_0. [para(1083(a,1),13(a,1,2)),demod(817(11))]. 1234 c(c(c(c_0) v c(c(c(c(c_0))))) v c_0) = c(c_0). [para(1087(a,1),12(a,1,1,2))]. 1247 c(c(c(c(c_0))) v c(c(c_0) v c_0)) = c(c(c_0)). [para(1087(a,1),28(a,1,1,1,1,2)),demod(825(5))]. 1294 c(c((c(c(c_0) v c(c(c(c(c_0))))) v c_0) v c(c(c_0))) v c(c_0)) = c(c(c_0) v c(c(c(c(c_0))))) v c_0. [para(1234(a,1),25(a,1,1,1,1,2,1))]. 1333 c(c(x v c(y v (z v (u v c(x))))) v c(z v (y v (u v c_0)))) = x. [para(27(a,1),34(a,1,1,2,1,2))]. 1414 c(c(c(c(c(c_0))) v c(c(c(c_0) v c_0))) v c(c(c_0))) = c(c(c(c_0))). [para(1247(a,1),12(a,1,1,2))]. 1455 c(c(c_0) v c(c(x v x))) v x = c_0. [para(152(a,1),12(a,1,1,1,1)),demod(547(12),24(8)),flip(a)]. 1477 c(c(x v c(y v c_0)) v c(y v ((c(z v c(c(z))) v c(c_0)) v (x v z)))) = x. [para(68(a,1),35(a,1,1,1,1,2,1,2))]. 1653 c(c((c(c_0) v c(c(c_0) v (c(x v c(y)) v ((c(x v c(y)) v c(x v y)) v ((c(x v c(y)) v c(x v y)) v c(x v y)))))) v x) v c(c_0)) = c(c_0) v c(c(c_0) v (c(x v c(y)) v ((c(x v c(y)) v c(x v y)) v ((c(x v c(y)) v c(x v y)) v c(x v y))))). [para(158(a,1),20(a,1,1,2,1)),demod(9(23),9(25),9(24),9(56),9(58),9(57))]. 1710 c(c(c(x v c(y v (z v (u v c(x))))) v c(c(y v (z v (u v c_0))))) v x) = c(x v c(y v (z v (u v c(x))))). [para(36(a,1),22(a,1,1,1,1,2,1,1))]. 1864 c_0 v (c(c_0) v c_0) = c_0. [para(680(a,1),45(a,1,1,2,1,2)),demod(9(10),9(9),126(13),9(7)),flip(a)]. 1887 c_0 v (x v (c(c_0) v c_0)) = x v c_0. [para(1864(a,1),9(a,1,2)),flip(a)]. 1893 (c(c_0 v c(c(c_0) v c_0)) v c(c_0)) v c_0 = c_0. [para(1864(a,1),26(a,1,1,2,1))]. 1897 c(c(c_0)) = c_0 v c_0. [para(1864(a,1),50(a,1,2)),demod(9(11),1060(15))]. 1898 (c(c_0 v c(c(c_0) v c_0)) v c(c_0)) v (x v c_0) = x v c_0. [para(1864(a,1),29(a,1,1,2,1))]. 1963 c(c_0 v (c(c(c_0 v c_0) v c(c(c(c_0) v c_0))) v c_0)) = c(c_0 v c_0). [back_demod(1414),demod(1897(3),1897(15),9(16),1897(20))]. 1975 c(c(c_0 v (c_0 v c_0)) v c(c_0)) = c_0. [back_demod(1294),demod(1897(5),1455(11),1897(4),1897(15),1455(21))]. 2022 (c(c_0) v c(c(c_0) v ((c(c_0) v c_0) v c_0))) v c_0 = c_0 v c_0. [back_demod(1060),demod(1897(18))]. 2058 (c_0 v c_0) v (x v c_0) = c_0 v (x v c_0). [back_demod(898),demod(1897(3),1897(16),9(17),56(16))]. 2078 c(c(c_0 v (x v c_0)) v c(x v c(c_0))) = x. [back_demod(861),demod(1897(3),2058(6))]. 2087 c(c(x v c((c_0 v c_0) v c(x))) v c(c_0 v c_0)) = x. [back_demod(842),demod(1897(3),1897(11))]. 2093 c(c(c_0) v c(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_demod(605),demod(1897(5),1897(9),1897(20))]. 2109 c(c(c_0 v (c(x v c(c(x))) v c_0)) v x) = c(x v c(c(x))). [back_demod(66),demod(1897(7),9(8))]. 2380 (c(x v (c_0 v c_0)) v c(x v c(c_0))) v x = c_0. [para(1897(a,1),26(a,1,1,1,1,2))]. 3326 c(c_0) v c(c(c_0) v c(c_0)) = c_0. [para(49(a,1),2078(a,1,1,2,1)),demod(56(12),1975(10)),flip(a)]. 3335 c(c(c_0) v c(x)) v c(c(c_0) v x) = c_0. [para(26(a,1),2078(a,1,1,2,1)),demod(141(13),1975(10)),flip(a)]. 3364 c(c_0) v (x v c(c(c_0) v c(c_0))) = x v c_0. [para(3326(a,1),9(a,1,2)),flip(a)]. 3365 (c(c_0) v c(c_0)) v c_0 = c(c_0) v c_0. [para(3326(a,1),23(a,1,2))]. 3376 (c(c_0) v c(c(c(c_0) v c(c_0)) v (c(c(c_0) v c(c_0)) v c_0))) v c(c(c_0) v c(c_0)) = c_0. [para(3326(a,1),169(a,1,1,2,1,2,2))]. 3521 c(c(c_0) v c(x)) v c_0 = (c(c_0) v x) v c_0. [para(3335(a,1),23(a,1,2)),flip(a)]. 3523 c(c(c_0) v c(x)) v (y v (z v c(c(c_0) v x))) = y v (z v c_0). [para(3335(a,1),18(a,1,2,2)),flip(a)]. 3579 (c(c_0) v c((c(c_0) v c_0) v ((c(c_0) v c_0) v c_0))) v c(c(c_0) v c(c_0)) = c_0. [back_demod(3376),demod(3521(16),9(15),3521(14))]. 3694 (c(c_0) v c(c_0)) v (x v c_0) = c(c_0) v (x v c_0). [para(3364(a,1),27(a,1,2))]. 3705 (c(c_0) v c((c(c_0) v c_0) v ((c(c_0) v c_0) v c_0))) v c_0 = c(c_0) v c_0. [para(158(a,1),3364(a,1,2)),demod(3364(28),3521(20),9(19),3521(18)),flip(a)]. 3707 x v ((c(c_0) v c(x v ((x v c(c(c_0) v c(c_0))) v ((x v c(c(c_0) v c(c_0))) v c_0)))) v c(c(c_0) v c(c_0))) = c_0. [para(3364(a,1),169(a,1,1,2,1,2,2)),demod(9(19),9(20),9(30))]. 3983 c(c(c_0) v c(c_0)) = c(c_0) v c_0. [para(3521(a,1),21(a,1,1,2,1,2)),demod(45(14)),flip(a)]. 4058 x v (c(c_0) v ((c(c_0) v c(x v ((x v (c(c_0) v c_0)) v ((x v (c(c_0) v c_0)) v c_0)))) v c_0)) = c_0. [back_demod(3707),demod(3983(8),3983(13),3983(24),9(23))]. 4071 c(c_0) v (c(c_0) v c_0) = c_0. [back_demod(3579),demod(3983(21),9(20),3705(19))]. 4107 c(c_0) v c_0 = c_0 v c_0. [para(4071(a,1),50(a,1,2)),demod(9(11),2022(15)),flip(a)]. 4108 c_0 v (c_0 v c_0) = c_0. [para(50(a,2),4071(a,1,2)),demod(9(11),49(10),4107(6),9(6),4107(5))]. 4109 c(c_0) v (x v (c(c_0) v (y v c_0))) = x v (y v c_0). [para(4071(a,1),30(a,1,2,2)),flip(a)]. 4117 x v (c(c_0) v ((c(c_0) v c(x v ((x v (c_0 v c_0)) v ((x v (c_0 v c_0)) v c_0)))) v c_0)) = c_0. [back_demod(4058),demod(4107(8),4107(12))]. 4148 (c(c_0) v c(c_0)) v c_0 = c_0 v c_0. [back_demod(3365),demod(4107(11))]. 4208 c(c_0 v c_0) = c(c_0). [back_demod(1963),demod(4107(9),13(11),4107(5),4108(5)),flip(a)]. 4225 c(c_0) v (x v c_0) = x v c_0. [back_demod(1898),demod(4107(5),4208(5),13(4),3694(8))]. 4228 c_0 v c_0 = c_0. [back_demod(1893),demod(4107(5),4208(5),13(4),4148(7))]. 4231 c_0 v (x v c_0) = x v c_0. [back_demod(1887),demod(4107(5),4228(4))]. 4254 c(c(x v c(c_0 v c(x))) v c(c_0)) = x. [back_demod(2087),demod(4228(3),4228(9))]. 4264 x v ((c(c_0) v c(x v ((x v c_0) v ((x v c_0) v c_0)))) v c_0) = c_0. [back_demod(4117),demod(4228(7),4228(9),4225(17))]. 4267 c(c_0) v (x v (y v c_0)) = x v (y v c_0). [back_demod(4109),demod(4225(7))]. 4284 c(c_0) v c_0 = c_0. [back_demod(4107),demod(4228(7))]. 4344 (c(x v c_0) v c(x v c(c_0))) v x = c_0. [back_demod(2380),demod(4228(3))]. 4350 c(c(c_0) v c(x v ((x v c_0) v ((x v c_0) v c_0)))) = x v c_0. [back_demod(2093),demod(4228(5),4228(7),4228(16))]. 4362 c(c(c_0)) = c_0. [back_demod(1897),demod(4228(6))]. 4367 c(c(c(x v c(c(x))) v c_0) v x) = c(x v c(c(x))). [back_demod(2109),demod(4231(8))]. 4719 x v ((x v c_0) v c_0) = x v c_0. [para(680(a,1),51(a,1,1,2,1,2,2)),demod(9(11),4267(12),9(10),4350(13),9(9),4267(10)),flip(a)]. 4749 c(c(c_0) v c(x v c_0)) = x v c_0. [para(3335(a,1),51(a,1,1,2,1,2,2,1,2)),demod(3523(16),4719(7),3335(17))]. 4768 x v (y v ((x v c_0) v c_0)) = y v (x v c_0). [para(4719(a,1),9(a,1,2)),flip(a)]. 4804 x v ((c(c_0) v c(x v c_0)) v c_0) = c_0. [back_demod(4264),demod(4768(10),9(7),4719(7))]. 4820 c(c(x v c_0) v c(c_0)) = x v c_0. [para(4749(a,1),28(a,1,1,1,1,2)),demod(9(5),4719(5),4284(7))]. 4833 c(c(x v (y v c_0)) v c(c(y v c_0) v (x v c(c_0)))) = x. [para(4820(a,1),19(a,1,1,1,1,2))]. 4843 c(c(x v c_0) v c((x v c_0) v (c(x v c_0) v c_0))) = x v c_0. [para(4820(a,1),21(a,1,1,2,1,2,1)),demod(9(11),4820(21))]. 4851 c(c(x v c_0) v c(c(x v c_0) v c_0)) = c_0. [para(4820(a,1),28(a,1,1,1,1,2)),demod(4231(4))]. 4859 x v (y v ((c(c_0) v c(x v c_0)) v c_0)) = y v c_0. [para(4804(a,1),9(a,1,2)),flip(a)]. 5006 c(x v c(c(x v c(c_0 v c(x))) v c_0)) = c(x v c(c_0 v c(x))). [para(4254(a,1),12(a,1,1,1))]. 5007 c(c(c(x v c(c_0 v c(x))) v c_0) v x) = c(x v c(c_0 v c(x))). [para(4254(a,1),12(a,1,1,2)),demod(4362(9))]. 5064 c(c(c_0) v c((c(c(x) v c_0) v c(c(x) v c(c_0))) v x)) = c(c(x) v c_0) v c(c(x) v c(c_0)). [para(4344(a,1),12(a,1,1,1,1))]. 5250 (x v c_0) v c_0 = c_0. [para(4719(a,1),53(a,1,2,1,2,1,2,1)),demod(4768(10),9(7),4719(7),9(11),4859(12))]. 5268 (x v c_0) v (y v c_0) = y v c_0. [para(5250(a,1),9(a,1,2)),flip(a)]. 5285 x v c_0 = c_0. [back_demod(4843),demod(5268(11),4851(11)),flip(a)]. 5388 c(c(c_0) v c((c(c_0) v c(c(x) v c(c_0))) v x)) = c(c_0) v c(c(x) v c(c_0)). [back_demod(5064),demod(5285(5),5285(17))]. 5408 c(x v c(c_0 v c(x))) = c(c(c_0) v x). [back_demod(5007),demod(5285(8)),flip(a)]. 5409 c(c(c_0) v x) = c(x v c(c_0)). [back_demod(5006),demod(5408(6),5285(6),5408(10)),flip(a)]. 5443 c(c(c_0) v c(c(c_0) v (x v c(c_0)))) = x. [back_demod(4833),demod(5285(2),5285(2),5285(4))]. 5525 c(x v c(c(x))) = c(c(c_0) v x). [back_demod(4367),demod(5285(6)),flip(a)]. 5860 c(x v c(y v (z v (u v c(x))))) = c(c(c_0) v x). [back_demod(1710),demod(5285(9),5285(9),5285(9),4362(10),5285(9)),flip(a)]. 5923 c(c(x v c(c_0)) v c(y v ((c(c(c_0) v z) v c(c_0)) v (x v z)))) = x. [back_demod(1477),demod(5285(2),5525(8))]. 5936 c(c(c_0) v c(c(c_0) v x)) = x. [back_demod(1333),demod(5860(7),5285(6),5285(6),5285(6),5409(8,R))]. 5995 (c(x v c(y v c(x v (c(c_0) v x)))) v c(c_0)) v (z v x) = c_0. [back_demod(808),demod(5285(11),5285(16))]. 5997 c(x v c(y v c(x v (c(c_0) v x)))) = c(c(c_0) v x). [back_demod(805),demod(5285(11),4362(12),5285(11)),flip(a)]. 6015 (c(x v c(c_0)) v c((c(c_0) v c(y v y)) v (x v y))) v (z v x) = c_0. [back_demod(771),demod(5285(17))]. 6129 c(c(c_0) v c(x v (c((y v c(x)) v c(z)) v c((y v c(x)) v z)))) = x. [back_demod(191),demod(5285(2))]. 6136 c(c(c_0) v c((c(c(c_0) v x) v c(c_0)) v c(y v x))) = c(c(c_0) v x) v c(c_0). [back_demod(122),demod(5525(4),5285(13),5409(15,R),5525(19))]. 6142 (c(c_0) v c(x v x)) v (y v x) = c_0. [back_demod(50),demod(5285(9))]. 6214 c(c(c_0) v c((c(c_0) v c(c(c_0) v (c(x v c(y)) v ((c(x v c(y)) v c(x v y)) v ((c(x v c(y)) v c(x v y)) v c(x v y)))))) v x)) = c(c_0) v c(c(c_0) v (c(x v c(y)) v ((c(x v c(y)) v c(x v y)) v ((c(x v c(y)) v c(x v y)) v c(x v y))))). [back_demod(1653),demod(5409(33,R))]. 6286 c(c(x v y) v c(c(c(c_0) v y) v (x v c(c_0)))) = x. [back_demod(103),demod(5525(6))]. 6292 x v c(c_0) = x. [back_demod(5443),demod(5936(11))]. 6316 x v ((x v y) v ((x v y) v y)) = x v y. [back_demod(618),demod(5936(13))]. 6322 c(c(c_0) v x) v (y v x) = c_0. [back_demod(5995),demod(5997(9),6292(7))]. 6324 c(c(x)) = x. [back_demod(5923),demod(6292(3),6292(8),6322(7),5285(3),6292(4))]. 6331 c(x) v (y v x) = c_0. [back_demod(6015),demod(6292(3),6142(8),6292(4))]. 6334 c(c(c_0) v x) = c(x). [back_demod(526),demod(6292(3),6142(8),6324(4),5285(3),6292(7))]. 6341 c(c(x v y) v c(c(y) v x)) = x. [back_demod(6286),demod(6334(6),6292(6))]. 6380 c(x) v c(y v x) = c(x). [back_demod(6136),demod(6334(6),6292(6),6334(9),6324(6),6334(8),6292(8))]. 6427 (c(c_0) v x) v x = c(c_0) v x. [back_demod(5388),demod(6292(8),6324(6),6334(9),6324(6),6292(10),6324(8))]. 6483 c(c_0) v x = x. [back_demod(6214),demod(6316(26),6334(14),12(11),6427(6),6334(6),6334(5),6324(2),6316(24),6334(12),12(9)),flip(a)]. 6524 x v (c((y v c(x)) v c(z)) v c((y v c(x)) v z)) = x. [back_demod(6129),demod(6483(15),6324(13))]. 6933 c(x v c(y)) v c(x v y) = c(x). [para(12(a,1),6324(a,1,1)),flip(a)]. 6936 x v c(x v (c(x v c(y)) v y)) = x v c(y). [para(21(a,1),6324(a,1,1)),demod(6324(4)),flip(a)]. 6941 x v c(y v c(x)) = x. [back_demod(6524),demod(6933(10))]. 7060 x v y = y v x. [para(6292(a,1),9(a,1,2)),demod(6292(4))]. 7119 x v c(x v y) = x v c(y). [back_demod(6936),demod(7060(4),6941(4))]. 7408 (x v y) v c(y) = c_0. [para(6331(a,1),7060(a,1)),flip(a)]. 7417 (x v (y v z)) v c(x v z) = c_0. [para(9(a,1),7408(a,1,1))]. 7443 (x v y) v c(x) = c_0. [para(7060(a,1),7408(a,1,1))]. 7549 (x v y) v (z v c(x)) = c_0. [para(7443(a,1),9(a,1,2)),demod(5285(2)),flip(a)]. 7550 (x v (y v z)) v c(y) = c_0. [para(9(a,1),7443(a,1,1))]. 7557 x v (y v c(z v c(x))) = y v x. [para(6941(a,1),9(a,1,2)),flip(a)]. 7561 x v c(c(x) v y) = x. [para(7060(a,1),6941(a,1,2,1))]. 7702 x v (y v c(c(x) v z)) = y v x. [para(7561(a,1),9(a,1,2)),flip(a)]. 7710 c(x) v c(x v y) = c(x). [para(6324(a,1),7561(a,1,2,1,1))]. 7960 ((x v y) v z) v c(y) = c_0. [para(6380(a,1),7549(a,1,2))]. 7965 ((x v y) v z) v c(x) = c_0. [para(7060(a,1),7550(a,1,1))]. 7966 c(x) v (y v c(x v z)) = y v c(x). [para(7710(a,1),9(a,1,2)),flip(a)]. 8508 x v c(y v x) = x v c(y). [para(7060(a,1),7119(a,1,2,1))]. 8514 x v ((y v x) v z) = (y v x) v z. [para(7960(a,1),7119(a,1,2,1)),demod(6292(5),6324(6),7060(5)),flip(a)]. 8515 x v ((x v y) v z) = (x v y) v z. [para(7965(a,1),7119(a,1,2,1)),demod(6292(5),6324(6),7060(5)),flip(a)]. 8607 x v (y v c(z v x)) = y v (x v c(z)). [para(8508(a,1),9(a,1,2)),flip(a)]. 8907 (x v (y v z)) v c(x v y) = c_0. [para(7060(a,1),7417(a,1,1,2))]. 11316 (x v y) v z = x v (y v z). [para(8907(a,1),7119(a,1,2,1)),demod(6292(5),6324(7),7060(6),9(6),9(5),8514(5),8515(5)),flip(a)]. 12284 c(x) v (c(y v x) v z) = c(x) v z. [para(6380(a,1),11316(a,1,1)),flip(a)]. 12465 c(x v y) v c(c(y) v x) = c(x). [para(6341(a,1),6324(a,1,1)),flip(a)]. 13649 c(x v y) v (z v c(c(y) v x)) = z v c(x). [para(12465(a,1),9(a,1,2)),flip(a)]. 13751 c(x v c(y v z)) = c(x v (z v c(y))) v c(x v c(z)). [para(7557(a,1),12465(a,1,2,1)),demod(6324(2),7060(4),8607(4),6324(10)),flip(a)]. 13886 c(c6 v (c(c4) v c(c5))) v c(c(c4) v c(c6)) != c(c(c4) v c(c5)) v c(c(c4) v c(c6)) # answer(DIST1). [back_demod(16),demod(13751(8),9(7))]. 15099 c(x v c(y)) v (c(x v (z v c(y))) v c(x v c(z))) = c(x v (z v c(y))) v c(x v c(z)). [para(7966(a,1),6380(a,1,2,1)),demod(13751(4),7060(12),13751(16))]. 15837 c(x v y) v (c(x v (z v y)) v u) = c(x v y) v u. [para(9(a,1),12284(a,1,2,1,1))]. 15909 c(x v (y v c(z))) v c(x v c(y)) = c(x v c(z)) v c(x v c(y)). [back_demod(15099),demod(15837(12)),flip(a)]. 16103 c(x v c(y v z)) = c(x v c(y)) v c(x v c(z)). [back_demod(13751),demod(15909(12))]. 22975 c(x v (y v z)) v c(y v c(x)) = c(y v z) v c(y v c(x)). [para(13649(a,1),12465(a,1,2,1)),demod(7060(6),11316(6),7702(5),16103(12),6324(9))]. 22976 $F # answer(DIST1). [resolve(22975,a,13886,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=362. Generated=224101. Kept=22964. proofs=4. Usable=172. Sos=7252. Demods=4263. Denials=1. Limbo=32, Disabled=15514. Hints=0. Weight_deleted=636. Literals_deleted=0. Forward_subsumed=198503. Back_subsumed=217. Sos_limit_deleted=1997. Sos_displaced=0. Sos_removed=0. New_demodulators=17394 (3 lex), Back_demodulated=15287. Back_unit_deleted=0. Demod_attempts=4127585. Demod_rewrites=529532. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=14.48. User_CPU=16.71, System_CPU=0.11, Wall_clock=17. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 4 proofs. Process 13586 exit (max_proofs) Mon Jun 19 16:43:23 2006