============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3829 was started by mccune on cleo.thornwood, Wed Nov 22 11:23:53 2006 The command was "/home/mccune/bin/prover9 -f a1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file a1.in formulas(sos). (((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (w v ((v6 v x) ^ (x v v7))) = x # label(A1). end_of_list. set(restrict_denials). formulas(goals). y v (x ^ (y ^ z)) = y # answer(McKenzie_1). y ^ (x v (y v z)) = y # 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 NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 y v (x ^ (y ^ z)) = y # answer(McKenzie_1) # label(goal). [goal]. 2 y ^ (x v (y v z)) = y # answer(McKenzie_2) # label(goal). [goal]. 3 ((x ^ y) v (y ^ z)) v y = y # answer(McKenzie_3) # label(goal). [goal]. 4 ((x v y) ^ (y v z)) ^ y = y # answer(McKenzie_4) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [assumption]. c1 v (c2 ^ (c1 ^ c3)) != c1 # answer(McKenzie_1). [deny(1)]. c4 ^ (c5 v (c4 v c6)) != c4 # answer(McKenzie_2). [deny(2)]. ((c7 ^ c8) v (c8 ^ c9)) v c8 != c8 # answer(McKenzie_3). [deny(3)]. ((c10 v c11) ^ (c11 v c12)) ^ c11 != c11 # answer(McKenzie_4). [deny(4)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 4). % (Horn set with more than one neg. clause) Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, v, ^ ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). restricted denial: (wt=9): 6 c1 v (c2 ^ (c1 ^ c3)) != c1 # answer(McKenzie_1). [deny(1)]. restricted denial: (wt=9): 7 c4 ^ (c5 v (c4 v c6)) != c4 # answer(McKenzie_2). [deny(2)]. restricted denial: (wt=11): 8 ((c7 ^ c8) v (c8 ^ c9)) v c8 != c8 # answer(McKenzie_3). [deny(3)]. restricted denial: (wt=11): 9 ((c10 v c11) ^ (c11 v c12)) ^ c11 != c11 # answer(McKenzie_4). [deny(4)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 6 c1 v (c2 ^ (c1 ^ c3)) != c1 # answer(McKenzie_1). [deny(1)]. 7 c4 ^ (c5 v (c4 v c6)) != c4 # answer(McKenzie_2). [deny(2)]. 8 ((c7 ^ c8) v (c8 ^ c9)) v c8 != c8 # answer(McKenzie_3). [deny(3)]. 9 ((c10 v c11) ^ (c11 v c12)) ^ c11 != c11 # answer(McKenzie_4). [deny(4)]. end_of_list. formulas(sos). 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [assumption]. end_of_list. formulas(demodulators). 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=29): 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [assumption]. given #2 (F,wt=21): 12 (((x v y) ^ y) v (y v y)) ^ (z v ((u v y) ^ (y v v))) = y. [para(5(a,1),5(a,1,1,2))]. given #3 (F,wt=25): 16 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (z v y) = y v y. [para(12(a,1),12(a,1,2,2))]. given #4 (T,wt=27): 17 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v ((w v y) ^ (y v v6))) = y. [para(16(a,1),5(a,1,1,2,1,1))]. given #5 (T,wt=33): 23 (((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(12(a,1),17(a,1,2,2))]. given #6 (A,wt=61): 10 (((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(5(a,1),5(a,1,1,2,1,1))]. given #7 (F,wt=31): 27 (((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(16(a,1),23(a,1,1,2,1,2))]. given #8 (F,wt=33): 33 (((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(17(a,1),10(a,1,1,1,1,2)),rewrite(17(17),17(22),17(26),17(27),17(31))]. given #9 (T,wt=21): 43 (((x v y) ^ y) v (z ^ y)) ^ (u v ((v v y) ^ (y v w))) = y. [para(5(a,1),33(a,1,1,2))]. given #10 (T,wt=23): 56 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(12(a,1),43(a,1,2,2))]. given #11 (A,wt=83): 11 (((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(5(a,1),5(a,1,1,2,1,2))]. given #12 (F,wt=21): 68 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(16(a,1),56(a,1,1,2))]. given #13 (F,wt=15): 93 ((x v x) v (x v x)) ^ (y v x) = x v x. [para(68(a,1),68(a,1,1,1))]. given #14 (T,wt=17): 91 ((x v x) v (y ^ (x v x))) ^ (z v x) = x v x. [para(68(a,1),56(a,1,1,1))]. given #15 (T,wt=19): 81 ((x v x) v ((x v x) v (x v x))) ^ (y v x) = x v x. [para(68(a,1),16(a,1,1,1))]. given #16 (A,wt=83): 13 (((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(5(a,1),5(a,1,2,2))]. given #17 (F,wt=23): 66 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (v v z) = y ^ z. [para(43(a,1),43(a,1,2,2))]. given #18 (F,wt=15): 113 ((x v x) v (y ^ x)) ^ (z v x) = x v x. [para(66(a,1),91(a,1,1,2))]. given #19 (T,wt=21): 111 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(66(a,1),56(a,1,1,2))]. given #20 (T,wt=23): 102 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(13(a,1),91(a,1,1,2))]. given #21 (A,wt=35): 14 (((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(12(a,1),5(a,1,2,2))]. given #22 (F,wt=21): 137 ((x v x) v (((x v x) v (y ^ x)) ^ z)) ^ (u v x) = x v x. [para(16(a,1),102(a,1,1,2,1,1))]. given #23 (F,wt=21): 147 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(66(a,1),102(a,1,1,2,1,1))]. given #24 (T,wt=13): 170 ((x v x) v x) ^ (y v x) = x v x. [para(5(a,1),147(a,1,1,2))]. given #25 (T,wt=17): 185 (((x v y) ^ y) v (y v y)) ^ (z v (y v y)) = y. [para(170(a,1),12(a,1,2,2))]. given #26 (A,wt=65): 15 (((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(5(a,1),12(a,1,2,2))]. given #27 (F,wt=17): 190 (((x v y) ^ y) v (z ^ y)) ^ (u v (y v y)) = y. [para(170(a,1),43(a,1,2,2))]. given #28 (F,wt=19): 203 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v (y v y))) = y. [para(185(a,1),66(a,1,1,1,1,2)),rewrite(185(8),185(9),185(15))]. given #29 (T,wt=21): 237 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v (w v (y v y)))) = y. [para(203(a,1),66(a,1,1,1,1,2)),rewrite(203(9),203(10),203(17))]. given #30 (T,wt=23): 104 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v ((w v y) ^ (y v v6)))) = y. [para(5(a,1),66(a,1,1,1,1,2)),rewrite(5(14),5(15),5(23))]. given #31 (A,wt=43): 18 (((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(16(a,1),5(a,1,1,2,1,2))]. given #32 (F,wt=23): 186 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v (y v y)) = y. [para(170(a,1),17(a,1,2,2))]. given #33 (F,wt=23): 201 (((x v x) v (x v x)) v x) ^ (y v (x v x)) = (x v x) v (x v x). [para(185(a,1),91(a,1,1,2))]. given #34 (T,wt=21): 337 (((x v y) ^ y) v (y v y)) ^ (z v ((y v y) v (y v y))) = y. [para(201(a,1),12(a,1,2,2))]. given #35 (T,wt=23): 221 ((x v x) v (y ^ (x v x))) ^ (z v ((x v x) v (x v x))) = x v x. [para(68(a,1),190(a,1,1,1))]. given #36 (A,wt=71): 19 (((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(17(a,1),5(a,1,2,2))]. given #37 (F,wt=21): 345 ((x v x) v (x v x)) ^ (y v ((x v x) v (x v x))) = x v x. [para(16(a,1),221(a,1,1,2))]. given #38 (F,wt=21): 347 ((x v x) v (y ^ x)) ^ (z v ((x v x) v (x v x))) = x v x. [para(66(a,1),221(a,1,1,2))]. given #39 (T,wt=23): 262 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v (w v (v6 v (y v y))))) = y. [para(237(a,1),66(a,1,1,1,1,2)),rewrite(237(10),237(11),237(19))]. given #40 (T,wt=25): 55 (((x v (y ^ z)) ^ (y ^ z)) v ((y ^ z) v (y ^ z))) ^ (u v z) = y ^ z. [para(43(a,1),12(a,1,2,2))]. given #41 (A,wt=81): 20 (((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(5(a,1),17(a,1,1,2,1,2))]. given #42 (F,wt=19): 417 (((x v y) ^ y) v (y v y)) ^ (z v (u v (y v y))) = y. [para(185(a,1),55(a,1,1,1,1,2)),rewrite(185(8),185(9),185(9),185(15))]. given #43 (F,wt=21): 418 (((x v y) ^ y) v (y v y)) ^ (z v (u v (v v (y v y)))) = y. [para(203(a,1),55(a,1,1,1,1,2)),rewrite(203(9),203(10),203(10),203(17))]. given #44 (T,wt=23): 413 (((x v y) ^ y) v (y v y)) ^ (z v (u v ((v v y) ^ (y v w)))) = y. [para(5(a,1),55(a,1,1,1,1,2)),rewrite(5(14),5(15),5(15),5(23))]. given #45 (T,wt=23): 419 (((x v y) ^ y) v (y v y)) ^ (z v (u v (v v (w v (y v y))))) = y. [para(237(a,1),55(a,1,1,1,1,2)),rewrite(237(10),237(11),237(11),237(19))]. given #46 (A,wt=81): 21 (((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(5(a,1),17(a,1,2,2))]. given #47 (F,wt=25): 86 ((x v x) v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (z v x) = x v x. [para(68(a,1),27(a,1,1,1))]. given #48 (F,wt=25): 105 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v (v v y)) = y v y. [para(16(a,1),66(a,1,1,1,1,2)),rewrite(16(12),16(14),16(20))]. given #49 (T,wt=19): 460 ((x v x) v (y ^ (x v x))) ^ (z v (u v x)) = x v x. [para(68(a,1),105(a,1,1,1))]. given #50 (T,wt=17): 492 ((x v x) v (x v x)) ^ (y v (z v x)) = x v x. [para(16(a,1),460(a,1,1,2))]. given #51 (A,wt=55): 22 (((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(17(a,1),12(a,1,2,2))]. given #52 (F,wt=17): 494 ((x v x) v (y ^ x)) ^ (z v (u v x)) = x v x. [para(66(a,1),460(a,1,1,2))]. given #53 (F,wt=23): 453 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v (u v y)) = y v y. [para(16(a,1),105(a,1,1,2))]. given #54 (T,wt=23): 464 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v (v v y)) = y v y. [para(66(a,1),105(a,1,1,2))]. given #55 (T,wt=23): 499 ((x v x) v (((x v x) v (y ^ x)) ^ z)) ^ (u v (v v x)) = x v x. [para(19(a,1),460(a,1,1,2))]. given #56 (A,wt=41): 24 (((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(16(a,1),17(a,1,1,2,1,2))]. given #57 (F,wt=25): 117 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (v v (w v z)) = y ^ z. [para(66(a,1),66(a,1,1,1,1,2)),rewrite(66(11),66(13),66(19))]. given #58 (F,wt=25): 121 (((x v y) v (x v y)) v (y v y)) ^ (z v (x v y)) = (x v y) v (x v y). [para(16(a,1),113(a,1,1,2))]. given #59 (T,wt=25): 128 (((x v y) v (x v y)) v (z ^ y)) ^ (u v (x v y)) = (x v y) v (x v y). [para(66(a,1),113(a,1,1,2))]. given #60 (T,wt=25): 184 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(170(a,1),5(a,1,2,2))]. given #61 (A,wt=69): 25 (((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(17(a,1),17(a,1,2,2))]. given #62 (F,wt=23): 604 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(66(a,1),184(a,1,1,2,1,1))]. given #63 (F,wt=15): 623 (((x v y) ^ y) v y) ^ (z v (y v y)) = y. [para(5(a,1),604(a,1,1,2))]. given #64 (T,wt=15): 651 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(623(a,1),12(a,1,2,2))]. given #65 (T,wt=11): 682 (x v x) v (x v x) = x v x. [para(68(a,1),651(a,1,1,1)),rewrite(681(8))]. given #66 (A,wt=35): 28 (((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(5(a,1),10(a,1,1,1,1,2)),rewrite(5(19),5(25),5(29),5(30),5(34))]. given #67 (F,wt=11): 791 (x v x) ^ (y v x) = x v x. [back_rewrite(93),rewrite(682(3))]. given #68 (F,wt=13): 681 (x v (x v x)) ^ (y v x) = x v x. [para(651(a,1),68(a,1,1,1))]. given #69 (T,wt=13): 688 (x v (y ^ x)) ^ (z v x) = x v x. [para(651(a,1),111(a,1,1,1))]. given #70 (T,wt=13): 763 (x v x) ^ (y v (z v x)) = x v x. [back_rewrite(492),rewrite(682(3))]. given #71 (A,wt=89): 29 (((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(5(a,1),10(a,1,1,2))]. given #72 (F,wt=13): 842 (((x v y) ^ y) v y) ^ (y v y) = y. [para(682(a,1),623(a,1,2))]. given #73 (F,wt=15): 656 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(623(a,1),43(a,1,2,2))]. given #74 (T,wt=15): 677 (x v (y ^ (x v x))) ^ (z v x) = x v x. [para(651(a,1),56(a,1,1,1))]. given #75 (T,wt=15): 726 ((x v x) v x) ^ (y v (z v x)) = x v x. [para(651(a,1),460(a,1,1,2))]. given #76 (A,wt=77): 30 (((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(5(a,1),10(a,1,2,2))]. given #77 (F,wt=15): 729 (x v (x v x)) ^ (y v (z v x)) = x v x. [para(651(a,1),453(a,1,1,1))]. given #78 (F,wt=15): 730 (x v (y ^ x)) ^ (z v (u v x)) = x v x. [para(651(a,1),464(a,1,1,1))]. given #79 (T,wt=15): 745 (x v ((x v x) ^ y)) ^ (z v x) = x v x. [back_rewrite(671),rewrite(682(3),682(3))]. given #80 (T,wt=15): 772 (x v x) ^ (y v (z v (x v x))) = x v x. [back_rewrite(433),rewrite(682(4),682(3),682(4))]. given #81 (A,wt=81): 31 (((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(10(a,1),12(a,1,2,2))]. given #82 (F,wt=17): 659 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v y)) = y. [para(623(a,1),104(a,1,2,2,2))]. given #83 (F,wt=17): 663 (((x v y) ^ y) v (y v y)) ^ (z v (u v y)) = y. [para(623(a,1),413(a,1,2,2,2))]. given #84 (T,wt=17): 718 (x v (x v x)) ^ (y v (z v (x v x))) = x v x. [para(651(a,1),417(a,1,1,1)),rewrite(682(3),682(5))]. given #85 (T,wt=17): 724 (x v (y ^ (x v x))) ^ (z v (u v x)) = x v x. [para(651(a,1),105(a,1,1,1))]. given #86 (A,wt=99): 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)) 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(10(a,1),17(a,1,2,2))]. given #87 (F,wt=17): 771 (x v x) ^ (y v (z v (u v (x v x)))) = x v x. [back_rewrite(434),rewrite(682(4),682(3),682(4))]. given #88 (F,wt=17): 793 ((x v x) v ((x v x) ^ y)) ^ (z v x) = x v x. [back_rewrite(86),rewrite(682(4),682(4))]. given #89 (T,wt=19): 678 (((x v (y v y)) ^ (y v y)) v y) ^ (z v y) = y v y. [para(651(a,1),56(a,1,1,2))]. given #90 (T,wt=19): 690 ((x v x) v ((x v (y ^ x)) ^ z)) ^ (u v x) = x v x. [para(651(a,1),102(a,1,1,2,1,1))]. given #91 (A,wt=69): 34 (((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(17(a,1),10(a,1,2,2))]. given #92 (F,wt=19): 699 (x v (y ^ (x v x))) ^ (z v (u v (x v x))) = x v x. [para(651(a,1),203(a,1,1,1)),rewrite(682(6))]. given #93 (F,wt=17): 1224 (x v (y ^ x)) ^ (z v (u v (x v x))) = x v x. [para(66(a,1),699(a,1,1,2))]. given #94 (T,wt=19): 719 (x v (x v x)) ^ (y v (z v (u v (x v x)))) = x v x. [para(651(a,1),418(a,1,1,1)),rewrite(682(3),682(5))]. given #95 (T,wt=19): 735 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v (w v y))) = y. [para(651(a,1),117(a,1,1,1,1,2)),rewrite(651(7),651(8),651(14))]. given #96 (A,wt=73): 35 (((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(10(a,1),10(a,1,1,1,1,2)),rewrite(10(36),10(46),10(53),10(57),10(64))]. given #97 (F,wt=19): 769 (x v x) ^ (y v (z v (u v (v v (x v x))))) = x v x. [back_rewrite(445),rewrite(682(4),682(3),682(4))]. given #98 (F,wt=19): 889 ((x v x) v ((y ^ x) v (y ^ x))) ^ (z v x) = x v x. [para(791(a,1),147(a,1,1,2))]. given #99 (T,wt=19): 909 ((x v y) v y) ^ (z v (x v y)) = (x v y) v (x v y). [para(651(a,1),688(a,1,1,2))]. given #100 (T,wt=19): 919 (((x v y) ^ y) v y) ^ (z v ((u v y) ^ (y v v))) = y. [para(43(a,1),29(a,1,1,1,1,2)),rewrite(43(13),43(15),43(16),43(20))]. given #101 (A,wt=95): 41 (((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(5(a,1),33(a,1,1,2,1,1,1,2))]. given #102 (F,wt=13): 1406 (((x v y) ^ y) v y) ^ (z v y) = y. [para(623(a,1),919(a,1,2,2))]. given #103 (F,wt=19): 971 (x v (((x v x) v (y ^ x)) ^ z)) ^ (u v x) = x v x. [para(19(a,1),677(a,1,1,2))]. given #104 (T,wt=19): 1015 ((x v x) v ((x v x) ^ y)) ^ (z v (x v x)) = x v x. [para(682(a,1),745(a,1,1,2,1)),rewrite(682(10))]. given #105 (T,wt=19): 1121 (((x v y) ^ y) v (y v y)) ^ (z v (u v (v v y))) = y. [para(659(a,1),55(a,1,1,1,1,2)),rewrite(659(8),659(9),659(9),659(15))]. given #106 (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 (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(5(a,1),33(a,1,1,2,1,2))]. given #107 (F,wt=19): 1411 (((x v y) ^ y) v y) ^ (z v ((u v y) v (u v y))) = y. [para(909(a,1),919(a,1,2,2))]. given #108 (F,wt=17): 1479 (((x v y) ^ y) v y) ^ ((z v y) v (z v y)) = y. [para(682(a,1),1411(a,1,2))]. given #109 (T,wt=21): 652 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v y) = y. [para(623(a,1),17(a,1,2,2))]. given #110 (T,wt=21): 701 (x v (y ^ (x v x))) ^ (z v (u v (v v (x v x)))) = x v x. [para(651(a,1),237(a,1,1,1)),rewrite(682(6))]. given #111 (A,wt=97): 44 (((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(5(a,1),33(a,1,2,2))]. given #112 (F,wt=19): 1514 (x v (y ^ x)) ^ (z v (u v (v v (x v x)))) = x v x. [para(66(a,1),701(a,1,1,2))]. given #113 (F,wt=19): 1516 ((x v x) v x) ^ (y v (z v (u v (x v x)))) = x v x. [para(186(a,1),701(a,1,1,2)),rewrite(682(5),682(10))]. given #114 (T,wt=21): 721 (x v (x v x)) ^ (y v (z v (u v (v v (x v x))))) = x v x. [para(651(a,1),419(a,1,1,1)),rewrite(682(3),682(5))]. given #115 (T,wt=21): 725 (((x v (y v y)) ^ (y v y)) v y) ^ (z v (u v y)) = y v y. [para(651(a,1),105(a,1,1,2))]. given #116 (A,wt=85): 45 (((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(33(a,1),12(a,1,2,2))]. given #117 (F,wt=21): 738 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ (v v (y v y)) = y. [para(651(a,1),184(a,1,1,2,1,1))]. given #118 (F,wt=19): 1604 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ (y v y) = y. [para(682(a,1),738(a,1,2))]. given #119 (T,wt=21): 747 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [back_rewrite(669),rewrite(682(3))]. given #120 (T,wt=17): 1648 (x v (((x v x) v x) ^ y)) ^ (z v x) = x v x. [para(651(a,1),747(a,1,1,2,1,2))]. given #121 (A,wt=49): 47 (((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(16(a,1),33(a,1,1,2,1,1,1,2))]. given #122 (F,wt=21): 796 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_rewrite(79),rewrite(682(4),682(3))]. given #123 (F,wt=17): 1703 (x v x) ^ (y v ((z v x) v (z v x))) = x v x. [para(121(a,1),796(a,1,2,2))]. given #124 (T,wt=19): 1704 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(682(a,1),796(a,1,2,2,1))]. given #125 (T,wt=5): 1793 x v x = x. [back_rewrite(1453),rewrite(1744(5),1744(6),791(3),1744(6))]. given #126 (A,wt=7): 1756 x ^ (y v x) = x. [para(104(a,1),1704(a,1,2,2)),rewrite(1744(5),1744(7))]. given #127 (F,wt=5): 2305 x ^ x = x. [back_rewrite(1791),rewrite(1821(2),1821(3),1821(2),1793(1),1821(3))]. given #128 (F,wt=7): 1821 (x v y) ^ y = y. [back_rewrite(1744),rewrite(1793(5))]. given #129 (T,wt=9): 1841 x ^ (y v (z v x)) = x. [back_rewrite(1703),rewrite(1793(1),1793(3),1793(4))]. given #130 (T,wt=9): 2180 (x ^ y) ^ y = x ^ y. [back_rewrite(826),rewrite(1793(1),1793(3),1821(4),1793(2),1793(3),1793(4),1793(3),1793(2),1793(3))]. given #131 (A,wt=29): 1796 ((x ^ (x v y)) v (((x ^ (x v y)) v x) ^ z)) ^ (u v (x ^ (x v y))) = x ^ (x v y). [back_rewrite(1790),rewrite(1793(1),1793(1),1793(3),1793(3),1793(5),1793(5),1793(7),1793(5),1793(8),1793(8),1793(12),1793(12),1793(14),1793(14),1793(16))]. given #132 (F,wt=11): 1838 (x ^ y) ^ (z v y) = x ^ y. [back_rewrite(1707),rewrite(1793(3),1793(2),1793(6))]. given #133 (F,wt=11): 1840 x ^ (y v (x ^ (x v z))) = x. [back_rewrite(1704),rewrite(1793(1),1793(1),1793(1),1793(5))]. given #134 (T,wt=9): 2333 x ^ (x ^ (x v y)) = x. [para(1793(a,1),1840(a,1,2))]. given #135 (T,wt=11): 1870 (x ^ y) ^ (z v x) = x ^ y. [back_rewrite(1662),rewrite(1793(1),1793(1),1793(3),1793(3),1821(4),1793(2),1793(2),1793(3),1793(2),1793(4),1793(4))]. given #136 (A,wt=31): 1799 ((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_rewrite(1787),rewrite(1793(1),1793(1),1793(4),1793(5),1793(5),1793(8),1793(8),1793(11),1793(12),1793(12),1793(15),1793(15),1793(18))]. given #137 (F,wt=9): 2335 (x ^ y) ^ x = x ^ y. [para(1793(a,1),1870(a,1,2))]. given #138 (F,wt=11): 1882 (x v (x ^ y)) ^ (z v x) = x. [back_rewrite(1648),rewrite(1793(1),1793(1),1793(5))]. given #139 (T,wt=7): 2339 x v (x ^ y) = x. [para(1882(a,1),1840(a,1,2,2)),rewrite(1882(4)),flip(a)]. given #140 (T,wt=7): 2344 x ^ (x v y) = x. [back_rewrite(2333),rewrite(2340(3))]. ============================== PROOF ================================= % Proof 1 at 2.26 (+ 0.01) seconds: McKenzie_2. % Length of proof is 52. % Level of proof is 27. % Maximum clause weight is 83. % Given clauses 140. 2 y ^ (x v (y v z)) = y # answer(McKenzie_2) # label(goal). [goal]. 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [assumption]. 7 c4 ^ (c5 v (c4 v c6)) != c4 # answer(McKenzie_2). [deny(2)]. 10 (((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(5(a,1),5(a,1,1,2,1,1))]. 12 (((x v y) ^ y) v (y v y)) ^ (z v ((u v y) ^ (y v v))) = y. [para(5(a,1),5(a,1,1,2))]. 13 (((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(5(a,1),5(a,1,2,2))]. 16 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (z v y) = y v y. [para(12(a,1),12(a,1,2,2))]. 17 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v ((w v y) ^ (y v v6))) = y. [para(16(a,1),5(a,1,1,2,1,1))]. 23 (((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(12(a,1),17(a,1,2,2))]. 27 (((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(16(a,1),23(a,1,1,2,1,2))]. 33 (((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(17(a,1),10(a,1,1,1,1,2)),rewrite(17(17),17(22),17(26),17(27),17(31))]. 43 (((x v y) ^ y) v (z ^ y)) ^ (u v ((v v y) ^ (y v w))) = y. [para(5(a,1),33(a,1,1,2))]. 56 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(12(a,1),43(a,1,2,2))]. 66 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (v v z) = y ^ z. [para(43(a,1),43(a,1,2,2))]. 68 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(16(a,1),56(a,1,1,2))]. 79 ((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(68(a,1),12(a,1,1,1))]. 91 ((x v x) v (y ^ (x v x))) ^ (z v x) = x v x. [para(68(a,1),56(a,1,1,1))]. 93 ((x v x) v (x v x)) ^ (y v x) = x v x. [para(68(a,1),68(a,1,1,1))]. 102 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(13(a,1),91(a,1,1,2))]. 147 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(66(a,1),102(a,1,1,2,1,1))]. 170 ((x v x) v x) ^ (y v x) = x v x. [para(5(a,1),147(a,1,1,2))]. 184 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(170(a,1),5(a,1,2,2))]. 604 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(66(a,1),184(a,1,1,2,1,1))]. 623 (((x v y) ^ y) v y) ^ (z v (y v y)) = y. [para(5(a,1),604(a,1,1,2))]. 651 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(623(a,1),12(a,1,2,2))]. 656 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(623(a,1),43(a,1,2,2))]. 669 (x v ((((x v x) v (x v x)) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [para(651(a,1),23(a,1,1,1))]. 671 (x v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (z v x) = x v x. [para(651(a,1),27(a,1,1,1))]. 681 (x v (x v x)) ^ (y v x) = x v x. [para(651(a,1),68(a,1,1,1))]. 682 (x v x) v (x v x) = x v x. [para(68(a,1),651(a,1,1,1)),rewrite(681(8))]. 745 (x v ((x v x) ^ y)) ^ (z v x) = x v x. [back_rewrite(671),rewrite(682(3),682(3))]. 747 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [back_rewrite(669),rewrite(682(3))]. 791 (x v x) ^ (y v x) = x v x. [back_rewrite(93),rewrite(682(3))]. 796 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_rewrite(79),rewrite(682(4),682(3))]. 889 ((x v x) v ((y ^ x) v (y ^ x))) ^ (z v x) = x v x. [para(791(a,1),147(a,1,1,2))]. 1015 ((x v x) v ((x v x) ^ y)) ^ (z v (x v x)) = x v x. [para(682(a,1),745(a,1,1,2,1)),rewrite(682(10))]. 1453 ((((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(43(a,1),1015(a,1,1,2))]. 1648 (x v (((x v x) v x) ^ y)) ^ (z v x) = x v x. [para(651(a,1),747(a,1,1,2,1,2))]. 1704 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(682(a,1),796(a,1,2,2,1))]. 1707 ((x ^ y) v (x ^ y)) ^ (z v (y v y)) = (x ^ y) v (x ^ y). [para(889(a,1),796(a,1,2,2))]. 1744 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(43(a,1),1704(a,1,2,2)),rewrite(656(7)),flip(a)]. 1793 x v x = x. [back_rewrite(1453),rewrite(1744(5),1744(6),791(3),1744(6))]. 1821 (x v y) ^ y = y. [back_rewrite(1744),rewrite(1793(5))]. 1838 (x ^ y) ^ (z v y) = x ^ y. [back_rewrite(1707),rewrite(1793(3),1793(2),1793(6))]. 1840 x ^ (y v (x ^ (x v z))) = x. [back_rewrite(1704),rewrite(1793(1),1793(1),1793(1),1793(5))]. 1882 (x v (x ^ y)) ^ (z v x) = x. [back_rewrite(1648),rewrite(1793(1),1793(1),1793(5))]. 2333 x ^ (x ^ (x v y)) = x. [para(1793(a,1),1840(a,1,2))]. 2339 x v (x ^ y) = x. [para(1882(a,1),1840(a,1,2,2)),rewrite(1882(4)),flip(a)]. 2340 x ^ (x ^ y) = x ^ y. [para(2339(a,1),1821(a,1,1))]. 2344 x ^ (x v y) = x. [back_rewrite(2333),rewrite(2340(3))]. 2361 x ^ (y v (x v z)) = x. [para(2344(a,1),1838(a,1,1)),rewrite(2344(5))]. 2362 $F # answer(McKenzie_2). [resolve(2361,a,7,a)]. ============================== end of proof ========================== % Redundant proof: 2363 $F # answer(McKenzie_2). [back_rewrite(7),rewrite(2361(7)),xx(a)]. % Disable descendants (x means already disabled): 7x given #141 (A,wt=27): 1824 ((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_rewrite(1741),rewrite(1793(3),1793(6),1821(6),1793(5),1793(5),1793(10),1793(12),1793(12),1793(13))]. given #142 (F,wt=9): 2340 x ^ (x ^ y) = x ^ y. [para(2339(a,1),1821(a,1,1))]. given #143 (F,wt=9): 2341 (x v y) v y = x v y. [para(1821(a,1),2339(a,1,2))]. given #144 (T,wt=9): 2361 x ^ (y v (x v z)) = x. [para(2344(a,1),1838(a,1,1)),rewrite(2344(5))]. given #145 (T,wt=11): 1953 x ^ (y v (z v (u v x))) = x. [back_rewrite(1516),rewrite(1793(1),1793(1),1793(1),1793(5))]. given #146 (A,wt=29): 1825 ((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_rewrite(1740),rewrite(1793(3),1793(6),1821(6),1793(5),1793(5),1793(10),1793(12),1793(12),1793(14))]. given #147 (F,wt=11): 2201 (x v (y ^ x)) ^ (z v x) = x. [back_rewrite(688),rewrite(1793(5))]. given #148 (F,wt=7): 2376 x v (y ^ x) = x. [para(2201(a,1),2344(a,1)),flip(a)]. given #149 (T,wt=9): 2443 x ^ (y ^ x) = y ^ x. [para(2376(a,1),1821(a,1,1))]. given #150 (T,wt=7): 2457 (x v y) ^ x = x. [para(2344(a,1),2443(a,1,2)),rewrite(2344(4))]. given #151 (A,wt=51): 1828 ((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_rewrite(1728),rewrite(1793(3),1793(6),1821(6),1793(5),1793(7),1793(7),1793(8),1793(11),1793(16),1793(19),1793(25))]. given #152 (F,wt=9): 2449 (x v y) v x = x v y. [para(2344(a,1),2376(a,1,2))]. given #153 (F,wt=9): 2454 (x v (y v z)) ^ z = z. [para(1841(a,1),2443(a,1,2)),rewrite(1841(6))]. given #154 (T,wt=9): 2458 (x v (y v z)) ^ y = y. [para(2361(a,1),2443(a,1,2)),rewrite(2361(6))]. given #155 (T,wt=9): 2489 x ^ ((y v x) v z) = x. [para(2449(a,1),1841(a,1,2))]. given #156 (A,wt=51): 1829 ((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_rewrite(1727),rewrite(1793(3),1793(6),1821(6),1793(5),1793(7),1793(7),1793(6),1793(10),1793(16),1793(19),1793(25))]. given #157 (F,wt=9): 2492 x ^ ((x v y) v z) = x. [para(2449(a,1),2361(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(2361(a,1),1838(a,1,1)),rewrite(2361(7))]. given #161 (A,wt=31): 1830 ((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_rewrite(1726),rewrite(1793(3),1793(6),1821(6),1793(5),1793(6),1793(11),1793(13),1793(13),1793(15))]. given #162 (F,wt=11): 2446 (x v y) v (z ^ y) = x v y. [para(1838(a,1),2376(a,1,2))]. ============================== PROOF ================================= % Proof 2 at 2.31 (+ 0.01) seconds: McKenzie_1. % Length of proof is 57. % Level of proof is 29. % Maximum clause weight is 83. % Given clauses 162. 1 y v (x ^ (y ^ z)) = y # answer(McKenzie_1) # label(goal). [goal]. 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [assumption]. 6 c1 v (c2 ^ (c1 ^ c3)) != c1 # answer(McKenzie_1). [deny(1)]. 10 (((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(5(a,1),5(a,1,1,2,1,1))]. 12 (((x v y) ^ y) v (y v y)) ^ (z v ((u v y) ^ (y v v))) = y. [para(5(a,1),5(a,1,1,2))]. 13 (((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(5(a,1),5(a,1,2,2))]. 16 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (z v y) = y v y. [para(12(a,1),12(a,1,2,2))]. 17 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v ((w v y) ^ (y v v6))) = y. [para(16(a,1),5(a,1,1,2,1,1))]. 23 (((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(12(a,1),17(a,1,2,2))]. 27 (((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(16(a,1),23(a,1,1,2,1,2))]. 33 (((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(17(a,1),10(a,1,1,1,1,2)),rewrite(17(17),17(22),17(26),17(27),17(31))]. 43 (((x v y) ^ y) v (z ^ y)) ^ (u v ((v v y) ^ (y v w))) = y. [para(5(a,1),33(a,1,1,2))]. 56 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(12(a,1),43(a,1,2,2))]. 66 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (v v z) = y ^ z. [para(43(a,1),43(a,1,2,2))]. 68 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(16(a,1),56(a,1,1,2))]. 79 ((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(68(a,1),12(a,1,1,1))]. 91 ((x v x) v (y ^ (x v x))) ^ (z v x) = x v x. [para(68(a,1),56(a,1,1,1))]. 93 ((x v x) v (x v x)) ^ (y v x) = x v x. [para(68(a,1),68(a,1,1,1))]. 102 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(13(a,1),91(a,1,1,2))]. 111 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(66(a,1),56(a,1,1,2))]. 147 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(66(a,1),102(a,1,1,2,1,1))]. 170 ((x v x) v x) ^ (y v x) = x v x. [para(5(a,1),147(a,1,1,2))]. 184 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(170(a,1),5(a,1,2,2))]. 604 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(66(a,1),184(a,1,1,2,1,1))]. 623 (((x v y) ^ y) v y) ^ (z v (y v y)) = y. [para(5(a,1),604(a,1,1,2))]. 651 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(623(a,1),12(a,1,2,2))]. 656 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(623(a,1),43(a,1,2,2))]. 669 (x v ((((x v x) v (x v x)) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [para(651(a,1),23(a,1,1,1))]. 671 (x v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (z v x) = x v x. [para(651(a,1),27(a,1,1,1))]. 681 (x v (x v x)) ^ (y v x) = x v x. [para(651(a,1),68(a,1,1,1))]. 682 (x v x) v (x v x) = x v x. [para(68(a,1),651(a,1,1,1)),rewrite(681(8))]. 688 (x v (y ^ x)) ^ (z v x) = x v x. [para(651(a,1),111(a,1,1,1))]. 745 (x v ((x v x) ^ y)) ^ (z v x) = x v x. [back_rewrite(671),rewrite(682(3),682(3))]. 747 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [back_rewrite(669),rewrite(682(3))]. 791 (x v x) ^ (y v x) = x v x. [back_rewrite(93),rewrite(682(3))]. 796 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_rewrite(79),rewrite(682(4),682(3))]. 889 ((x v x) v ((y ^ x) v (y ^ x))) ^ (z v x) = x v x. [para(791(a,1),147(a,1,1,2))]. 1015 ((x v x) v ((x v x) ^ y)) ^ (z v (x v x)) = x v x. [para(682(a,1),745(a,1,1,2,1)),rewrite(682(10))]. 1453 ((((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(43(a,1),1015(a,1,1,2))]. 1648 (x v (((x v x) v x) ^ y)) ^ (z v x) = x v x. [para(651(a,1),747(a,1,1,2,1,2))]. 1704 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(682(a,1),796(a,1,2,2,1))]. 1707 ((x ^ y) v (x ^ y)) ^ (z v (y v y)) = (x ^ y) v (x ^ y). [para(889(a,1),796(a,1,2,2))]. 1744 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(43(a,1),1704(a,1,2,2)),rewrite(656(7)),flip(a)]. 1793 x v x = x. [back_rewrite(1453),rewrite(1744(5),1744(6),791(3),1744(6))]. 1821 (x v y) ^ y = y. [back_rewrite(1744),rewrite(1793(5))]. 1838 (x ^ y) ^ (z v y) = x ^ y. [back_rewrite(1707),rewrite(1793(3),1793(2),1793(6))]. 1840 x ^ (y v (x ^ (x v z))) = x. [back_rewrite(1704),rewrite(1793(1),1793(1),1793(1),1793(5))]. 1882 (x v (x ^ y)) ^ (z v x) = x. [back_rewrite(1648),rewrite(1793(1),1793(1),1793(5))]. 2201 (x v (y ^ x)) ^ (z v x) = x. [back_rewrite(688),rewrite(1793(5))]. 2333 x ^ (x ^ (x v y)) = x. [para(1793(a,1),1840(a,1,2))]. 2339 x v (x ^ y) = x. [para(1882(a,1),1840(a,1,2,2)),rewrite(1882(4)),flip(a)]. 2340 x ^ (x ^ y) = x ^ y. [para(2339(a,1),1821(a,1,1))]. 2344 x ^ (x v y) = x. [back_rewrite(2333),rewrite(2340(3))]. 2376 x v (y ^ x) = x. [para(2201(a,1),2344(a,1)),flip(a)]. 2446 (x v y) v (z ^ y) = x v y. [para(1838(a,1),2376(a,1,2))]. 2555 x v (y ^ (x ^ z)) = x. [para(2339(a,1),2446(a,1,1)),rewrite(2339(5))]. 2556 $F # answer(McKenzie_1). [resolve(2555,a,6,a)]. ============================== end of proof ========================== % Redundant proof: 2567 $F # answer(McKenzie_1). [back_rewrite(6),rewrite(2555(7)),xx(a)]. % Disable descendants (x means already disabled): 6x given #163 (F,wt=9): 2555 x v (y ^ (x ^ z)) = x. [para(2339(a,1),2446(a,1,1)),rewrite(2339(5))]. given #164 (T,wt=9): 2558 x v (y ^ (z ^ x)) = x. [para(2376(a,1),2446(a,1,1)),rewrite(2376(5))]. given #165 (T,wt=9): 2572 x v ((x ^ y) ^ z) = x. [para(2335(a,1),2555(a,1,2))]. given #166 (A,wt=31): 1831 ((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_rewrite(1725),rewrite(1793(3),1793(6),1821(6),1793(3),1793(5),1793(11),1793(13),1793(13),1793(15))]. given #167 (F,wt=9): 2585 x v ((y ^ x) ^ z) = x. [para(2335(a,1),2558(a,1,2))]. given #168 (F,wt=11): 2448 (x v y) v (y ^ z) = x v y. [para(1870(a,1),2376(a,1,2))]. given #169 (T,wt=11): 2455 (x v y) ^ (z ^ y) = z ^ y. [para(1838(a,1),2443(a,1,2)),rewrite(1838(6))]. given #170 (T,wt=11): 2456 (x v y) ^ (y ^ z) = y ^ z. [para(1870(a,1),2443(a,1,2)),rewrite(1870(6))]. given #171 (A,wt=23): 1832 ((x v y) v ((y v (z ^ (x v y))) ^ u)) ^ (v v (x v y)) = x v y. [back_rewrite(1723),rewrite(1793(3),1793(5),1821(4),1793(2),1793(4),1793(9),1793(12))]. given #172 (F,wt=11): 2459 (x v (y v (z v u))) ^ u = u. [para(1953(a,1),2443(a,1,2)),rewrite(1953(8))]. given #173 (F,wt=11): 2490 (x ^ y) ^ (y v z) = x ^ y. [para(2449(a,1),1838(a,1,2))]. given #174 (T,wt=11): 2491 (x ^ y) ^ (x v z) = x ^ y. [para(2449(a,1),1870(a,1,2))]. given #175 (T,wt=11): 2493 x ^ (y v ((z v x) v u)) = x. [para(2449(a,1),1953(a,1,2,2))]. given #176 (A,wt=29): 1835 ((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_rewrite(1716),rewrite(1793(3),1793(5),1821(4),1793(2),1793(4),1793(8),1793(10),1793(15))]. given #177 (F,wt=11): 2494 x ^ ((y v (z v x)) v u) = x. [para(2449(a,1),1953(a,1,2))]. given #178 (F,wt=11): 2530 x ^ (y v ((x v z) v u)) = x. [para(2492(a,1),1838(a,1,1)),rewrite(2492(7))]. given #179 (T,wt=11): 2532 (x v y) ^ (x ^ z) = x ^ z. [para(2339(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): 1839 x ^ (y v ((z v x) ^ (x v u))) = x. [back_rewrite(1706),rewrite(1793(1),1793(1),1793(2),1821(2),1793(2),1793(3),1821(3),1793(6))]. given #182 (F,wt=11): 2536 (x v (y v (z v u))) ^ z = z. [para(2368(a,1),2443(a,1,2)),rewrite(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)),rewrite(2449(5))]. given #185 (T,wt=11): 2580 x v (y ^ (z ^ (x ^ u))) = x. [para(2555(a,1),2446(a,1,1)),rewrite(2555(7))]. given #186 (A,wt=21): 1842 (x v (((x ^ y) v x) ^ z)) ^ (u v ((v v x) ^ (x v w))) = x. [back_rewrite(1702),rewrite(1793(1),1793(2),1821(2),1793(1),1793(5),1793(6),1793(10))]. given #187 (F,wt=11): 2592 x v (y ^ (z ^ (u ^ x))) = x. [para(2558(a,1),2446(a,1,1)),rewrite(2558(7))]. given #188 (F,wt=11): 2598 (x v y) v (x ^ z) = x v y. [para(2457(a,1),2572(a,1,2,1))]. given #189 (T,wt=11): 2605 x v (y ^ ((x ^ z) ^ u)) = x. [para(2572(a,1),2446(a,1,1)),rewrite(2572(7))]. given #190 (T,wt=11): 2634 x v (y ^ ((z ^ x) ^ u)) = x. [para(2585(a,1),2446(a,1,1)),rewrite(2585(7))]. given #191 (A,wt=31): 1844 ((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_rewrite(1700),rewrite(1793(3),1793(5),1821(4),1793(4),1793(9),1793(11),1793(16))]. given #192 (F,wt=11): 2638 x v ((y ^ (x ^ z)) ^ u) = x. [para(2555(a,1),2448(a,1,1)),rewrite(2555(7))]. given #193 (F,wt=11): 2639 x v ((y ^ (z ^ x)) ^ u) = x. [para(2558(a,1),2448(a,1,1)),rewrite(2558(7))]. given #194 (T,wt=11): 2640 x v (((x ^ y) ^ z) ^ u) = x. [para(2572(a,1),2448(a,1,1)),rewrite(2572(7))]. given #195 (T,wt=11): 2641 x v (((y ^ x) ^ z) ^ u) = x. [para(2585(a,1),2448(a,1,1)),rewrite(2585(7))]. given #196 (A,wt=25): 1850 ((x ^ y) v ((((x ^ y) ^ z) v (u ^ (x ^ y))) ^ v)) ^ (w v y) = x ^ y. [back_rewrite(1693),rewrite(1793(3),1793(5),1821(4),1793(4),1793(6),1793(9),1793(13))]. given #197 (F,wt=11): 2643 (x v ((y v z) v u)) ^ z = z. [para(2489(a,1),2455(a,1,2)),rewrite(2489(7))]. given #198 (F,wt=11): 2644 (x v ((y v z) v u)) ^ y = y. [para(2492(a,1),2455(a,1,2)),rewrite(2492(7))]. given #199 (T,wt=11): 2667 ((x v (y v z)) v u) ^ z = z. [para(2449(a,1),2459(a,1,1))]. given #200 (T,wt=11): 2676 x ^ (((y v x) v z) v u) = x. [para(2489(a,1),2490(a,1,1)),rewrite(2489(7))]. given #201 (A,wt=17): 1855 (x v (((x ^ y) v (z ^ x)) ^ u)) ^ (v v x) = x. [back_rewrite(1685),rewrite(1793(1),1793(2),1821(2),1793(1),1793(2),1793(6),1793(7),1821(7),1793(8))]. given #202 (F,wt=11): 2677 x ^ (((x v y) v z) v u) = x. [para(2492(a,1),2490(a,1,1)),rewrite(2492(7))]. given #203 (F,wt=11): 2742 ((x v (y v z)) v u) ^ y = y. [para(2458(a,1),2532(a,1,2)),rewrite(2458(7))]. given #204 (T,wt=11): 2743 (((x v y) v z) v u) ^ y = y. [para(2495(a,1),2532(a,1,2)),rewrite(2495(7))]. given #205 (T,wt=11): 2744 (((x v y) v z) v u) ^ x = x. [para(2496(a,1),2532(a,1,2)),rewrite(2496(7))]. given #206 (A,wt=29): 1872 (x v (((((x ^ y) v (z ^ x)) ^ u) v (v ^ x)) ^ w)) ^ (v6 v ((v7 v x) ^ (x v v8))) = x. [back_rewrite(1660),rewrite(1793(1),1793(2),1821(2),1793(1),1793(1),1793(2),1793(5),1793(9),1793(10),1793(14))]. given #207 (F,wt=11): 2752 x ^ ((y v x) ^ (x v z)) = x. [para(1793(a,1),1839(a,1,2))]. ============================== PROOF ================================= % Proof 3 at 2.41 (+ 0.01) seconds: McKenzie_4. % Length of proof is 58. % Level of proof is 29. % Maximum clause weight is 89. % Given clauses 207. 4 ((x v y) ^ (y v z)) ^ y = y # answer(McKenzie_4) # label(goal). [goal]. 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [assumption]. 9 ((c10 v c11) ^ (c11 v c12)) ^ c11 != c11 # answer(McKenzie_4). [deny(4)]. 10 (((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(5(a,1),5(a,1,1,2,1,1))]. 12 (((x v y) ^ y) v (y v y)) ^ (z v ((u v y) ^ (y v v))) = y. [para(5(a,1),5(a,1,1,2))]. 13 (((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(5(a,1),5(a,1,2,2))]. 16 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (z v y) = y v y. [para(12(a,1),12(a,1,2,2))]. 17 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v ((w v y) ^ (y v v6))) = y. [para(16(a,1),5(a,1,1,2,1,1))]. 23 (((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(12(a,1),17(a,1,2,2))]. 27 (((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(16(a,1),23(a,1,1,2,1,2))]. 29 (((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(5(a,1),10(a,1,1,2))]. 33 (((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(17(a,1),10(a,1,1,1,1,2)),rewrite(17(17),17(22),17(26),17(27),17(31))]. 43 (((x v y) ^ y) v (z ^ y)) ^ (u v ((v v y) ^ (y v w))) = y. [para(5(a,1),33(a,1,1,2))]. 56 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(12(a,1),43(a,1,2,2))]. 66 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (v v z) = y ^ z. [para(43(a,1),43(a,1,2,2))]. 68 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(16(a,1),56(a,1,1,2))]. 79 ((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(68(a,1),12(a,1,1,1))]. 91 ((x v x) v (y ^ (x v x))) ^ (z v x) = x v x. [para(68(a,1),56(a,1,1,1))]. 93 ((x v x) v (x v x)) ^ (y v x) = x v x. [para(68(a,1),68(a,1,1,1))]. 102 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(13(a,1),91(a,1,1,2))]. 111 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(66(a,1),56(a,1,1,2))]. 147 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(66(a,1),102(a,1,1,2,1,1))]. 170 ((x v x) v x) ^ (y v x) = x v x. [para(5(a,1),147(a,1,1,2))]. 184 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(170(a,1),5(a,1,2,2))]. 604 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(66(a,1),184(a,1,1,2,1,1))]. 623 (((x v y) ^ y) v y) ^ (z v (y v y)) = y. [para(5(a,1),604(a,1,1,2))]. 651 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(623(a,1),12(a,1,2,2))]. 656 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(623(a,1),43(a,1,2,2))]. 669 (x v ((((x v x) v (x v x)) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [para(651(a,1),23(a,1,1,1))]. 671 (x v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (z v x) = x v x. [para(651(a,1),27(a,1,1,1))]. 681 (x v (x v x)) ^ (y v x) = x v x. [para(651(a,1),68(a,1,1,1))]. 682 (x v x) v (x v x) = x v x. [para(68(a,1),651(a,1,1,1)),rewrite(681(8))]. 688 (x v (y ^ x)) ^ (z v x) = x v x. [para(651(a,1),111(a,1,1,1))]. 745 (x v ((x v x) ^ y)) ^ (z v x) = x v x. [back_rewrite(671),rewrite(682(3),682(3))]. 747 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [back_rewrite(669),rewrite(682(3))]. 791 (x v x) ^ (y v x) = x v x. [back_rewrite(93),rewrite(682(3))]. 796 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_rewrite(79),rewrite(682(4),682(3))]. 1015 ((x v x) v ((x v x) ^ y)) ^ (z v (x v x)) = x v x. [para(682(a,1),745(a,1,1,2,1)),rewrite(682(10))]. 1453 ((((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(43(a,1),1015(a,1,1,2))]. 1648 (x v (((x v x) v x) ^ y)) ^ (z v x) = x v x. [para(651(a,1),747(a,1,1,2,1,2))]. 1704 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(682(a,1),796(a,1,2,2,1))]. 1706 (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(29(a,1),796(a,1,2,2))]. 1744 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(43(a,1),1704(a,1,2,2)),rewrite(656(7)),flip(a)]. 1793 x v x = x. [back_rewrite(1453),rewrite(1744(5),1744(6),791(3),1744(6))]. 1821 (x v y) ^ y = y. [back_rewrite(1744),rewrite(1793(5))]. 1839 x ^ (y v ((z v x) ^ (x v u))) = x. [back_rewrite(1706),rewrite(1793(1),1793(1),1793(2),1821(2),1793(2),1793(3),1821(3),1793(6))]. 1840 x ^ (y v (x ^ (x v z))) = x. [back_rewrite(1704),rewrite(1793(1),1793(1),1793(1),1793(5))]. 1882 (x v (x ^ y)) ^ (z v x) = x. [back_rewrite(1648),rewrite(1793(1),1793(1),1793(5))]. 2201 (x v (y ^ x)) ^ (z v x) = x. [back_rewrite(688),rewrite(1793(5))]. 2333 x ^ (x ^ (x v y)) = x. [para(1793(a,1),1840(a,1,2))]. 2339 x v (x ^ y) = x. [para(1882(a,1),1840(a,1,2,2)),rewrite(1882(4)),flip(a)]. 2340 x ^ (x ^ y) = x ^ y. [para(2339(a,1),1821(a,1,1))]. 2344 x ^ (x v y) = x. [back_rewrite(2333),rewrite(2340(3))]. 2376 x v (y ^ x) = x. [para(2201(a,1),2344(a,1)),flip(a)]. 2443 x ^ (y ^ x) = y ^ x. [para(2376(a,1),1821(a,1,1))]. 2752 x ^ ((y v x) ^ (x v z)) = x. [para(1793(a,1),1839(a,1,2))]. 3224 ((x v y) ^ (y v z)) ^ y = y. [para(2752(a,1),2443(a,1,2)),rewrite(2752(8))]. 3225 $F # answer(McKenzie_4). [resolve(3224,a,9,a)]. ============================== end of proof ========================== % Redundant proof: 3252 $F # answer(McKenzie_4). [back_rewrite(9),rewrite(3224(9)),xx(a)]. % Disable descendants (x means already disabled): 9x given #208 (F,wt=11): 2825 x v (((x ^ y) v x) ^ z) = x. [para(1842(a,1),2344(a,1)),flip(a)]. given #209 (T,wt=9): 3254 x v ((x ^ y) v x) = x. [para(1756(a,1),2825(a,1,2))]. given #210 (T,wt=7): 3294 (x ^ y) v x = x. [para(3254(a,1),1756(a,1,2)),rewrite(1821(3)),flip(a)]. given #211 (A,wt=33): 1873 ((x ^ y) v (((((z ^ (x ^ y)) v (u ^ (x ^ y))) ^ v) v (w ^ (x ^ y))) ^ v6)) ^ (v7 v x) = x ^ y. [back_rewrite(1657),rewrite(1793(1),1793(1),1793(3),1793(3),1821(4),1793(2),1793(2),1793(3),1793(3),1793(4),1793(4),1793(4),1793(8),1793(8),1793(13),1793(15),1793(15))]. given #212 (F,wt=7): 3315 (x ^ y) v y = y. [para(2443(a,1),3294(a,1,1))]. given #213 (F,wt=9): 3314 x v (y v x) = y v x. [para(1821(a,1),3294(a,1,1))]. given #214 (T,wt=9): 3316 x v (x v y) = x v y. [para(2457(a,1),3294(a,1,1))]. given #215 (T,wt=9): 3370 (x ^ (y ^ z)) v y = y. [para(2555(a,1),3314(a,1,2)),rewrite(2555(6))]. given #216 (A,wt=13): 1874 (x ^ y) ^ (z v (u v x)) = x ^ y. [back_rewrite(1656),rewrite(1793(1),1793(1),1793(3),1793(3),1821(4),1793(2),1793(2),1793(3),1793(3),1793(4),1793(3),1793(2),1793(5),1793(5))]. given #217 (F,wt=9): 3371 (x ^ (y ^ z)) v z = z. [para(2558(a,1),3314(a,1,2)),rewrite(2558(6))]. given #218 (F,wt=9): 3372 ((x ^ y) ^ z) v x = x. [para(2572(a,1),3314(a,1,2)),rewrite(2572(6))]. given #219 (T,wt=9): 3373 ((x ^ y) ^ z) v y = y. [para(2585(a,1),3314(a,1,2)),rewrite(2585(6))]. given #220 (T,wt=11): 3224 ((x v y) ^ (y v z)) ^ y = y. [para(2752(a,1),2443(a,1,2)),rewrite(2752(8))]. given #221 (A,wt=33): 1877 ((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_rewrite(1653),rewrite(1793(1),1793(3),1821(4),1793(2),1793(3),1793(4),1793(4),1793(4),1793(8),1793(10),1793(15))]. given #222 (F,wt=11): 3226 x ^ ((x v y) ^ (x v z)) = x. [para(2449(a,1),2752(a,1,2,1))]. given #223 (F,wt=11): 3321 (x ^ y) v (z v y) = z v y. [para(2455(a,1),3294(a,1,1))]. given #224 (T,wt=11): 3322 (x ^ y) v (z v x) = z v x. [para(2456(a,1),3294(a,1,1))]. given #225 (T,wt=11): 3324 (x ^ y) v (x v z) = x v z. [para(2532(a,1),3294(a,1,1))]. given #226 (A,wt=49): 1881 (((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_rewrite(1649),rewrite(1793(10),1793(27))]. given #227 (F,wt=11): 3325 (x ^ y) v (y v z) = y v z. [para(2533(a,1),3294(a,1,1))]. given #228 (F,wt=11): 3375 (x ^ (y ^ (z ^ u))) v z = z. [para(2580(a,1),3314(a,1,2)),rewrite(2580(8))]. given #229 (T,wt=11): 3376 (x ^ (y ^ (z ^ u))) v u = u. [para(2592(a,1),3314(a,1,2)),rewrite(2592(8))]. given #230 (T,wt=11): 3377 (x ^ ((y ^ z) ^ u)) v y = y. [para(2605(a,1),3314(a,1,2)),rewrite(2605(8))]. given #231 (A,wt=21): 1885 (x v ((x v (((y ^ x) v (z ^ x)) ^ u)) ^ v)) ^ (w v x) = x. [back_rewrite(1645),rewrite(1793(1),1793(1),1793(10))]. given #232 (F,wt=11): 3378 (x ^ ((y ^ z) ^ u)) v z = z. [para(2634(a,1),3314(a,1,2)),rewrite(2634(8))]. given #233 (F,wt=11): 3379 ((x ^ (y ^ z)) ^ u) v y = y. [para(2638(a,1),3314(a,1,2)),rewrite(2638(8))]. given #234 (T,wt=11): 3380 ((x ^ (y ^ z)) ^ u) v z = z. [para(2639(a,1),3314(a,1,2)),rewrite(2639(8))]. given #235 (T,wt=11): 3381 (((x ^ y) ^ z) ^ u) v x = x. [para(2640(a,1),3314(a,1,2)),rewrite(2640(8))]. given #236 (A,wt=23): 1889 (((x ^ y) v (z ^ x)) ^ u) ^ (v v x) = ((x ^ y) v (z ^ x)) ^ u. [back_rewrite(1641),rewrite(1793(1),1793(1),1793(2),1793(6),1793(6),1793(7),1821(10),1793(5),1793(5),1793(6),1793(9),1793(9),1793(10),1793(13),1793(9),1793(5),1793(7),1793(7),1793(8))]. given #237 (F,wt=11): 3382 (((x ^ y) ^ z) ^ u) v y = y. [para(2641(a,1),3314(a,1,2)),rewrite(2641(8))]. given #238 (F,wt=11): 3383 x ^ ((y v x) ^ (z v x)) = x. [para(3314(a,1),2752(a,1,2,2))]. given #239 (T,wt=11): 3451 ((x v y) ^ (x v z)) ^ x = x. [para(2449(a,1),3224(a,1,1,1))]. given #240 (T,wt=11): 3470 ((x v y) ^ (z v y)) ^ y = y. [para(3314(a,1),3224(a,1,1,2))]. given #241 (A,wt=57): 1906 ((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_rewrite(1609),rewrite(1821(10),1793(26))]. given #242 (F,wt=11): 3551 x ^ ((x v y) ^ (z v x)) = x. [para(3314(a,1),3226(a,1,2,2))]. given #243 (F,wt=11): 3941 ((x v y) ^ (z v x)) ^ x = x. [para(3314(a,1),3451(a,1,1,2))]. given #244 (T,wt=13): 2003 (x ^ y) ^ (z v (u v y)) = x ^ y. [back_rewrite(1404),rewrite(1821(4),1793(3),1793(4))]. given #245 (T,wt=13): 2066 x ^ (y v (z v (u v (v v x)))) = x. [back_rewrite(1270),rewrite(1821(2),1793(1),1793(1))]. given #246 (A,wt=29): 1917 ((x v y) v (((x v y) v (((z ^ y) v (u ^ y)) ^ v)) ^ w)) ^ (v6 v (x v y)) = x v y. [back_rewrite(1592),rewrite(1821(4),1793(3),1793(12))]. given #247 (F,wt=13): 2342 (x ^ (y ^ z)) ^ y = x ^ (y ^ z). [para(2339(a,1),1838(a,1,2))]. given #248 (F,wt=13): 2343 ((x ^ y) ^ z) ^ x = (x ^ y) ^ z. [para(2339(a,1),1870(a,1,2))]. given #249 (T,wt=13): 2444 (x v (y v z)) v z = x v (y v z). [para(1841(a,1),2376(a,1,2))]. given #250 (T,wt=13): 2445 (x ^ (y ^ z)) ^ z = x ^ (y ^ z). [para(2376(a,1),1838(a,1,2))]. given #251 (A,wt=49): 1941 ((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_rewrite(1540),rewrite(1793(20),1793(28))]. given #252 (F,wt=13): 2447 ((x ^ y) ^ z) ^ y = (x ^ y) ^ z. [para(2376(a,1),1870(a,1,2))]. given #253 (F,wt=13): 2450 (x v (y v z)) v y = x v (y v z). [para(2361(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): 1945 ((x v y) v (((z ^ y) v (u ^ y)) ^ v)) ^ (w v (v6 v (v7 v (x v y)))) = x v y. [back_rewrite(1534),rewrite(1793(2),1793(9),1793(14))]. given #257 (F,wt=13): 2534 x ^ (y v (z v (u v (x v v)))) = x. [para(2368(a,1),1838(a,1,1)),rewrite(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): 1950 (((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_rewrite(1522),rewrite(1793(17),1793(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)),rewrite(2446(7))]. given #263 (F,wt=13): 2568 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(2555(a,1),1821(a,1,1))]. given #264 (T,wt=13): 2581 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(2558(a,1),1821(a,1,1))]. given #265 (T,wt=13): 2584 (x v y) v (z ^ (y ^ u)) = x v y. [para(1870(a,1),2558(a,1,2,2))]. given #266 (A,wt=21): 1956 (x v (((y ^ x) v (z ^ x)) ^ u)) ^ (v v (w v (v6 v x))) = x. [back_rewrite(1513),rewrite(1793(1),1793(6),1793(10))]. given #267 (F,wt=13): 2593 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(2572(a,1),1821(a,1,1))]. given #268 (F,wt=13): 2623 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(2585(a,1),1821(a,1,1))]. given #269 (T,wt=13): 2625 (x v y) v ((z ^ y) ^ u) = x v y. [para(1838(a,1),2585(a,1,2,1))]. given #270 (T,wt=13): 2627 (x v y) v ((y ^ z) ^ u) = x v y. [para(1870(a,1),2585(a,1,2,1))]. given #271 (A,wt=39): 1960 ((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_rewrite(1494),rewrite(1793(3),1793(5),1821(4),1793(4),1793(6),1793(13),1793(15),1793(20))]. given #272 (F,wt=13): 2635 (x v (y v z)) ^ (z ^ u) = z ^ u. [para(2448(a,1),2454(a,1,1,2))]. given #273 (F,wt=13): 2636 (x ^ y) ^ ((z v x) v u) = x ^ y. [para(2448(a,1),2489(a,1,2,1))]. given #274 (T,wt=13): 2637 ((x v y) v z) ^ (y ^ u) = y ^ u. [para(2448(a,1),2495(a,1,1,1))]. given #275 (T,wt=13): 2642 (x v (y v (z v (u v v)))) ^ v = v. [para(1953(a,1),2455(a,1,2)),rewrite(1953(9))]. given #276 (A,wt=39): 1961 ((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_rewrite(1493),rewrite(1793(3),1793(5),1821(4),1793(4),1793(8),1793(13),1793(15),1793(20))]. given #277 (F,wt=13): 2645 (x v (y v (z v (u v v)))) ^ u = u. [para(2368(a,1),2455(a,1,2)),rewrite(2368(9))]. given #278 (F,wt=13): 2674 (x ^ y) ^ (z v (y v u)) = x ^ y. [para(2490(a,1),1838(a,1,1)),rewrite(2490(7))]. given #279 (T,wt=13): 2675 x ^ ((y v (z v (u v x))) v v) = x. [para(1953(a,1),2490(a,1,1)),rewrite(1953(9))]. given #280 (T,wt=13): 2678 x ^ ((y v (z v (x v u))) v v) = x. [para(2368(a,1),2490(a,1,1)),rewrite(2368(9))]. given #281 (A,wt=23): 1963 ((x v y) v (((z ^ (x v y)) v y) ^ u)) ^ (v v (x v y)) = x v y. [back_rewrite(1491),rewrite(1793(3),1793(5),1821(4),1793(4),1793(9),1793(12))]. given #282 (F,wt=13): 2679 (x v y) v (z ^ (u ^ x)) = x v y. [para(2490(a,1),2558(a,1,2,2))]. given #283 (F,wt=13): 2680 (x v y) v ((z ^ x) ^ u) = x v y. [para(2490(a,1),2585(a,1,2,1))]. given #284 (T,wt=13): 2681 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(2490(a,1),2455(a,1,2)),rewrite(2490(7))]. given #285 (T,wt=13): 2682 (x ^ y) ^ ((y v z) v u) = x ^ y. [para(2490(a,1),2490(a,1,1)),rewrite(2490(7))]. given #286 (A,wt=25): 1968 (((x ^ (y v z)) v z) ^ u) ^ (v v (y v z)) = ((x ^ (y v z)) v z) ^ u. [back_rewrite(1485),rewrite(1793(3),1793(8),1821(10),1793(7),1793(11),1793(13),1793(9),1793(7),1793(10))]. given #287 (F,wt=13): 2683 (x ^ y) ^ (z v (x v u)) = x ^ y. [para(2491(a,1),1838(a,1,1)),rewrite(2491(7))]. given #288 (F,wt=13): 2684 (x v y) v (z ^ (x ^ u)) = x v y. [para(2491(a,1),2558(a,1,2,2))]. given #289 (T,wt=13): 2685 (x v y) v ((x ^ z) ^ u) = x v y. [para(2491(a,1),2585(a,1,2,1))]. given #290 (T,wt=13): 2686 (x v (y v z)) ^ (y ^ u) = y ^ u. [para(2491(a,1),2455(a,1,2)),rewrite(2491(7))]. given #291 (A,wt=51): 1990 ((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_rewrite(1428),rewrite(1821(4),1793(4),1793(3))]. given #292 (F,wt=13): 2687 (x ^ y) ^ ((x v z) v u) = x ^ y. [para(2491(a,1),2490(a,1,1)),rewrite(2491(7))]. given #293 (F,wt=13): 2688 x ^ (y v (z v ((u v x) v v))) = x. [para(2493(a,1),1838(a,1,1)),rewrite(2493(9))]. given #294 (T,wt=13): 2698 (x v (y v ((z v u) v v))) ^ u = u. [para(2493(a,1),2455(a,1,2)),rewrite(2493(9))]. given #295 (T,wt=13): 2699 x ^ ((y v ((z v x) v u)) v v) = x. [para(2493(a,1),2490(a,1,1)),rewrite(2493(9))]. given #296 (A,wt=35): 2002 (((((x ^ y) v (z ^ y)) ^ u) v (v ^ y)) ^ w) ^ (v6 v y) = ((((x ^ y) v (z ^ y)) ^ u) v (v ^ y)) ^ w. [back_rewrite(1407),rewrite(1793(1),1793(9),1821(16),1793(8),1793(15),1793(10))]. given #297 (F,wt=13): 2723 x ^ (y v ((z v (u v x)) v v)) = x. [para(2494(a,1),1838(a,1,1)),rewrite(2494(9))]. given #298 (F,wt=13): 2734 (x v ((y v (z v u)) v v)) ^ u = u. [para(2494(a,1),2455(a,1,2)),rewrite(2494(9))]. given #299 (T,wt=13): 2735 x ^ (((y v (z v x)) v u) v v) = x. [para(2494(a,1),2490(a,1,1)),rewrite(2494(9))]. given #300 (T,wt=13): 2736 x ^ (y v (z v ((x v u) v v))) = x. [para(2530(a,1),1838(a,1,1)),rewrite(2530(9))]. given #301 (A,wt=23): 2004 (((x ^ y) v (z ^ y)) ^ u) ^ (v v y) = ((x ^ y) v (z ^ y)) ^ u. [back_rewrite(1401),rewrite(1821(10),1793(9),1793(5))]. given #302 (F,wt=13): 2740 (x v (y v ((z v u) v v))) ^ z = z. [para(2530(a,1),2455(a,1,2)),rewrite(2530(9))]. given #303 (F,wt=13): 2741 x ^ ((y v ((x v z) v u)) v v) = x. [para(2530(a,1),2490(a,1,1)),rewrite(2530(9))]. given #304 (T,wt=13): 2745 ((x v (y v (z v u))) v v) ^ u = u. [para(2459(a,1),2532(a,1,2)),rewrite(2459(9))]. given #305 (T,wt=13): 2746 ((x v y) v z) ^ (x ^ u) = x ^ u. [para(2532(a,1),2532(a,1,2)),rewrite(2532(7))]. given #306 (A,wt=53): 2005 (((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_rewrite(1392),rewrite(1821(8),1793(25))]. given #307 (F,wt=13): 2747 ((x v (y v (z v u))) v v) ^ z = z. [para(2368(a,1),2533(a,1,2)),rewrite(2368(9))]. given #308 (F,wt=13): 2748 ((x v y) v z) ^ (u ^ x) = u ^ x. [para(2490(a,1),2533(a,1,2)),rewrite(2490(7))]. given #309 (T,wt=13): 2749 ((x v ((y v z) v u)) v v) ^ z = z. [para(2493(a,1),2533(a,1,2)),rewrite(2493(9))]. given #310 (T,wt=13): 2750 (((x v (y v z)) v u) v v) ^ z = z. [para(2494(a,1),2533(a,1,2)),rewrite(2494(9))]. given #311 (A,wt=25): 2007 (x v (((((y ^ x) v (z ^ x)) ^ u) v (v ^ x)) ^ w)) ^ (v6 v (v7 v x)) = x. [back_rewrite(1389),rewrite(1821(2),1793(1),1793(11))]. given #312 (F,wt=13): 2751 ((x v ((y v z) v u)) v v) ^ y = y. [para(2530(a,1),2533(a,1,2)),rewrite(2530(9))]. given #313 (F,wt=13): 2756 (x v ((y v z) ^ (z v u))) ^ z = z. [para(1839(a,1),2443(a,1,2)),rewrite(1839(10))]. given #314 (T,wt=13): 2757 x ^ (y v ((x v z) ^ (x v u))) = x. [para(2449(a,1),1839(a,1,2,2,1))]. given #315 (T,wt=13): 2758 x ^ (((y v x) ^ (x v z)) v u) = x. [para(2449(a,1),1839(a,1,2))]. given #316 (A,wt=49): 2010 ((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_rewrite(1385),rewrite(1821(10),1793(13),1793(23))]. given #317 (F,wt=13): 2772 x ^ (y v ((z v (x v u)) v v)) = x. [para(2537(a,1),1838(a,1,1)),rewrite(2537(9))]. given #318 (F,wt=13): 2777 (x v ((y v (z v u)) v v)) ^ z = z. [para(2537(a,1),2455(a,1,2)),rewrite(2537(9))]. given #319 (T,wt=13): 2778 x ^ (((y v (x v z)) v u) v v) = x. [para(2537(a,1),2490(a,1,1)),rewrite(2537(9))]. given #320 (T,wt=13): 2779 (((x v (y v z)) v u) v v) ^ y = y. [para(2537(a,1),2533(a,1,2)),rewrite(2537(9))]. given #321 (A,wt=35): 2022 (((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_rewrite(1364),rewrite(1793(7),1793(11),1821(8),1793(10),1793(13),1793(20))]. given #322 (F,wt=13): 2805 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(2580(a,1),2446(a,1,1)),rewrite(2580(9))]. given #323 (F,wt=13): 2806 x v ((y ^ (z ^ (x ^ u))) ^ v) = x. [para(2580(a,1),2448(a,1,1)),rewrite(2580(9))]. given #324 (T,wt=13): 2842 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(2592(a,1),2446(a,1,1)),rewrite(2592(9))]. given #325 (T,wt=13): 2843 x v ((y ^ (z ^ (u ^ x))) ^ v) = x. [para(2592(a,1),2448(a,1,1)),rewrite(2592(9))]. given #326 (A,wt=33): 2023 ((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_rewrite(1363),rewrite(1793(1),1793(3),1821(4),1793(2),1793(3),1793(4),1793(6),1793(8),1793(10),1793(15))]. given #327 (F,wt=13): 2871 x v (y ^ (z ^ ((x ^ u) ^ v))) = x. [para(2605(a,1),2446(a,1,1)),rewrite(2605(9))]. given #328 (F,wt=13): 2872 x v ((y ^ ((x ^ z) ^ u)) ^ v) = x. [para(2605(a,1),2448(a,1,1)),rewrite(2605(9))]. given #329 (T,wt=13): 2892 x v (y ^ (z ^ ((u ^ x) ^ v))) = x. [para(2634(a,1),2446(a,1,1)),rewrite(2634(9))]. given #330 (T,wt=13): 2893 x v ((y ^ ((z ^ x) ^ u)) ^ v) = x. [para(2634(a,1),2448(a,1,1)),rewrite(2634(9))]. given #331 (A,wt=63): 2030 ((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_rewrite(1348),rewrite(1793(1),1793(5),1821(8),1793(4),1793(4),1793(10),1793(17),1793(21),1793(28))]. given #332 (F,wt=13): 2942 x v (y ^ ((z ^ (x ^ u)) ^ v)) = x. [para(2638(a,1),2446(a,1,1)),rewrite(2638(9))]. given #333 (F,wt=13): 2943 x v (((y ^ (x ^ z)) ^ u) ^ v) = x. [para(2638(a,1),2448(a,1,1)),rewrite(2638(9))]. given #334 (T,wt=13): 2963 x v (y ^ ((z ^ (u ^ x)) ^ v)) = x. [para(2639(a,1),2446(a,1,1)),rewrite(2639(9))]. given #335 (T,wt=13): 2964 x v (((y ^ (z ^ x)) ^ u) ^ v) = x. [para(2639(a,1),2448(a,1,1)),rewrite(2639(9))]. given #336 (A,wt=47): 2031 ((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_rewrite(1347),rewrite(1793(1),1793(6),1821(10),1793(5),1793(10),1793(13),1793(17),1793(21),1793(19))]. given #337 (F,wt=13): 2987 x v (y ^ (((x ^ z) ^ u) ^ v)) = x. [para(2640(a,1),2446(a,1,1)),rewrite(2640(9))]. given #338 (F,wt=13): 2988 x v ((((x ^ y) ^ z) ^ u) ^ v) = x. [para(2640(a,1),2448(a,1,1)),rewrite(2640(9))]. given #339 (T,wt=13): 3008 x v (y ^ (((z ^ x) ^ u) ^ v)) = x. [para(2641(a,1),2446(a,1,1)),rewrite(2641(9))]. given #340 (T,wt=13): 3009 x v ((((y ^ x) ^ z) ^ u) ^ v) = x. [para(2641(a,1),2448(a,1,1)),rewrite(2641(9))]. given #341 (A,wt=47): 2032 ((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_rewrite(1346),rewrite(1793(1),1793(6),1821(10),1793(5),1793(5),1793(13),1793(17),1793(21),1793(19))]. given #342 (F,wt=13): 3071 x ^ (y v (((z v x) v u) v v)) = x. [para(2676(a,1),1838(a,1,1)),rewrite(2676(9))]. given #343 (F,wt=13): 3081 (x v (((y v z) v u) v v)) ^ z = z. [para(2676(a,1),2455(a,1,2)),rewrite(2676(9))]. given #344 (T,wt=13): 3082 x ^ ((((y v x) v z) v u) v v) = x. [para(2676(a,1),2490(a,1,1)),rewrite(2676(9))]. given #345 (T,wt=13): 3083 ((((x v y) v z) v u) v v) ^ y = y. [para(2676(a,1),2533(a,1,2)),rewrite(2676(9))]. given #346 (A,wt=15): 2036 x ^ (y v (z v (u v (v v (w v x))))) = x. [back_rewrite(1339),rewrite(1793(1),1793(2),1821(2),1793(1),1793(1),1793(1),1793(7))]. given #347 (F,wt=13): 3103 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(1855(a,1),2344(a,1)),flip(a)]. given #348 (F,wt=11): 9112 x v ((x ^ y) v (z ^ x)) = x. [para(1756(a,1),3103(a,1,2))]. given #349 (T,wt=11): 9271 x v ((x ^ y) v (x ^ z)) = x. [para(2335(a,1),9112(a,1,2,2))]. given #350 (T,wt=11): 9276 x v ((y ^ x) v (z ^ x)) = x. [para(2443(a,1),9112(a,1,2,1))]. given #351 (A,wt=41): 2046 (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_rewrite(1317),rewrite(1821(2),1793(1))]. given #352 (F,wt=11): 9320 ((x ^ y) v (z ^ x)) v x = x. [para(9112(a,1),3314(a,1,2)),rewrite(9112(8))]. given #353 (F,wt=11): 9432 x v ((y ^ x) v (x ^ z)) = x. [para(2443(a,1),9271(a,1,2,1))]. ============================== PROOF ================================= % Proof 4 at 4.36 (+ 0.03) seconds: McKenzie_3. % Length of proof is 76. % Level of proof is 31. % Maximum clause weight is 89. % Given clauses 353. 3 ((x ^ y) v (y ^ z)) v y = y # answer(McKenzie_3) # label(goal). [goal]. 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v ((v6 v y) ^ (y v v7))) = y # label(A1). [assumption]. 8 ((c7 ^ c8) v (c8 ^ c9)) v c8 != c8 # answer(McKenzie_3). [deny(3)]. 10 (((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(5(a,1),5(a,1,1,2,1,1))]. 12 (((x v y) ^ y) v (y v y)) ^ (z v ((u v y) ^ (y v v))) = y. [para(5(a,1),5(a,1,1,2))]. 13 (((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(5(a,1),5(a,1,2,2))]. 16 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (z v y) = y v y. [para(12(a,1),12(a,1,2,2))]. 17 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (v v ((w v y) ^ (y v v6))) = y. [para(16(a,1),5(a,1,1,2,1,1))]. 23 (((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(12(a,1),17(a,1,2,2))]. 27 (((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(16(a,1),23(a,1,1,2,1,2))]. 29 (((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(5(a,1),10(a,1,1,2))]. 33 (((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(17(a,1),10(a,1,1,1,1,2)),rewrite(17(17),17(22),17(26),17(27),17(31))]. 43 (((x v y) ^ y) v (z ^ y)) ^ (u v ((v v y) ^ (y v w))) = y. [para(5(a,1),33(a,1,1,2))]. 47 (((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(16(a,1),33(a,1,1,2,1,1,1,2))]. 56 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(12(a,1),43(a,1,2,2))]. 66 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (v v z) = y ^ z. [para(43(a,1),43(a,1,2,2))]. 68 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(16(a,1),56(a,1,1,2))]. 79 ((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(68(a,1),12(a,1,1,1))]. 91 ((x v x) v (y ^ (x v x))) ^ (z v x) = x v x. [para(68(a,1),56(a,1,1,1))]. 93 ((x v x) v (x v x)) ^ (y v x) = x v x. [para(68(a,1),68(a,1,1,1))]. 102 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(13(a,1),91(a,1,1,2))]. 104 (((x v y) ^ y) v (z ^ y)) ^ (u v (v v ((w v y) ^ (y v v6)))) = y. [para(5(a,1),66(a,1,1,1,1,2)),rewrite(5(14),5(15),5(23))]. 111 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(66(a,1),56(a,1,1,2))]. 147 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (v v x) = x v x. [para(66(a,1),102(a,1,1,2,1,1))]. 170 ((x v x) v x) ^ (y v x) = x v x. [para(5(a,1),147(a,1,1,2))]. 184 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(170(a,1),5(a,1,2,2))]. 604 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ (w v (y v y)) = y. [para(66(a,1),184(a,1,1,2,1,1))]. 623 (((x v y) ^ y) v y) ^ (z v (y v y)) = y. [para(5(a,1),604(a,1,1,2))]. 651 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(623(a,1),12(a,1,2,2))]. 656 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(623(a,1),43(a,1,2,2))]. 669 (x v ((((x v x) v (x v x)) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [para(651(a,1),23(a,1,1,1))]. 671 (x v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (z v x) = x v x. [para(651(a,1),27(a,1,1,1))]. 681 (x v (x v x)) ^ (y v x) = x v x. [para(651(a,1),68(a,1,1,1))]. 682 (x v x) v (x v x) = x v x. [para(68(a,1),651(a,1,1,1)),rewrite(681(8))]. 688 (x v (y ^ x)) ^ (z v x) = x v x. [para(651(a,1),111(a,1,1,1))]. 738 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ (v v (y v y)) = y. [para(651(a,1),184(a,1,1,2,1,1))]. 745 (x v ((x v x) ^ y)) ^ (z v x) = x v x. [back_rewrite(671),rewrite(682(3),682(3))]. 747 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (u v x) = x v x. [back_rewrite(669),rewrite(682(3))]. 791 (x v x) ^ (y v x) = x v x. [back_rewrite(93),rewrite(682(3))]. 796 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_rewrite(79),rewrite(682(4),682(3))]. 919 (((x v y) ^ y) v y) ^ (z v ((u v y) ^ (y v v))) = y. [para(43(a,1),29(a,1,1,1,1,2)),rewrite(43(13),43(15),43(16),43(20))]. 1015 ((x v x) v ((x v x) ^ y)) ^ (z v (x v x)) = x v x. [para(682(a,1),745(a,1,1,2,1)),rewrite(682(10))]. 1453 ((((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(43(a,1),1015(a,1,1,2))]. 1604 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ (y v y) = y. [para(682(a,1),738(a,1,2))]. 1648 (x v (((x v x) v x) ^ y)) ^ (z v x) = x v x. [para(651(a,1),747(a,1,1,2,1,2))]. 1662 (((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(1648(a,1),919(a,1,2,2))]. 1685 (((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(682(a,1),47(a,1,2,2,2)),rewrite(682(7),682(7))]. 1702 (((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(1604(a,1),47(a,1,1,2,1,2)),rewrite(682(7),682(7))]. 1704 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(682(a,1),796(a,1,2,2,1))]. 1744 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(43(a,1),1704(a,1,2,2)),rewrite(656(7)),flip(a)]. 1756 x ^ (y v x) = x. [para(104(a,1),1704(a,1,2,2)),rewrite(1744(5),1744(7))]. 1793 x v x = x. [back_rewrite(1453),rewrite(1744(5),1744(6),791(3),1744(6))]. 1821 (x v y) ^ y = y. [back_rewrite(1744),rewrite(1793(5))]. 1840 x ^ (y v (x ^ (x v z))) = x. [back_rewrite(1704),rewrite(1793(1),1793(1),1793(1),1793(5))]. 1842 (x v (((x ^ y) v x) ^ z)) ^ (u v ((v v x) ^ (x v w))) = x. [back_rewrite(1702),rewrite(1793(1),1793(2),1821(2),1793(1),1793(5),1793(6),1793(10))]. 1855 (x v (((x ^ y) v (z ^ x)) ^ u)) ^ (v v x) = x. [back_rewrite(1685),rewrite(1793(1),1793(2),1821(2),1793(1),1793(2),1793(6),1793(7),1821(7),1793(8))]. 1870 (x ^ y) ^ (z v x) = x ^ y. [back_rewrite(1662),rewrite(1793(1),1793(1),1793(3),1793(3),1821(4),1793(2),1793(2),1793(3),1793(2),1793(4),1793(4))]. 1882 (x v (x ^ y)) ^ (z v x) = x. [back_rewrite(1648),rewrite(1793(1),1793(1),1793(5))]. 2201 (x v (y ^ x)) ^ (z v x) = x. [back_rewrite(688),rewrite(1793(5))]. 2333 x ^ (x ^ (x v y)) = x. [para(1793(a,1),1840(a,1,2))]. 2335 (x ^ y) ^ x = x ^ y. [para(1793(a,1),1870(a,1,2))]. 2339 x v (x ^ y) = x. [para(1882(a,1),1840(a,1,2,2)),rewrite(1882(4)),flip(a)]. 2340 x ^ (x ^ y) = x ^ y. [para(2339(a,1),1821(a,1,1))]. 2344 x ^ (x v y) = x. [back_rewrite(2333),rewrite(2340(3))]. 2376 x v (y ^ x) = x. [para(2201(a,1),2344(a,1)),flip(a)]. 2443 x ^ (y ^ x) = y ^ x. [para(2376(a,1),1821(a,1,1))]. 2825 x v (((x ^ y) v x) ^ z) = x. [para(1842(a,1),2344(a,1)),flip(a)]. 3103 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(1855(a,1),2344(a,1)),flip(a)]. 3254 x v ((x ^ y) v x) = x. [para(1756(a,1),2825(a,1,2))]. 3294 (x ^ y) v x = x. [para(3254(a,1),1756(a,1,2)),rewrite(1821(3)),flip(a)]. 3314 x v (y v x) = y v x. [para(1821(a,1),3294(a,1,1))]. 9112 x v ((x ^ y) v (z ^ x)) = x. [para(1756(a,1),3103(a,1,2))]. 9271 x v ((x ^ y) v (x ^ z)) = x. [para(2335(a,1),9112(a,1,2,2))]. 9432 x v ((y ^ x) v (x ^ z)) = x. [para(2443(a,1),9271(a,1,2,1))]. 10040 ((x ^ y) v (y ^ z)) v y = y. [para(9432(a,1),3314(a,1,2)),rewrite(9432(8))]. 10041 $F # answer(McKenzie_3). [resolve(10040,a,8,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=353. Generated=100723. Kept=10030. proofs=4. Usable=186. Sos=7012. Demods=7219. Limbo=22, Disabled=2814. Hints=0. Weight_deleted=7952. Literals_deleted=0. Forward_subsumed=82738. Back_subsumed=290. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=10025 (0 lex), Back_demodulated=2519. Back_unit_deleted=0. Demod_attempts=4195530. Demod_rewrites=281830. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=15.02. User_CPU=4.36, System_CPU=0.03, Wall_clock=5. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 4 proofs. Process 3829 exit (max_proofs) Wed Nov 22 11:23:58 2006