============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5087 was started by mccune on cleo, Tue Nov 3 09:41:43 2009 The command was "/home/mccune/LADR/bin/prover9 -f a2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file a2.in assign(max_seconds,30). formulas(sos). (((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (((w v x) ^ (v6 v x)) v v7) = x # label(A2). end_of_list. formulas(goals). y v (x ^ (y ^ z)) = y & y ^ (x v (y v z)) = y & ((x ^ y) v (y ^ z)) v y = y & ((x v y) ^ (y v z)) ^ y = y # answer(McKenzie). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 y v (x ^ (y ^ z)) = y & y ^ (x v (y v z)) = y & ((x ^ y) v (y ^ z)) v y = y & ((x v y) ^ (y v z)) ^ y = y # answer(McKenzie) # 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 y) ^ (v6 v y)) v v7) = y # label(A2). [assumption]. c1 v (c2 ^ (c1 ^ c3)) != c1 | c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, v, ^ ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 4). % (nonunit Horn with equality) Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) kept: 2 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ w)) ^ (((v5 v y) ^ (v6 v y)) v v7) = y # label(A2). [assumption]. kept: 3 c1 v (c2 ^ (c1 ^ c3)) != c1 | c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie). [deny(1)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ w)) ^ (((v5 v y) ^ (v6 v y)) v v7) = y # label(A2). [assumption]. 3 c1 v (c2 ^ (c1 ^ c3)) != c1 | c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie). [deny(1)]. end_of_list. formulas(demodulators). 2 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ w)) ^ (((v5 v y) ^ (v6 v y)) v v7) = y # label(A2). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=29): 2 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ w)) ^ (((v5 v y) ^ (v6 v y)) v v7) = y # label(A2). [assumption]. given #2 (I,wt=40): 3 c1 v (c2 ^ (c1 ^ c3)) != c1 | c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie). [deny(1)]. given #3 (A,wt=61): 4 (((x v ((y v z) ^ (u v z))) ^ ((y v z) ^ (u v z))) v ((z v (w ^ ((y v z) ^ (u v z)))) ^ v5)) ^ (((v6 v ((y v z) ^ (u v z))) ^ (v7 v ((y v z) ^ (u v z)))) v v8) = (y v z) ^ (u v z). [para(2(a,1),2(a,1,1,2,1,1))]. given #4 (T,wt=21): 6 (((x v y) ^ y) v (y v y)) ^ (((z v y) ^ (u v y)) v w) = y. [para(2(a,1),2(a,1,1,2))]. given #5 (T,wt=25): 16 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (y v z) = y v y. [para(6(a,1),6(a,1,2,1))]. given #6 (T,wt=27): 14 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (((w v y) ^ (v5 v y)) v v6) = y. [para(6(a,1),4(a,1,1,1,1,2)),rewrite([6(11),6(13),6(17),6(18),6(22)])]. given #7 (T,wt=33): 21 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (w ^ y)) ^ v5)) ^ (((v6 v y) ^ (v7 v y)) v v8) = y. [para(14(a,1),4(a,1,1,1,1,2)),rewrite([14(17),14(22),14(26),14(27),14(31)])]. given #8 (A,wt=83): 5 (((x v (((y v z) ^ (u v z)) v w)) ^ (((y v z) ^ (u v z)) v w)) v (((v5 ^ ((((y v z) ^ (u v z)) v w) v (((y v z) ^ (u v z)) v w))) v z) ^ v6)) ^ (((v7 v (((y v z) ^ (u v z)) v w)) ^ (v8 v (((y v z) ^ (u v z)) v w))) v v9) = ((y v z) ^ (u v z)) v w. [para(2(a,1),2(a,1,1,2,1,2))]. given #9 (T,wt=21): 30 (((x v y) ^ y) v (z ^ y)) ^ (((u v y) ^ (w v y)) v v5) = y. [para(2(a,1),21(a,1,1,2))]. given #10 (T,wt=23): 52 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (y v u) = y v y. [para(6(a,1),30(a,1,2,1))]. given #11 (T,wt=21): 61 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (y v z) = y v y. [para(16(a,1),52(a,1,1,2))]. given #12 (T,wt=15): 76 ((x v x) v (x v x)) ^ (x v y) = x v x. [para(61(a,1),61(a,1,1,1))]. given #13 (A,wt=83): 7 (((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)) ^ (z v v8) = ((y ^ (z v z)) v (u ^ z)) ^ w. [para(2(a,1),2(a,1,2,1))]. given #14 (T,wt=17): 75 ((x v x) v (y ^ (x v x))) ^ (x v z) = x v x. [para(61(a,1),52(a,1,1,1))]. given #15 (T,wt=19): 67 ((x v x) v ((x v x) v (x v x))) ^ (x v y) = x v x. [para(61(a,1),16(a,1,1,1))]. given #16 (T,wt=23): 59 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (z v w) = y ^ z. [para(30(a,1),30(a,1,2,1))]. given #17 (T,wt=15): 97 ((x v x) v (y ^ x)) ^ (x v z) = x v x. [para(59(a,1),75(a,1,1,2))]. given #18 (A,wt=35): 8 (((x v y) ^ y) v (((((z ^ (y v y)) v (u ^ y)) ^ w) v (v5 ^ y)) ^ v6)) ^ (((v7 v y) ^ (v8 v y)) v v9) = y. [para(2(a,1),4(a,1,1,1,1,2)),rewrite([2(19),2(25),2(29),2(30),2(34)])]. given #19 (T,wt=21): 93 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (y v u) = y v y. [para(59(a,1),52(a,1,1,2))]. given #20 (T,wt=23): 85 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (x v w) = x v x. [para(7(a,1),75(a,1,1,2))]. given #21 (T,wt=21): 138 ((x v x) v (((x v x) v (y ^ x)) ^ z)) ^ (x v u) = x v x. [para(16(a,1),85(a,1,1,2,1,1))]. given #22 (T,wt=21): 145 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (x v w) = x v x. [para(59(a,1),85(a,1,1,2,1,1))]. given #23 (A,wt=89): 9 (((x v ((y v ((z v u) ^ u)) ^ (w v ((z v u) ^ u)))) ^ ((y v ((z v u) ^ u)) ^ (w v ((z v u) ^ u)))) v u) ^ (((v5 v ((y v ((z v u) ^ u)) ^ (w v ((z v u) ^ u)))) ^ (v6 v ((y v ((z v u) ^ u)) ^ (w v ((z v u) ^ u))))) v v7) = (y v ((z v u) ^ u)) ^ (w v ((z v u) ^ u)). [para(2(a,1),4(a,1,1,2))]. given #24 (T,wt=13): 163 ((x v x) v x) ^ (x v y) = x v x. [para(2(a,1),145(a,1,1,2))]. given #25 (T,wt=17): 199 (((x v y) ^ y) v (y v y)) ^ ((y v y) v z) = y. [para(163(a,1),6(a,1,2,1))]. given #26 (T,wt=17): 204 (((x v y) ^ y) v (z ^ y)) ^ ((y v y) v u) = y. [para(163(a,1),30(a,1,2,1))]. given #27 (T,wt=19): 187 (((x v y) ^ y) v y) ^ (((z v y) ^ (u v y)) v w) = y. [para(30(a,1),9(a,1,1,1,1,2)),rewrite([30(13),30(15),30(16),30(20)])]. given #28 (A,wt=77): 10 (((x v (((y ^ (z v z)) v (u ^ z)) ^ (w v (u ^ z)))) ^ (((y ^ (z v z)) v (u ^ z)) ^ (w v (u ^ z)))) v (((u ^ z) v (v5 ^ (((y ^ (z v z)) v (u ^ z)) ^ (w v (u ^ z))))) ^ v6)) ^ (z v v7) = ((y ^ (z v z)) v (u ^ z)) ^ (w v (u ^ z)). [para(2(a,1),4(a,1,2,1))]. given #29 (T,wt=13): 260 (((x v y) ^ y) v y) ^ (y v z) = y. [para(187(a,1),187(a,1,2,1))]. given #30 (T,wt=15): 239 (((x v y) ^ y) v (y v y)) ^ (y v z) = y. [para(187(a,1),6(a,1,2,1))]. given #31 (T,wt=11): 302 (x v x) v (x v x) = x v x. [para(61(a,1),239(a,1,1,1)),rewrite([301(8)])]. given #32 (T,wt=11): 316 (x v x) ^ (x v y) = x v x. [back_rewrite(76),rewrite([302(3)])]. given #33 (A,wt=73): 11 (((x v ((y v z) ^ (u v z))) ^ ((y v z) ^ (u v z))) v ((((z v (w ^ ((y v z) ^ (u v z)))) ^ v5) v (v6 ^ ((y v z) ^ (u v z)))) ^ v7)) ^ (((v8 v ((y v z) ^ (u v z))) ^ (v9 v ((y v z) ^ (u v z)))) v v10) = (y v z) ^ (u v z). [para(4(a,1),4(a,1,1,1,1,2)),rewrite([4(36),4(46),4(53),4(57),4(64)])]. given #34 (T,wt=13): 301 (x v (x v x)) ^ (x v y) = x v x. [para(239(a,1),61(a,1,1,1))]. given #35 (T,wt=13): 303 (x v x) ^ ((x v x) v y) = x v x. [para(76(a,1),239(a,1,1,1)),rewrite([302(4),302(3)])]. given #36 (T,wt=13): 306 (x v (y ^ x)) ^ (x v z) = x v x. [para(239(a,1),93(a,1,1,1))]. given #37 (T,wt=15): 246 (((x v y) ^ y) v (z ^ y)) ^ (y v u) = y. [para(187(a,1),30(a,1,2,1))]. given #38 (A,wt=65): 13 (((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))) ^ (z v v5) = ((y ^ (z v z)) v (u ^ z)) ^ w. [para(2(a,1),6(a,1,2,1))]. given #39 (T,wt=15): 259 (((x v y) ^ y) v y) ^ ((y v y) v z) = y. [para(163(a,1),187(a,1,2,1))]. given #40 (T,wt=15): 300 (x v (y ^ (x v x))) ^ (x v z) = x v x. [para(239(a,1),52(a,1,1,1))]. given #41 (T,wt=15): 308 (x v (x v x)) ^ ((x v x) v y) = x v x. [para(239(a,1),199(a,1,1,1)),rewrite([302(3),302(5)])]. given #42 (T,wt=17): 279 (((x v y) ^ y) v (z ^ y)) ^ ((y v u) v w) = y. [para(260(a,1),59(a,1,1,1,1,2)),rewrite([260(6),260(7),260(12)])]. given #43 (A,wt=81): 15 (((x v ((y v (z ^ ((u v y) ^ (w v y)))) ^ v5)) ^ ((y v (z ^ ((u v y) ^ (w v y)))) ^ v5)) v (((y v (z ^ ((u v y) ^ (w v y)))) ^ v5) v ((y v (z ^ ((u v y) ^ (w v y)))) ^ v5))) ^ (((u v y) ^ (w v y)) v v6) = (y v (z ^ ((u v y) ^ (w v y)))) ^ v5. [para(4(a,1),6(a,1,2,1))]. given #44 (T,wt=17): 389 (x v (y ^ (x v x))) ^ ((x v x) v z) = x v x. [para(239(a,1),246(a,1,1,1))]. given #45 (T,wt=15): 454 (x v (y ^ x)) ^ ((x v x) v z) = x v x. [para(59(a,1),389(a,1,1,2))]. given #46 (T,wt=19): 274 (((x v (y v y)) ^ (y v y)) v y) ^ (y v z) = y v y. [para(260(a,1),52(a,1,1,2))]. given #47 (T,wt=19): 285 ((x v x) v ((x v (y ^ x)) ^ z)) ^ (x v u) = x v x. [para(260(a,1),85(a,1,1,2,1,1))]. given #48 (A,wt=43): 17 (((x v (y v z)) ^ (y v z)) v (((u ^ ((y v z) v (y v z))) v (y v y)) ^ w)) ^ (((v5 v (y v z)) ^ (v6 v (y v z))) v v7) = y v z. [para(16(a,1),2(a,1,1,2,1,2))]. given #49 (T,wt=19): 350 ((x v x) v ((y ^ x) v (y ^ x))) ^ (x v z) = x v x. [para(316(a,1),145(a,1,1,2))]. given #50 (T,wt=19): 382 ((x v y) v x) ^ ((x v y) v z) = (x v y) v (x v y). [para(260(a,1),306(a,1,1,2))]. given #51 (T,wt=19): 413 (((x v y) ^ y) v (z ^ y)) ^ (((y v u) v w) v v5) = y. [para(279(a,1),59(a,1,1,1,1,2)),rewrite([279(8),279(9),279(15)])]. given #52 (T,wt=19): 428 (x v (y ^ (x v x))) ^ (((x v x) v z) v u) = x v x. [para(239(a,1),279(a,1,1,1))]. given #53 (A,wt=71): 18 (((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)) ^ (y v v7) = ((y v y) v (z ^ y)) ^ u. [para(14(a,1),2(a,1,2,1))]. given #54 (T,wt=15): 581 (x v x) ^ (((x v x) v y) v z) = x v x. [para(260(a,1),428(a,1,1,2))]. given #55 (T,wt=17): 577 (x v (x v x)) ^ (((x v x) v y) v z) = x v x. [para(52(a,1),428(a,1,1,2))]. given #56 (T,wt=17): 579 (x v (y ^ x)) ^ (((x v x) v z) v u) = x v x. [para(59(a,1),428(a,1,1,2))]. given #57 (T,wt=17): 580 ((x v x) v x) ^ (((x v x) v y) v z) = x v x. [para(199(a,1),428(a,1,1,2)),rewrite([302(5),302(9)])]. given #58 (A,wt=81): 19 (((x v (((y v z) ^ (u v z)) v w)) ^ (((y v z) ^ (u v z)) v w)) v ((((((y v z) ^ (u v z)) v w) v (((y v z) ^ (u v z)) v w)) v z) ^ v5)) ^ (((v6 v (((y v z) ^ (u v z)) v w)) ^ (v7 v (((y v z) ^ (u v z)) v w))) v v8) = ((y v z) ^ (u v z)) v w. [para(2(a,1),14(a,1,1,2,1,2))]. given #59 (T,wt=19): 535 (((x v y) ^ y) v y) ^ (((y v z) v (y v z)) v u) = y. [para(382(a,1),187(a,1,2,1))]. given #60 (T,wt=17): 647 (((x v y) ^ y) v y) ^ ((y v z) v (y v z)) = y. [para(302(a,1),535(a,1,2))]. given #61 (T,wt=19): 609 (x v (((x v x) v (y ^ x)) ^ z)) ^ (x v u) = x v x. [para(18(a,1),300(a,1,1,2))]. given #62 (T,wt=21): 240 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (y v w) = y. [para(187(a,1),14(a,1,2,1))]. given #63 (A,wt=81): 20 (((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)) ^ (z v v7) = ((y ^ (z v z)) v (u ^ z)) ^ w. [para(2(a,1),14(a,1,2,1))]. given #64 (T,wt=21): 247 (((x v (y ^ z)) ^ (y ^ z)) v (y ^ z)) ^ (z v u) = y ^ z. [para(30(a,1),187(a,1,2,1))]. given #65 (T,wt=15): 710 (((x v y) ^ y) v y) ^ ((y v z) v u) = y. [para(260(a,1),247(a,1,1,1,1,2)),rewrite([260(6),260(7),260(11)])]. given #66 (T,wt=17): 712 (((x v y) ^ y) v y) ^ (((y v z) v u) v w) = y. [para(279(a,1),247(a,1,1,1,1,2)),rewrite([279(8),279(9),279(14)])]. given #67 (T,wt=17): 716 (x v x) ^ ((((x v x) v y) v z) v u) = x v x. [para(61(a,1),712(a,1,1,1)),rewrite([302(3)])]. given #68 (A,wt=69): 22 (((x v (((y v y) v (z ^ y)) ^ (u v (z ^ y)))) ^ (((y v y) v (z ^ y)) ^ (u v (z ^ y)))) v (((z ^ y) v (w ^ (((y v y) v (z ^ y)) ^ (u v (z ^ y))))) ^ v5)) ^ (y v v6) = ((y v y) v (z ^ y)) ^ (u v (z ^ y)). [para(14(a,1),4(a,1,2,1))]. given #69 (T,wt=19): 714 (((x v y) ^ y) v y) ^ ((((y v z) v u) v w) v v5) = y. [para(413(a,1),247(a,1,1,1,1,2)),rewrite([413(9),413(10),413(16)])]. given #70 (T,wt=19): 717 (x v (x v x)) ^ ((((x v x) v y) v z) v u) = x v x. [para(239(a,1),712(a,1,1,1))]. given #71 (T,wt=19): 731 (x v x) ^ (((((x v x) v y) v z) v u) v w) = x v x. [para(61(a,1),714(a,1,1,1)),rewrite([302(3)])]. given #72 (T,wt=21): 314 (x v x) ^ (((y v (x v x)) ^ (z v (x v x))) v u) = x v x. [back_rewrite(248),rewrite([302(3)])]. given #73 (A,wt=99): 23 (((x v ((y v (z ^ ((u v y) ^ (w v y)))) ^ v5)) ^ ((y v (z ^ ((u v y) ^ (w v y)))) ^ v5)) v (((((y v (z ^ ((u v y) ^ (w v y)))) ^ v5) v ((y v (z ^ ((u v y) ^ (w v y)))) ^ v5)) v (v6 ^ ((y v (z ^ ((u v y) ^ (w v y)))) ^ v5))) ^ v7)) ^ (((u v y) ^ (w v y)) v v8) = (y v (z ^ ((u v y) ^ (w v y)))) ^ v5. [para(4(a,1),14(a,1,2,1))]. given #74 (T,wt=19): 758 (x v x) ^ (((x v x) ^ (y v (x v x))) v z) = x v x. [para(302(a,1),314(a,1,2,1,1))]. given #75 (T,wt=7): 783 x ^ (x v y) = x. [para(246(a,1),758(a,1,2,1)),rewrite([764(5),764(7)])]. given #76 (T,wt=9): 836 (x v x) v x = x v x. [para(783(a,1),580(a,1))]. given #77 (T,wt=13): 764 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(30(a,1),758(a,1,2,1)),rewrite([246(7)]),flip(a)]. given #78 (A,wt=13): 882 x ^ (((y v x) ^ (z v x)) v u) = x. [para(764(a,1),30(a,1,1))]. given #79 (T,wt=5): 922 x v x = x. [para(764(a,1),302(a,1,1)),rewrite([764(5),764(6)])]. given #80 (T,wt=5): 925 x ^ x = x. [para(302(a,1),764(a,1,1,1)),rewrite([922(1),922(1),922(2),922(2),922(2),922(2),922(3),922(2)])]. given #81 (T,wt=7): 924 (x v y) ^ y = y. [para(764(a,1),302(a,2)),rewrite([922(5),922(7),922(5)])]. given #82 (T,wt=9): 894 (x v (y ^ x)) ^ x = x. [para(764(a,1),75(a,1,2)),rewrite([764(5),764(5),764(8)])]. given #83 (A,wt=11): 896 (x ^ y) ^ (y v z) = x ^ y. [para(764(a,1),59(a,1,1))]. given #84 (T,wt=9): 931 x ^ ((x v y) v z) = x. [para(764(a,1),279(a,1,1))]. given #85 (T,wt=9): 948 (x ^ y) ^ y = x ^ y. [para(764(a,1),247(a,1,2)),rewrite([924(2),924(4),924(4),924(3),922(3),924(4)])]. given #86 (T,wt=9): 962 x ^ ((y v x) v z) = x. [back_rewrite(846),rewrite([922(1),922(1),922(4)])]. given #87 (T,wt=7): 1267 x ^ (y v x) = x. [para(922(a,1),962(a,1,2))]. given #88 (A,wt=27): 927 (x v ((((x v (y ^ x)) ^ z) v (u ^ x)) ^ w)) ^ (((v5 v x) ^ (v6 v x)) v v7) = x. [para(764(a,1),11(a,1,1,1,1,2,2)),rewrite([924(2),924(2),924(3),924(4),924(4),922(3),924(3),924(2),924(2),924(2),924(3),924(3),922(2),924(2),924(5),924(6),924(6),922(5),924(5),924(9),924(10),924(10),922(9),924(9),924(10),924(11),924(11),922(10),924(10),924(14),924(15),924(15),922(14),924(14)])]. given #89 (T,wt=11): 939 x ^ (((x v y) v z) v u) = x. [para(764(a,1),413(a,1,1))]. given #90 (T,wt=11): 955 (x v (x ^ y)) ^ (x v z) = x. [back_rewrite(911),rewrite([922(1),922(5)])]. given #91 (T,wt=7): 1282 x v (x ^ y) = x. [para(955(a,1),925(a,1)),flip(a)]. given #92 (T,wt=9): 1286 x ^ (x ^ y) = x ^ y. [para(1282(a,1),924(a,1,1))]. given #93 (A,wt=23): 928 (((x ^ y) v (z ^ y)) ^ u) ^ (y v w) = ((x ^ y) v (z ^ y)) ^ u. [para(764(a,1),13(a,1,1,1,1,2,1,1,2)),rewrite([924(3),924(7),924(7),922(6),924(8),924(10),924(6),924(6),922(5),924(7),924(10),924(10),922(9),924(11),922(13),922(9),924(6),924(8),924(8),922(7),924(9)])]. given #94 (T,wt=9): 1287 (x v y) v y = x v y. [para(924(a,1),1282(a,1,2))]. given #95 (T,wt=9): 1289 (x ^ y) ^ x = x ^ y. [para(1282(a,1),1267(a,1,2))]. given #96 (T,wt=11): 1176 (x v (y ^ x)) ^ (x v z) = x. [back_rewrite(306),rewrite([922(5)])]. given #97 (T,wt=7): 1304 x v (y ^ x) = x. [para(1176(a,1),925(a,1)),flip(a)]. given #98 (A,wt=21): 929 (((x ^ y) v (z ^ y)) ^ u) ^ y = ((x ^ y) v (z ^ y)) ^ u. [para(764(a,1),13(a,1,2)),rewrite([924(2),924(2),922(1),924(3),924(7),924(7),922(6),924(8),924(10),924(6),924(6),922(5),924(7),924(10),924(10),922(9),924(11),922(13),922(9),924(7),924(7),922(6),924(8)])]. given #99 (T,wt=9): 1346 (x v y) v x = x v y. [para(783(a,1),1304(a,1,2))]. given #100 (T,wt=7): 1386 (x v y) ^ x = x. [para(1346(a,1),924(a,1,1))]. given #101 (T,wt=9): 1350 x ^ (y ^ x) = y ^ x. [para(1304(a,1),924(a,1,1))]. given #102 (T,wt=9): 1389 ((x v y) v z) ^ x = x. [para(931(a,1),1350(a,1,2)),rewrite([931(6)])]. given #103 (A,wt=21): 936 (x v (((y ^ x) v x) ^ z)) ^ (((u v x) ^ (w v x)) v v5) = x. [para(764(a,1),17(a,1,1,1,1,2)),rewrite([924(3),924(3),922(2),924(2),924(2),924(2),922(1),924(2),924(2),922(1),922(1),924(3),924(3),922(2),924(6),924(6),922(5),924(7),924(7),922(6),924(11),924(11),922(10)])]. given #104 (T,wt=9): 1390 ((x v y) v z) ^ y = y. [para(962(a,1),1350(a,1,2)),rewrite([962(6)])]. given #105 (T,wt=11): 1262 x ^ ((y v x) ^ (z v x)) = x. [para(922(a,1),882(a,1,2))]. given #106 (T,wt=11): 1269 x ^ (((y v x) v z) v u) = x. [para(962(a,1),896(a,1,1)),rewrite([962(7)])]. given #107 (T,wt=11): 1280 (x ^ y) ^ (x v z) = x ^ y. [para(955(a,1),882(a,1,2,1))]. given #108 (A,wt=31): 937 ((x v y) v (((z ^ (x v y)) v x) ^ u)) ^ (((w v (x v y)) ^ (v5 v (x v y))) v v6) = x v y. [para(764(a,1),17(a,1,1,2,1,2)),rewrite([924(2),924(4),924(4),924(3),924(4),922(4),924(8),924(10),924(15)])]. given #109 (T,wt=11): 1351 (x v y) v (z ^ x) = x v y. [para(896(a,1),1304(a,1,2))]. given #110 (T,wt=11): 1388 (x v y) ^ (z ^ x) = z ^ x. [para(896(a,1),1350(a,1,2)),rewrite([896(6)])]. given #111 (T,wt=11): 1391 (((x v y) v z) v u) ^ x = x. [para(939(a,1),1350(a,1,2)),rewrite([939(8)])]. given #112 (T,wt=11): 1404 x v (((y ^ x) v x) ^ z) = x. [para(936(a,1),1267(a,1)),flip(a)]. given #113 (A,wt=13): 951 x ^ ((((x v y) v z) v u) v w) = x. [para(764(a,1),714(a,1,1,1,1)),rewrite([924(2),925(1),924(2),922(1),924(2),924(7)])]. given #114 (T,wt=9): 1466 x v ((y ^ x) v x) = x. [para(783(a,1),1404(a,1,2))]. given #115 (T,wt=7): 1499 (x ^ y) v y = y. [para(1466(a,1),924(a,1,1)),rewrite([1267(3)]),flip(a)]. given #116 (T,wt=7): 1521 (x ^ y) v x = x. [para(1289(a,1),1499(a,1,1))]. given #117 (T,wt=9): 1487 x v (y ^ (z ^ x)) = x. [para(1388(a,1),1404(a,1,2))]. given #118 (A,wt=29): 974 ((x v y) v ((z ^ (x v y)) v x)) ^ (((u v (x v y)) ^ (w v (x v y))) v v5) = x v y. [back_rewrite(832),rewrite([924(4),922(4),922(4)])]. given #119 (F,wt=31): 1534 c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie). [back_rewrite(3),rewrite([1531(7)]),xx(a)]. given #120 (T,wt=9): 1512 x v (x v y) = x v y. [para(783(a,1),1499(a,1,1))]. given #121 (T,wt=9): 1517 x v (y v x) = y v x. [para(1267(a,1),1499(a,1,1))]. given #122 (T,wt=9): 1531 x v (y ^ (x ^ z)) = x. [para(1521(a,1),1351(a,1,1)),rewrite([1521(5)])]. given #123 (T,wt=9): 1543 x v ((y ^ x) ^ z) = x. [para(1289(a,1),1487(a,1,2))]. given #124 (A,wt=33): 975 (x v (y ^ ((z v x) ^ (u v x)))) ^ (((z v x) ^ (u v x)) v w) = x v (y ^ ((z v x) ^ (u v x))). [back_rewrite(830),rewrite([924(12),922(16),922(11)])]. given #125 (F,wt=22): 1583 ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie). [back_rewrite(1534),rewrite([1566(7)]),xx(a)]. given #126 (T,wt=9): 1566 x ^ (y v (x v z)) = x. [para(1517(a,1),931(a,1,2))]. given #127 (T,wt=9): 1567 x ^ (y v (z v x)) = x. [para(1517(a,1),962(a,1,2))]. given #128 (T,wt=9): 1571 (x v (y v z)) ^ y = y. [para(1517(a,1),1389(a,1,1))]. given #129 (T,wt=9): 1572 (x v (y v z)) ^ z = z. [para(1517(a,1),1390(a,1,1))]. given #130 (A,wt=25): 976 ((x v (y ^ (z v x))) ^ u) ^ ((z v x) v w) = (x v (y ^ (z v x))) ^ u. [back_rewrite(829),rewrite([924(10),922(13),922(9)])]. given #131 (T,wt=9): 1582 (x ^ (y ^ z)) v z = z. [para(1487(a,1),1517(a,1,2)),rewrite([1487(6)])]. given #132 (T,wt=9): 1587 x v ((x ^ y) ^ z) = x. [para(1289(a,1),1531(a,1,2))]. given #133 (T,wt=9): 1593 (x ^ (y ^ z)) v y = y. [para(1531(a,1),1517(a,1,2)),rewrite([1531(6)])]. given #134 (T,wt=9): 1612 ((x ^ y) ^ z) v y = y. [para(1543(a,1),1517(a,1,2)),rewrite([1543(6)])]. given #135 (A,wt=19): 977 ((x ^ y) v (z ^ y)) ^ (y v u) = (x ^ y) v (z ^ y). [back_rewrite(828),rewrite([922(1),922(5),924(8),922(4),922(7),922(10),922(7),922(6)])]. given #136 (T,wt=9): 1739 ((x ^ y) ^ z) v x = x. [para(1587(a,1),1517(a,1,2)),rewrite([1587(6)])]. given #137 (T,wt=11): 1410 (x v y) ^ (x ^ z) = x ^ z. [para(1282(a,1),1390(a,1,1,1))]. given #138 (T,wt=11): 1419 x ^ ((x v y) ^ (z v x)) = x. [para(1346(a,1),1262(a,1,2,1))]. given #139 (T,wt=11): 1420 x ^ ((y v x) ^ (x v z)) = x. [para(1346(a,1),1262(a,1,2,2))]. given #140 (A,wt=51): 978 ((((x ^ y) v (z ^ y)) ^ (u v (z ^ y))) v ((z ^ y) v (w ^ (((x ^ y) v (z ^ y)) ^ (u v (z ^ y)))))) ^ (y v v5) = ((x ^ y) v (z ^ y)) ^ (u v (z ^ y)). [back_rewrite(823),rewrite([922(1),922(8),924(14),922(8),922(19)])]. given #141 (F,wt=11): 1886 ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 # answer(McKenzie). [back_rewrite(1583),rewrite([1872(20)]),xx(b)]. given #142 (T,wt=11): 1421 ((x v y) ^ (z v y)) ^ y = y. [para(1262(a,1),1350(a,1,2)),rewrite([1262(8)])]. given #143 (T,wt=11): 1430 (((x v y) v z) v u) ^ y = y. [para(1269(a,1),1350(a,1,2)),rewrite([1269(8)])]. given #144 (T,wt=11): 1433 (x v y) v (x ^ z) = x v y. [para(1280(a,1),1304(a,1,2))]. given #145 (T,wt=11): 1514 (x ^ y) v (y v z) = y v z. [para(896(a,1),1499(a,1,1))]. given #146 (A,wt=35): 979 (((x ^ y) v (z ^ y)) v (((z ^ y) v (u ^ ((x ^ y) v (z ^ y)))) ^ w)) ^ (y v v5) = (x ^ y) v (z ^ y). [back_rewrite(822),rewrite([922(1),922(5),924(8),922(5),922(14)])]. given #147 (T,wt=11): 1525 (x ^ y) v (x v z) = x v z. [para(1280(a,1),1499(a,1,1))]. given #148 (T,wt=11): 1540 (x v y) v (z ^ y) = x v y. [para(1267(a,1),1487(a,1,2,2))]. given #149 (T,wt=11): 1565 (x ^ y) ^ (z v y) = x ^ y. [para(1517(a,1),896(a,1,2))]. given #150 (T,wt=11): 1568 x ^ ((y v (x v z)) v u) = x. [para(1517(a,1),939(a,1,2,1))]. given #151 (A,wt=15): 980 (x v ((y ^ x) v (z ^ x))) ^ (x v u) = x. [back_rewrite(818),rewrite([922(1),922(7)])]. given #152 (T,wt=11): 1569 x ^ (y v ((x v z) v u)) = x. [para(1517(a,1),939(a,1,2))]. given #153 (T,wt=11): 1573 x ^ ((y v (z v x)) v u) = x. [para(1517(a,1),1269(a,1,2,1))]. given #154 (T,wt=11): 1574 x ^ (y v ((z v x) v u)) = x. [para(1517(a,1),1269(a,1,2))]. given #155 (T,wt=11): 1575 (x ^ y) ^ (z v x) = x ^ y. [para(1517(a,1),1280(a,1,2))]. given #156 (A,wt=25): 981 (x v (((((y ^ x) v (z ^ x)) ^ u) v (w ^ x)) ^ v5)) ^ ((v6 v x) v v7) = x. [back_rewrite(815),rewrite([924(2),922(1)])]. given #157 (T,wt=11): 1576 (x v y) ^ (z ^ y) = z ^ y. [para(1517(a,1),1388(a,1,1))]. given #158 (T,wt=11): 1577 ((x v (y v z)) v u) ^ y = y. [para(1517(a,1),1391(a,1,1,1))]. given #159 (T,wt=11): 1578 (x v ((y v z) v u)) ^ y = y. [para(1517(a,1),1391(a,1,1))]. given #160 (T,wt=11): 1600 (x v y) v (y ^ z) = x v y. [para(1267(a,1),1543(a,1,2,1))]. given #161 (A,wt=27): 982 (x v ((((y ^ x) v (z ^ x)) ^ u) v (w ^ x))) ^ (((v5 v x) ^ (v6 v x)) v v7) = x. [back_rewrite(814),rewrite([924(2),922(1)])]. given #162 (T,wt=11): 1662 ((x v (y v z)) v u) ^ z = z. [para(1567(a,1),1388(a,1,2)),rewrite([1567(7)])]. given #163 (T,wt=11): 1669 (x v y) ^ (y ^ z) = y ^ z. [para(1521(a,1),1571(a,1,1,2))]. given #164 (T,wt=11): 1712 (x ^ y) v (z v y) = z v y. [para(1267(a,1),1582(a,1,1,2))]. given #165 (T,wt=11): 1722 x v (y ^ (z ^ (u ^ x))) = x. [para(1582(a,1),1351(a,1,1)),rewrite([1582(7)])]. given #166 (A,wt=27): 983 (x v ((((y ^ x) v (z ^ x)) v (u ^ x)) ^ w)) ^ (((v5 v x) ^ (v6 v x)) v v7) = x. [back_rewrite(813),rewrite([924(2),922(1)])]. given #167 (T,wt=11): 1749 x v (y ^ (z ^ (x ^ u))) = x. [para(1593(a,1),1351(a,1,1)),rewrite([1593(7)])]. given #168 (T,wt=11): 1758 (x ^ y) v (z v x) = z v x. [para(1267(a,1),1612(a,1,1,1))]. given #169 (T,wt=11): 1767 x v (y ^ ((z ^ x) ^ u)) = x. [para(1612(a,1),1351(a,1,1)),rewrite([1612(7)])]. given #170 (T,wt=11): 1834 x v (y ^ ((x ^ z) ^ u)) = x. [para(1739(a,1),1351(a,1,1)),rewrite([1739(7)])]. given #171 (A,wt=49): 986 ((((x v y) ^ (z v y)) v u) v (((w ^ (((x v y) ^ (z v y)) v u)) v y) ^ v5)) ^ ((v6 v (((x v y) ^ (z v y)) v u)) v v7) = ((x v y) ^ (z v y)) v u. [back_rewrite(809),rewrite([924(10),922(13)])]. given #172 (T,wt=11): 1850 x ^ ((x v y) ^ (x v z)) = x. [para(1346(a,1),1419(a,1,2,2))]. given #173 (T,wt=11): 1851 ((x v y) ^ (z v x)) ^ x = x. [para(1419(a,1),1350(a,1,2)),rewrite([1419(8)])]. given #174 (T,wt=11): 1872 ((x v y) ^ (y v z)) ^ y = y. [para(1420(a,1),1350(a,1,2)),rewrite([1420(8)])]. given #175 (T,wt=11): 1949 (x v ((y v z) v u)) ^ z = z. [para(1517(a,1),1430(a,1,1))]. given #176 (A,wt=59): 987 ((((x v y) ^ (z v y)) v u) v ((w ^ (((x v y) ^ (z v y)) v u)) v y)) ^ (((v5 v (((x v y) ^ (z v y)) v u)) ^ (v6 v (((x v y) ^ (z v y)) v u))) v v7) = ((x v y) ^ (z v y)) v u. [back_rewrite(808),rewrite([924(10),922(13)])]. given #177 (T,wt=11): 1959 x v ((y ^ (z ^ x)) ^ u) = x. [para(1582(a,1),1433(a,1,1)),rewrite([1582(7)])]. given #178 (T,wt=11): 1960 x v ((y ^ (x ^ z)) ^ u) = x. [para(1593(a,1),1433(a,1,1)),rewrite([1593(7)])]. given #179 (T,wt=11): 1961 x v (((y ^ x) ^ z) ^ u) = x. [para(1612(a,1),1433(a,1,1)),rewrite([1612(7)])]. given #180 (T,wt=11): 1962 x v (((x ^ y) ^ z) ^ u) = x. [para(1739(a,1),1433(a,1,1)),rewrite([1739(7)])]. given #181 (A,wt=41): 988 (((x v y) v z) v (((u ^ ((x v y) v z)) v y) ^ w)) ^ (((v5 v ((x v y) v z)) ^ (v6 v ((x v y) v z))) v v7) = (x v y) v z. [back_rewrite(807),rewrite([924(6),922(7)])]. given #182 (T,wt=11): 1979 (x ^ (y ^ (z ^ u))) v u = u. [para(1582(a,1),1514(a,1,2)),rewrite([1582(7)])]. given #183 (T,wt=11): 1980 (x ^ (y ^ (z ^ u))) v z = z. [para(1593(a,1),1514(a,1,2)),rewrite([1593(7)])]. given #184 (T,wt=11): 1981 (x ^ ((y ^ z) ^ u)) v z = z. [para(1612(a,1),1514(a,1,2)),rewrite([1612(7)])]. given #185 (T,wt=11): 1984 (x ^ ((y ^ z) ^ u)) v y = y. [para(1739(a,1),1514(a,1,2)),rewrite([1739(7)])]. given #186 (A,wt=37): 1013 ((x v (y ^ (((x v z) v u) v w))) ^ v5) ^ ((((x v z) v u) v w) v v6) = (x v (y ^ (((x v z) v u) v w))) ^ v5. [back_rewrite(745),rewrite([924(14),922(19),922(13)])]. given #187 (T,wt=11): 2046 ((x ^ (y ^ z)) ^ u) v z = z. [para(1582(a,1),1525(a,1,2)),rewrite([1582(7)])]. given #188 (T,wt=11): 2047 ((x ^ (y ^ z)) ^ u) v y = y. [para(1593(a,1),1525(a,1,2)),rewrite([1593(7)])]. given #189 (T,wt=11): 2048 (((x ^ y) ^ z) ^ u) v y = y. [para(1612(a,1),1525(a,1,2)),rewrite([1612(7)])]. given #190 (T,wt=11): 2050 (((x ^ y) ^ z) ^ u) v x = x. [para(1739(a,1),1525(a,1,2)),rewrite([1739(7)])]. given #191 (A,wt=47): 1015 (((((x v y) v z) v u) v w) v (((v5 ^ ((((x v y) v z) v u) v w)) v x) ^ v6)) ^ (((((x v y) v z) v u) v w) v v7) = (((x v y) v z) v u) v w. [back_rewrite(741),rewrite([922(9),922(27)])]. given #192 (T,wt=11): 2093 x ^ (y v (z v (x v u))) = x. [para(1566(a,1),1565(a,1,1)),rewrite([1566(7)])]. given #193 (T,wt=11): 2094 x ^ (y v (z v (u v x))) = x. [para(1567(a,1),1565(a,1,1)),rewrite([1567(7)])]. given #194 (T,wt=11): 2128 x v ((y ^ x) v (z ^ x)) = x. [para(980(a,1),925(a,1)),flip(a)]. given #195 (T,wt=11): 2341 (x v (y v (z v u))) ^ z = z. [para(1566(a,1),1576(a,1,2)),rewrite([1566(7)])]. given #196 (A,wt=47): 1016 (((((x v y) v z) v u) v w) v ((x v (v5 ^ ((((x v y) v z) v u) v w))) ^ v6)) ^ (((((x v y) v z) v u) v w) v v7) = (((x v y) v z) v u) v w. [back_rewrite(740),rewrite([922(9),922(27)])]. given #197 (T,wt=11): 2342 (x v (y v (z v u))) ^ u = u. [para(1567(a,1),1576(a,1,2)),rewrite([1567(7)])]. given #198 (T,wt=11): 2816 ((x v y) ^ (x v z)) ^ x = x. [para(1850(a,1),1350(a,1,2)),rewrite([1850(8)])]. given #199 (T,wt=11): 3469 x v ((x ^ y) v (z ^ x)) = x. [para(1289(a,1),2128(a,1,2,1))]. given #200 (T,wt=11): 3470 x v ((y ^ x) v (x ^ z)) = x. [para(1289(a,1),2128(a,1,2,2))]. ============================== PROOF ================================= % Proof 1 at 1.53 (+ 0.03) seconds: McKenzie. % Length of proof is 70. % Level of proof is 24. % Maximum clause weight is 89.000. % Given clauses 200. 1 y v (x ^ (y ^ z)) = y & y ^ (x v (y v z)) = y & ((x ^ y) v (y ^ z)) v y = y & ((x v y) ^ (y v z)) ^ y = y # answer(McKenzie) # label(non_clause) # label(goal). [goal]. 2 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ w)) ^ (((v5 v y) ^ (v6 v y)) v v7) = y # label(A2). [assumption]. 3 c1 v (c2 ^ (c1 ^ c3)) != c1 | c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie). [deny(1)]. 4 (((x v ((y v z) ^ (u v z))) ^ ((y v z) ^ (u v z))) v ((z v (w ^ ((y v z) ^ (u v z)))) ^ v5)) ^ (((v6 v ((y v z) ^ (u v z))) ^ (v7 v ((y v z) ^ (u v z)))) v v8) = (y v z) ^ (u v z). [para(2(a,1),2(a,1,1,2,1,1))]. 6 (((x v y) ^ y) v (y v y)) ^ (((z v y) ^ (u v y)) v w) = y. [para(2(a,1),2(a,1,1,2))]. 7 (((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)) ^ (z v v8) = ((y ^ (z v z)) v (u ^ z)) ^ w. [para(2(a,1),2(a,1,2,1))]. 9 (((x v ((y v ((z v u) ^ u)) ^ (w v ((z v u) ^ u)))) ^ ((y v ((z v u) ^ u)) ^ (w v ((z v u) ^ u)))) v u) ^ (((v5 v ((y v ((z v u) ^ u)) ^ (w v ((z v u) ^ u)))) ^ (v6 v ((y v ((z v u) ^ u)) ^ (w v ((z v u) ^ u))))) v v7) = (y v ((z v u) ^ u)) ^ (w v ((z v u) ^ u)). [para(2(a,1),4(a,1,1,2))]. 14 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (((w v y) ^ (v5 v y)) v v6) = y. [para(6(a,1),4(a,1,1,1,1,2)),rewrite([6(11),6(13),6(17),6(18),6(22)])]. 16 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (y v z) = y v y. [para(6(a,1),6(a,1,2,1))]. 17 (((x v (y v z)) ^ (y v z)) v (((u ^ ((y v z) v (y v z))) v (y v y)) ^ w)) ^ (((v5 v (y v z)) ^ (v6 v (y v z))) v v7) = y v z. [para(16(a,1),2(a,1,1,2,1,2))]. 21 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (w ^ y)) ^ v5)) ^ (((v6 v y) ^ (v7 v y)) v v8) = y. [para(14(a,1),4(a,1,1,1,1,2)),rewrite([14(17),14(22),14(26),14(27),14(31)])]. 30 (((x v y) ^ y) v (z ^ y)) ^ (((u v y) ^ (w v y)) v v5) = y. [para(2(a,1),21(a,1,1,2))]. 52 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (y v u) = y v y. [para(6(a,1),30(a,1,2,1))]. 59 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (z v w) = y ^ z. [para(30(a,1),30(a,1,2,1))]. 61 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (y v z) = y v y. [para(16(a,1),52(a,1,1,2))]. 75 ((x v x) v (y ^ (x v x))) ^ (x v z) = x v x. [para(61(a,1),52(a,1,1,1))]. 85 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (x v w) = x v x. [para(7(a,1),75(a,1,1,2))]. 93 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (y v u) = y v y. [para(59(a,1),52(a,1,1,2))]. 145 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (x v w) = x v x. [para(59(a,1),85(a,1,1,2,1,1))]. 187 (((x v y) ^ y) v y) ^ (((z v y) ^ (u v y)) v w) = y. [para(30(a,1),9(a,1,1,1,1,2)),rewrite([30(13),30(15),30(16),30(20)])]. 239 (((x v y) ^ y) v (y v y)) ^ (y v z) = y. [para(187(a,1),6(a,1,2,1))]. 246 (((x v y) ^ y) v (z ^ y)) ^ (y v u) = y. [para(187(a,1),30(a,1,2,1))]. 248 ((x v x) v (x v x)) ^ (((y v (x v x)) ^ (z v (x v x))) v u) = x v x. [para(61(a,1),187(a,1,1,1))]. 260 (((x v y) ^ y) v y) ^ (y v z) = y. [para(187(a,1),187(a,1,2,1))]. 279 (((x v y) ^ y) v (z ^ y)) ^ ((y v u) v w) = y. [para(260(a,1),59(a,1,1,1,1,2)),rewrite([260(6),260(7),260(12)])]. 301 (x v (x v x)) ^ (x v y) = x v x. [para(239(a,1),61(a,1,1,1))]. 302 (x v x) v (x v x) = x v x. [para(61(a,1),239(a,1,1,1)),rewrite([301(8)])]. 306 (x v (y ^ x)) ^ (x v z) = x v x. [para(239(a,1),93(a,1,1,1))]. 314 (x v x) ^ (((y v (x v x)) ^ (z v (x v x))) v u) = x v x. [back_rewrite(248),rewrite([302(3)])]. 758 (x v x) ^ (((x v x) ^ (y v (x v x))) v z) = x v x. [para(302(a,1),314(a,1,2,1,1))]. 764 ((x v y) ^ y) v ((x v y) ^ y) = y. [para(30(a,1),758(a,1,2,1)),rewrite([246(7)]),flip(a)]. 783 x ^ (x v y) = x. [para(246(a,1),758(a,1,2,1)),rewrite([764(5),764(7)])]. 818 ((x v x) v ((y ^ x) v (z ^ x))) ^ (x v u) = x v x. [para(783(a,1),145(a,1,1,2))]. 846 (x v x) ^ ((y v (x v x)) v z) = x v x. [para(783(a,1),314(a,1,2,1))]. 882 x ^ (((y v x) ^ (z v x)) v u) = x. [para(764(a,1),30(a,1,1))]. 896 (x ^ y) ^ (y v z) = x ^ y. [para(764(a,1),59(a,1,1))]. 911 ((x v x) v (x ^ y)) ^ (x v z) = x v x. [para(764(a,1),145(a,1,1,2,1))]. 922 x v x = x. [para(764(a,1),302(a,1,1)),rewrite([764(5),764(6)])]. 924 (x v y) ^ y = y. [para(764(a,1),302(a,2)),rewrite([922(5),922(7),922(5)])]. 925 x ^ x = x. [para(302(a,1),764(a,1,1,1)),rewrite([922(1),922(1),922(2),922(2),922(2),922(2),922(3),922(2)])]. 931 x ^ ((x v y) v z) = x. [para(764(a,1),279(a,1,1))]. 936 (x v (((y ^ x) v x) ^ z)) ^ (((u v x) ^ (w v x)) v v5) = x. [para(764(a,1),17(a,1,1,1,1,2)),rewrite([924(3),924(3),922(2),924(2),924(2),924(2),922(1),924(2),924(2),922(1),922(1),924(3),924(3),922(2),924(6),924(6),922(5),924(7),924(7),922(6),924(11),924(11),922(10)])]. 955 (x v (x ^ y)) ^ (x v z) = x. [back_rewrite(911),rewrite([922(1),922(5)])]. 962 x ^ ((y v x) v z) = x. [back_rewrite(846),rewrite([922(1),922(1),922(4)])]. 980 (x v ((y ^ x) v (z ^ x))) ^ (x v u) = x. [back_rewrite(818),rewrite([922(1),922(7)])]. 1176 (x v (y ^ x)) ^ (x v z) = x. [back_rewrite(306),rewrite([922(5)])]. 1262 x ^ ((y v x) ^ (z v x)) = x. [para(922(a,1),882(a,1,2))]. 1267 x ^ (y v x) = x. [para(922(a,1),962(a,1,2))]. 1282 x v (x ^ y) = x. [para(955(a,1),925(a,1)),flip(a)]. 1289 (x ^ y) ^ x = x ^ y. [para(1282(a,1),1267(a,1,2))]. 1304 x v (y ^ x) = x. [para(1176(a,1),925(a,1)),flip(a)]. 1346 (x v y) v x = x v y. [para(783(a,1),1304(a,1,2))]. 1350 x ^ (y ^ x) = y ^ x. [para(1304(a,1),924(a,1,1))]. 1351 (x v y) v (z ^ x) = x v y. [para(896(a,1),1304(a,1,2))]. 1404 x v (((y ^ x) v x) ^ z) = x. [para(936(a,1),1267(a,1)),flip(a)]. 1420 x ^ ((y v x) ^ (x v z)) = x. [para(1346(a,1),1262(a,1,2,2))]. 1466 x v ((y ^ x) v x) = x. [para(783(a,1),1404(a,1,2))]. 1499 (x ^ y) v y = y. [para(1466(a,1),924(a,1,1)),rewrite([1267(3)]),flip(a)]. 1517 x v (y v x) = y v x. [para(1267(a,1),1499(a,1,1))]. 1521 (x ^ y) v x = x. [para(1289(a,1),1499(a,1,1))]. 1531 x v (y ^ (x ^ z)) = x. [para(1521(a,1),1351(a,1,1)),rewrite([1521(5)])]. 1534 c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie). [back_rewrite(3),rewrite([1531(7)]),xx(a)]. 1566 x ^ (y v (x v z)) = x. [para(1517(a,1),931(a,1,2))]. 1583 ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie). [back_rewrite(1534),rewrite([1566(7)]),xx(a)]. 1872 ((x v y) ^ (y v z)) ^ y = y. [para(1420(a,1),1350(a,1,2)),rewrite([1420(8)])]. 1886 ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 # answer(McKenzie). [back_rewrite(1583),rewrite([1872(20)]),xx(b)]. 2128 x v ((y ^ x) v (z ^ x)) = x. [para(980(a,1),925(a,1)),flip(a)]. 3470 x v ((y ^ x) v (x ^ z)) = x. [para(1289(a,1),2128(a,1,2,2))]. 3682 ((x ^ y) v (y ^ z)) v y = y. [para(3470(a,1),1517(a,1,2)),rewrite([3470(8)])]. 3683 $F # answer(McKenzie). [resolve(3682,a,1886,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=200. Generated=33280. Kept=3681. proofs=1. Usable=102. Sos=2187. Demods=2309. Limbo=21, Disabled=1372. Hints=0. Kept_by_rule=0, Deleted_by_rule=2603. Forward_subsumed=26996. Back_subsumed=95. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=3676 (0 lex), Back_demodulated=1275. Back_unit_deleted=0. Demod_attempts=1635083. Demod_rewrites=109748. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=3. Megabytes=5.39. User_CPU=1.53, System_CPU=0.03, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 5087 exit (max_proofs) Tue Nov 3 09:41:45 2009