============================== Prover9 =============================== Prover9 (32) version 2009-02A, February 2009. Process 11586 was started by mccune on cleo, Wed Feb 25 09:32:41 2009 The command was "/home/mccune/bin/prover9 -f a1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file a1.in assign(max_seconds,30). 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(non_clause) # label(goal). [goal]. 2 y ^ (x v (y v z)) = y # answer(McKenzie_2) # label(non_clause) # label(goal). [goal]. 3 ((x ^ y) v (y ^ z)) v y = y # answer(McKenzie_3) # label(non_clause) # label(goal). [goal]. 4 ((x v y) ^ (y v z)) ^ y = y # answer(McKenzie_4) # label(non_clause) # 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)) ^ w)) ^ (v5 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: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 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) Auto_process settings: (no changes). kept: 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ w)) ^ (v5 v ((v6 v y) ^ (y v v7))) = y # label(A1). [assumption]. kept: 6 c1 v (c2 ^ (c1 ^ c3)) != c1 # answer(McKenzie_1). [deny(1)]. kept: 7 c4 ^ (c5 v (c4 v c6)) != c4 # answer(McKenzie_2). [deny(2)]. kept: 8 ((c7 ^ c8) v (c8 ^ c9)) v c8 != c8 # answer(McKenzie_3). [deny(3)]. kept: 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)) ^ w)) ^ (v5 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)) ^ w)) ^ (v5 v ((v6 v y) ^ (y v v7))) = y # label(A1). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=29): 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ w)) ^ (v5 v ((v6 v y) ^ (y v v7))) = y # label(A1). [assumption]. given #2 (A,wt=61): 10 (((x v ((y v z) ^ (z v u))) ^ ((y v z) ^ (z v u))) v ((z v (w ^ ((y v z) ^ (z v u)))) ^ v5)) ^ (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 #3 (T,wt=21): 12 (((x v y) ^ y) v (y v y)) ^ (z v ((u v y) ^ (y v w))) = y. [para(5(a,1),5(a,1,1,2))]. given #4 (T,wt=25): 22 (((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 #5 (T,wt=27): 20 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (w v ((v5 v y) ^ (y v v6))) = y. [para(12(a,1),10(a,1,1,1,1,2)),rewrite([12(11),12(13),12(17),12(18),12(22)])]. given #6 (T,wt=33): 27 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (w ^ y)) ^ v5)) ^ (v6 v ((v7 v y) ^ (y v v8))) = y. [para(20(a,1),10(a,1,1,1,1,2)),rewrite([20(17),20(22),20(26),20(27),20(31)])]. given #7 (A,wt=83): 11 (((x v (y v ((z v u) ^ (u v w)))) ^ (y v ((z v u) ^ (u v w)))) v (((v5 ^ ((y v ((z v u) ^ (u v w))) v (y v ((z v u) ^ (u v w))))) v u) ^ v6)) ^ (v7 v ((v8 v (y v ((z v u) ^ (u v w)))) ^ ((y v ((z v u) ^ (u v w))) v v9))) = y v ((z v u) ^ (u v w)). [para(5(a,1),5(a,1,1,2,1,2))]. given #8 (T,wt=21): 36 (((x v y) ^ y) v (z ^ y)) ^ (u v ((w v y) ^ (y v v5))) = y. [para(5(a,1),27(a,1,1,2))]. given #9 (T,wt=23): 58 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(12(a,1),36(a,1,2,2))]. given #10 (T,wt=21): 67 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(22(a,1),58(a,1,1,2))]. given #11 (T,wt=15): 82 ((x v x) v (x v x)) ^ (y v x) = x v x. [para(67(a,1),67(a,1,1,1))]. given #12 (A,wt=83): 13 (((x v (((y ^ (z v z)) v (u ^ z)) ^ w)) ^ (((y ^ (z v z)) v (u ^ z)) ^ w)) v (((v5 ^ ((((y ^ (z v z)) v (u ^ z)) ^ w) v (((y ^ (z v z)) v (u ^ z)) ^ w))) v (v6 ^ (((y ^ (z v z)) v (u ^ z)) ^ w))) ^ v7)) ^ (v8 v z) = ((y ^ (z v z)) v (u ^ z)) ^ w. [para(5(a,1),5(a,1,2,2))]. given #13 (T,wt=17): 81 ((x v x) v (y ^ (x v x))) ^ (z v x) = x v x. [para(67(a,1),58(a,1,1,1))]. given #14 (T,wt=19): 73 ((x v x) v ((x v x) v (x v x))) ^ (y v x) = x v x. [para(67(a,1),22(a,1,1,1))]. given #15 (T,wt=23): 65 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (w v z) = y ^ z. [para(36(a,1),36(a,1,2,2))]. given #16 (T,wt=15): 103 ((x v x) v (y ^ x)) ^ (z v x) = x v x. [para(65(a,1),81(a,1,1,2))]. given #17 (A,wt=35): 14 (((x v y) ^ y) v (((((z ^ (y v y)) v (u ^ y)) ^ w) v (v5 ^ 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 #18 (T,wt=21): 99 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(65(a,1),58(a,1,1,2))]. given #19 (T,wt=23): 91 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (w v x) = x v x. [para(13(a,1),81(a,1,1,2))]. given #20 (T,wt=21): 144 ((x v x) v (((x v x) v (y ^ x)) ^ z)) ^ (u v x) = x v x. [para(22(a,1),91(a,1,1,2,1,1))]. given #21 (T,wt=21): 151 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (w v x) = x v x. [para(65(a,1),91(a,1,1,2,1,1))]. given #22 (A,wt=89): 15 (((x v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) ^ ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) v u) ^ (v5 v ((v6 v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) ^ (((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w)) v v7))) = (y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w). [para(5(a,1),10(a,1,1,2))]. given #23 (T,wt=13): 169 ((x v x) v x) ^ (y v x) = x v x. [para(5(a,1),151(a,1,1,2))]. given #24 (T,wt=17): 205 (((x v y) ^ y) v (y v y)) ^ (z v (y v y)) = y. [para(169(a,1),12(a,1,2,2))]. given #25 (T,wt=17): 210 (((x v y) ^ y) v (z ^ y)) ^ (u v (y v y)) = y. [para(169(a,1),36(a,1,2,2))]. given #26 (T,wt=19): 193 (((x v y) ^ y) v y) ^ (z v ((u v y) ^ (y v w))) = y. [para(36(a,1),15(a,1,1,1,1,2)),rewrite([36(13),36(15),36(16),36(20)])]. given #27 (A,wt=77): 16 (((x v (((y ^ (z v z)) v (u ^ z)) ^ ((u ^ z) v w))) ^ (((y ^ (z v z)) v (u ^ z)) ^ ((u ^ z) v w))) v (((u ^ z) v (v5 ^ (((y ^ (z v z)) v (u ^ z)) ^ ((u ^ z) v w)))) ^ v6)) ^ (v7 v z) = ((y ^ (z v z)) v (u ^ z)) ^ ((u ^ z) v w). [para(5(a,1),10(a,1,2,2))]. given #28 (T,wt=13): 266 (((x v y) ^ y) v y) ^ (z v y) = y. [para(193(a,1),193(a,1,2,2))]. given #29 (T,wt=15): 245 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(193(a,1),12(a,1,2,2))]. given #30 (T,wt=11): 308 (x v x) v (x v x) = x v x. [para(67(a,1),245(a,1,1,1)),rewrite([307(8)])]. given #31 (T,wt=11): 322 (x v x) ^ (y v x) = x v x. [back_rewrite(82),rewrite([308(3)])]. given #32 (A,wt=73): 17 (((x v ((y v z) ^ (z v u))) ^ ((y v z) ^ (z v u))) v ((((z v (w ^ ((y v z) ^ (z v u)))) ^ v5) 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 #33 (T,wt=13): 307 (x v (x v x)) ^ (y v x) = x v x. [para(245(a,1),67(a,1,1,1))]. given #34 (T,wt=13): 309 (x v x) ^ (y v (x v x)) = x v x. [para(82(a,1),245(a,1,1,1)),rewrite([308(4),308(3)])]. given #35 (T,wt=13): 312 (x v (y ^ x)) ^ (z v x) = x v x. [para(245(a,1),99(a,1,1,1))]. given #36 (T,wt=15): 252 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(193(a,1),36(a,1,2,2))]. given #37 (A,wt=65): 19 (((x v (((y ^ (z v z)) v (u ^ z)) ^ w)) ^ (((y ^ (z v z)) v (u ^ z)) ^ w)) v ((((y ^ (z v z)) v (u ^ z)) ^ w) v (((y ^ (z v z)) v (u ^ z)) ^ w))) ^ (v5 v z) = ((y ^ (z v z)) v (u ^ z)) ^ w. [para(5(a,1),12(a,1,2,2))]. given #38 (T,wt=15): 265 (((x v y) ^ y) v y) ^ (z v (y v y)) = y. [para(169(a,1),193(a,1,2,2))]. given #39 (T,wt=15): 306 (x v (y ^ (x v x))) ^ (z v x) = x v x. [para(245(a,1),58(a,1,1,1))]. given #40 (T,wt=15): 314 (x v (x v x)) ^ (y v (x v x)) = x v x. [para(245(a,1),205(a,1,1,1)),rewrite([308(3),308(5)])]. given #41 (T,wt=17): 285 (((x v y) ^ y) v (z ^ y)) ^ (u v (w v y)) = y. [para(266(a,1),65(a,1,1,1,1,2)),rewrite([266(6),266(7),266(12)])]. given #42 (A,wt=81): 21 (((x v ((y v (z ^ ((u v y) ^ (y v w)))) ^ v5)) ^ ((y v (z ^ ((u v y) ^ (y v w)))) ^ v5)) v (((y v (z ^ ((u v y) ^ (y v w)))) ^ v5) v ((y v (z ^ ((u v y) ^ (y v w)))) ^ v5))) ^ (v6 v ((u v y) ^ (y v w))) = (y v (z ^ ((u v y) ^ (y v w)))) ^ v5. [para(10(a,1),12(a,1,2,2))]. given #43 (T,wt=17): 395 (x v (y ^ (x v x))) ^ (z v (x v x)) = x v x. [para(245(a,1),252(a,1,1,1))]. given #44 (T,wt=15): 460 (x v (y ^ x)) ^ (z v (x v x)) = x v x. [para(65(a,1),395(a,1,1,2))]. given #45 (T,wt=19): 280 (((x v (y v y)) ^ (y v y)) v y) ^ (z v y) = y v y. [para(266(a,1),58(a,1,1,2))]. given #46 (T,wt=19): 291 ((x v x) v ((x v (y ^ x)) ^ z)) ^ (u v x) = x v x. [para(266(a,1),91(a,1,1,2,1,1))]. given #47 (A,wt=43): 23 (((x v (y v z)) ^ (y v z)) v (((u ^ ((y v z) v (y v z))) v (z v z)) ^ w)) ^ (v5 v ((v6 v (y v z)) ^ ((y v z) v v7))) = y v z. [para(22(a,1),5(a,1,1,2,1,2))]. given #48 (T,wt=19): 356 ((x v x) v ((y ^ x) v (y ^ x))) ^ (z v x) = x v x. [para(322(a,1),151(a,1,1,2))]. given #49 (T,wt=19): 388 ((x v y) v y) ^ (z v (x v y)) = (x v y) v (x v y). [para(266(a,1),312(a,1,1,2))]. given #50 (T,wt=19): 419 (((x v y) ^ y) v (z ^ y)) ^ (u v (w v (v5 v y))) = y. [para(285(a,1),65(a,1,1,1,1,2)),rewrite([285(8),285(9),285(15)])]. given #51 (T,wt=19): 434 (x v (y ^ (x v x))) ^ (z v (u v (x v x))) = x v x. [para(245(a,1),285(a,1,1,1))]. given #52 (A,wt=71): 24 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v (((w ^ ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))) v (v5 ^ (((y v y) v (z ^ y)) ^ u))) ^ v6)) ^ (v7 v y) = ((y v y) v (z ^ y)) ^ u. [para(20(a,1),5(a,1,2,2))]. given #53 (T,wt=15): 587 (x v x) ^ (y v (z v (x v x))) = x v x. [para(266(a,1),434(a,1,1,2))]. given #54 (T,wt=17): 583 (x v (x v x)) ^ (y v (z v (x v x))) = x v x. [para(58(a,1),434(a,1,1,2))]. given #55 (T,wt=17): 585 (x v (y ^ x)) ^ (z v (u v (x v x))) = x v x. [para(65(a,1),434(a,1,1,2))]. given #56 (T,wt=17): 586 ((x v x) v x) ^ (y v (z v (x v x))) = x v x. [para(205(a,1),434(a,1,1,2)),rewrite([308(5),308(9)])]. given #57 (A,wt=81): 25 (((x v (y v ((z v u) ^ (u v w)))) ^ (y v ((z v u) ^ (u v w)))) v ((((y v ((z v u) ^ (u v w))) v (y v ((z v u) ^ (u v w)))) v u) ^ v5)) ^ (v6 v ((v7 v (y v ((z v u) ^ (u v w)))) ^ ((y v ((z v u) ^ (u v w))) v v8))) = y v ((z v u) ^ (u v w)). [para(5(a,1),20(a,1,1,2,1,2))]. given #58 (T,wt=19): 541 (((x v y) ^ y) v y) ^ (z v ((u v y) v (u v y))) = y. [para(388(a,1),193(a,1,2,2))]. given #59 (T,wt=17): 653 (((x v y) ^ y) v y) ^ ((z v y) v (z v y)) = y. [para(308(a,1),541(a,1,2))]. given #60 (T,wt=19): 615 (x v (((x v x) v (y ^ x)) ^ z)) ^ (u v x) = x v x. [para(24(a,1),306(a,1,1,2))]. given #61 (T,wt=21): 246 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (w v y) = y. [para(193(a,1),20(a,1,2,2))]. given #62 (A,wt=81): 26 (((x v (((y ^ (z v z)) v (u ^ z)) ^ w)) ^ (((y ^ (z v z)) v (u ^ z)) ^ w)) v ((((((y ^ (z v z)) v (u ^ z)) ^ w) v (((y ^ (z v z)) v (u ^ z)) ^ w)) v (v5 ^ (((y ^ (z v z)) v (u ^ z)) ^ w))) ^ v6)) ^ (v7 v z) = ((y ^ (z v z)) v (u ^ z)) ^ w. [para(5(a,1),20(a,1,2,2))]. given #63 (T,wt=21): 253 (((x v (y ^ z)) ^ (y ^ z)) v (y ^ z)) ^ (u v z) = y ^ z. [para(36(a,1),193(a,1,2,2))]. given #64 (T,wt=15): 716 (((x v y) ^ y) v y) ^ (z v (u v y)) = y. [para(266(a,1),253(a,1,1,1,1,2)),rewrite([266(6),266(7),266(11)])]. given #65 (T,wt=17): 718 (((x v y) ^ y) v y) ^ (z v (u v (w v y))) = y. [para(285(a,1),253(a,1,1,1,1,2)),rewrite([285(8),285(9),285(14)])]. given #66 (T,wt=17): 722 (x v x) ^ (y v (z v (u v (x v x)))) = x v x. [para(67(a,1),718(a,1,1,1)),rewrite([308(3)])]. given #67 (A,wt=69): 28 (((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 (w ^ (((y v y) v (z ^ y)) ^ ((z ^ y) v u)))) ^ v5)) ^ (v6 v y) = ((y v y) v (z ^ y)) ^ ((z ^ y) v u). [para(20(a,1),10(a,1,2,2))]. given #68 (T,wt=19): 720 (((x v y) ^ y) v y) ^ (z v (u v (w v (v5 v y)))) = y. [para(419(a,1),253(a,1,1,1,1,2)),rewrite([419(9),419(10),419(16)])]. given #69 (T,wt=19): 723 (x v (x v x)) ^ (y v (z v (u v (x v x)))) = x v x. [para(245(a,1),718(a,1,1,1))]. given #70 (T,wt=19): 737 (x v x) ^ (y v (z v (u v (w v (x v x))))) = x v x. [para(67(a,1),720(a,1,1,1)),rewrite([308(3)])]. given #71 (T,wt=21): 320 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_rewrite(254),rewrite([308(3)])]. given #72 (A,wt=99): 29 (((x v ((y v (z ^ ((u v y) ^ (y v w)))) ^ v5)) ^ ((y v (z ^ ((u v y) ^ (y v w)))) ^ v5)) v (((((y v (z ^ ((u v y) ^ (y v w)))) ^ v5) v ((y v (z ^ ((u v y) ^ (y v w)))) ^ v5)) v (v6 ^ ((y v (z ^ ((u v y) ^ (y v w)))) ^ v5))) ^ v7)) ^ (v8 v ((u v y) ^ (y v w))) = (y v (z ^ ((u v y) ^ (y v w)))) ^ v5. [para(10(a,1),20(a,1,2,2))]. given #73 (T,wt=19): 764 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(308(a,1),320(a,1,2,2,1))]. given #74 (T,wt=7): 789 x ^ (y v x) = x. [para(252(a,1),764(a,1,2,2)),rewrite([770(5),770(7)])]. given #75 (T,wt=9): 836 x v (x v x) = x v x. [para(789(a,1),583(a,1))]. given #76 (T,wt=9): 843 ((x v y) ^ y) v y = y. [para(789(a,1),716(a,1))]. given #77 (A,wt=15): 850 x ^ (y v (z v (u v (w v (v5 v x))))) = x. [back_rewrite(762),rewrite([843(3)])]. given #78 (T,wt=5): 975 x ^ x = x. [para(843(a,1),789(a,1,2))]. given #79 (T,wt=5): 976 x v x = x. [para(843(a,1),843(a,1,1,1)),rewrite([975(1)])]. given #80 (T,wt=7): 1096 (x v y) ^ y = y. [back_rewrite(770),rewrite([976(5)])]. given #81 (T,wt=9): 856 x ^ (y v (z v x)) = x. [back_rewrite(716),rewrite([843(3)])]. given #82 (A,wt=13): 852 x ^ (y v (z v (u v (w v x)))) = x. [back_rewrite(720),rewrite([843(3)])]. given #83 (T,wt=9): 1000 x ^ (x ^ (x v y)) = x. [back_rewrite(974),rewrite([976(1),976(1),976(1),976(4)])]. given #84 (T,wt=9): 1020 (x v (y ^ x)) ^ x = x. [back_rewrite(938),rewrite([976(4)])]. given #85 (T,wt=9): 1044 (x ^ y) ^ y = x ^ y. [back_rewrite(855),rewrite([976(1),976(2),976(3)])]. given #86 (T,wt=11): 854 x ^ (y v (z v (u v x))) = x. [back_rewrite(718),rewrite([843(3)])]. given #87 (A,wt=39): 853 ((x v (y ^ ((z v x) ^ (x v u)))) ^ w) ^ (v5 v (v6 v ((z v x) ^ (x v u)))) = (x v (y ^ ((z v x) ^ (x v u)))) ^ w. [back_rewrite(719),rewrite([843(21)])]. given #88 (T,wt=11): 868 (x ^ y) ^ (z v y) = x ^ y. [back_rewrite(253),rewrite([843(6)])]. given #89 (T,wt=11): 1035 x ^ ((y v x) ^ (x v z)) = x. [back_rewrite(887),rewrite([976(3),843(3)])]. given #90 (T,wt=11): 1036 x ^ (y v (x ^ (x v z))) = x. [back_rewrite(885),rewrite([976(3),843(3)])]. given #91 (T,wt=11): 1259 (x v (y ^ x)) ^ (z v x) = x. [back_rewrite(312),rewrite([976(5)])]. given #92 (A,wt=13): 857 (x ^ y) ^ (z v (u v y)) = x ^ y. [back_rewrite(714),rewrite([843(6)])]. given #93 (T,wt=7): 1394 x v (y ^ x) = x. [para(1259(a,1),1000(a,1,2)),rewrite([1020(3)]),flip(a)]. given #94 (T,wt=7): 1480 x ^ (x v y) = x. [para(1394(a,1),1036(a,1,2))]. ============================== PROOF ================================= % Proof 1 at 1.02 (+ 0.01) seconds: McKenzie_2. % Length of proof is 43. % Level of proof is 20. % Maximum clause weight is 89. % Given clauses 94. 2 y ^ (x v (y v z)) = y # answer(McKenzie_2) # label(non_clause) # label(goal). [goal]. 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ w)) ^ (v5 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 (w ^ ((y v z) ^ (z v u)))) ^ v5)) ^ (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 w))) = y. [para(5(a,1),5(a,1,1,2))]. 15 (((x v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) ^ ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) v u) ^ (v5 v ((v6 v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) ^ (((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w)) v v7))) = (y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w). [para(5(a,1),10(a,1,1,2))]. 20 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (w v ((v5 v y) ^ (y v v6))) = y. [para(12(a,1),10(a,1,1,1,1,2)),rewrite([12(11),12(13),12(17),12(18),12(22)])]. 22 (((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))]. 27 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (w ^ y)) ^ v5)) ^ (v6 v ((v7 v y) ^ (y v v8))) = y. [para(20(a,1),10(a,1,1,1,1,2)),rewrite([20(17),20(22),20(26),20(27),20(31)])]. 36 (((x v y) ^ y) v (z ^ y)) ^ (u v ((w v y) ^ (y v v5))) = y. [para(5(a,1),27(a,1,1,2))]. 58 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(12(a,1),36(a,1,2,2))]. 65 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (w v z) = y ^ z. [para(36(a,1),36(a,1,2,2))]. 67 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(22(a,1),58(a,1,1,2))]. 99 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(65(a,1),58(a,1,1,2))]. 193 (((x v y) ^ y) v y) ^ (z v ((u v y) ^ (y v w))) = y. [para(36(a,1),15(a,1,1,1,1,2)),rewrite([36(13),36(15),36(16),36(20)])]. 245 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(193(a,1),12(a,1,2,2))]. 252 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(193(a,1),36(a,1,2,2))]. 253 (((x v (y ^ z)) ^ (y ^ z)) v (y ^ z)) ^ (u v z) = y ^ z. [para(36(a,1),193(a,1,2,2))]. 254 ((x v x) v (x v x)) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [para(67(a,1),193(a,1,1,1))]. 266 (((x v y) ^ y) v y) ^ (z v y) = y. [para(193(a,1),193(a,1,2,2))]. 307 (x v (x v x)) ^ (y v x) = x v x. [para(245(a,1),67(a,1,1,1))]. 308 (x v x) v (x v x) = x v x. [para(67(a,1),245(a,1,1,1)),rewrite([307(8)])]. 312 (x v (y ^ x)) ^ (z v x) = x v x. [para(245(a,1),99(a,1,1,1))]. 320 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_rewrite(254),rewrite([308(3)])]. 716 (((x v y) ^ y) v y) ^ (z v (u v y)) = y. [para(266(a,1),253(a,1,1,1,1,2)),rewrite([266(6),266(7),266(11)])]. 764 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(308(a,1),320(a,1,2,2,1))]. 770 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(36(a,1),764(a,1,2,2)),rewrite([252(7)]),flip(a)]. 789 x ^ (y v x) = x. [para(252(a,1),764(a,1,2,2)),rewrite([770(5),770(7)])]. 843 ((x v y) ^ y) v y = y. [para(789(a,1),716(a,1))]. 868 (x ^ y) ^ (z v y) = x ^ y. [back_rewrite(253),rewrite([843(6)])]. 885 (((x v y) ^ y) v (y v y)) ^ (z v (y ^ (y v u))) = y. [para(843(a,1),12(a,1,2,2,1))]. 938 (x v (y ^ x)) ^ x = x v x. [para(843(a,1),312(a,1,2))]. 974 (x v x) ^ ((x v x) ^ ((x v x) v y)) = x v x. [para(843(a,1),764(a,1,2))]. 975 x ^ x = x. [para(843(a,1),789(a,1,2))]. 976 x v x = x. [para(843(a,1),843(a,1,1,1)),rewrite([975(1)])]. 1000 x ^ (x ^ (x v y)) = x. [back_rewrite(974),rewrite([976(1),976(1),976(1),976(4)])]. 1020 (x v (y ^ x)) ^ x = x. [back_rewrite(938),rewrite([976(4)])]. 1036 x ^ (y v (x ^ (x v z))) = x. [back_rewrite(885),rewrite([976(3),843(3)])]. 1259 (x v (y ^ x)) ^ (z v x) = x. [back_rewrite(312),rewrite([976(5)])]. 1394 x v (y ^ x) = x. [para(1259(a,1),1000(a,1,2)),rewrite([1020(3)]),flip(a)]. 1480 x ^ (x v y) = x. [para(1394(a,1),1036(a,1,2))]. 1489 x ^ (y v (x v z)) = x. [para(1480(a,1),868(a,1,1)),rewrite([1480(5)])]. 1490 $F # answer(McKenzie_2). [resolve(1489,a,7,a)]. ============================== end of proof ========================== % Redundant proof: 1493 $F # answer(McKenzie_2). [back_rewrite(7),rewrite([1489(7)]),xx(a)]. % Disable descendants (x means already disabled): 7x given #95 (T,wt=9): 1454 (x v (x ^ y)) ^ x = x. [back_rewrite(1006),rewrite([1394(2)])]. given #96 (T,wt=9): 1466 (x v y) v y = x v y. [para(789(a,1),1394(a,1,2))]. given #97 (A,wt=15): 860 x ^ (y v (z v ((u v x) ^ (x v w)))) = x. [back_rewrite(711),rewrite([843(3)])]. given #98 (T,wt=9): 1468 x ^ (y ^ x) = y ^ x. [para(1394(a,1),1096(a,1,1))]. ============================== PROOF ================================= % Proof 2 at 1.03 (+ 0.01) seconds: McKenzie_4. % Length of proof is 43. % Level of proof is 20. % Maximum clause weight is 89. % Given clauses 98. 4 ((x v y) ^ (y v z)) ^ y = y # answer(McKenzie_4) # label(non_clause) # label(goal). [goal]. 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ w)) ^ (v5 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 (w ^ ((y v z) ^ (z v u)))) ^ v5)) ^ (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 w))) = y. [para(5(a,1),5(a,1,1,2))]. 15 (((x v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) ^ ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) v u) ^ (v5 v ((v6 v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) ^ (((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w)) v v7))) = (y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w). [para(5(a,1),10(a,1,1,2))]. 20 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (w v ((v5 v y) ^ (y v v6))) = y. [para(12(a,1),10(a,1,1,1,1,2)),rewrite([12(11),12(13),12(17),12(18),12(22)])]. 22 (((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))]. 27 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (w ^ y)) ^ v5)) ^ (v6 v ((v7 v y) ^ (y v v8))) = y. [para(20(a,1),10(a,1,1,1,1,2)),rewrite([20(17),20(22),20(26),20(27),20(31)])]. 36 (((x v y) ^ y) v (z ^ y)) ^ (u v ((w v y) ^ (y v v5))) = y. [para(5(a,1),27(a,1,1,2))]. 58 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(12(a,1),36(a,1,2,2))]. 65 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (w v z) = y ^ z. [para(36(a,1),36(a,1,2,2))]. 67 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(22(a,1),58(a,1,1,2))]. 99 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(65(a,1),58(a,1,1,2))]. 193 (((x v y) ^ y) v y) ^ (z v ((u v y) ^ (y v w))) = y. [para(36(a,1),15(a,1,1,1,1,2)),rewrite([36(13),36(15),36(16),36(20)])]. 245 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(193(a,1),12(a,1,2,2))]. 252 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(193(a,1),36(a,1,2,2))]. 253 (((x v (y ^ z)) ^ (y ^ z)) v (y ^ z)) ^ (u v z) = y ^ z. [para(36(a,1),193(a,1,2,2))]. 254 ((x v x) v (x v x)) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [para(67(a,1),193(a,1,1,1))]. 266 (((x v y) ^ y) v y) ^ (z v y) = y. [para(193(a,1),193(a,1,2,2))]. 307 (x v (x v x)) ^ (y v x) = x v x. [para(245(a,1),67(a,1,1,1))]. 308 (x v x) v (x v x) = x v x. [para(67(a,1),245(a,1,1,1)),rewrite([307(8)])]. 312 (x v (y ^ x)) ^ (z v x) = x v x. [para(245(a,1),99(a,1,1,1))]. 320 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_rewrite(254),rewrite([308(3)])]. 716 (((x v y) ^ y) v y) ^ (z v (u v y)) = y. [para(266(a,1),253(a,1,1,1,1,2)),rewrite([266(6),266(7),266(11)])]. 764 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(308(a,1),320(a,1,2,2,1))]. 770 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(36(a,1),764(a,1,2,2)),rewrite([252(7)]),flip(a)]. 789 x ^ (y v x) = x. [para(252(a,1),764(a,1,2,2)),rewrite([770(5),770(7)])]. 843 ((x v y) ^ y) v y = y. [para(789(a,1),716(a,1))]. 887 (((x v y) ^ y) v (y v y)) ^ ((z v y) ^ (y v u)) = y. [para(843(a,1),12(a,1,2))]. 938 (x v (y ^ x)) ^ x = x v x. [para(843(a,1),312(a,1,2))]. 974 (x v x) ^ ((x v x) ^ ((x v x) v y)) = x v x. [para(843(a,1),764(a,1,2))]. 975 x ^ x = x. [para(843(a,1),789(a,1,2))]. 976 x v x = x. [para(843(a,1),843(a,1,1,1)),rewrite([975(1)])]. 1000 x ^ (x ^ (x v y)) = x. [back_rewrite(974),rewrite([976(1),976(1),976(1),976(4)])]. 1020 (x v (y ^ x)) ^ x = x. [back_rewrite(938),rewrite([976(4)])]. 1035 x ^ ((y v x) ^ (x v z)) = x. [back_rewrite(887),rewrite([976(3),843(3)])]. 1096 (x v y) ^ y = y. [back_rewrite(770),rewrite([976(5)])]. 1259 (x v (y ^ x)) ^ (z v x) = x. [back_rewrite(312),rewrite([976(5)])]. 1394 x v (y ^ x) = x. [para(1259(a,1),1000(a,1,2)),rewrite([1020(3)]),flip(a)]. 1468 x ^ (y ^ x) = y ^ x. [para(1394(a,1),1096(a,1,1))]. 1505 ((x v y) ^ (y v z)) ^ y = y. [para(1035(a,1),1468(a,1,2)),rewrite([1035(8)])]. 1506 $F # answer(McKenzie_4). [resolve(1505,a,9,a)]. ============================== end of proof ========================== % Redundant proof: 1510 $F # answer(McKenzie_4). [back_rewrite(9),rewrite([1505(9)]),xx(a)]. % Disable descendants (x means already disabled): 9x given #99 (T,wt=7): 1508 (x v y) ^ x = x. [para(1480(a,1),1468(a,1,2)),rewrite([1480(4)])]. given #100 (T,wt=9): 1489 x ^ (y v (x v z)) = x. [para(1480(a,1),868(a,1,1)),rewrite([1480(5)])]. given #101 (T,wt=9): 1492 (x v y) v x = x v y. [para(1480(a,1),1394(a,1,2))]. given #102 (A,wt=37): 871 ((x v (y ^ ((z v x) ^ (x v u)))) ^ w) ^ (v5 v ((z v x) ^ (x v u))) = (x v (y ^ ((z v x) ^ (x v u)))) ^ w. [back_rewrite(244),rewrite([843(21)])]. given #103 (T,wt=9): 1499 (x v (y v z)) ^ z = z. [para(856(a,1),1468(a,1,2)),rewrite([856(6)])]. given #104 (T,wt=9): 1514 (x v (y v z)) ^ y = y. [para(1489(a,1),1468(a,1,2)),rewrite([1489(6)])]. given #105 (T,wt=9): 1520 x ^ ((y v x) v z) = x. [para(1492(a,1),856(a,1,2))]. given #106 (T,wt=9): 1536 x ^ ((x v y) v z) = x. [para(1492(a,1),1489(a,1,2))]. given #107 (A,wt=13): 873 x ^ (y v ((z v x) ^ (x v u))) = x. [back_rewrite(193),rewrite([843(3)])]. given #108 (T,wt=9): 1547 ((x v y) v z) ^ y = y. [para(1492(a,1),1499(a,1,1))]. given #109 (T,wt=9): 1548 ((x v y) v z) ^ x = x. [para(1492(a,1),1514(a,1,1))]. given #110 (T,wt=11): 1442 (x ^ y) ^ (z v x) = x ^ y. [back_rewrite(1130),rewrite([1394(2),1394(3),1394(4),1394(5)])]. given #111 (T,wt=9): 1563 (x ^ y) ^ x = x ^ y. [para(976(a,1),1442(a,1,2))]. given #112 (A,wt=31): 984 ((x v y) v (((z ^ (x v y)) v y) ^ u)) ^ (w v ((v5 v (x v y)) ^ ((x v y) v v6))) = x v y. [back_rewrite(951),rewrite([975(3),976(4),976(4)])]. given #113 (T,wt=7): 1570 x v (x ^ y) = x. [para(1563(a,1),1394(a,1,2))]. given #114 (T,wt=9): 1571 x ^ (x ^ y) = x ^ y. [para(1563(a,1),1468(a,1,2)),rewrite([1563(4)])]. given #115 (T,wt=11): 1477 (x v y) v (z ^ y) = x v y. [para(868(a,1),1394(a,1,2))]. ============================== PROOF ================================= % Proof 3 at 1.05 (+ 0.01) seconds: McKenzie_1. % Length of proof is 50. % Level of proof is 22. % Maximum clause weight is 89. % Given clauses 115. 1 y v (x ^ (y ^ z)) = y # answer(McKenzie_1) # label(non_clause) # label(goal). [goal]. 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ w)) ^ (v5 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 (w ^ ((y v z) ^ (z v u)))) ^ v5)) ^ (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 w))) = y. [para(5(a,1),5(a,1,1,2))]. 15 (((x v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) ^ ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) v u) ^ (v5 v ((v6 v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) ^ (((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w)) v v7))) = (y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w). [para(5(a,1),10(a,1,1,2))]. 20 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (w v ((v5 v y) ^ (y v v6))) = y. [para(12(a,1),10(a,1,1,1,1,2)),rewrite([12(11),12(13),12(17),12(18),12(22)])]. 22 (((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))]. 24 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v (((w ^ ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))) v (v5 ^ (((y v y) v (z ^ y)) ^ u))) ^ v6)) ^ (v7 v y) = ((y v y) v (z ^ y)) ^ u. [para(20(a,1),5(a,1,2,2))]. 27 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (w ^ y)) ^ v5)) ^ (v6 v ((v7 v y) ^ (y v v8))) = y. [para(20(a,1),10(a,1,1,1,1,2)),rewrite([20(17),20(22),20(26),20(27),20(31)])]. 36 (((x v y) ^ y) v (z ^ y)) ^ (u v ((w v y) ^ (y v v5))) = y. [para(5(a,1),27(a,1,1,2))]. 58 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(12(a,1),36(a,1,2,2))]. 65 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (w v z) = y ^ z. [para(36(a,1),36(a,1,2,2))]. 67 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(22(a,1),58(a,1,1,2))]. 99 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(65(a,1),58(a,1,1,2))]. 193 (((x v y) ^ y) v y) ^ (z v ((u v y) ^ (y v w))) = y. [para(36(a,1),15(a,1,1,1,1,2)),rewrite([36(13),36(15),36(16),36(20)])]. 245 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(193(a,1),12(a,1,2,2))]. 252 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(193(a,1),36(a,1,2,2))]. 253 (((x v (y ^ z)) ^ (y ^ z)) v (y ^ z)) ^ (u v z) = y ^ z. [para(36(a,1),193(a,1,2,2))]. 254 ((x v x) v (x v x)) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [para(67(a,1),193(a,1,1,1))]. 266 (((x v y) ^ y) v y) ^ (z v y) = y. [para(193(a,1),193(a,1,2,2))]. 306 (x v (y ^ (x v x))) ^ (z v x) = x v x. [para(245(a,1),58(a,1,1,1))]. 307 (x v (x v x)) ^ (y v x) = x v x. [para(245(a,1),67(a,1,1,1))]. 308 (x v x) v (x v x) = x v x. [para(67(a,1),245(a,1,1,1)),rewrite([307(8)])]. 312 (x v (y ^ x)) ^ (z v x) = x v x. [para(245(a,1),99(a,1,1,1))]. 320 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_rewrite(254),rewrite([308(3)])]. 615 (x v (((x v x) v (y ^ x)) ^ z)) ^ (u v x) = x v x. [para(24(a,1),306(a,1,1,2))]. 689 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v ((w ^ ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))) v (w ^ ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))))) ^ (v5 v y) = ((y v y) v (z ^ y)) ^ u. [para(615(a,1),24(a,1,1,2))]. 716 (((x v y) ^ y) v y) ^ (z v (u v y)) = y. [para(266(a,1),253(a,1,1,1,1,2)),rewrite([266(6),266(7),266(11)])]. 764 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(308(a,1),320(a,1,2,2,1))]. 770 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(36(a,1),764(a,1,2,2)),rewrite([252(7)]),flip(a)]. 789 x ^ (y v x) = x. [para(252(a,1),764(a,1,2,2)),rewrite([770(5),770(7)])]. 843 ((x v y) ^ y) v y = y. [para(789(a,1),716(a,1))]. 868 (x ^ y) ^ (z v y) = x ^ y. [back_rewrite(253),rewrite([843(6)])]. 938 (x v (y ^ x)) ^ x = x v x. [para(843(a,1),312(a,1,2))]. 974 (x v x) ^ ((x v x) ^ ((x v x) v y)) = x v x. [para(843(a,1),764(a,1,2))]. 975 x ^ x = x. [para(843(a,1),789(a,1,2))]. 976 x v x = x. [para(843(a,1),843(a,1,1,1)),rewrite([975(1)])]. 1000 x ^ (x ^ (x v y)) = x. [back_rewrite(974),rewrite([976(1),976(1),976(1),976(4)])]. 1020 (x v (y ^ x)) ^ x = x. [back_rewrite(938),rewrite([976(4)])]. 1096 (x v y) ^ y = y. [back_rewrite(770),rewrite([976(5)])]. 1130 (((x v (y ^ x)) ^ z) v (u ^ ((x v (y ^ x)) ^ z))) ^ (w v x) = (x v (y ^ x)) ^ z. [back_rewrite(689),rewrite([976(1),976(5),1096(8),976(4),976(7),976(10),976(8),976(11),976(14),976(12),976(11)])]. 1259 (x v (y ^ x)) ^ (z v x) = x. [back_rewrite(312),rewrite([976(5)])]. 1394 x v (y ^ x) = x. [para(1259(a,1),1000(a,1,2)),rewrite([1020(3)]),flip(a)]. 1442 (x ^ y) ^ (z v x) = x ^ y. [back_rewrite(1130),rewrite([1394(2),1394(3),1394(4),1394(5)])]. 1477 (x v y) v (z ^ y) = x v y. [para(868(a,1),1394(a,1,2))]. 1563 (x ^ y) ^ x = x ^ y. [para(976(a,1),1442(a,1,2))]. 1570 x v (x ^ y) = x. [para(1563(a,1),1394(a,1,2))]. 1625 x v (y ^ (x ^ z)) = x. [para(1570(a,1),1477(a,1,1)),rewrite([1570(5)])]. 1626 $F # answer(McKenzie_1). [resolve(1625,a,6,a)]. ============================== end of proof ========================== % Redundant proof: 1628 $F # answer(McKenzie_1). [back_rewrite(6),rewrite([1625(7)]),xx(a)]. % Disable descendants (x means already disabled): 6x given #116 (T,wt=9): 1613 x v (y ^ (z ^ x)) = x. [para(1394(a,1),1477(a,1,1)),rewrite([1394(5)])]. given #117 (A,wt=23): 986 (((x ^ y) v (z ^ y)) ^ u) ^ (w v y) = ((x ^ y) v (z ^ y)) ^ u. [back_rewrite(941),rewrite([976(1),976(5),975(9),976(5),976(9),976(13),976(9),976(7)])]. given #118 (T,wt=9): 1625 x v (y ^ (x ^ z)) = x. [para(1570(a,1),1477(a,1,1)),rewrite([1570(5)])]. given #119 (T,wt=9): 1655 x v ((y ^ x) ^ z) = x. [para(1563(a,1),1613(a,1,2))]. given #120 (T,wt=9): 1713 x v ((x ^ y) ^ z) = x. [para(1563(a,1),1625(a,1,2))]. given #121 (T,wt=11): 1491 x ^ (y v (z v (x v u))) = x. [para(1480(a,1),857(a,1,1)),rewrite([1480(6)])]. given #122 (A,wt=63): 987 (((x v y) ^ (y v z)) v ((((y v (u ^ ((x v y) ^ (y v z)))) ^ w) v (v5 ^ ((x v y) ^ (y v z)))) ^ v6)) ^ (v7 v ((v8 v ((x v y) ^ (y v z))) ^ (((x v y) ^ (y v z)) v v9))) = (x v y) ^ (y v z). [back_rewrite(935),rewrite([975(7)])]. given #123 (T,wt=11): 1501 (x v (y v (z v u))) ^ u = u. [para(854(a,1),1468(a,1,2)),rewrite([854(8)])]. given #124 (T,wt=11): 1504 (x v y) ^ (z ^ y) = z ^ y. [para(868(a,1),1468(a,1,2)),rewrite([868(6)])]. given #125 (T,wt=11): 1505 ((x v y) ^ (y v z)) ^ y = y. [para(1035(a,1),1468(a,1,2)),rewrite([1035(8)])]. given #126 (T,wt=11): 1524 x ^ (y v ((z v x) v u)) = x. [para(1492(a,1),854(a,1,2,2))]. given #127 (A,wt=53): 988 ((((x ^ y) v (z ^ y)) ^ ((z ^ y) v u)) v (((z ^ y) v (w ^ (((x ^ y) v (z ^ y)) ^ ((z ^ y) v u)))) ^ v5)) ^ (v6 v y) = ((x ^ y) v (z ^ y)) ^ ((z ^ y) v u). [back_rewrite(928),rewrite([976(1),976(7),975(13),976(8),976(20)])]. given #128 (T,wt=11): 1525 x ^ ((y v (z v x)) v u) = x. [para(1492(a,1),854(a,1,2))]. given #129 (T,wt=11): 1529 (x ^ y) ^ (y v z) = x ^ y. [para(1492(a,1),868(a,1,2))]. given #130 (T,wt=11): 1530 x ^ ((x v y) ^ (x v z)) = x. [para(1492(a,1),1035(a,1,2,1))]. given #131 (T,wt=11): 1550 x ^ (y v ((x v z) v u)) = x. [para(1536(a,1),868(a,1,1)),rewrite([1536(7)])]. given #132 (A,wt=29): 991 (x v (((((y ^ x) v (z ^ x)) ^ u) v (w ^ x)) ^ v5)) ^ (v6 v ((v7 v x) ^ (x v v8))) = x. [back_rewrite(913),rewrite([975(1),976(1)])]. given #133 (T,wt=11): 1559 (x v y) ^ (z ^ x) = z ^ x. [para(1394(a,1),1547(a,1,1,1))]. given #134 (T,wt=11): 1565 (x v y) v (y ^ z) = x v y. [para(1442(a,1),1394(a,1,2))]. given #135 (T,wt=11): 1567 (x v y) ^ (y ^ z) = y ^ z. [para(1442(a,1),1468(a,1,2)),rewrite([1442(6)])]. given #136 (T,wt=11): 1568 (x ^ y) ^ (x v z) = x ^ y. [para(1492(a,1),1442(a,1,2))]. given #137 (A,wt=49): 993 ((((x ^ y) v (z ^ y)) ^ u) v (((w ^ (((x ^ y) v (z ^ y)) ^ u)) v (v5 ^ (((x ^ y) v (z ^ y)) ^ u))) ^ v6)) ^ (v7 v y) = ((x ^ y) v (z ^ y)) ^ u. [back_rewrite(907),rewrite([976(1),976(5),975(9),976(5),976(9),976(13),976(10),976(20)])]. given #138 (T,wt=11): 1603 (x v y) ^ (x ^ z) = x ^ z. [para(1570(a,1),1547(a,1,1,1))]. given #139 (T,wt=11): 1617 (x v y) v (z ^ x) = x v y. [para(1492(a,1),1477(a,1,1)),rewrite([1492(5)])]. given #140 (T,wt=11): 1656 x v (y ^ (z ^ (u ^ x))) = x. [para(1613(a,1),1477(a,1,1)),rewrite([1613(7)])]. given #141 (T,wt=11): 1714 x v (y ^ (z ^ (x ^ u))) = x. [para(1625(a,1),1477(a,1,1)),rewrite([1625(7)])]. given #142 (A,wt=61): 995 ((x v ((y v z) ^ (z v u))) v (((w ^ (x v ((y v z) ^ (z v u)))) v z) ^ v5)) ^ (v6 v ((v7 v (x v ((y v z) ^ (z v u)))) ^ ((x v ((y v z) ^ (z v u))) v v8))) = x v ((y v z) ^ (z v u)). [back_rewrite(899),rewrite([975(9),976(13)])]. given #143 (T,wt=11): 1731 (x v y) v (x ^ z) = x v y. [para(1480(a,1),1655(a,1,2,1))]. given #144 (T,wt=11): 1746 x v (y ^ ((z ^ x) ^ u)) = x. [para(1655(a,1),1477(a,1,1)),rewrite([1655(7)])]. given #145 (T,wt=11): 1765 x v (y ^ ((x ^ z) ^ u)) = x. [para(1713(a,1),1477(a,1,1)),rewrite([1713(7)])]. given #146 (T,wt=11): 1767 (x v (y v (z v u))) ^ z = z. [para(1491(a,1),1468(a,1,2)),rewrite([1491(8)])]. given #147 (A,wt=51): 998 (((x v y) ^ (y v z)) v ((y v (u ^ ((x v y) ^ (y v z)))) ^ w)) ^ (v5 v ((v6 v ((x v y) ^ (y v z))) ^ (((x v y) ^ (y v z)) v v7))) = (x v y) ^ (y v z). [back_rewrite(881),rewrite([975(7)])]. given #148 (T,wt=11): 1768 x ^ ((y v (x v z)) v u) = x. [para(1492(a,1),1491(a,1,2))]. given #149 (T,wt=11): 1802 (x v ((y v z) v u)) ^ z = z. [para(1492(a,1),1501(a,1,1,2))]. given #150 (T,wt=11): 1803 ((x v (y v z)) v u) ^ z = z. [para(1492(a,1),1501(a,1,1))]. given #151 (T,wt=11): 1813 (x v ((y v z) v u)) ^ y = y. [para(1536(a,1),1504(a,1,2)),rewrite([1536(7)])]. given #152 (A,wt=23): 999 (x v (((y ^ x) v (z ^ x)) ^ u)) ^ (w v ((v5 v x) ^ (x v v6))) = x. [back_rewrite(875),rewrite([975(1),976(1)])]. given #153 (T,wt=11): 1821 ((x v y) ^ (x v z)) ^ x = x. [para(1492(a,1),1505(a,1,1,1))]. given #154 (T,wt=11): 1828 x ^ (((y v x) v z) v u) = x. [para(1492(a,1),1524(a,1,2))]. given #155 (T,wt=11): 1895 x ^ (((x v y) v z) v u) = x. [para(1536(a,1),1529(a,1,1)),rewrite([1536(7)])]. given #156 (T,wt=11): 1996 ((x v (y v z)) v u) ^ y = y. [para(1489(a,1),1559(a,1,2)),rewrite([1489(7)])]. given #157 (A,wt=35): 1017 ((x v (y ^ ((z v x) ^ (x v u)))) ^ w) ^ ((z v x) ^ (x v u)) = (x v (y ^ ((z v x) ^ (x v u)))) ^ w. [back_rewrite(947),rewrite([976(27),843(21)])]. given #158 (T,wt=11): 1999 (((x v y) v z) v u) ^ y = y. [para(1520(a,1),1559(a,1,2)),rewrite([1520(7)])]. given #159 (T,wt=11): 2000 (((x v y) v z) v u) ^ x = x. [para(1536(a,1),1559(a,1,2)),rewrite([1536(7)])]. given #160 (T,wt=11): 2017 x v ((y ^ (z ^ x)) ^ u) = x. [para(1613(a,1),1565(a,1,1)),rewrite([1613(7)])]. given #161 (T,wt=11): 2019 x v ((y ^ (x ^ z)) ^ u) = x. [para(1625(a,1),1565(a,1,1)),rewrite([1625(7)])]. given #162 (A,wt=21): 1019 (((x ^ y) v (z ^ y)) ^ u) ^ y = ((x ^ y) v (z ^ y)) ^ u. [back_rewrite(942),rewrite([976(1),976(6),976(11),976(15),976(19),843(15),976(6)])]. given #163 (T,wt=11): 2020 x v (((y ^ x) ^ z) ^ u) = x. [para(1655(a,1),1565(a,1,1)),rewrite([1655(7)])]. given #164 (T,wt=11): 2021 x v (((x ^ y) ^ z) ^ u) = x. [para(1713(a,1),1565(a,1,1)),rewrite([1713(7)])]. given #165 (T,wt=13): 1428 (x ^ y) ^ (z v (u v x)) = x ^ y. [back_rewrite(1172),rewrite([1394(2),1394(3),1394(4),1394(6)])]. given #166 (T,wt=13): 1469 (x v (y v z)) v z = x v (y v z). [para(856(a,1),1394(a,1,2))]. given #167 (A,wt=35): 1041 (((((x ^ y) v (z ^ y)) ^ u) v (w ^ y)) ^ v5) ^ (v6 v y) = ((((x ^ y) v (z ^ y)) ^ u) v (w ^ y)) ^ v5. [back_rewrite(867),rewrite([976(1),976(10)])]. given #168 (T,wt=13): 1476 (x ^ (y ^ z)) ^ z = x ^ (y ^ z). [para(1394(a,1),868(a,1,2))]. given #169 (T,wt=13): 1500 (x v (y v (z v (u v w)))) ^ w = w. [para(852(a,1),1468(a,1,2)),rewrite([852(10)])]. given #170 (T,wt=13): 1507 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(857(a,1),1468(a,1,2)),rewrite([857(8)])]. given #171 (T,wt=13): 1512 x ^ (y v (z v (u v (x v w)))) = x. [para(1489(a,1),857(a,1,1)),rewrite([1489(8)])]. given #172 (A,wt=25): 1042 (((x ^ (y v z)) v z) ^ u) ^ (w v (y v z)) = ((x ^ (y v z)) v z) ^ u. [back_rewrite(863),rewrite([976(3),976(3),976(10),976(10)])]. given #173 (T,wt=13): 1513 (x v (y v z)) v y = x v (y v z). [para(1489(a,1),1394(a,1,2))]. given #174 (T,wt=13): 1521 x ^ (y v (z v ((u v x) v w))) = x. [para(1492(a,1),852(a,1,2,2,2))]. given #175 (T,wt=13): 1522 x ^ (y v ((z v (u v x)) v w)) = x. [para(1492(a,1),852(a,1,2,2))]. given #176 (T,wt=13): 1523 x ^ ((y v (z v (u v x))) v w) = x. [para(1492(a,1),852(a,1,2))]. given #177 (A,wt=25): 1043 (((x ^ y) v (z ^ y)) ^ u) ^ (w v (v5 v y)) = ((x ^ y) v (z ^ y)) ^ u. [back_rewrite(858),rewrite([976(1),976(8)])]. given #178 (T,wt=13): 1531 (x ^ y) ^ (z v (y v u)) = x ^ y. [para(1492(a,1),857(a,1,2,2))]. given #179 (T,wt=13): 1532 (x ^ y) ^ ((z v y) v u) = x ^ y. [para(1492(a,1),857(a,1,2))]. given #180 (T,wt=13): 1549 ((x v y) v z) v y = (x v y) v z. [para(1520(a,1),1394(a,1,2))]. given #181 (T,wt=13): 1551 x ^ (y v (z v ((x v u) v w))) = x. [para(1536(a,1),857(a,1,1)),rewrite([1536(8)])]. given #182 (A,wt=33): 1062 (x v (y ^ ((z v x) ^ (x v u)))) ^ (w v ((z v x) ^ (x v u))) = x v (y ^ ((z v x) ^ (x v u))). [back_rewrite(830),rewrite([976(23),843(18)])]. given #183 (T,wt=13): 1552 ((x v y) v z) v x = (x v y) v z. [para(1536(a,1),1394(a,1,2))]. given #184 (T,wt=13): 1555 (x v ((y v z) ^ (z v u))) ^ z = z. [para(873(a,1),1468(a,1,2)),rewrite([873(10)])]. given #185 (T,wt=13): 1556 x ^ (y v ((x v z) ^ (x v u))) = x. [para(1492(a,1),873(a,1,2,2,1))]. given #186 (T,wt=13): 1557 x ^ (((y v x) ^ (x v z)) v u) = x. [para(1492(a,1),873(a,1,2))]. given #187 (A,wt=19): 1063 ((x ^ y) v (z ^ y)) ^ (u v y) = (x ^ y) v (z ^ y). [back_rewrite(829),rewrite([976(1),976(5),976(9),976(12),976(15),843(12),976(6)])]. given #188 (T,wt=13): 1566 ((x ^ y) ^ z) ^ y = (x ^ y) ^ z. [para(1394(a,1),1442(a,1,2))]. given #189 (T,wt=13): 1596 (x ^ (y ^ z)) ^ y = x ^ (y ^ z). [para(1570(a,1),868(a,1,2))]. given #190 (T,wt=13): 1604 ((x ^ y) ^ z) ^ x = (x ^ y) ^ z. [para(1570(a,1),1442(a,1,2))]. given #191 (T,wt=13): 1622 ((x v y) v z) ^ (u ^ y) = u ^ y. [para(1477(a,1),1547(a,1,1,1))]. given #192 (A,wt=15): 1066 (x v ((y ^ x) v (z ^ x))) ^ (u v x) = x. [back_rewrite(821),rewrite([976(1),976(7)])]. given #193 (T,wt=11): 3829 x v ((y ^ x) v (z ^ x)) = x. [para(1066(a,1),1480(a,1)),flip(a)]. given #194 (T,wt=9): 3919 x v ((y ^ x) v x) = x. [para(975(a,1),3829(a,1,2,2))]. given #195 (T,wt=7): 4042 (x ^ y) v y = y. [para(3919(a,1),789(a,1,2)),rewrite([1096(3)]),flip(a)]. given #196 (T,wt=7): 4115 (x ^ y) v x = x. [para(1563(a,1),4042(a,1,1))]. given #197 (A,wt=37): 1102 ((x v (y ^ (z v (u v (w v x))))) ^ v5) ^ (v6 v (z v (u v (w v x)))) = (x v (y ^ (z v (u v (w v x))))) ^ v5. [back_rewrite(751),rewrite([1096(14),976(19),976(13)])]. given #198 (T,wt=9): 4093 x v (y v x) = y v x. [para(789(a,1),4042(a,1,1))]. given #199 (T,wt=9): 4104 x v (x v y) = x v y. [para(1480(a,1),4042(a,1,1))]. given #200 (T,wt=9): 4135 (x ^ (y ^ z)) v z = z. [para(1476(a,1),4042(a,1,1))]. given #201 (T,wt=9): 4153 ((x ^ y) ^ z) v y = y. [para(1566(a,1),4042(a,1,1))]. given #202 (A,wt=47): 1104 ((x v (y v (z v (u v w)))) v (((v5 ^ (x v (y v (z v (u v w))))) v w) ^ v6)) ^ (v7 v (x v (y v (z v (u v w))))) = x v (y v (z v (u v w))). [back_rewrite(747),rewrite([976(9),976(27)])]. given #203 (T,wt=9): 4154 (x ^ (y ^ z)) v y = y. [para(1596(a,1),4042(a,1,1))]. given #204 (T,wt=9): 4155 ((x ^ y) ^ z) v x = x. [para(1604(a,1),4042(a,1,1))]. given #205 (T,wt=11): 3956 x v ((x ^ y) v (z ^ x)) = x. [para(1563(a,1),3829(a,1,2,1))]. given #206 (T,wt=11): 3957 x v ((y ^ x) v (x ^ z)) = x. [para(1563(a,1),3829(a,1,2,2))]. ============================== PROOF ================================= % Proof 4 at 1.76 (+ 0.02) seconds: McKenzie_3. % Length of proof is 61. % Level of proof is 24. % Maximum clause weight is 89. % Given clauses 206. 3 ((x ^ y) v (y ^ z)) v y = y # answer(McKenzie_3) # label(non_clause) # label(goal). [goal]. 5 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ w)) ^ (v5 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 (w ^ ((y v z) ^ (z v u)))) ^ v5)) ^ (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 w))) = y. [para(5(a,1),5(a,1,1,2))]. 13 (((x v (((y ^ (z v z)) v (u ^ z)) ^ w)) ^ (((y ^ (z v z)) v (u ^ z)) ^ w)) v (((v5 ^ ((((y ^ (z v z)) v (u ^ z)) ^ w) v (((y ^ (z v z)) v (u ^ z)) ^ w))) v (v6 ^ (((y ^ (z v z)) v (u ^ z)) ^ w))) ^ v7)) ^ (v8 v z) = ((y ^ (z v z)) v (u ^ z)) ^ w. [para(5(a,1),5(a,1,2,2))]. 15 (((x v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) ^ ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) v u) ^ (v5 v ((v6 v ((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w))) ^ (((y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w)) v v7))) = (y v ((z v u) ^ u)) ^ (((z v u) ^ u) v w). [para(5(a,1),10(a,1,1,2))]. 20 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (w v ((v5 v y) ^ (y v v6))) = y. [para(12(a,1),10(a,1,1,1,1,2)),rewrite([12(11),12(13),12(17),12(18),12(22)])]. 22 (((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))]. 24 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v (((w ^ ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))) v (v5 ^ (((y v y) v (z ^ y)) ^ u))) ^ v6)) ^ (v7 v y) = ((y v y) v (z ^ y)) ^ u. [para(20(a,1),5(a,1,2,2))]. 27 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (w ^ y)) ^ v5)) ^ (v6 v ((v7 v y) ^ (y v v8))) = y. [para(20(a,1),10(a,1,1,1,1,2)),rewrite([20(17),20(22),20(26),20(27),20(31)])]. 36 (((x v y) ^ y) v (z ^ y)) ^ (u v ((w v y) ^ (y v v5))) = y. [para(5(a,1),27(a,1,1,2))]. 58 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (u v y) = y v y. [para(12(a,1),36(a,1,2,2))]. 65 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (w v z) = y ^ z. [para(36(a,1),36(a,1,2,2))]. 67 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (z v y) = y v y. [para(22(a,1),58(a,1,1,2))]. 81 ((x v x) v (y ^ (x v x))) ^ (z v x) = x v x. [para(67(a,1),58(a,1,1,1))]. 91 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (w v x) = x v x. [para(13(a,1),81(a,1,1,2))]. 99 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (u v y) = y v y. [para(65(a,1),58(a,1,1,2))]. 151 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (w v x) = x v x. [para(65(a,1),91(a,1,1,2,1,1))]. 193 (((x v y) ^ y) v y) ^ (z v ((u v y) ^ (y v w))) = y. [para(36(a,1),15(a,1,1,1,1,2)),rewrite([36(13),36(15),36(16),36(20)])]. 245 (((x v y) ^ y) v (y v y)) ^ (z v y) = y. [para(193(a,1),12(a,1,2,2))]. 252 (((x v y) ^ y) v (z ^ y)) ^ (u v y) = y. [para(193(a,1),36(a,1,2,2))]. 253 (((x v (y ^ z)) ^ (y ^ z)) v (y ^ z)) ^ (u v z) = y ^ z. [para(36(a,1),193(a,1,2,2))]. 254 ((x v x) v (x v x)) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [para(67(a,1),193(a,1,1,1))]. 266 (((x v y) ^ y) v y) ^ (z v y) = y. [para(193(a,1),193(a,1,2,2))]. 306 (x v (y ^ (x v x))) ^ (z v x) = x v x. [para(245(a,1),58(a,1,1,1))]. 307 (x v (x v x)) ^ (y v x) = x v x. [para(245(a,1),67(a,1,1,1))]. 308 (x v x) v (x v x) = x v x. [para(67(a,1),245(a,1,1,1)),rewrite([307(8)])]. 312 (x v (y ^ x)) ^ (z v x) = x v x. [para(245(a,1),99(a,1,1,1))]. 320 (x v x) ^ (y v ((z v (x v x)) ^ ((x v x) v u))) = x v x. [back_rewrite(254),rewrite([308(3)])]. 615 (x v (((x v x) v (y ^ x)) ^ z)) ^ (u v x) = x v x. [para(24(a,1),306(a,1,1,2))]. 689 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v ((w ^ ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))) v (w ^ ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))))) ^ (v5 v y) = ((y v y) v (z ^ y)) ^ u. [para(615(a,1),24(a,1,1,2))]. 716 (((x v y) ^ y) v y) ^ (z v (u v y)) = y. [para(266(a,1),253(a,1,1,1,1,2)),rewrite([266(6),266(7),266(11)])]. 764 (x v x) ^ (y v ((x v x) ^ ((x v x) v z))) = x v x. [para(308(a,1),320(a,1,2,2,1))]. 770 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(36(a,1),764(a,1,2,2)),rewrite([252(7)]),flip(a)]. 789 x ^ (y v x) = x. [para(252(a,1),764(a,1,2,2)),rewrite([770(5),770(7)])]. 821 ((x v x) v ((y ^ x) v (z ^ x))) ^ (u v x) = x v x. [para(789(a,1),151(a,1,1,2))]. 843 ((x v y) ^ y) v y = y. [para(789(a,1),716(a,1))]. 885 (((x v y) ^ y) v (y v y)) ^ (z v (y ^ (y v u))) = y. [para(843(a,1),12(a,1,2,2,1))]. 938 (x v (y ^ x)) ^ x = x v x. [para(843(a,1),312(a,1,2))]. 974 (x v x) ^ ((x v x) ^ ((x v x) v y)) = x v x. [para(843(a,1),764(a,1,2))]. 975 x ^ x = x. [para(843(a,1),789(a,1,2))]. 976 x v x = x. [para(843(a,1),843(a,1,1,1)),rewrite([975(1)])]. 1000 x ^ (x ^ (x v y)) = x. [back_rewrite(974),rewrite([976(1),976(1),976(1),976(4)])]. 1020 (x v (y ^ x)) ^ x = x. [back_rewrite(938),rewrite([976(4)])]. 1036 x ^ (y v (x ^ (x v z))) = x. [back_rewrite(885),rewrite([976(3),843(3)])]. 1066 (x v ((y ^ x) v (z ^ x))) ^ (u v x) = x. [back_rewrite(821),rewrite([976(1),976(7)])]. 1096 (x v y) ^ y = y. [back_rewrite(770),rewrite([976(5)])]. 1130 (((x v (y ^ x)) ^ z) v (u ^ ((x v (y ^ x)) ^ z))) ^ (w v x) = (x v (y ^ x)) ^ z. [back_rewrite(689),rewrite([976(1),976(5),1096(8),976(4),976(7),976(10),976(8),976(11),976(14),976(12),976(11)])]. 1259 (x v (y ^ x)) ^ (z v x) = x. [back_rewrite(312),rewrite([976(5)])]. 1394 x v (y ^ x) = x. [para(1259(a,1),1000(a,1,2)),rewrite([1020(3)]),flip(a)]. 1442 (x ^ y) ^ (z v x) = x ^ y. [back_rewrite(1130),rewrite([1394(2),1394(3),1394(4),1394(5)])]. 1480 x ^ (x v y) = x. [para(1394(a,1),1036(a,1,2))]. 1563 (x ^ y) ^ x = x ^ y. [para(976(a,1),1442(a,1,2))]. 3829 x v ((y ^ x) v (z ^ x)) = x. [para(1066(a,1),1480(a,1)),flip(a)]. 3919 x v ((y ^ x) v x) = x. [para(975(a,1),3829(a,1,2,2))]. 3957 x v ((y ^ x) v (x ^ z)) = x. [para(1563(a,1),3829(a,1,2,2))]. 4042 (x ^ y) v y = y. [para(3919(a,1),789(a,1,2)),rewrite([1096(3)]),flip(a)]. 4093 x v (y v x) = y v x. [para(789(a,1),4042(a,1,1))]. 4701 ((x ^ y) v (y ^ z)) v y = y. [para(3957(a,1),4093(a,1,2)),rewrite([3957(8)])]. 4702 $F # answer(McKenzie_3). [resolve(4701,a,8,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=206. Generated=38095. Kept=4691. proofs=4. Usable=116. Sos=2825. Demods=3037. Limbo=97, Disabled=1657. Hints=0. Kept_by_rule=0, Deleted_by_rule=2637. Forward_subsumed=30764. Back_subsumed=109. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=4685 (0 lex), Back_demodulated=1543. Back_unit_deleted=0. Demod_attempts=1732461. Demod_rewrites=113997. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=6.78. User_CPU=1.76, System_CPU=0.02, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 4 proofs. Process 11586 exit (max_proofs) Wed Feb 25 09:32:43 2009