============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13092 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:11 2006 The command was "/home/mccune/bin/prover9 -f a1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file a1.in clauses(sos). (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). end_of_list. assign(max_proofs,4). % assign(max_proofs, 4) -> set(restrict_denials). set(restrict_denials). clauses(goals). x v (y ^ (x ^ z)) = x # answer(McKenzie_1). x ^ (y v (x v z)) = x # answer(McKenzie_2). ((x ^ y) v (y ^ z)) v y = y # answer(McKenzie_3). ((x v y) ^ (y v z)) ^ y = y # answer(McKenzie_4). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). c1 v (c2 ^ (c1 ^ c3)) != c1 # answer(McKenzie_1). c4 ^ (c5 v (c4 v c6)) != c4 # answer(McKenzie_2). ((c7 ^ c8) v (c8 ^ c9)) v c8 != c8 # answer(McKenzie_3). ((c10 v c11) ^ (c11 v c12)) ^ c11 != c11 # answer(McKenzie_4). 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) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [input]. 2 c1 v (c2 ^ (c1 ^ c3)) != c1 # answer(McKenzie_1). [clausify]. 3 c4 ^ (c5 v (c4 v c6)) != c4 # answer(McKenzie_2). [clausify]. 4 ((c7 ^ c8) v (c8 ^ c9)) v c8 != c8 # answer(McKenzie_3). [clausify]. 5 ((c10 v c11) ^ (c11 v c12)) ^ c11 != c11 # answer(McKenzie_4). [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). 2 c1 v (c2 ^ (c1 ^ c3)) != c1 # answer(McKenzie_1). [clausify]. 3 c4 ^ (c5 v (c4 v c6)) != c4 # answer(McKenzie_2). [clausify]. 4 ((c7 ^ c8) v (c8 ^ c9)) v c8 != c8 # answer(McKenzie_3). [clausify]. 5 ((c10 v c11) ^ (c11 v c12)) ^ c11 != c11 # answer(McKenzie_4). [clausify]. end_of_list. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, v, ^ ]). After inverse_order: Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, v, ^ ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: no changes. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 6 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [input]. end_of_list. clauses(demodulators). 6 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [input]. end_of_list. clauses(denials). 7 c1 v (c2 ^ (c1 ^ c3)) != c1 # answer(McKenzie_1). [clausify]. 8 c4 ^ (c5 v (c4 v c6)) != c4 # answer(McKenzie_2). [clausify]. 9 ((c7 ^ c8) v (c8 ^ c9)) v c8 != c8 # answer(McKenzie_3). [clausify]. 10 ((c10 v c11) ^ (c11 v c12)) ^ c11 != c11 # answer(McKenzie_4). [clausify]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=29): 6 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [input]. given #2 (F,wt=21): 13 (((x v y) ^ y) v (y v y)) ^ (z v ((u v y) ^ (y v v))) = y. [para(6(a,1),6(a,1,1,2))]. given #3 (F,wt=25): 17 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (z v y) = y v y. [para(13(a,1),13(a,1,2,2))]. given #4 (T,wt=27): 18 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v ((w v y) ^ (y v v6))) = y. [para(17(a,1),6(a,1,1,2,1,1))]. given #5 (T,wt=33): 24 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (z ^ (y v y))) ^ u)) ^ (v v y) = y v y. [para(13(a,1),18(a,1,2,2))]. given #6 (A,wt=61): 11 (((x v ((y v z) ^ (z v u))) ^ ((y v z) ^ (z v u))) v ((z v (v ^ ((y v z) ^ (z v u)))) ^ w)) ^ (v6 v ((v7 v ((y v z) ^ (z v u))) ^ (((y v z) ^ (z v u)) v v8))) = (y v z) ^ (z v u). [para(6(a,1),6(a,1,1,2,1,1))]. given #7 (F,wt=31): 28 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (y v y)) ^ z)) ^ (u v y) = y v y. [para(17(a,1),24(a,1,1,2,1,2))]. given #8 (F,wt=33): 34 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) ^ (v6 v ((v7 v y) ^ (y v v8))) = y. [para(18(a,1),11(a,1,1,1,1,2)),demod(18(17),18(22),18(26),18(27),18(31))]. given #9 (T,wt=21): 44 (((x v y) ^ y) v (z ^ y)) ^ (u v ((v v y) ^ (y v w))) = y. [para(6(a,1),34(a,1,1,2))]. given #10 (T,wt=23): 57 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(13(a,1),44(a,1,2,2))]. given #11 (A,wt=83): 12 (((x v (y v ((z v u) ^ (u v v)))) ^ (y v ((z v u) ^ (u v v)))) v (((w ^ ((y v ((z v u) ^ (u v v))) v (y v ((z v u) ^ (u v v))))) v u) ^ v6)) ^ (v7 v ((v8 v (y v ((z v u) ^ (u v v)))) ^ ((y v ((z v u) ^ (u v v))) v v9))) = y v ((z v u) ^ (u v v)). [para(6(a,1),6(a,1,1,2,1,2))]. given #12 (F,wt=21): 69 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(17(a,1),57(a,1,1,2))]. given #13 (F,wt=15): 94 ((x v x) v (x v x)) ^ (y v x) = x v x. [para(69(a,1),69(a,1,1,1))]. given #14 (T,wt=17): 92 ((x v x) v (y ^ (x v x))) ^ (z v x) = x v x. [para(69(a,1),57(a,1,1,1))]. given #15 (T,wt=19): 82 ((x v x) v ((x v x) v (x v x))) ^ (y v x) = x v x. [para(69(a,1),17(a,1,1,1))]. given #16 (A,wt=83): 14 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v (((w ^ ((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v))) v (v6 ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v7)) ^ (v8 v z) = ((y ^ (z v z)) v (u ^ z)) ^ v. [para(6(a,1),6(a,1,2,2))]. given #17 (F,wt=23): 67 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (v v z) = y ^ z. [para(44(a,1),44(a,1,2,2))]. given #18 (F,wt=15): 114 ((x v x) v (y ^ x)) ^ (z v x) = x v x. [para(67(a,1),92(a,1,1,2))]. given #19 (T,wt=21): 112 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(67(a,1),57(a,1,1,2))]. given #20 (T,wt=23): 103 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(14(a,1),92(a,1,1,2))]. given #21 (A,wt=35): 15 (((x v (y v y)) ^ (y v y)) v (((z ^ ((y v y) v (y v y))) v (u ^ (y v y))) ^ v)) ^ (w v y) = y v y. [para(13(a,1),6(a,1,2,2))]. given #22 (F,wt=21): 138 ((x v x) v (((x v x) v (y ^ x)) ^ z)) ^ (u v x) = x v x. [para(17(a,1),103(a,1,1,2,1,1))]. given #23 (F,wt=21): 148 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(67(a,1),103(a,1,1,2,1,1))]. given #24 (T,wt=13): 171 ((x v x) v x) ^ (y v x) = x v x. [para(6(a,1),148(a,1,1,2))]. given #25 (T,wt=17): 186 (((x v y) ^ y) v (y v y)) ^ (z v (y v y)) = y. [para(171(a,1),13(a,1,2,2))]. given #26 (A,wt=65): 16 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v ((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ (w v z) = ((y ^ (z v z)) v (u ^ z)) ^ v. [para(6(a,1),13(a,1,2,2))]. given #27 (F,wt=17): 191 (((x v y) ^ y) v (z ^ y)) ^ (u v (y v y)) = y. [para(171(a,1),44(a,1,2,2))]. given #28 (F,wt=19): 204 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v (y v y))) = y. [para(186(a,1),67(a,1,1,1,1,2)),demod(186(8),186(9),186(15))]. given #29 (T,wt=21): 238 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v (w v (y v y)))) = y. [para(204(a,1),67(a,1,1,1,1,2)),demod(204(9),204(10),204(17))]. given #30 (T,wt=23): 105 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v ((w v y) ^ (y v v6)))) = y. [para(6(a,1),67(a,1,1,1,1,2)),demod(6(14),6(15),6(23))]. given #31 (A,wt=43): 19 (((x v (y v z)) ^ (y v z)) v (((u ^ ((y v z) v (y v z))) v (z v z)) ^ v)) ^ (w v ((v6 v (y v z)) ^ ((y v z) v v7))) = y v z. [para(17(a,1),6(a,1,1,2,1,2))]. given #32 (F,wt=23): 187 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v (y v y)) = y. [para(171(a,1),18(a,1,2,2))]. given #33 (F,wt=23): 202 (((x v x) v (x v x)) v x) ^ (y v (x v x)) = (x v x) v (x v x). [para(186(a,1),92(a,1,1,2))]. given #34 (T,wt=21): 338 (((x v y) ^ y) v (y v y)) ^ (z v ((y v y) v (y v y))) = y. [para(202(a,1),13(a,1,2,2))]. given #35 (T,wt=23): 222 ((x v x) v (y ^ (x v x))) ^ (z v ((x v x) v (x v x))) = x v x. [para(69(a,1),191(a,1,1,1))]. given #36 (A,wt=71): 20 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v (((v ^ ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))) v (w ^ (((y v y) v (z ^ y)) ^ u))) ^ v6)) ^ (v7 v y) = ((y v y) v (z ^ y)) ^ u. [para(18(a,1),6(a,1,2,2))]. given #37 (F,wt=21): 346 ((x v x) v (x v x)) ^ (y v ((x v x) v (x v x))) = x v x. [para(17(a,1),222(a,1,1,2))]. given #38 (F,wt=21): 348 ((x v x) v (y ^ x)) ^ (z v ((x v x) v (x v x))) = x v x. [para(67(a,1),222(a,1,1,2))]. given #39 (T,wt=23): 263 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v (w v (v6 v (y v y))))) = y. [para(238(a,1),67(a,1,1,1,1,2)),demod(238(10),238(11),238(19))]. given #40 (T,wt=25): 56 (((x v (y ^ z)) ^ (y ^ z)) v ((y ^ z) v (y ^ z))) ^ (u v z) = y ^ z. [para(44(a,1),13(a,1,2,2))]. given #41 (A,wt=81): 21 (((x v (y v ((z v u) ^ (u v v)))) ^ (y v ((z v u) ^ (u v v)))) v ((((y v ((z v u) ^ (u v v))) v (y v ((z v u) ^ (u v v)))) v u) ^ w)) ^ (v6 v ((v7 v (y v ((z v u) ^ (u v v)))) ^ ((y v ((z v u) ^ (u v v))) v v8))) = y v ((z v u) ^ (u v v)). [para(6(a,1),18(a,1,1,2,1,2))]. given #42 (F,wt=19): 418 (((x v y) ^ y) v (y v y)) ^ (z v (u v (y v y))) = y. [para(186(a,1),56(a,1,1,1,1,2)),demod(186(8),186(9),186(9),186(15))]. given #43 (F,wt=21): 419 (((x v y) ^ y) v (y v y)) ^ (z v (u v (v v (y v y)))) = y. [para(204(a,1),56(a,1,1,1,1,2)),demod(204(9),204(10),204(10),204(17))]. given #44 (T,wt=23): 414 (((x v y) ^ y) v (y v y)) ^ (z v (u v ((v v y) ^ (y v w)))) = y. [para(6(a,1),56(a,1,1,1,1,2)),demod(6(14),6(15),6(15),6(23))]. given #45 (T,wt=23): 420 (((x v y) ^ y) v (y v y)) ^ (z v (u v (v v (w v (y v y))))) = y. [para(238(a,1),56(a,1,1,1,1,2)),demod(238(10),238(11),238(11),238(19))]. given #46 (A,wt=81): 22 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v ((((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v)) v (w ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v6)) ^ (v7 v z) = ((y ^ (z v z)) v (u ^ z)) ^ v. [para(6(a,1),18(a,1,2,2))]. given #47 (F,wt=25): 87 ((x v x) v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (z v x) = x v x. [para(69(a,1),28(a,1,1,1))]. given #48 (F,wt=25): 106 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v (v v y)) = y v y. [para(17(a,1),67(a,1,1,1,1,2)),demod(17(12),17(14),17(20))]. given #49 (T,wt=19): 461 ((x v x) v (y ^ (x v x))) ^ (z v (u v x)) = x v x. [para(69(a,1),106(a,1,1,1))]. given #50 (T,wt=17): 493 ((x v x) v (x v x)) ^ (y v (z v x)) = x v x. [para(17(a,1),461(a,1,1,2))]. given #51 (A,wt=55): 23 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))) ^ (v v y) = ((y v y) v (z ^ y)) ^ u. [para(18(a,1),13(a,1,2,2))]. given #52 (F,wt=17): 495 ((x v x) v (y ^ x)) ^ (z v (u v x)) = x v x. [para(67(a,1),461(a,1,1,2))]. given #53 (F,wt=23): 454 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v (u v y)) = y v y. [para(17(a,1),106(a,1,1,2))]. given #54 (T,wt=23): 465 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v (v v y)) = y v y. [para(67(a,1),106(a,1,1,2))]. given #55 (T,wt=23): 500 ((x v x) v (((x v x) v (y ^ x)) ^ z)) ^ (u v (v v x)) = x v x. [para(20(a,1),461(a,1,1,2))]. given #56 (A,wt=41): 25 (((x v (y v z)) ^ (y v z)) v ((((y v z) v (y v z)) v (z v z)) ^ u)) ^ (v v ((w v (y v z)) ^ ((y v z) v v6))) = y v z. [para(17(a,1),18(a,1,1,2,1,2))]. given #57 (F,wt=25): 118 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (v v (w v z)) = y ^ z. [para(67(a,1),67(a,1,1,1,1,2)),demod(67(11),67(13),67(19))]. given #58 (F,wt=25): 122 (((x v y) v (x v y)) v (y v y)) ^ (z v (x v y)) = (x v y) v (x v y). [para(17(a,1),114(a,1,1,2))]. given #59 (T,wt=25): 129 (((x v y) v (x v y)) v (z ^ y)) ^ (u v (x v y)) = (x v y) v (x v y). [para(67(a,1),114(a,1,1,2))]. given #60 (T,wt=25): 185 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(171(a,1),6(a,1,2,2))]. given #61 (A,wt=69): 26 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v ((((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u)) v (v ^ (((y v y) v (z ^ y)) ^ u))) ^ w)) ^ (v6 v y) = ((y v y) v (z ^ y)) ^ u. [para(18(a,1),18(a,1,2,2))]. given #62 (F,wt=23): 605 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(67(a,1),185(a,1,1,2,1,1))]. given #63 (F,wt=15): 624 (((x v y) ^ y) v y) ^ (z v (y v y)) = y. [para(6(a,1),605(a,1,1,2))]. given #64 (T,wt=15): 652 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(624(a,1),13(a,1,2,2))]. given #65 (T,wt=11): 683 (x v x) v (x v x) = x v x. [para(69(a,1),652(a,1,1,1)),demod(682(8))]. given #66 (A,wt=35): 29 (((x v y) ^ y) v (((((z ^ (y v y)) v (u ^ y)) ^ v) v (w ^ y)) ^ v6)) ^ (v7 v ((v8 v y) ^ (y v v9))) = y. [para(6(a,1),11(a,1,1,1,1,2)),demod(6(19),6(25),6(29),6(30),6(34))]. given #67 (F,wt=11): 792 (x v x) ^ (y v x) = x v x. [back_demod(94),demod(683(3))]. given #68 (F,wt=13): 682 (x v (x v x)) ^ (y v x) = x v x. [para(652(a,1),69(a,1,1,1))]. given #69 (T,wt=13): 689 (x v (y ^ x)) ^ (z v x) = x v x. [para(652(a,1),112(a,1,1,1))]. given #70 (T,wt=13): 764 (x v x) ^ (y v (z v x)) = x v x. [back_demod(493),demod(683(3))]. given #71 (A,wt=89): 30 (((x v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v))) ^ ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v))) v u) ^ (w v ((v6 v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v))) ^ (((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v)) v v7))) = (y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v). [para(6(a,1),11(a,1,1,2))]. given #72 (F,wt=13): 843 (((x v y) ^ y) v y) ^ (y v y) = y. [para(683(a,1),624(a,1,2))]. given #73 (F,wt=15): 657 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(624(a,1),44(a,1,2,2))]. given #74 (T,wt=15): 678 (x v (y ^ (x v x))) ^ (z v x) = x v x. [para(652(a,1),57(a,1,1,1))]. given #75 (T,wt=15): 727 ((x v x) v x) ^ (y v (z v x)) = x v x. [para(652(a,1),461(a,1,1,2))]. given #76 (A,wt=77): 31 (((x v (((y ^ (z v z)) v (u ^ z)) ^ ((u ^ z) v v))) ^ (((y ^ (z v z)) v (u ^ z)) ^ ((u ^ z) v v))) v (((u ^ z) v (w ^ (((y ^ (z v z)) v (u ^ z)) ^ ((u ^ z) v v)))) ^ v6)) ^ (v7 v z) = ((y ^ (z v z)) v (u ^ z)) ^ ((u ^ z) v v). [para(6(a,1),11(a,1,2,2))]. given #77 (F,wt=15): 730 (x v (x v x)) ^ (y v (z v x)) = x v x. [para(652(a,1),454(a,1,1,1))]. given #78 (F,wt=15): 731 (x v (y ^ x)) ^ (z v (u v x)) = x v x. [para(652(a,1),465(a,1,1,1))]. given #79 (T,wt=15): 746 (x v ((x v x) ^ y)) ^ (z v x) = x v x. [back_demod(672),demod(683(3),683(3))]. given #80 (T,wt=15): 773 (x v x) ^ (y v (z v (x v x))) = x v x. [back_demod(434),demod(683(4),683(3),683(4))]. given #81 (A,wt=81): 32 (((x v ((y v (z ^ ((u v y) ^ (y v v)))) ^ w)) ^ ((y v (z ^ ((u v y) ^ (y v v)))) ^ w)) v (((y v (z ^ ((u v y) ^ (y v v)))) ^ w) v ((y v (z ^ ((u v y) ^ (y v v)))) ^ w))) ^ (v6 v ((u v y) ^ (y v v))) = (y v (z ^ ((u v y) ^ (y v v)))) ^ w. [para(11(a,1),13(a,1,2,2))]. given #82 (F,wt=17): 660 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v y)) = y. [para(624(a,1),105(a,1,2,2,2))]. given #83 (F,wt=17): 664 (((x v y) ^ y) v (y v y)) ^ (z v (u v y)) = y. [para(624(a,1),414(a,1,2,2,2))]. given #84 (T,wt=17): 719 (x v (x v x)) ^ (y v (z v (x v x))) = x v x. [para(652(a,1),418(a,1,1,1)),demod(683(3),683(5))]. given #85 (T,wt=17): 725 (x v (y ^ (x v x))) ^ (z v (u v x)) = x v x. [para(652(a,1),106(a,1,1,1))]. given #86 (A,wt=99): 33 (((x v ((y v (z ^ ((u v y) ^ (y v v)))) ^ w)) ^ ((y v (z ^ ((u v y) ^ (y v v)))) ^ w)) v (((((y v (z ^ ((u v y) ^ (y v v)))) ^ w) v ((y v (z ^ ((u v y) ^ (y v v)))) ^ w)) v (v6 ^ ((y v (z ^ ((u v y) ^ (y v v)))) ^ w))) ^ v7)) ^ (v8 v ((u v y) ^ (y v v))) = (y v (z ^ ((u v y) ^ (y v v)))) ^ w. [para(11(a,1),18(a,1,2,2))]. given #87 (F,wt=17): 772 (x v x) ^ (y v (z v (u v (x v x)))) = x v x. [back_demod(435),demod(683(4),683(3),683(4))]. given #88 (F,wt=17): 794 ((x v x) v ((x v x) ^ y)) ^ (z v x) = x v x. [back_demod(87),demod(683(4),683(4))]. given #89 (T,wt=19): 679 (((x v (y v y)) ^ (y v y)) v y) ^ (z v y) = y v y. [para(652(a,1),57(a,1,1,2))]. given #90 (T,wt=19): 691 ((x v x) v ((x v (y ^ x)) ^ z)) ^ (u v x) = x v x. [para(652(a,1),103(a,1,1,2,1,1))]. given #91 (A,wt=69): 35 (((x v (((y v y) v (z ^ y)) ^ ((z ^ y) v u))) ^ (((y v y) v (z ^ y)) ^ ((z ^ y) v u))) v (((z ^ y) v (v ^ (((y v y) v (z ^ y)) ^ ((z ^ y) v u)))) ^ w)) ^ (v6 v y) = ((y v y) v (z ^ y)) ^ ((z ^ y) v u). [para(18(a,1),11(a,1,2,2))]. given #92 (F,wt=19): 700 (x v (y ^ (x v x))) ^ (z v (u v (x v x))) = x v x. [para(652(a,1),204(a,1,1,1)),demod(683(6))]. given #93 (F,wt=17): 1225 (x v (y ^ x)) ^ (z v (u v (x v x))) = x v x. [para(67(a,1),700(a,1,1,2))]. given #94 (T,wt=19): 720 (x v (x v x)) ^ (y v (z v (u v (x v x)))) = x v x. [para(652(a,1),419(a,1,1,1)),demod(683(3),683(5))]. given #95 (T,wt=19): 736 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v (w v y))) = y. [para(652(a,1),118(a,1,1,1,1,2)),demod(652(7),652(8),652(14))]. given #96 (A,wt=73): 36 (((x v ((y v z) ^ (z v u))) ^ ((y v z) ^ (z v u))) v ((((z v (v ^ ((y v z) ^ (z v u)))) ^ w) v (v6 ^ ((y v z) ^ (z v u)))) ^ v7)) ^ (v8 v ((v9 v ((y v z) ^ (z v u))) ^ (((y v z) ^ (z v u)) v v10))) = (y v z) ^ (z v u). [para(11(a,1),11(a,1,1,1,1,2)),demod(11(36),11(46),11(53),11(57),11(64))]. given #97 (F,wt=19): 770 (x v x) ^ (y v (z v (u v (v v (x v x))))) = x v x. [back_demod(446),demod(683(4),683(3),683(4))]. given #98 (F,wt=19): 890 ((x v x) v ((y ^ x) v (y ^ x))) ^ (z v x) = x v x. [para(792(a,1),148(a,1,1,2))]. given #99 (T,wt=19): 910 ((x v y) v y) ^ (z v (x v y)) = (x v y) v (x v y). [para(652(a,1),689(a,1,1,2))]. given #100 (T,wt=19): 920 (((x v y) ^ y) v y) ^ (z v ((u v y) ^ (y v v))) = y. [para(44(a,1),30(a,1,1,1,1,2)),demod(44(13),44(15),44(16),44(20))]. given #101 (A,wt=95): 42 (((x v (y v ((z v u) ^ (u v v)))) ^ (y v ((z v u) ^ (u v v)))) v ((((((y v ((z v u) ^ (u v v))) v (y v ((z v u) ^ (u v v)))) v u) ^ w) v (v6 ^ (y v ((z v u) ^ (u v v))))) ^ v7)) ^ (v8 v ((v9 v (y v ((z v u) ^ (u v v)))) ^ ((y v ((z v u) ^ (u v v))) v v10))) = y v ((z v u) ^ (u v v)). [para(6(a,1),34(a,1,1,2,1,1,1,2))]. given #102 (F,wt=13): 1407 (((x v y) ^ y) v y) ^ (z v y) = y. [para(624(a,1),920(a,1,2,2))]. given #103 (F,wt=19): 972 (x v (((x v x) v (y ^ x)) ^ z)) ^ (u v x) = x v x. [para(20(a,1),678(a,1,1,2))]. given #104 (T,wt=19): 1016 ((x v x) v ((x v x) ^ y)) ^ (z v (x v x)) = x v x. [para(683(a,1),746(a,1,1,2,1)),demod(683(10))]. given #105 (T,wt=19): 1122 (((x v y) ^ y) v (y v y)) ^ (z v (u v (v v y))) = y. [para(660(a,1),56(a,1,1,1,1,2)),demod(660(8),660(9),660(9),660(15))]. given #106 (A,wt=95): 43 (((x v (y v ((z v u) ^ (u v v)))) ^ (y v ((z v u) ^ (u v v)))) v ((((((y v ((z v u) ^ (u v v))) v (y v ((z v u) ^ (u v v)))) v (w ^ (y v ((z v u) ^ (u v v))))) ^ v6) v u) ^ v7)) ^ (v8 v ((v9 v (y v ((z v u) ^ (u v v)))) ^ ((y v ((z v u) ^ (u v v))) v v10))) = y v ((z v u) ^ (u v v)). [para(6(a,1),34(a,1,1,2,1,2))]. given #107 (F,wt=19): 1412 (((x v y) ^ y) v y) ^ (z v ((u v y) v (u v y))) = y. [para(910(a,1),920(a,1,2,2))]. given #108 (F,wt=17): 1480 (((x v y) ^ y) v y) ^ ((z v y) v (z v y)) = y. [para(683(a,1),1412(a,1,2))]. given #109 (T,wt=21): 653 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v y) = y. [para(624(a,1),18(a,1,2,2))]. given #110 (T,wt=21): 702 (x v (y ^ (x v x))) ^ (z v (u v (v v (x v x)))) = x v x. [para(652(a,1),238(a,1,1,1)),demod(683(6))]. given #111 (A,wt=97): 45 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v ((((((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v)) v (w ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v6) v (v7 ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v8)) ^ (v9 v z) = ((y ^ (z v z)) v (u ^ z)) ^ v. [para(6(a,1),34(a,1,2,2))]. given #112 (F,wt=19): 1515 (x v (y ^ x)) ^ (z v (u v (v v (x v x)))) = x v x. [para(67(a,1),702(a,1,1,2))]. given #113 (F,wt=19): 1517 ((x v x) v x) ^ (y v (z v (u v (x v x)))) = x v x. [para(187(a,1),702(a,1,1,2)),demod(683(5),683(10))]. given #114 (T,wt=21): 722 (x v (x v x)) ^ (y v (z v (u v (v v (x v x))))) = x v x. [para(652(a,1),420(a,1,1,1)),demod(683(3),683(5))]. given #115 (T,wt=21): 726 (((x v (y v y)) ^ (y v y)) v y) ^ (z v (u v y)) = y v y. [para(652(a,1),106(a,1,1,2))]. given #116 (A,wt=85): 46 (((x v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) ^ (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) v ((((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w) v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w))) ^ (v6 v y) = ((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w. [para(34(a,1),13(a,1,2,2))]. given #117 (F,wt=21): 739 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ (v v (y v y)) = y. [para(652(a,1),185(a,1,1,2,1,1))]. given #118 (F,wt=19): 1605 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ (y v y) = y. [para(683(a,1),739(a,1,2))]. given #119 (T,wt=21): 748 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [back_demod(670),demod(683(3))]. given #120 (T,wt=17): 1649 (x v (((x v x) v x) ^ y)) ^ (z v x) = x v x. [para(652(a,1),748(a,1,1,2,1,2))]. given #121 (A,wt=49): 48 (((x v (y v z)) ^ (y v z)) v ((((((y v z) v (y v z)) v (z v z)) ^ u) v (v ^ (y v z))) ^ w)) ^ (v6 v ((v7 v (y v z)) ^ ((y v z) v v8))) = y v z. [para(17(a,1),34(a,1,1,2,1,1,1,2))]. given #122 (F,wt=21): 797 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_demod(80),demod(683(4),683(3))]. given #123 (F,wt=17): 1704 (x v x) ^ (y v ((z v x) v (z v x))) = x v x. [para(122(a,1),797(a,1,2,2))]. given #124 (T,wt=19): 1705 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(683(a,1),797(a,1,2,2,1))]. given #125 (T,wt=5): 1794 x v x = x. [back_demod(1454),demod(1745(5),1745(6),792(3),1745(6))]. given #126 (A,wt=7): 1757 x ^ (y v x) = x. [para(105(a,1),1705(a,1,2,2)),demod(1745(5),1745(7))]. given #127 (F,wt=5): 2306 x ^ x = x. [back_demod(1792),demod(1822(2),1822(3),1822(2),1794(1),1822(3))]. given #128 (F,wt=7): 1822 (x v y) ^ y = y. [back_demod(1745),demod(1794(5))]. given #129 (T,wt=9): 1842 x ^ (y v (z v x)) = x. [back_demod(1704),demod(1794(1),1794(3),1794(4))]. given #130 (T,wt=9): 2181 (x ^ y) ^ y = x ^ y. [back_demod(827),demod(1794(1),1794(3),1822(4),1794(2),1794(3),1794(4),1794(3),1794(2),1794(3))]. given #131 (A,wt=29): 1797 ((x ^ (x v y)) v (((x ^ (x v y)) v x) ^ z)) ^ (u v (x ^ (x v y))) = x ^ (x v y). [back_demod(1791),demod(1794(1),1794(1),1794(3),1794(3),1794(5),1794(5),1794(7),1794(5),1794(8),1794(8),1794(12),1794(12),1794(14),1794(14),1794(16))]. given #132 (F,wt=11): 1839 (x ^ y) ^ (z v y) = x ^ y. [back_demod(1708),demod(1794(3),1794(2),1794(6))]. given #133 (F,wt=11): 1841 x ^ (y v (x ^ (x v z))) = x. [back_demod(1705),demod(1794(1),1794(1),1794(1),1794(5))]. given #134 (T,wt=9): 2334 x ^ (x ^ (x v y)) = x. [para(1794(a,1),1841(a,1,2))]. given #135 (T,wt=11): 1871 (x ^ y) ^ (z v x) = x ^ y. [back_demod(1663),demod(1794(1),1794(1),1794(3),1794(3),1822(4),1794(2),1794(2),1794(3),1794(2),1794(4),1794(4))]. given #136 (A,wt=31): 1800 ((x v (y ^ (y v z))) v y) ^ (u v (v v (w v (x v (y ^ (y v z)))))) = x v (y ^ (y v z)). [back_demod(1788),demod(1794(1),1794(1),1794(4),1794(5),1794(5),1794(8),1794(8),1794(11),1794(12),1794(12),1794(15),1794(15),1794(18))]. given #137 (F,wt=9): 2336 (x ^ y) ^ x = x ^ y. [para(1794(a,1),1871(a,1,2))]. given #138 (F,wt=11): 1883 (x v (x ^ y)) ^ (z v x) = x. [back_demod(1649),demod(1794(1),1794(1),1794(5))]. given #139 (T,wt=7): 2340 x v (x ^ y) = x. [para(1883(a,1),1841(a,1,2,2)),demod(1883(4)),flip(a)]. given #140 (T,wt=7): 2345 x ^ (x v y) = x. [back_demod(2334),demod(2341(3))]. ============================== PROOF ================================= % Proof 1 at 2.25 (+ 0.03) seconds: McKenzie_2. % Length of proof is 51. % Level of proof is 27. % Maximum clause weight is 83. % Given clauses 140. 6 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [input]. 8 c4 ^ (c5 v (c4 v c6)) != c4 # answer(McKenzie_2). [clausify]. 11 (((x v ((y v z) ^ (z v u))) ^ ((y v z) ^ (z v u))) v ((z v (v ^ ((y v z) ^ (z v u)))) ^ w)) ^ (v6 v ((v7 v ((y v z) ^ (z v u))) ^ (((y v z) ^ (z v u)) v v8))) = (y v z) ^ (z v u). [para(6(a,1),6(a,1,1,2,1,1))]. 13 (((x v y) ^ y) v (y v y)) ^ (z v ((u v y) ^ (y v v))) = y. [para(6(a,1),6(a,1,1,2))]. 14 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v (((w ^ ((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v))) v (v6 ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v7)) ^ (v8 v z) = ((y ^ (z v z)) v (u ^ z)) ^ v. [para(6(a,1),6(a,1,2,2))]. 17 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (z v y) = y v y. [para(13(a,1),13(a,1,2,2))]. 18 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v ((w v y) ^ (y v v6))) = y. [para(17(a,1),6(a,1,1,2,1,1))]. 24 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (z ^ (y v y))) ^ u)) ^ (v v y) = y v y. [para(13(a,1),18(a,1,2,2))]. 28 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (y v y)) ^ z)) ^ (u v y) = y v y. [para(17(a,1),24(a,1,1,2,1,2))]. 34 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) ^ (v6 v ((v7 v y) ^ (y v v8))) = y. [para(18(a,1),11(a,1,1,1,1,2)),demod(18(17),18(22),18(26),18(27),18(31))]. 44 (((x v y) ^ y) v (z ^ y)) ^ (u v ((v v y) ^ (y v w))) = y. [para(6(a,1),34(a,1,1,2))]. 57 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(13(a,1),44(a,1,2,2))]. 67 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (v v z) = y ^ z. [para(44(a,1),44(a,1,2,2))]. 69 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(17(a,1),57(a,1,1,2))]. 80 ((x v x) v ((x v x) v (x v x))) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [para(69(a,1),13(a,1,1,1))]. 92 ((x v x) v (y ^ (x v x))) ^ (z v x) = x v x. [para(69(a,1),57(a,1,1,1))]. 94 ((x v x) v (x v x)) ^ (y v x) = x v x. [para(69(a,1),69(a,1,1,1))]. 103 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(14(a,1),92(a,1,1,2))]. 148 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(67(a,1),103(a,1,1,2,1,1))]. 171 ((x v x) v x) ^ (y v x) = x v x. [para(6(a,1),148(a,1,1,2))]. 185 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(171(a,1),6(a,1,2,2))]. 605 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(67(a,1),185(a,1,1,2,1,1))]. 624 (((x v y) ^ y) v y) ^ (z v (y v y)) = y. [para(6(a,1),605(a,1,1,2))]. 652 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(624(a,1),13(a,1,2,2))]. 657 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(624(a,1),44(a,1,2,2))]. 670 (x v ((((x v x) v (x v x)) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [para(652(a,1),24(a,1,1,1))]. 672 (x v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (z v x) = x v x. [para(652(a,1),28(a,1,1,1))]. 682 (x v (x v x)) ^ (y v x) = x v x. [para(652(a,1),69(a,1,1,1))]. 683 (x v x) v (x v x) = x v x. [para(69(a,1),652(a,1,1,1)),demod(682(8))]. 746 (x v ((x v x) ^ y)) ^ (z v x) = x v x. [back_demod(672),demod(683(3),683(3))]. 748 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [back_demod(670),demod(683(3))]. 792 (x v x) ^ (y v x) = x v x. [back_demod(94),demod(683(3))]. 797 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_demod(80),demod(683(4),683(3))]. 890 ((x v x) v ((y ^ x) v (y ^ x))) ^ (z v x) = x v x. [para(792(a,1),148(a,1,1,2))]. 1016 ((x v x) v ((x v x) ^ y)) ^ (z v (x v x)) = x v x. [para(683(a,1),746(a,1,1,2,1)),demod(683(10))]. 1454 ((((x v y) ^ y) v ((x v y) ^ y)) v y) ^ (z v (((x v y) ^ y) v ((x v y) ^ y))) = ((x v y) ^ y) v ((x v y) ^ y). [para(44(a,1),1016(a,1,1,2))]. 1649 (x v (((x v x) v x) ^ y)) ^ (z v x) = x v x. [para(652(a,1),748(a,1,1,2,1,2))]. 1705 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(683(a,1),797(a,1,2,2,1))]. 1708 ((x ^ y) v (x ^ y)) ^ (z v (y v y)) = (x ^ y) v (x ^ y). [para(890(a,1),797(a,1,2,2))]. 1745 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(44(a,1),1705(a,1,2,2)),demod(657(7)),flip(a)]. 1794 x v x = x. [back_demod(1454),demod(1745(5),1745(6),792(3),1745(6))]. 1822 (x v y) ^ y = y. [back_demod(1745),demod(1794(5))]. 1839 (x ^ y) ^ (z v y) = x ^ y. [back_demod(1708),demod(1794(3),1794(2),1794(6))]. 1841 x ^ (y v (x ^ (x v z))) = x. [back_demod(1705),demod(1794(1),1794(1),1794(1),1794(5))]. 1883 (x v (x ^ y)) ^ (z v x) = x. [back_demod(1649),demod(1794(1),1794(1),1794(5))]. 2334 x ^ (x ^ (x v y)) = x. [para(1794(a,1),1841(a,1,2))]. 2340 x v (x ^ y) = x. [para(1883(a,1),1841(a,1,2,2)),demod(1883(4)),flip(a)]. 2341 x ^ (x ^ y) = x ^ y. [para(2340(a,1),1822(a,1,1))]. 2345 x ^ (x v y) = x. [back_demod(2334),demod(2341(3))]. 2362 x ^ (y v (x v z)) = x. [para(2345(a,1),1839(a,1,1)),demod(2345(5))]. 2363 $F # answer(McKenzie_2). [resolve(2362,a,8,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 8. given #141 (A,wt=27): 1825 ((x v (y v z)) v (((x v (y v z)) v z) ^ u)) ^ (x v (y v z)) = x v (y v z). [back_demod(1742),demod(1794(3),1794(6),1822(6),1794(5),1794(5),1794(10),1794(12),1794(12),1794(13))]. given #142 (F,wt=9): 2341 x ^ (x ^ y) = x ^ y. [para(2340(a,1),1822(a,1,1))]. given #143 (F,wt=9): 2342 (x v y) v y = x v y. [para(1822(a,1),2340(a,1,2))]. given #144 (T,wt=9): 2362 x ^ (y v (x v z)) = x. [para(2345(a,1),1839(a,1,1)),demod(2345(5))]. given #145 (T,wt=11): 1954 x ^ (y v (z v (u v x))) = x. [back_demod(1517),demod(1794(1),1794(1),1794(1),1794(5))]. given #146 (A,wt=29): 1826 ((x v (y v z)) v (((x v (y v z)) v z) ^ u)) ^ (v v (x v (y v z))) = x v (y v z). [back_demod(1741),demod(1794(3),1794(6),1822(6),1794(5),1794(5),1794(10),1794(12),1794(12),1794(14))]. given #147 (F,wt=11): 2202 (x v (y ^ x)) ^ (z v x) = x. [back_demod(689),demod(1794(5))]. given #148 (F,wt=7): 2376 x v (y ^ x) = x. [para(2202(a,1),2345(a,1)),flip(a)]. given #149 (T,wt=9): 2443 x ^ (y ^ x) = y ^ x. [para(2376(a,1),1822(a,1,1))]. given #150 (T,wt=7): 2457 (x v y) ^ x = x. [para(2345(a,1),2443(a,1,2)),demod(2345(4))]. given #151 (A,wt=51): 1829 ((x v (y v z)) v (((((u ^ (x v (y v z))) v (v ^ (x v (y v z)))) ^ w) v z) ^ v6)) ^ (v7 v ((v8 v (x v (y v z))) ^ ((x v (y v z)) v v9))) = x v (y v z). [back_demod(1729),demod(1794(3),1794(6),1822(6),1794(5),1794(7),1794(7),1794(8),1794(11),1794(16),1794(19),1794(25))]. given #152 (F,wt=9): 2449 (x v y) v x = x v y. [para(2345(a,1),2376(a,1,2))]. given #153 (F,wt=9): 2454 (x v (y v z)) ^ z = z. [para(1842(a,1),2443(a,1,2)),demod(1842(6))]. given #154 (T,wt=9): 2458 (x v (y v z)) ^ y = y. [para(2362(a,1),2443(a,1,2)),demod(2362(6))]. given #155 (T,wt=9): 2489 x ^ ((y v x) v z) = x. [para(2449(a,1),1842(a,1,2))]. given #156 (A,wt=51): 1830 ((x v (y v z)) v (((((u ^ (x v (y v z))) v z) ^ v) v (w ^ (x v (y v z)))) ^ v6)) ^ (v7 v ((v8 v (x v (y v z))) ^ ((x v (y v z)) v v9))) = x v (y v z). [back_demod(1728),demod(1794(3),1794(6),1822(6),1794(5),1794(7),1794(7),1794(6),1794(10),1794(16),1794(19),1794(25))]. given #157 (F,wt=9): 2492 x ^ ((x v y) v z) = x. [para(2449(a,1),2362(a,1,2))]. given #158 (F,wt=9): 2495 ((x v y) v z) ^ y = y. [para(2449(a,1),2454(a,1,1))]. given #159 (T,wt=9): 2496 ((x v y) v z) ^ x = x. [para(2449(a,1),2458(a,1,1))]. given #160 (T,wt=11): 2368 x ^ (y v (z v (x v u))) = x. [para(2362(a,1),1839(a,1,1)),demod(2362(7))]. given #161 (A,wt=31): 1831 ((x v (y v z)) v (((u ^ (x v (y v z))) v z) ^ v)) ^ (w v (x v (y v z))) = x v (y v z). [back_demod(1727),demod(1794(3),1794(6),1822(6),1794(5),1794(6),1794(11),1794(13),1794(13),1794(15))]. given #162 (F,wt=11): 2446 (x v y) v (z ^ y) = x v y. [para(1839(a,1),2376(a,1,2))]. ============================== PROOF ================================= % Proof 2 at 2.31 (+ 0.03) seconds: McKenzie_1. % Length of proof is 56. % Level of proof is 29. % Maximum clause weight is 83. % Given clauses 162. 6 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [input]. 7 c1 v (c2 ^ (c1 ^ c3)) != c1 # answer(McKenzie_1). [clausify]. 11 (((x v ((y v z) ^ (z v u))) ^ ((y v z) ^ (z v u))) v ((z v (v ^ ((y v z) ^ (z v u)))) ^ w)) ^ (v6 v ((v7 v ((y v z) ^ (z v u))) ^ (((y v z) ^ (z v u)) v v8))) = (y v z) ^ (z v u). [para(6(a,1),6(a,1,1,2,1,1))]. 13 (((x v y) ^ y) v (y v y)) ^ (z v ((u v y) ^ (y v v))) = y. [para(6(a,1),6(a,1,1,2))]. 14 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v (((w ^ ((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v))) v (v6 ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v7)) ^ (v8 v z) = ((y ^ (z v z)) v (u ^ z)) ^ v. [para(6(a,1),6(a,1,2,2))]. 17 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (z v y) = y v y. [para(13(a,1),13(a,1,2,2))]. 18 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v ((w v y) ^ (y v v6))) = y. [para(17(a,1),6(a,1,1,2,1,1))]. 24 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (z ^ (y v y))) ^ u)) ^ (v v y) = y v y. [para(13(a,1),18(a,1,2,2))]. 28 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (y v y)) ^ z)) ^ (u v y) = y v y. [para(17(a,1),24(a,1,1,2,1,2))]. 34 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) ^ (v6 v ((v7 v y) ^ (y v v8))) = y. [para(18(a,1),11(a,1,1,1,1,2)),demod(18(17),18(22),18(26),18(27),18(31))]. 44 (((x v y) ^ y) v (z ^ y)) ^ (u v ((v v y) ^ (y v w))) = y. [para(6(a,1),34(a,1,1,2))]. 57 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(13(a,1),44(a,1,2,2))]. 67 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (v v z) = y ^ z. [para(44(a,1),44(a,1,2,2))]. 69 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(17(a,1),57(a,1,1,2))]. 80 ((x v x) v ((x v x) v (x v x))) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [para(69(a,1),13(a,1,1,1))]. 92 ((x v x) v (y ^ (x v x))) ^ (z v x) = x v x. [para(69(a,1),57(a,1,1,1))]. 94 ((x v x) v (x v x)) ^ (y v x) = x v x. [para(69(a,1),69(a,1,1,1))]. 103 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(14(a,1),92(a,1,1,2))]. 112 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(67(a,1),57(a,1,1,2))]. 148 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(67(a,1),103(a,1,1,2,1,1))]. 171 ((x v x) v x) ^ (y v x) = x v x. [para(6(a,1),148(a,1,1,2))]. 185 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(171(a,1),6(a,1,2,2))]. 605 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(67(a,1),185(a,1,1,2,1,1))]. 624 (((x v y) ^ y) v y) ^ (z v (y v y)) = y. [para(6(a,1),605(a,1,1,2))]. 652 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(624(a,1),13(a,1,2,2))]. 657 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(624(a,1),44(a,1,2,2))]. 670 (x v ((((x v x) v (x v x)) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [para(652(a,1),24(a,1,1,1))]. 672 (x v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (z v x) = x v x. [para(652(a,1),28(a,1,1,1))]. 682 (x v (x v x)) ^ (y v x) = x v x. [para(652(a,1),69(a,1,1,1))]. 683 (x v x) v (x v x) = x v x. [para(69(a,1),652(a,1,1,1)),demod(682(8))]. 689 (x v (y ^ x)) ^ (z v x) = x v x. [para(652(a,1),112(a,1,1,1))]. 746 (x v ((x v x) ^ y)) ^ (z v x) = x v x. [back_demod(672),demod(683(3),683(3))]. 748 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [back_demod(670),demod(683(3))]. 792 (x v x) ^ (y v x) = x v x. [back_demod(94),demod(683(3))]. 797 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_demod(80),demod(683(4),683(3))]. 890 ((x v x) v ((y ^ x) v (y ^ x))) ^ (z v x) = x v x. [para(792(a,1),148(a,1,1,2))]. 1016 ((x v x) v ((x v x) ^ y)) ^ (z v (x v x)) = x v x. [para(683(a,1),746(a,1,1,2,1)),demod(683(10))]. 1454 ((((x v y) ^ y) v ((x v y) ^ y)) v y) ^ (z v (((x v y) ^ y) v ((x v y) ^ y))) = ((x v y) ^ y) v ((x v y) ^ y). [para(44(a,1),1016(a,1,1,2))]. 1649 (x v (((x v x) v x) ^ y)) ^ (z v x) = x v x. [para(652(a,1),748(a,1,1,2,1,2))]. 1705 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(683(a,1),797(a,1,2,2,1))]. 1708 ((x ^ y) v (x ^ y)) ^ (z v (y v y)) = (x ^ y) v (x ^ y). [para(890(a,1),797(a,1,2,2))]. 1745 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(44(a,1),1705(a,1,2,2)),demod(657(7)),flip(a)]. 1794 x v x = x. [back_demod(1454),demod(1745(5),1745(6),792(3),1745(6))]. 1822 (x v y) ^ y = y. [back_demod(1745),demod(1794(5))]. 1839 (x ^ y) ^ (z v y) = x ^ y. [back_demod(1708),demod(1794(3),1794(2),1794(6))]. 1841 x ^ (y v (x ^ (x v z))) = x. [back_demod(1705),demod(1794(1),1794(1),1794(1),1794(5))]. 1883 (x v (x ^ y)) ^ (z v x) = x. [back_demod(1649),demod(1794(1),1794(1),1794(5))]. 2202 (x v (y ^ x)) ^ (z v x) = x. [back_demod(689),demod(1794(5))]. 2334 x ^ (x ^ (x v y)) = x. [para(1794(a,1),1841(a,1,2))]. 2340 x v (x ^ y) = x. [para(1883(a,1),1841(a,1,2,2)),demod(1883(4)),flip(a)]. 2341 x ^ (x ^ y) = x ^ y. [para(2340(a,1),1822(a,1,1))]. 2345 x ^ (x v y) = x. [back_demod(2334),demod(2341(3))]. 2376 x v (y ^ x) = x. [para(2202(a,1),2345(a,1)),flip(a)]. 2446 (x v y) v (z ^ y) = x v y. [para(1839(a,1),2376(a,1,2))]. 2555 x v (y ^ (x ^ z)) = x. [para(2340(a,1),2446(a,1,1)),demod(2340(5))]. 2556 $F # answer(McKenzie_1). [resolve(2555,a,7,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 7. given #163 (F,wt=9): 2555 x v (y ^ (x ^ z)) = x. [para(2340(a,1),2446(a,1,1)),demod(2340(5))]. given #164 (T,wt=9): 2558 x v (y ^ (z ^ x)) = x. [para(2376(a,1),2446(a,1,1)),demod(2376(5))]. given #165 (T,wt=9): 2571 x v ((x ^ y) ^ z) = x. [para(2336(a,1),2555(a,1,2))]. given #166 (A,wt=31): 1832 ((x v (y v z)) v ((z v (u ^ (x v (y v z)))) ^ v)) ^ (w v (x v (y v z))) = x v (y v z). [back_demod(1726),demod(1794(3),1794(6),1822(6),1794(3),1794(5),1794(11),1794(13),1794(13),1794(15))]. given #167 (F,wt=9): 2584 x v ((y ^ x) ^ z) = x. [para(2336(a,1),2558(a,1,2))]. given #168 (F,wt=11): 2448 (x v y) v (y ^ z) = x v y. [para(1871(a,1),2376(a,1,2))]. given #169 (T,wt=11): 2455 (x v y) ^ (z ^ y) = z ^ y. [para(1839(a,1),2443(a,1,2)),demod(1839(6))]. given #170 (T,wt=11): 2456 (x v y) ^ (y ^ z) = y ^ z. [para(1871(a,1),2443(a,1,2)),demod(1871(6))]. given #171 (A,wt=23): 1833 ((x v y) v ((y v (z ^ (x v y))) ^ u)) ^ (v v (x v y)) = x v y. [back_demod(1724),demod(1794(3),1794(5),1822(4),1794(2),1794(4),1794(9),1794(12))]. given #172 (F,wt=11): 2459 (x v (y v (z v u))) ^ u = u. [para(1954(a,1),2443(a,1,2)),demod(1954(8))]. given #173 (F,wt=11): 2490 (x ^ y) ^ (y v z) = x ^ y. [para(2449(a,1),1839(a,1,2))]. given #174 (T,wt=11): 2491 (x ^ y) ^ (x v z) = x ^ y. [para(2449(a,1),1871(a,1,2))]. given #175 (T,wt=11): 2493 x ^ (y v ((z v x) v u)) = x. [para(2449(a,1),1954(a,1,2,2))]. given #176 (A,wt=29): 1836 ((x v y) v ((y v (x v y)) ^ z)) ^ (u v ((v v (x v y)) ^ ((x v y) v w))) = x v y. [back_demod(1717),demod(1794(3),1794(5),1822(4),1794(2),1794(4),1794(8),1794(10),1794(15))]. given #177 (F,wt=11): 2494 x ^ ((y v (z v x)) v u) = x. [para(2449(a,1),1954(a,1,2))]. given #178 (F,wt=11): 2530 x ^ (y v ((x v z) v u)) = x. [para(2492(a,1),1839(a,1,1)),demod(2492(7))]. given #179 (T,wt=11): 2532 (x v y) ^ (x ^ z) = x ^ z. [para(2340(a,1),2495(a,1,1,1))]. given #180 (T,wt=11): 2533 (x v y) ^ (z ^ x) = z ^ x. [para(2376(a,1),2495(a,1,1,1))]. given #181 (A,wt=13): 1840 x ^ (y v ((z v x) ^ (x v u))) = x. [back_demod(1707),demod(1794(1),1794(1),1794(2),1822(2),1794(2),1794(3),1822(3),1794(6))]. given #182 (F,wt=11): 2536 (x v (y v (z v u))) ^ z = z. [para(2368(a,1),2443(a,1,2)),demod(2368(8))]. given #183 (F,wt=11): 2537 x ^ ((y v (x v z)) v u) = x. [para(2449(a,1),2368(a,1,2))]. given #184 (T,wt=11): 2559 (x v y) v (z ^ x) = x v y. [para(2449(a,1),2446(a,1,1)),demod(2449(5))]. given #185 (T,wt=11): 2579 x v (y ^ (z ^ (x ^ u))) = x. [para(2555(a,1),2446(a,1,1)),demod(2555(7))]. given #186 (A,wt=21): 1843 (x v (((x ^ y) v x) ^ z)) ^ (u v ((v v x) ^ (x v w))) = x. [back_demod(1703),demod(1794(1),1794(2),1822(2),1794(1),1794(5),1794(6),1794(10))]. given #187 (F,wt=11): 2591 x v (y ^ (z ^ (u ^ x))) = x. [para(2558(a,1),2446(a,1,1)),demod(2558(7))]. given #188 (F,wt=11): 2597 (x v y) v (x ^ z) = x v y. [para(2457(a,1),2571(a,1,2,1))]. given #189 (T,wt=11): 2604 x v (y ^ ((x ^ z) ^ u)) = x. [para(2571(a,1),2446(a,1,1)),demod(2571(7))]. given #190 (T,wt=11): 2633 x v (y ^ ((z ^ x) ^ u)) = x. [para(2584(a,1),2446(a,1,1)),demod(2584(7))]. given #191 (A,wt=31): 1845 ((x v y) v ((((x v y) ^ z) v y) ^ u)) ^ (v v ((w v (x v y)) ^ ((x v y) v v6))) = x v y. [back_demod(1701),demod(1794(3),1794(5),1822(4),1794(4),1794(9),1794(11),1794(16))]. given #192 (F,wt=11): 2637 x v ((y ^ (x ^ z)) ^ u) = x. [para(2555(a,1),2448(a,1,1)),demod(2555(7))]. given #193 (F,wt=11): 2638 x v ((y ^ (z ^ x)) ^ u) = x. [para(2558(a,1),2448(a,1,1)),demod(2558(7))]. given #194 (T,wt=11): 2639 x v (((x ^ y) ^ z) ^ u) = x. [para(2571(a,1),2448(a,1,1)),demod(2571(7))]. given #195 (T,wt=11): 2640 x v (((y ^ x) ^ z) ^ u) = x. [para(2584(a,1),2448(a,1,1)),demod(2584(7))]. given #196 (A,wt=25): 1851 ((x ^ y) v ((((x ^ y) ^ z) v (u ^ (x ^ y))) ^ v)) ^ (w v y) = x ^ y. [back_demod(1694),demod(1794(3),1794(5),1822(4),1794(4),1794(6),1794(9),1794(13))]. given #197 (F,wt=11): 2642 (x v ((y v z) v u)) ^ z = z. [para(2489(a,1),2455(a,1,2)),demod(2489(7))]. given #198 (F,wt=11): 2643 (x v ((y v z) v u)) ^ y = y. [para(2492(a,1),2455(a,1,2)),demod(2492(7))]. given #199 (T,wt=11): 2666 ((x v (y v z)) v u) ^ z = z. [para(2449(a,1),2459(a,1,1))]. given #200 (T,wt=11): 2675 x ^ (((y v x) v z) v u) = x. [para(2489(a,1),2490(a,1,1)),demod(2489(7))]. given #201 (A,wt=17): 1856 (x v (((x ^ y) v (z ^ x)) ^ u)) ^ (v v x) = x. [back_demod(1686),demod(1794(1),1794(2),1822(2),1794(1),1794(2),1794(6),1794(7),1822(7),1794(8))]. given #202 (F,wt=11): 2676 x ^ (((x v y) v z) v u) = x. [para(2492(a,1),2490(a,1,1)),demod(2492(7))]. given #203 (F,wt=11): 2741 ((x v (y v z)) v u) ^ y = y. [para(2458(a,1),2532(a,1,2)),demod(2458(7))]. given #204 (T,wt=11): 2742 (((x v y) v z) v u) ^ y = y. [para(2495(a,1),2532(a,1,2)),demod(2495(7))]. given #205 (T,wt=11): 2743 (((x v y) v z) v u) ^ x = x. [para(2496(a,1),2532(a,1,2)),demod(2496(7))]. given #206 (A,wt=29): 1873 (x v (((((x ^ y) v (z ^ x)) ^ u) v (v ^ x)) ^ w)) ^ (v6 v ((v7 v x) ^ (x v v8))) = x. [back_demod(1661),demod(1794(1),1794(2),1822(2),1794(1),1794(1),1794(2),1794(5),1794(9),1794(10),1794(14))]. given #207 (F,wt=11): 2751 x ^ ((y v x) ^ (x v z)) = x. [para(1794(a,1),1840(a,1,2))]. ============================== PROOF ================================= % Proof 3 at 2.40 (+ 0.03) seconds: McKenzie_4. % Length of proof is 57. % Level of proof is 29. % Maximum clause weight is 89. % Given clauses 207. 6 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [input]. 10 ((c10 v c11) ^ (c11 v c12)) ^ c11 != c11 # answer(McKenzie_4). [clausify]. 11 (((x v ((y v z) ^ (z v u))) ^ ((y v z) ^ (z v u))) v ((z v (v ^ ((y v z) ^ (z v u)))) ^ w)) ^ (v6 v ((v7 v ((y v z) ^ (z v u))) ^ (((y v z) ^ (z v u)) v v8))) = (y v z) ^ (z v u). [para(6(a,1),6(a,1,1,2,1,1))]. 13 (((x v y) ^ y) v (y v y)) ^ (z v ((u v y) ^ (y v v))) = y. [para(6(a,1),6(a,1,1,2))]. 14 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v (((w ^ ((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v))) v (v6 ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v7)) ^ (v8 v z) = ((y ^ (z v z)) v (u ^ z)) ^ v. [para(6(a,1),6(a,1,2,2))]. 17 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (z v y) = y v y. [para(13(a,1),13(a,1,2,2))]. 18 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v ((w v y) ^ (y v v6))) = y. [para(17(a,1),6(a,1,1,2,1,1))]. 24 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (z ^ (y v y))) ^ u)) ^ (v v y) = y v y. [para(13(a,1),18(a,1,2,2))]. 28 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (y v y)) ^ z)) ^ (u v y) = y v y. [para(17(a,1),24(a,1,1,2,1,2))]. 30 (((x v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v))) ^ ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v))) v u) ^ (w v ((v6 v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v))) ^ (((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v)) v v7))) = (y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v). [para(6(a,1),11(a,1,1,2))]. 34 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) ^ (v6 v ((v7 v y) ^ (y v v8))) = y. [para(18(a,1),11(a,1,1,1,1,2)),demod(18(17),18(22),18(26),18(27),18(31))]. 44 (((x v y) ^ y) v (z ^ y)) ^ (u v ((v v y) ^ (y v w))) = y. [para(6(a,1),34(a,1,1,2))]. 57 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(13(a,1),44(a,1,2,2))]. 67 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (v v z) = y ^ z. [para(44(a,1),44(a,1,2,2))]. 69 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(17(a,1),57(a,1,1,2))]. 80 ((x v x) v ((x v x) v (x v x))) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [para(69(a,1),13(a,1,1,1))]. 92 ((x v x) v (y ^ (x v x))) ^ (z v x) = x v x. [para(69(a,1),57(a,1,1,1))]. 94 ((x v x) v (x v x)) ^ (y v x) = x v x. [para(69(a,1),69(a,1,1,1))]. 103 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(14(a,1),92(a,1,1,2))]. 112 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(67(a,1),57(a,1,1,2))]. 148 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(67(a,1),103(a,1,1,2,1,1))]. 171 ((x v x) v x) ^ (y v x) = x v x. [para(6(a,1),148(a,1,1,2))]. 185 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(171(a,1),6(a,1,2,2))]. 605 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(67(a,1),185(a,1,1,2,1,1))]. 624 (((x v y) ^ y) v y) ^ (z v (y v y)) = y. [para(6(a,1),605(a,1,1,2))]. 652 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(624(a,1),13(a,1,2,2))]. 657 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(624(a,1),44(a,1,2,2))]. 670 (x v ((((x v x) v (x v x)) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [para(652(a,1),24(a,1,1,1))]. 672 (x v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (z v x) = x v x. [para(652(a,1),28(a,1,1,1))]. 682 (x v (x v x)) ^ (y v x) = x v x. [para(652(a,1),69(a,1,1,1))]. 683 (x v x) v (x v x) = x v x. [para(69(a,1),652(a,1,1,1)),demod(682(8))]. 689 (x v (y ^ x)) ^ (z v x) = x v x. [para(652(a,1),112(a,1,1,1))]. 746 (x v ((x v x) ^ y)) ^ (z v x) = x v x. [back_demod(672),demod(683(3),683(3))]. 748 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [back_demod(670),demod(683(3))]. 792 (x v x) ^ (y v x) = x v x. [back_demod(94),demod(683(3))]. 797 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_demod(80),demod(683(4),683(3))]. 1016 ((x v x) v ((x v x) ^ y)) ^ (z v (x v x)) = x v x. [para(683(a,1),746(a,1,1,2,1)),demod(683(10))]. 1454 ((((x v y) ^ y) v ((x v y) ^ y)) v y) ^ (z v (((x v y) ^ y) v ((x v y) ^ y))) = ((x v y) ^ y) v ((x v y) ^ y). [para(44(a,1),1016(a,1,1,2))]. 1649 (x v (((x v x) v x) ^ y)) ^ (z v x) = x v x. [para(652(a,1),748(a,1,1,2,1,2))]. 1705 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(683(a,1),797(a,1,2,2,1))]. 1707 (x v x) ^ (y v ((z v ((u v (x v x)) ^ (x v x))) ^ (((u v (x v x)) ^ (x v x)) v v))) = x v x. [para(30(a,1),797(a,1,2,2))]. 1745 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(44(a,1),1705(a,1,2,2)),demod(657(7)),flip(a)]. 1794 x v x = x. [back_demod(1454),demod(1745(5),1745(6),792(3),1745(6))]. 1822 (x v y) ^ y = y. [back_demod(1745),demod(1794(5))]. 1840 x ^ (y v ((z v x) ^ (x v u))) = x. [back_demod(1707),demod(1794(1),1794(1),1794(2),1822(2),1794(2),1794(3),1822(3),1794(6))]. 1841 x ^ (y v (x ^ (x v z))) = x. [back_demod(1705),demod(1794(1),1794(1),1794(1),1794(5))]. 1883 (x v (x ^ y)) ^ (z v x) = x. [back_demod(1649),demod(1794(1),1794(1),1794(5))]. 2202 (x v (y ^ x)) ^ (z v x) = x. [back_demod(689),demod(1794(5))]. 2334 x ^ (x ^ (x v y)) = x. [para(1794(a,1),1841(a,1,2))]. 2340 x v (x ^ y) = x. [para(1883(a,1),1841(a,1,2,2)),demod(1883(4)),flip(a)]. 2341 x ^ (x ^ y) = x ^ y. [para(2340(a,1),1822(a,1,1))]. 2345 x ^ (x v y) = x. [back_demod(2334),demod(2341(3))]. 2376 x v (y ^ x) = x. [para(2202(a,1),2345(a,1)),flip(a)]. 2443 x ^ (y ^ x) = y ^ x. [para(2376(a,1),1822(a,1,1))]. 2751 x ^ ((y v x) ^ (x v z)) = x. [para(1794(a,1),1840(a,1,2))]. 3223 ((x v y) ^ (y v z)) ^ y = y. [para(2751(a,1),2443(a,1,2)),demod(2751(8))]. 3224 $F # answer(McKenzie_4). [resolve(3223,a,10,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 10. given #208 (F,wt=11): 2824 x v (((x ^ y) v x) ^ z) = x. [para(1843(a,1),2345(a,1)),flip(a)]. given #209 (T,wt=9): 3252 x v ((x ^ y) v x) = x. [para(1757(a,1),2824(a,1,2))]. given #210 (T,wt=7): 3292 (x ^ y) v x = x. [para(3252(a,1),1757(a,1,2)),demod(1822(3)),flip(a)]. given #211 (A,wt=33): 1874 ((x ^ y) v (((((z ^ (x ^ y)) v (u ^ (x ^ y))) ^ v) v (w ^ (x ^ y))) ^ v6)) ^ (v7 v x) = x ^ y. [back_demod(1658),demod(1794(1),1794(1),1794(3),1794(3),1822(4),1794(2),1794(2),1794(3),1794(3),1794(4),1794(4),1794(4),1794(8),1794(8),1794(13),1794(15),1794(15))]. given #212 (F,wt=7): 3313 (x ^ y) v y = y. [para(2443(a,1),3292(a,1,1))]. given #213 (F,wt=9): 3312 x v (y v x) = y v x. [para(1822(a,1),3292(a,1,1))]. given #214 (T,wt=9): 3314 x v (x v y) = x v y. [para(2457(a,1),3292(a,1,1))]. given #215 (T,wt=9): 3368 (x ^ (y ^ z)) v y = y. [para(2555(a,1),3312(a,1,2)),demod(2555(6))]. given #216 (A,wt=13): 1875 (x ^ y) ^ (z v (u v x)) = x ^ y. [back_demod(1657),demod(1794(1),1794(1),1794(3),1794(3),1822(4),1794(2),1794(2),1794(3),1794(3),1794(4),1794(3),1794(2),1794(5),1794(5))]. given #217 (F,wt=9): 3369 (x ^ (y ^ z)) v z = z. [para(2558(a,1),3312(a,1,2)),demod(2558(6))]. given #218 (F,wt=9): 3370 ((x ^ y) ^ z) v x = x. [para(2571(a,1),3312(a,1,2)),demod(2571(6))]. given #219 (T,wt=9): 3371 ((x ^ y) ^ z) v y = y. [para(2584(a,1),3312(a,1,2)),demod(2584(6))]. given #220 (T,wt=11): 3223 ((x v y) ^ (y v z)) ^ y = y. [para(2751(a,1),2443(a,1,2)),demod(2751(8))]. given #221 (A,wt=33): 1878 ((x v y) v (((z ^ (x v y)) v (y ^ u)) ^ v)) ^ (w v ((v6 v (x v y)) ^ ((x v y) v v7))) = x v y. [back_demod(1654),demod(1794(1),1794(3),1822(4),1794(2),1794(3),1794(4),1794(4),1794(4),1794(8),1794(10),1794(15))]. given #222 (F,wt=11): 3225 x ^ ((x v y) ^ (x v z)) = x. [para(2449(a,1),2751(a,1,2,1))]. given #223 (F,wt=11): 3319 (x ^ y) v (z v y) = z v y. [para(2455(a,1),3292(a,1,1))]. given #224 (T,wt=11): 3320 (x ^ y) v (z v x) = z v x. [para(2456(a,1),3292(a,1,1))]. given #225 (T,wt=11): 3322 (x ^ y) v (x v z) = x v z. [para(2532(a,1),3292(a,1,1))]. given #226 (A,wt=49): 1882 (((x v y) ^ (y v z)) v ((((x v y) ^ (y v z)) v ((y v (u ^ ((x v y) ^ (y v z)))) ^ v)) ^ w)) ^ (v6 v ((x v y) ^ (y v z))) = (x v y) ^ (y v z). [back_demod(1650),demod(1794(10),1794(27))]. given #227 (F,wt=11): 3323 (x ^ y) v (y v z) = y v z. [para(2533(a,1),3292(a,1,1))]. given #228 (F,wt=11): 3373 (x ^ (y ^ (z ^ u))) v z = z. [para(2579(a,1),3312(a,1,2)),demod(2579(8))]. given #229 (T,wt=11): 3374 (x ^ (y ^ (z ^ u))) v u = u. [para(2591(a,1),3312(a,1,2)),demod(2591(8))]. given #230 (T,wt=11): 3375 (x ^ ((y ^ z) ^ u)) v y = y. [para(2604(a,1),3312(a,1,2)),demod(2604(8))]. given #231 (A,wt=21): 1886 (x v ((x v (((y ^ x) v (z ^ x)) ^ u)) ^ v)) ^ (w v x) = x. [back_demod(1646),demod(1794(1),1794(1),1794(10))]. given #232 (F,wt=11): 3376 (x ^ ((y ^ z) ^ u)) v z = z. [para(2633(a,1),3312(a,1,2)),demod(2633(8))]. given #233 (F,wt=11): 3377 ((x ^ (y ^ z)) ^ u) v y = y. [para(2637(a,1),3312(a,1,2)),demod(2637(8))]. given #234 (T,wt=11): 3378 ((x ^ (y ^ z)) ^ u) v z = z. [para(2638(a,1),3312(a,1,2)),demod(2638(8))]. given #235 (T,wt=11): 3379 (((x ^ y) ^ z) ^ u) v x = x. [para(2639(a,1),3312(a,1,2)),demod(2639(8))]. given #236 (A,wt=23): 1890 (((x ^ y) v (z ^ x)) ^ u) ^ (v v x) = ((x ^ y) v (z ^ x)) ^ u. [back_demod(1642),demod(1794(1),1794(1),1794(2),1794(6),1794(6),1794(7),1822(10),1794(5),1794(5),1794(6),1794(9),1794(9),1794(10),1794(13),1794(9),1794(5),1794(7),1794(7),1794(8))]. given #237 (F,wt=11): 3380 (((x ^ y) ^ z) ^ u) v y = y. [para(2640(a,1),3312(a,1,2)),demod(2640(8))]. given #238 (F,wt=11): 3381 x ^ ((y v x) ^ (z v x)) = x. [para(3312(a,1),2751(a,1,2,2))]. given #239 (T,wt=11): 3449 ((x v y) ^ (x v z)) ^ x = x. [para(2449(a,1),3223(a,1,1,1))]. given #240 (T,wt=11): 3468 ((x v y) ^ (z v y)) ^ y = y. [para(3312(a,1),3223(a,1,1,2))]. given #241 (A,wt=57): 1907 ((x v ((y v z) ^ (z v u))) v (((x v ((y v z) ^ (z v u))) v ((z v (v ^ ((y v z) ^ (z v u)))) ^ w)) ^ v6)) ^ (v7 v (x v ((y v z) ^ (z v u)))) = x v ((y v z) ^ (z v u)). [back_demod(1610),demod(1822(10),1794(26))]. given #242 (F,wt=11): 3549 x ^ ((x v y) ^ (z v x)) = x. [para(3312(a,1),3225(a,1,2,2))]. given #243 (F,wt=11): 3939 ((x v y) ^ (z v x)) ^ x = x. [para(3312(a,1),3449(a,1,1,2))]. given #244 (T,wt=13): 2004 (x ^ y) ^ (z v (u v y)) = x ^ y. [back_demod(1405),demod(1822(4),1794(3),1794(4))]. given #245 (T,wt=13): 2067 x ^ (y v (z v (u v (v v x)))) = x. [back_demod(1271),demod(1822(2),1794(1),1794(1))]. given #246 (A,wt=29): 1918 ((x v y) v (((x v y) v (((z ^ y) v (u ^ y)) ^ v)) ^ w)) ^ (v6 v (x v y)) = x v y. [back_demod(1593),demod(1822(4),1794(3),1794(12))]. given #247 (F,wt=13): 2343 (x ^ (y ^ z)) ^ y = x ^ (y ^ z). [para(2340(a,1),1839(a,1,2))]. given #248 (F,wt=13): 2344 ((x ^ y) ^ z) ^ x = (x ^ y) ^ z. [para(2340(a,1),1871(a,1,2))]. given #249 (T,wt=13): 2444 (x v (y v z)) v z = x v (y v z). [para(1842(a,1),2376(a,1,2))]. given #250 (T,wt=13): 2445 (x ^ (y ^ z)) ^ z = x ^ (y ^ z). [para(2376(a,1),1839(a,1,2))]. given #251 (A,wt=49): 1942 ((x v ((y v z) ^ (z v u))) v ((z v (v ^ ((y v z) ^ (z v u)))) ^ w)) ^ (v6 v (v7 v (v8 v (x v ((y v z) ^ (z v u)))))) = x v ((y v z) ^ (z v u)). [back_demod(1541),demod(1794(20),1794(28))]. given #252 (F,wt=13): 2447 ((x ^ y) ^ z) ^ y = (x ^ y) ^ z. [para(2376(a,1),1871(a,1,2))]. given #253 (F,wt=13): 2450 (x v (y v z)) v y = x v (y v z). [para(2362(a,1),2376(a,1,2))]. given #254 (T,wt=13): 2497 ((x v y) v z) v y = (x v y) v z. [para(2489(a,1),2376(a,1,2))]. given #255 (T,wt=13): 2531 ((x v y) v z) v x = (x v y) v z. [para(2492(a,1),2376(a,1,2))]. given #256 (A,wt=27): 1946 ((x v y) v (((z ^ y) v (u ^ y)) ^ v)) ^ (w v (v6 v (v7 v (x v y)))) = x v y. [back_demod(1535),demod(1794(2),1794(9),1794(14))]. given #257 (F,wt=13): 2534 x ^ (y v (z v (u v (x v v)))) = x. [para(2368(a,1),1839(a,1,1)),demod(2368(9))]. given #258 (F,wt=13): 2560 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(2446(a,1),2454(a,1,1,2))]. given #259 (T,wt=13): 2561 (x ^ y) ^ ((z v y) v u) = x ^ y. [para(2446(a,1),2489(a,1,2,1))]. given #260 (T,wt=13): 2564 ((x v y) v z) ^ (u ^ y) = u ^ y. [para(2446(a,1),2495(a,1,1,1))]. given #261 (A,wt=43): 1951 (((x v y) ^ (y v z)) v ((y v (u ^ ((x v y) ^ (y v z)))) ^ v)) ^ (w v (v6 v (v7 v ((x v y) ^ (y v z))))) = (x v y) ^ (y v z). [back_demod(1523),demod(1794(17),1794(24))]. given #262 (F,wt=13): 2566 (x v y) v (z ^ (u ^ y)) = x v y. [para(2446(a,1),2446(a,1,1)),demod(2446(7))]. given #263 (F,wt=13): 2567 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(2555(a,1),1822(a,1,1))]. given #264 (T,wt=13): 2580 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(2558(a,1),1822(a,1,1))]. given #265 (T,wt=13): 2583 (x v y) v (z ^ (y ^ u)) = x v y. [para(1871(a,1),2558(a,1,2,2))]. given #266 (A,wt=21): 1957 (x v (((y ^ x) v (z ^ x)) ^ u)) ^ (v v (w v (v6 v x))) = x. [back_demod(1514),demod(1794(1),1794(6),1794(10))]. given #267 (F,wt=13): 2592 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(2571(a,1),1822(a,1,1))]. given #268 (F,wt=13): 2622 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(2584(a,1),1822(a,1,1))]. given #269 (T,wt=13): 2624 (x v y) v ((z ^ y) ^ u) = x v y. [para(1839(a,1),2584(a,1,2,1))]. given #270 (T,wt=13): 2626 (x v y) v ((y ^ z) ^ u) = x v y. [para(1871(a,1),2584(a,1,2,1))]. given #271 (A,wt=39): 1961 ((x v y) v (((((z ^ (x v y)) v (u ^ (x v y))) ^ v) v y) ^ w)) ^ (v6 v ((v7 v (x v y)) ^ ((x v y) v v8))) = x v y. [back_demod(1495),demod(1794(3),1794(5),1822(4),1794(4),1794(6),1794(13),1794(15),1794(20))]. given #272 (F,wt=13): 2634 (x v (y v z)) ^ (z ^ u) = z ^ u. [para(2448(a,1),2454(a,1,1,2))]. given #273 (F,wt=13): 2635 (x ^ y) ^ ((z v x) v u) = x ^ y. [para(2448(a,1),2489(a,1,2,1))]. given #274 (T,wt=13): 2636 ((x v y) v z) ^ (y ^ u) = y ^ u. [para(2448(a,1),2495(a,1,1,1))]. given #275 (T,wt=13): 2641 (x v (y v (z v (u v v)))) ^ v = v. [para(1954(a,1),2455(a,1,2)),demod(1954(9))]. given #276 (A,wt=39): 1962 ((x v y) v (((((z ^ (x v y)) v y) ^ u) v (v ^ (x v y))) ^ w)) ^ (v6 v ((v7 v (x v y)) ^ ((x v y) v v8))) = x v y. [back_demod(1494),demod(1794(3),1794(5),1822(4),1794(4),1794(8),1794(13),1794(15),1794(20))]. given #277 (F,wt=13): 2644 (x v (y v (z v (u v v)))) ^ u = u. [para(2368(a,1),2455(a,1,2)),demod(2368(9))]. given #278 (F,wt=13): 2673 (x ^ y) ^ (z v (y v u)) = x ^ y. [para(2490(a,1),1839(a,1,1)),demod(2490(7))]. given #279 (T,wt=13): 2674 x ^ ((y v (z v (u v x))) v v) = x. [para(1954(a,1),2490(a,1,1)),demod(1954(9))]. given #280 (T,wt=13): 2677 x ^ ((y v (z v (x v u))) v v) = x. [para(2368(a,1),2490(a,1,1)),demod(2368(9))]. given #281 (A,wt=23): 1964 ((x v y) v (((z ^ (x v y)) v y) ^ u)) ^ (v v (x v y)) = x v y. [back_demod(1492),demod(1794(3),1794(5),1822(4),1794(4),1794(9),1794(12))]. given #282 (F,wt=13): 2678 (x v y) v (z ^ (u ^ x)) = x v y. [para(2490(a,1),2558(a,1,2,2))]. given #283 (F,wt=13): 2679 (x v y) v ((z ^ x) ^ u) = x v y. [para(2490(a,1),2584(a,1,2,1))]. given #284 (T,wt=13): 2680 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(2490(a,1),2455(a,1,2)),demod(2490(7))]. given #285 (T,wt=13): 2681 (x ^ y) ^ ((y v z) v u) = x ^ y. [para(2490(a,1),2490(a,1,1)),demod(2490(7))]. given #286 (A,wt=25): 1969 (((x ^ (y v z)) v z) ^ u) ^ (v v (y v z)) = ((x ^ (y v z)) v z) ^ u. [back_demod(1486),demod(1794(3),1794(8),1822(10),1794(7),1794(11),1794(13),1794(9),1794(7),1794(10))]. given #287 (F,wt=13): 2682 (x ^ y) ^ (z v (x v u)) = x ^ y. [para(2491(a,1),1839(a,1,1)),demod(2491(7))]. given #288 (F,wt=13): 2683 (x v y) v (z ^ (x ^ u)) = x v y. [para(2491(a,1),2558(a,1,2,2))]. given #289 (T,wt=13): 2684 (x v y) v ((x ^ z) ^ u) = x v y. [para(2491(a,1),2584(a,1,2,1))]. given #290 (T,wt=13): 2685 (x v (y v z)) ^ (y ^ u) = y ^ u. [para(2491(a,1),2455(a,1,2)),demod(2491(7))]. given #291 (A,wt=51): 1991 ((x v y) v (((((x v y) v (((((z ^ y) v (u ^ y)) ^ v) v (w ^ y)) ^ v6)) ^ v7) v (v8 ^ (x v y))) ^ v9)) ^ (v10 v ((v11 v (x v y)) ^ ((x v y) v v12))) = x v y. [back_demod(1429),demod(1822(4),1794(4),1794(3))]. given #292 (F,wt=13): 2686 (x ^ y) ^ ((x v z) v u) = x ^ y. [para(2491(a,1),2490(a,1,1)),demod(2491(7))]. given #293 (F,wt=13): 2687 x ^ (y v (z v ((u v x) v v))) = x. [para(2493(a,1),1839(a,1,1)),demod(2493(9))]. given #294 (T,wt=13): 2697 (x v (y v ((z v u) v v))) ^ u = u. [para(2493(a,1),2455(a,1,2)),demod(2493(9))]. given #295 (T,wt=13): 2698 x ^ ((y v ((z v x) v u)) v v) = x. [para(2493(a,1),2490(a,1,1)),demod(2493(9))]. given #296 (A,wt=35): 2003 (((((x ^ y) v (z ^ y)) ^ u) v (v ^ y)) ^ w) ^ (v6 v y) = ((((x ^ y) v (z ^ y)) ^ u) v (v ^ y)) ^ w. [back_demod(1408),demod(1794(1),1794(9),1822(16),1794(8),1794(15),1794(10))]. given #297 (F,wt=13): 2722 x ^ (y v ((z v (u v x)) v v)) = x. [para(2494(a,1),1839(a,1,1)),demod(2494(9))]. given #298 (F,wt=13): 2733 (x v ((y v (z v u)) v v)) ^ u = u. [para(2494(a,1),2455(a,1,2)),demod(2494(9))]. given #299 (T,wt=13): 2734 x ^ (((y v (z v x)) v u) v v) = x. [para(2494(a,1),2490(a,1,1)),demod(2494(9))]. given #300 (T,wt=13): 2735 x ^ (y v (z v ((x v u) v v))) = x. [para(2530(a,1),1839(a,1,1)),demod(2530(9))]. given #301 (A,wt=23): 2005 (((x ^ y) v (z ^ y)) ^ u) ^ (v v y) = ((x ^ y) v (z ^ y)) ^ u. [back_demod(1402),demod(1822(10),1794(9),1794(5))]. given #302 (F,wt=13): 2739 (x v (y v ((z v u) v v))) ^ z = z. [para(2530(a,1),2455(a,1,2)),demod(2530(9))]. given #303 (F,wt=13): 2740 x ^ ((y v ((x v z) v u)) v v) = x. [para(2530(a,1),2490(a,1,1)),demod(2530(9))]. given #304 (T,wt=13): 2744 ((x v (y v (z v u))) v v) ^ u = u. [para(2459(a,1),2532(a,1,2)),demod(2459(9))]. given #305 (T,wt=13): 2745 ((x v y) v z) ^ (x ^ u) = x ^ u. [para(2532(a,1),2532(a,1,2)),demod(2532(7))]. given #306 (A,wt=53): 2006 (((x v y) ^ (y v z)) v ((((y v (u ^ ((x v y) ^ (y v z)))) ^ v) v (w ^ ((x v y) ^ (y v z)))) ^ v6)) ^ (v7 v (v8 v ((x v y) ^ (y v z)))) = (x v y) ^ (y v z). [back_demod(1393),demod(1822(8),1794(25))]. given #307 (F,wt=13): 2746 ((x v (y v (z v u))) v v) ^ z = z. [para(2368(a,1),2533(a,1,2)),demod(2368(9))]. given #308 (F,wt=13): 2747 ((x v y) v z) ^ (u ^ x) = u ^ x. [para(2490(a,1),2533(a,1,2)),demod(2490(7))]. given #309 (T,wt=13): 2748 ((x v ((y v z) v u)) v v) ^ z = z. [para(2493(a,1),2533(a,1,2)),demod(2493(9))]. given #310 (T,wt=13): 2749 (((x v (y v z)) v u) v v) ^ z = z. [para(2494(a,1),2533(a,1,2)),demod(2494(9))]. given #311 (A,wt=25): 2008 (x v (((((y ^ x) v (z ^ x)) ^ u) v (v ^ x)) ^ w)) ^ (v6 v (v7 v x)) = x. [back_demod(1390),demod(1822(2),1794(1),1794(11))]. given #312 (F,wt=13): 2750 ((x v ((y v z) v u)) v v) ^ y = y. [para(2530(a,1),2533(a,1,2)),demod(2530(9))]. given #313 (F,wt=13): 2755 (x v ((y v z) ^ (z v u))) ^ z = z. [para(1840(a,1),2443(a,1,2)),demod(1840(10))]. given #314 (T,wt=13): 2756 x ^ (y v ((x v z) ^ (x v u))) = x. [para(2449(a,1),1840(a,1,2,2,1))]. given #315 (T,wt=13): 2757 x ^ (((y v x) ^ (x v z)) v u) = x. [para(2449(a,1),1840(a,1,2))]. given #316 (A,wt=49): 2011 ((x v ((y v z) ^ (z v u))) v (((v ^ (x v ((y v z) ^ (z v u)))) v z) ^ w)) ^ (v6 v (v7 v (x v ((y v z) ^ (z v u))))) = x v ((y v z) ^ (z v u)). [back_demod(1386),demod(1822(10),1794(13),1794(23))]. given #317 (F,wt=13): 2771 x ^ (y v ((z v (x v u)) v v)) = x. [para(2537(a,1),1839(a,1,1)),demod(2537(9))]. given #318 (F,wt=13): 2776 (x v ((y v (z v u)) v v)) ^ z = z. [para(2537(a,1),2455(a,1,2)),demod(2537(9))]. given #319 (T,wt=13): 2777 x ^ (((y v (x v z)) v u) v v) = x. [para(2537(a,1),2490(a,1,1)),demod(2537(9))]. given #320 (T,wt=13): 2778 (((x v (y v z)) v u) v v) ^ y = y. [para(2537(a,1),2533(a,1,2)),demod(2537(9))]. given #321 (A,wt=35): 2023 (((x v y) ^ (y v z)) v (((u ^ ((x v y) ^ (y v z))) v y) ^ v)) ^ (w v (y v z)) = (x v y) ^ (y v z). [back_demod(1365),demod(1794(7),1794(11),1822(8),1794(10),1794(13),1794(20))]. given #322 (F,wt=13): 2804 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(2579(a,1),2446(a,1,1)),demod(2579(9))]. given #323 (F,wt=13): 2805 x v ((y ^ (z ^ (x ^ u))) ^ v) = x. [para(2579(a,1),2448(a,1,1)),demod(2579(9))]. given #324 (T,wt=13): 2841 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(2591(a,1),2446(a,1,1)),demod(2591(9))]. given #325 (T,wt=13): 2842 x v ((y ^ (z ^ (u ^ x))) ^ v) = x. [para(2591(a,1),2448(a,1,1)),demod(2591(9))]. given #326 (A,wt=33): 2024 ((x v y) v (((z ^ (x v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v (x v y)) ^ ((x v y) v v7))) = x v y. [back_demod(1364),demod(1794(1),1794(3),1822(4),1794(2),1794(3),1794(4),1794(6),1794(8),1794(10),1794(15))]. given #327 (F,wt=13): 2870 x v (y ^ (z ^ ((x ^ u) ^ v))) = x. [para(2604(a,1),2446(a,1,1)),demod(2604(9))]. given #328 (F,wt=13): 2871 x v ((y ^ ((x ^ z) ^ u)) ^ v) = x. [para(2604(a,1),2448(a,1,1)),demod(2604(9))]. given #329 (T,wt=13): 2891 x v (y ^ (z ^ ((u ^ x) ^ v))) = x. [para(2633(a,1),2446(a,1,1)),demod(2633(9))]. given #330 (T,wt=13): 2892 x v ((y ^ ((z ^ x) ^ u)) ^ v) = x. [para(2633(a,1),2448(a,1,1)),demod(2633(9))]. given #331 (A,wt=63): 2031 ((x v (y v (z v u))) v ((((u v (v ^ (x v (y v (z v u))))) ^ w) v (v6 ^ (x v (y v (z v u))))) ^ v7)) ^ (v8 v ((v9 v (x v (y v (z v u)))) ^ ((x v (y v (z v u))) v v10))) = x v (y v (z v u)). [back_demod(1349),demod(1794(1),1794(5),1822(8),1794(4),1794(4),1794(10),1794(17),1794(21),1794(28))]. given #332 (F,wt=13): 2941 x v (y ^ ((z ^ (x ^ u)) ^ v)) = x. [para(2637(a,1),2446(a,1,1)),demod(2637(9))]. given #333 (F,wt=13): 2942 x v (((y ^ (x ^ z)) ^ u) ^ v) = x. [para(2637(a,1),2448(a,1,1)),demod(2637(9))]. given #334 (T,wt=13): 2962 x v (y ^ ((z ^ (u ^ x)) ^ v)) = x. [para(2638(a,1),2446(a,1,1)),demod(2638(9))]. given #335 (T,wt=13): 2963 x v (((y ^ (z ^ x)) ^ u) ^ v) = x. [para(2638(a,1),2448(a,1,1)),demod(2638(9))]. given #336 (A,wt=47): 2032 ((x v (y v (z v (u v v)))) v (((w ^ (x v (y v (z v (u v v))))) v v) ^ v6)) ^ (v7 v (x v (y v (z v (u v v))))) = x v (y v (z v (u v v))). [back_demod(1348),demod(1794(1),1794(6),1822(10),1794(5),1794(10),1794(13),1794(17),1794(21),1794(19))]. given #337 (F,wt=13): 2986 x v (y ^ (((x ^ z) ^ u) ^ v)) = x. [para(2639(a,1),2446(a,1,1)),demod(2639(9))]. given #338 (F,wt=13): 2987 x v ((((x ^ y) ^ z) ^ u) ^ v) = x. [para(2639(a,1),2448(a,1,1)),demod(2639(9))]. given #339 (T,wt=13): 3007 x v (y ^ (((z ^ x) ^ u) ^ v)) = x. [para(2640(a,1),2446(a,1,1)),demod(2640(9))]. given #340 (T,wt=13): 3008 x v ((((y ^ x) ^ z) ^ u) ^ v) = x. [para(2640(a,1),2448(a,1,1)),demod(2640(9))]. given #341 (A,wt=47): 2033 ((x v (y v (z v (u v v)))) v ((v v (w ^ (x v (y v (z v (u v v)))))) ^ v6)) ^ (v7 v (x v (y v (z v (u v v))))) = x v (y v (z v (u v v))). [back_demod(1347),demod(1794(1),1794(6),1822(10),1794(5),1794(5),1794(13),1794(17),1794(21),1794(19))]. given #342 (F,wt=13): 3070 x ^ (y v (((z v x) v u) v v)) = x. [para(2675(a,1),1839(a,1,1)),demod(2675(9))]. given #343 (F,wt=13): 3080 (x v (((y v z) v u) v v)) ^ z = z. [para(2675(a,1),2455(a,1,2)),demod(2675(9))]. given #344 (T,wt=13): 3081 x ^ ((((y v x) v z) v u) v v) = x. [para(2675(a,1),2490(a,1,1)),demod(2675(9))]. given #345 (T,wt=13): 3082 ((((x v y) v z) v u) v v) ^ y = y. [para(2675(a,1),2533(a,1,2)),demod(2675(9))]. given #346 (A,wt=15): 2037 x ^ (y v (z v (u v (v v (w v x))))) = x. [back_demod(1340),demod(1794(1),1794(2),1822(2),1794(1),1794(1),1794(1),1794(7))]. given #347 (F,wt=13): 3102 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(1856(a,1),2345(a,1)),flip(a)]. given #348 (F,wt=11): 9078 x v ((x ^ y) v (z ^ x)) = x. [para(1757(a,1),3102(a,1,2))]. given #349 (T,wt=11): 9236 x v ((x ^ y) v (x ^ z)) = x. [para(2336(a,1),9078(a,1,2,2))]. given #350 (T,wt=11): 9241 x v ((y ^ x) v (z ^ x)) = x. [para(2443(a,1),9078(a,1,2,1))]. given #351 (A,wt=41): 2047 (x v (((((((((y ^ x) v (z ^ x)) ^ u) v (v ^ x)) ^ w) v (v6 ^ x)) ^ v7) v (v8 ^ x)) ^ v9)) ^ (v10 v ((v11 v x) ^ (x v v12))) = x. [back_demod(1318),demod(1822(2),1794(1))]. given #352 (F,wt=11): 9285 ((x ^ y) v (z ^ x)) v x = x. [para(9078(a,1),3312(a,1,2)),demod(9078(8))]. given #353 (F,wt=11): 9396 x v ((y ^ x) v (x ^ z)) = x. [para(2443(a,1),9236(a,1,2,1))]. ============================== PROOF ================================= % Proof 4 at 4.31 (+ 0.06) seconds: McKenzie_3. % Length of proof is 75. % Level of proof is 31. % Maximum clause weight is 89. % Given clauses 353. 6 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [input]. 9 ((c7 ^ c8) v (c8 ^ c9)) v c8 != c8 # answer(McKenzie_3). [clausify]. 11 (((x v ((y v z) ^ (z v u))) ^ ((y v z) ^ (z v u))) v ((z v (v ^ ((y v z) ^ (z v u)))) ^ w)) ^ (v6 v ((v7 v ((y v z) ^ (z v u))) ^ (((y v z) ^ (z v u)) v v8))) = (y v z) ^ (z v u). [para(6(a,1),6(a,1,1,2,1,1))]. 13 (((x v y) ^ y) v (y v y)) ^ (z v ((u v y) ^ (y v v))) = y. [para(6(a,1),6(a,1,1,2))]. 14 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v (((w ^ ((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v))) v (v6 ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v7)) ^ (v8 v z) = ((y ^ (z v z)) v (u ^ z)) ^ v. [para(6(a,1),6(a,1,2,2))]. 17 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (z v y) = y v y. [para(13(a,1),13(a,1,2,2))]. 18 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v ((w v y) ^ (y v v6))) = y. [para(17(a,1),6(a,1,1,2,1,1))]. 24 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (z ^ (y v y))) ^ u)) ^ (v v y) = y v y. [para(13(a,1),18(a,1,2,2))]. 28 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (y v y)) ^ z)) ^ (u v y) = y v y. [para(17(a,1),24(a,1,1,2,1,2))]. 30 (((x v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v))) ^ ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v))) v u) ^ (w v ((v6 v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v))) ^ (((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v)) v v7))) = (y v ((z v u) ^ u)) ^ (((z v u) ^ u) v v). [para(6(a,1),11(a,1,1,2))]. 34 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) ^ (v6 v ((v7 v y) ^ (y v v8))) = y. [para(18(a,1),11(a,1,1,1,1,2)),demod(18(17),18(22),18(26),18(27),18(31))]. 44 (((x v y) ^ y) v (z ^ y)) ^ (u v ((v v y) ^ (y v w))) = y. [para(6(a,1),34(a,1,1,2))]. 48 (((x v (y v z)) ^ (y v z)) v ((((((y v z) v (y v z)) v (z v z)) ^ u) v (v ^ (y v z))) ^ w)) ^ (v6 v ((v7 v (y v z)) ^ ((y v z) v v8))) = y v z. [para(17(a,1),34(a,1,1,2,1,1,1,2))]. 57 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(13(a,1),44(a,1,2,2))]. 67 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (v v z) = y ^ z. [para(44(a,1),44(a,1,2,2))]. 69 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(17(a,1),57(a,1,1,2))]. 80 ((x v x) v ((x v x) v (x v x))) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [para(69(a,1),13(a,1,1,1))]. 92 ((x v x) v (y ^ (x v x))) ^ (z v x) = x v x. [para(69(a,1),57(a,1,1,1))]. 94 ((x v x) v (x v x)) ^ (y v x) = x v x. [para(69(a,1),69(a,1,1,1))]. 103 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(14(a,1),92(a,1,1,2))]. 105 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v ((w v y) ^ (y v v6)))) = y. [para(6(a,1),67(a,1,1,1,1,2)),demod(6(14),6(15),6(23))]. 112 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(67(a,1),57(a,1,1,2))]. 148 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(67(a,1),103(a,1,1,2,1,1))]. 171 ((x v x) v x) ^ (y v x) = x v x. [para(6(a,1),148(a,1,1,2))]. 185 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(171(a,1),6(a,1,2,2))]. 605 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(67(a,1),185(a,1,1,2,1,1))]. 624 (((x v y) ^ y) v y) ^ (z v (y v y)) = y. [para(6(a,1),605(a,1,1,2))]. 652 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(624(a,1),13(a,1,2,2))]. 657 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(624(a,1),44(a,1,2,2))]. 670 (x v ((((x v x) v (x v x)) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [para(652(a,1),24(a,1,1,1))]. 672 (x v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (z v x) = x v x. [para(652(a,1),28(a,1,1,1))]. 682 (x v (x v x)) ^ (y v x) = x v x. [para(652(a,1),69(a,1,1,1))]. 683 (x v x) v (x v x) = x v x. [para(69(a,1),652(a,1,1,1)),demod(682(8))]. 689 (x v (y ^ x)) ^ (z v x) = x v x. [para(652(a,1),112(a,1,1,1))]. 739 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ (v v (y v y)) = y. [para(652(a,1),185(a,1,1,2,1,1))]. 746 (x v ((x v x) ^ y)) ^ (z v x) = x v x. [back_demod(672),demod(683(3),683(3))]. 748 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [back_demod(670),demod(683(3))]. 792 (x v x) ^ (y v x) = x v x. [back_demod(94),demod(683(3))]. 797 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_demod(80),demod(683(4),683(3))]. 920 (((x v y) ^ y) v y) ^ (z v ((u v y) ^ (y v v))) = y. [para(44(a,1),30(a,1,1,1,1,2)),demod(44(13),44(15),44(16),44(20))]. 1016 ((x v x) v ((x v x) ^ y)) ^ (z v (x v x)) = x v x. [para(683(a,1),746(a,1,1,2,1)),demod(683(10))]. 1454 ((((x v y) ^ y) v ((x v y) ^ y)) v y) ^ (z v (((x v y) ^ y) v ((x v y) ^ y))) = ((x v y) ^ y) v ((x v y) ^ y). [para(44(a,1),1016(a,1,1,2))]. 1605 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ (y v y) = y. [para(683(a,1),739(a,1,2))]. 1649 (x v (((x v x) v x) ^ y)) ^ (z v x) = x v x. [para(652(a,1),748(a,1,1,2,1,2))]. 1663 (((x v (((y v y) v y) ^ z)) ^ (((y v y) v y) ^ z)) v (((y v y) v y) ^ z)) ^ (u v (y v y)) = ((y v y) v y) ^ z. [para(1649(a,1),920(a,1,2,2))]. 1686 (((x v (y v y)) ^ (y v y)) v ((((y v y) ^ z) v (u ^ (y v y))) ^ v)) ^ (w v ((v6 v (y v y)) ^ (y v y))) = y v y. [para(683(a,1),48(a,1,2,2,2)),demod(683(7),683(7))]. 1703 (((x v (y v y)) ^ (y v y)) v ((((y v y) ^ z) v y) ^ u)) ^ (v v ((w v (y v y)) ^ ((y v y) v v6))) = y v y. [para(1605(a,1),48(a,1,1,2,1,2)),demod(683(7),683(7))]. 1705 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(683(a,1),797(a,1,2,2,1))]. 1745 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(44(a,1),1705(a,1,2,2)),demod(657(7)),flip(a)]. 1757 x ^ (y v x) = x. [para(105(a,1),1705(a,1,2,2)),demod(1745(5),1745(7))]. 1794 x v x = x. [back_demod(1454),demod(1745(5),1745(6),792(3),1745(6))]. 1822 (x v y) ^ y = y. [back_demod(1745),demod(1794(5))]. 1841 x ^ (y v (x ^ (x v z))) = x. [back_demod(1705),demod(1794(1),1794(1),1794(1),1794(5))]. 1843 (x v (((x ^ y) v x) ^ z)) ^ (u v ((v v x) ^ (x v w))) = x. [back_demod(1703),demod(1794(1),1794(2),1822(2),1794(1),1794(5),1794(6),1794(10))]. 1856 (x v (((x ^ y) v (z ^ x)) ^ u)) ^ (v v x) = x. [back_demod(1686),demod(1794(1),1794(2),1822(2),1794(1),1794(2),1794(6),1794(7),1822(7),1794(8))]. 1871 (x ^ y) ^ (z v x) = x ^ y. [back_demod(1663),demod(1794(1),1794(1),1794(3),1794(3),1822(4),1794(2),1794(2),1794(3),1794(2),1794(4),1794(4))]. 1883 (x v (x ^ y)) ^ (z v x) = x. [back_demod(1649),demod(1794(1),1794(1),1794(5))]. 2202 (x v (y ^ x)) ^ (z v x) = x. [back_demod(689),demod(1794(5))]. 2334 x ^ (x ^ (x v y)) = x. [para(1794(a,1),1841(a,1,2))]. 2336 (x ^ y) ^ x = x ^ y. [para(1794(a,1),1871(a,1,2))]. 2340 x v (x ^ y) = x. [para(1883(a,1),1841(a,1,2,2)),demod(1883(4)),flip(a)]. 2341 x ^ (x ^ y) = x ^ y. [para(2340(a,1),1822(a,1,1))]. 2345 x ^ (x v y) = x. [back_demod(2334),demod(2341(3))]. 2376 x v (y ^ x) = x. [para(2202(a,1),2345(a,1)),flip(a)]. 2443 x ^ (y ^ x) = y ^ x. [para(2376(a,1),1822(a,1,1))]. 2824 x v (((x ^ y) v x) ^ z) = x. [para(1843(a,1),2345(a,1)),flip(a)]. 3102 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(1856(a,1),2345(a,1)),flip(a)]. 3252 x v ((x ^ y) v x) = x. [para(1757(a,1),2824(a,1,2))]. 3292 (x ^ y) v x = x. [para(3252(a,1),1757(a,1,2)),demod(1822(3)),flip(a)]. 3312 x v (y v x) = y v x. [para(1822(a,1),3292(a,1,1))]. 9078 x v ((x ^ y) v (z ^ x)) = x. [para(1757(a,1),3102(a,1,2))]. 9236 x v ((x ^ y) v (x ^ z)) = x. [para(2336(a,1),9078(a,1,2,2))]. 9396 x v ((y ^ x) v (x ^ z)) = x. [para(2443(a,1),9236(a,1,2,1))]. 9827 ((x ^ y) v (y ^ z)) v y = y. [para(9396(a,1),3312(a,1,2)),demod(9396(8))]. 9828 $F # answer(McKenzie_3). [resolve(9827,a,9,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=353. Generated=100719. Kept=9819. proofs=4. Usable=185. Sos=6802. Demods=7009. Denials=1. Limbo=22, Disabled=2813. Hints=0. Weight_deleted=7952. Literals_deleted=0. Forward_subsumed=82726. Back_subsumed=290. Sos_limit_deleted=222. Sos_displaced=0. Sos_removed=0. New_demodulators=9814 (0 lex), Back_demodulated=2515. Back_unit_deleted=0. Demod_attempts=4195275. Demod_rewrites=281814. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=12.49. User_CPU=4.32, System_CPU=0.06, Wall_clock=5. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 4 proofs. Process 13092 exit (max_proofs) Mon Jun 19 16:41:16 2006