============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 26923 was started by mccune on cleo, Fri Apr 13 09:16:20 2007 The command was "/home/mccune/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(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 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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, v, ^ ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 4). % (nonunit Horn with equality) Auto_process settings: % set(back_unit_deletion). % (Horn set with negative nonunits) % set(back_unit_deletion) -> set(unit_deletion). ============================== 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)) ^ v)) ^ (((w 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)) ^ v)) ^ (((w v y) ^ (v6 v y)) v v7) = y # label(A2). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=29): 2 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w 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 (v ^ ((y v z) ^ (u v z)))) ^ w)) ^ (((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 v) = 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)) ^ (((v v y) ^ (w 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 (v ^ y)) ^ w)) ^ (((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 v)) ^ (((y v z) ^ (u v z)) v v)) v (((w ^ ((((y v z) ^ (u v z)) v v) v (((y v z) ^ (u v z)) v v))) v z) ^ v6)) ^ (((v7 v (((y v z) ^ (u v z)) v v)) ^ (v8 v (((y v z) ^ (u v z)) v v))) v v9) = ((y v z) ^ (u v z)) v v. [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) ^ (v v y)) v w) = 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)) ^ 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)) ^ (z v v8) = ((y ^ (z v z)) v (u ^ z)) ^ v. [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 v) = 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)) ^ v) v (w ^ 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 v) = 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 v) = 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)) ^ (v v ((z v u) ^ u)))) ^ ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) v u) ^ (((w v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) ^ (v6 v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u))))) v v7) = (y v ((z v u) ^ u)) ^ (v 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 v) = 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)) ^ (v v (u ^ z)))) ^ (((y ^ (z v z)) v (u ^ z)) ^ (v v (u ^ z)))) v (((u ^ z) v (w ^ (((y ^ (z v z)) v (u ^ z)) ^ (v v (u ^ z))))) ^ v6)) ^ (z v v7) = ((y ^ (z v z)) v (u ^ z)) ^ (v 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 (v ^ ((y v z) ^ (u v z)))) ^ w) 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)) ^ 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))) ^ (z v w) = ((y ^ (z v z)) v (u ^ z)) ^ v. [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 v) = 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) ^ (v v y)))) ^ w)) ^ ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) v (((y v (z ^ ((u v y) ^ (v v y)))) ^ w) v ((y v (z ^ ((u v y) ^ (v v y)))) ^ w))) ^ (((u v y) ^ (v v y)) v v6) = (y v (z ^ ((u v y) ^ (v v y)))) ^ w. [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)) ^ v)) ^ (((w 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 v) v w) = 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 (((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)) ^ (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 v)) ^ (((y v z) ^ (u v z)) v v)) v ((((((y v z) ^ (u v z)) v v) v (((y v z) ^ (u v z)) v v)) v z) ^ w)) ^ (((v6 v (((y v z) ^ (u v z)) v v)) ^ (v7 v (((y v z) ^ (u v z)) v v))) v v8) = ((y v z) ^ (u v z)) v v. [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 v) = 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)) ^ 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)) ^ (z v v7) = ((y ^ (z v z)) v (u ^ z)) ^ v. [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 v) = 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 (v ^ (((y v y) v (z ^ y)) ^ (u v (z ^ y))))) ^ w)) ^ (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 v) v w) = 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 v) = 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) ^ (v v y)))) ^ w)) ^ ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) v (((((y v (z ^ ((u v y) ^ (v v y)))) ^ w) v ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) v (v6 ^ ((y v (z ^ ((u v y) ^ (v v y)))) ^ w))) ^ v7)) ^ (((u v y) ^ (v v y)) v v8) = (y v (z ^ ((u v y) ^ (v v y)))) ^ w. [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)) ^ v)) ^ (((w 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 v) = ((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) ^ (v v x)) v w) = 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)) ^ (((v v (x v y)) ^ (w 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 v) = 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)) ^ (v v (x v y))) v w) = 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 v) = 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 v) = (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 (v ^ (((x ^ y) v (z ^ y)) ^ (u v (z ^ y)))))) ^ (y v w) = ((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)))) ^ v)) ^ (y v w) = (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 (v ^ x)) ^ w)) ^ ((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 (v ^ x))) ^ (((w 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)) ^ v)) ^ (((w 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 (((v ^ (((x v y) ^ (z v y)) v u)) v y) ^ w)) ^ ((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 ((v ^ (((x v y) ^ (z v y)) v u)) v y)) ^ (((w 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) ^ v)) ^ (((w 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 v))) ^ w) ^ ((((x v z) v u) v v) v v6) = (x v (y ^ (((x v z) v u) v v))) ^ w. [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 v) v (((w ^ ((((x v y) v z) v u) v v)) v x) ^ v6)) ^ (((((x v y) v z) v u) v v) v v7) = (((x v y) v z) v u) v v. [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 v) v ((x v (w ^ ((((x v y) v z) v u) v v))) ^ v6)) ^ (((((x v y) v z) v u) v v) v v7) = (((x v y) v z) v u) v v. [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.42 (+ 0.03) seconds: McKenzie. % Length of proof is 70. % Level of proof is 24. % Maximum clause weight is 89. % 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(goal). [goal]. 2 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w 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 (v ^ ((y v z) ^ (u v z)))) ^ w)) ^ (((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 v) = y. [para(2(a,1),2(a,1,1,2))]. 7 (((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)) ^ (z v v8) = ((y ^ (z v z)) v (u ^ z)) ^ v. [para(2(a,1),2(a,1,2,1))]. 9 (((x v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) ^ ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) v u) ^ (((w v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) ^ (v6 v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u))))) v v7) = (y v ((z v u) ^ u)) ^ (v 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)) ^ (((v v y) ^ (w 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)) ^ v)) ^ (((w 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 (v ^ y)) ^ w)) ^ (((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) ^ (v v y)) v w) = 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 v) = 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 v) = 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 v) = 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 v) = 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 v) = 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) ^ (v v x)) v w) = 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. Weight_deleted=2603. Literals_deleted=0. 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.35. User_CPU=1.42, System_CPU=0.03, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 26923 exit (max_proofs) Fri Apr 13 09:16:22 2007