============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 14728 was started by hoefnepe on europa, Fri Sep 21 17:40:10 2007 The command was "../../../kleene/Prover9/bin/prover9 -f eq3iv.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file eq3iv.in op(500,infix_left,"+"). op(490,infix_left,";"). op(480,postfix,"*"). op(450,postfix,"^"). formulas(sos). x + y = y + x. x + 0 = x. x + (y + z) = x + y + z. x ; 1 = x & 1 ; x = x. x ; (y ; z) = x ; y ; z. 0 ; x = 0. x + x = x. (x + y) ; z = x ; z + y ; z. x + y = y -> z ; x + z ; y = z ; y. 1 + x ; x * = x *. x ; y + z + y = y -> x * ; z + y = y. x ; x ^ = x ^. y + (x ; y + z) = x ; y + z -> y + (x ^ + x * ; z) = x ^ + x * ; z. y + x ; y = x ; y -> y + x ^ = x ^. end_of_list. formulas(goals). (all p (p + 1 = 1 & p ; p = p -> (p ; x) ^ + (p ; x ; p) ^ = (p ; x) ^)). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x ; 1 = x & 1 ; x = x. [assumption]. 2 x + y = y -> z ; x + z ; y = z ; y. [assumption]. 3 x ; y + z + y = y -> x * ; z + y = y. [assumption]. 4 y + (x ; y + z) = x ; y + z -> y + (x ^ + x * ; z) = x ^ + x * ; z. [assumption]. 5 y + x ; y = x ; y -> y + x ^ = x ^. [assumption]. 6 (all p (p + 1 = 1 & p ; p = p -> (p ; x) ^ + (p ; x ; p) ^ = (p ; x) ^)) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x + y = y + x. [assumption]. x + 0 = x. [assumption]. x + (y + z) = x + y + z. [assumption]. x ; 1 = x. [clausify(1)]. 1 ; x = x. [clausify(1)]. x ; (y ; z) = x ; y ; z. [assumption]. 0 ; x = 0. [assumption]. x + x = x. [assumption]. (x + y) ; z = x ; z + y ; z. [assumption]. x + y != y | z ; y = z ; x + z ; y. [clausify(2)]. 1 + x ; x * = x *. [assumption]. x ; y + z + y != y | x * ; z + y = y. [clausify(3)]. x ; x ^ = x ^. [assumption]. x ; y + z != y + (x ; y + z) | x ^ + x * ; z = y + (x ^ + x * ; z). [clausify(4)]. x ; y != y + x ; y | x ^ = y + x ^. [clausify(5)]. c2 + 1 = 1. [deny(6)]. c2 ; c2 = c2. [deny(6)]. (c2 ; c1) ^ != (c2 ; c1) ^ + (c2 ; c1 ; c2) ^. [deny(6)]. 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([ 1, 0, c1, c2, +, ;, ^, * ]). 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, 2). % (nonunit Horn with equality) Auto_process settings: (no changes). % Operation + is commutative; C redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 7 x + y = y + x. [assumption]. 8 x + 0 = x. [assumption]. 10 x + y + z = x + (y + z). [copy(9),flip(a)]. 11 x ; 1 = x. [clausify(1)]. 12 1 ; x = x. [clausify(1)]. 14 x ; y ; z = x ; (y ; z). [copy(13),flip(a)]. 15 0 ; x = 0. [assumption]. 16 x + x = x. [assumption]. 17 (x + y) ; z = x ; z + y ; z. [assumption]. 19 x + y != y | z ; x + z ; y = z ; y. [copy(18),flip(b)]. 20 1 + x ; x * = x *. [assumption]. 22 x + (y ; x + z) != x | y * ; z + x = x. [copy(21),rewrite(7(3))]. 23 x ; x ^ = x ^. [assumption]. 25 x + (y ; x + z) != y ; x + z | x + (y ^ + y * ; z) = y ^ + y * ; z. [copy(24),flip(a),flip(b)]. 27 x + y ; x != y ; x | x + y ^ = y ^. [copy(26),flip(a),flip(b)]. 29 1 + c2 = 1. [copy(28),rewrite(7(3))]. 30 c2 ; c2 = c2. [deny(6)]. 32 (c2 ; c1) ^ + (c2 ; (c1 ; c2)) ^ != (c2 ; c1) ^. [copy(31),rewrite(14(13)),flip(a)]. end_of_list. formulas(demodulators). 7 x + y = y + x. [assumption]. % (lex-dep) 8 x + 0 = x. [assumption]. 10 x + y + z = x + (y + z). [copy(9),flip(a)]. 11 x ; 1 = x. [clausify(1)]. 12 1 ; x = x. [clausify(1)]. 14 x ; y ; z = x ; (y ; z). [copy(13),flip(a)]. 15 0 ; x = 0. [assumption]. 16 x + x = x. [assumption]. 17 (x + y) ; z = x ; z + y ; z. [assumption]. 20 1 + x ; x * = x *. [assumption]. 23 x ; x ^ = x ^. [assumption]. 29 1 + c2 = 1. [copy(28),rewrite(7(3))]. 30 c2 ; c2 = c2. [deny(6)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 7 x + y = y + x. [assumption]. given #2 (I,wt=5): 8 x + 0 = x. [assumption]. given #3 (I,wt=11): 10 x + y + z = x + (y + z). [copy(9),flip(a)]. % Operation + is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 34 x + (y + z) = z + (x + y). [para(10(a,1),7(a,1))]. given #4 (I,wt=5): 11 x ; 1 = x. [clausify(1)]. given #5 (I,wt=5): 12 1 ; x = x. [clausify(1)]. given #6 (I,wt=11): 14 x ; y ; z = x ; (y ; z). [copy(13),flip(a)]. given #7 (I,wt=5): 15 0 ; x = 0. [assumption]. given #8 (I,wt=5): 16 x + x = x. [assumption]. given #9 (I,wt=13): 17 (x + y) ; z = x ; z + y ; z. [assumption]. given #10 (I,wt=16): 19 x + y != y | z ; x + z ; y = z ; y. [copy(18),flip(b)]. given #11 (I,wt=9): 20 1 + x ; x * = x *. [assumption]. given #12 (I,wt=17): 22 x + (y ; x + z) != x | y * ; z + x = x. [copy(21),rewrite(7(3))]. given #13 (I,wt=7): 23 x ; x ^ = x ^. [assumption]. given #14 (I,wt=30): 25 x + (y ; x + z) != y ; x + z | x + (y ^ + y * ; z) = y ^ + y * ; z. [copy(24),flip(a),flip(b)]. given #15 (I,wt=16): 27 x + y ; x != y ; x | x + y ^ = y ^. [copy(26),flip(a),flip(b)]. given #16 (I,wt=5): 29 1 + c2 = 1. [copy(28),rewrite(7(3))]. given #17 (I,wt=5): 30 c2 ; c2 = c2. [deny(6)]. given #18 (I,wt=16): 32 (c2 ; c1) ^ + (c2 ; (c1 ; c2)) ^ != (c2 ; c1) ^. [copy(31),rewrite(14(13)),flip(a)]. given #19 (A,wt=5): 33 0 + x = x. [para(8(a,1),7(a,1)),flip(a)]. given #20 (T,wt=4): 45 0 * = 1. [para(15(a,1),20(a,1,2)),rewrite(8(3)),flip(a)]. given #21 (T,wt=4): 60 0 ^ = 0. [para(23(a,1),15(a,1))]. given #22 (T,wt=7): 43 1 + 1 * = 1 *. [para(12(a,1),20(a,1,2))]. given #23 (T,wt=7): 74 x + 1 ^ = 1 ^. [para(12(a,1),27(a,1,2)),rewrite(16(1),12(2)),xx(a)]. given #24 (A,wt=11): 35 x + (y + z) = y + (x + z). [para(7(a,1),10(a,1,1)),rewrite(10(2))]. given #25 (T,wt=7): 79 x + c2 ; x = x. [para(29(a,1),17(a,1,1)),rewrite(12(2),12(2)),flip(a)]. given #26 (T,wt=5): 108 c2 ; 0 = 0. [para(79(a,1),33(a,1)),flip(a)]. given #27 (T,wt=7): 84 c2 + c2 ^ = c2 ^. [para(30(a,1),27(a,1,2)),rewrite(16(3),30(4)),xx(a)]. given #28 (T,wt=7): 91 1 ^ + x = 1 ^. [para(74(a,1),7(a,1)),flip(a)]. given #29 (A,wt=9): 36 x + (x + y) = x + y. [para(16(a,1),10(a,1,1)),flip(a)]. given #30 (T,wt=7): 122 1 + x * = x *. [para(20(a,1),36(a,1,2)),rewrite(20(7))]. given #31 (T,wt=9): 38 x + (y + x) = y + x. [para(16(a,1),10(a,2,2)),rewrite(7(2))]. given #32 (T,wt=9): 77 1 + (c2 + x) = 1 + x. [para(29(a,1),10(a,1,1)),flip(a)]. given #33 (T,wt=7): 139 c2 + x * = x *. [para(20(a,1),77(a,2)),rewrite(96(6))]. given #34 (A,wt=16): 39 x + y != x | z ; y + z ; x = z ; x. [para(7(a,1),19(a,1))]. given #35 (T,wt=7): 146 x + x ; c2 = x. [hyper(39,a,29,a),rewrite(11(4),7(3),11(5))]. given #36 (T,wt=8): 157 c2 != 1 | x ; c2 = x. [back_rewrite(80),rewrite(146(6)),flip(b)]. given #37 (T,wt=9): 78 c2 + (x + 1) = x + 1. [para(29(a,1),10(a,2,2)),rewrite(7(4))]. given #38 (T,wt=9): 81 c2 ; (c2 ; x) = c2 ; x. [para(30(a,1),14(a,1,1)),flip(a)]. given #39 (A,wt=14): 40 0 != x | y ; x + y ; 0 = y ; 0. [para(8(a,1),19(a,1)),flip(a)]. given #40 (T,wt=9): 100 1 + (x + c2) = x + 1. [para(29(a,1),35(a,1,2)),flip(a)]. given #41 (T,wt=9): 110 0 != x | c2 * ; x = 0. [para(108(a,1),22(a,1,2,1)),rewrite(33(3),33(2),7(7),33(7)),flip(a)]. given #42 (T,wt=6): 177 c2 * ; 0 = 0. [hyper(110,a,146,a(flip)),rewrite(15(6),16(5))]. given #43 (T,wt=9): 171 c2 ; x + c2 ^ = c2 ^. [para(81(a,1),27(a,1,2)),rewrite(16(5),81(6)),xx(a)]. given #44 (A,wt=20): 41 x + (y + z) != z | u ; (x + y) + u ; z = u ; z. [para(10(a,1),19(a,1))]. given #45 (T,wt=9): 180 c2 ^ + c2 ; x = c2 ^. [para(171(a,1),7(a,1)),flip(a)]. given #46 (T,wt=10): 55 x + y != x | y + x = x. [para(15(a,1),22(a,1,2,1)),rewrite(33(2),45(4),12(4))]. given #47 (T,wt=10): 133 x * + x ; x * = x *. [para(20(a,1),38(a,1,2)),rewrite(7(4),20(8))]. given #48 (T,wt=10): 152 x * != 1 | y ; x * = y. [para(122(a,1),39(a,1)),rewrite(11(7),7(6),125(6),11(7))]. given #49 (A,wt=13): 42 1 + (x ; x * + y) = x * + y. [para(20(a,1),10(a,1,1)),flip(a)]. given #50 (T,wt=10): 178 0 != x | c2 * * ; x = 0. [para(177(a,1),22(a,1,2,1)),rewrite(33(3),33(2),7(8),33(8)),flip(a)]. given #51 (T,wt=7): 233 c2 * * ; 0 = 0. [hyper(178,a,177,a(flip)),rewrite(177(7))]. given #52 (T,wt=10): 231 c2 ^ + c2 * = 1 + c2 ^. [para(171(a,1),42(a,1,2)),rewrite(7(9)),flip(a)]. given #53 (T,wt=11): 58 x ; (x ^ ; y) = x ^ ; y. [para(23(a,1),14(a,1,1)),flip(a)]. given #54 (A,wt=15): 44 1 + x ; (y ; (x ; y) *) = (x ; y) *. [para(14(a,1),20(a,1,2))]. given #55 (T,wt=9): 244 x ; x ^ ^ = x ^ ^. [para(23(a,1),58(a,1,2)),rewrite(23(7))]. given #56 (T,wt=9): 261 x ^ + x ^ ^ = x ^. [para(244(a,1),27(a,1,2)),rewrite(16(5),244(5),7(9)),xx(a)]. given #57 (T,wt=10): 246 x ^ + x ^ ; y = x ^. [para(58(a,1),27(a,1,2)),rewrite(16(5),58(5),7(9)),xx(a)]. given #58 (T,wt=10): 249 (x ; 0) * = 1 + x ; 0. [para(15(a,1),44(a,1,2,2)),flip(a)]. given #59 (A,wt=13): 46 x + y ; (y * ; x) = y * ; x. [para(20(a,1),17(a,1,1)),rewrite(12(4),14(5)),flip(a)]. given #60 (T,wt=8): 290 x * ; 1 ^ = 1 ^. [para(46(a,1),91(a,1))]. given #61 (T,wt=6): 301 (x *) ^ = 1 ^. [para(290(a,1),27(a,1,2)),rewrite(16(5),290(6),91(10)),flip(b),xx(a)]. given #62 (T,wt=8): 294 c2 * ; c2 ^ = c2 ^. [para(46(a,1),180(a,1))]. given #63 (T,wt=9): 298 x ^ * ; x ^ = x ^. [para(46(a,1),246(a,1))]. given #64 (A,wt=20): 47 1 + (x ; (x + y) * + y ; (x + y) *) = (x + y) *. [para(17(a,1),20(a,1,2))]. given #65 (T,wt=9): 305 (1 + x ; 0) ^ = 1 ^. [para(249(a,1),301(a,1,1))]. given #66 (T,wt=10): 277 x ^ + x ^ ^ ^ = x ^. [para(244(a,1),246(a,1,2))]. given #67 (T,wt=10): 304 x * ; 1 ^ ^ = 1 ^ ^. [para(301(a,1),244(a,1,2,1)),rewrite(301(7))]. given #68 (T,wt=11): 85 x ; 0 + x ; y = x ; y. [hyper(19,a,33,a)]. given #69 (A,wt=22): 48 x ; x * != x * | y + y ; (x ; x *) = y ; (x ; x *). [para(20(a,1),19(a,1)),rewrite(11(6)),flip(a)]. given #70 (T,wt=7): 341 x + x ; 0 = x. [para(11(a,1),85(a,1,2)),rewrite(7(3),11(5))]. given #71 (T,wt=8): 352 0 != 1 | x ; 0 = x. [para(15(a,1),48(a,1)),rewrite(45(3),45(6),11(6),341(6),45(6),11(6)),flip(b)]. given #72 (T,wt=9): 337 x ; 0 + x ^ = x ^. [hyper(27,a,85,a)]. given #73 (T,wt=10): 351 0 != x | y ; 0 = y ; x. [back_rewrite(40),rewrite(339(6)),flip(b)]. given #74 (A,wt=17): 49 x + (y + z ; x) != x | z * ; y + x = x. [para(7(a,1),22(a,1,2))]. given #75 (T,wt=6): 379 c2 * ; x = x. [para(79(a,1),49(a,1,2)),rewrite(16(1),7(5),127(5)),xx(a)]. given #76 (T,wt=4): 393 c2 * = 1. [para(379(a,1),11(a,1)),flip(a)]. given #77 (T,wt=6): 399 1 * ; 0 = 0. [back_rewrite(233),rewrite(393(2))]. given #78 (T,wt=8): 382 x * ; x * = x *. [para(133(a,1),49(a,1,2)),rewrite(16(3),7(8),125(8)),xx(a)]. given #79 (A,wt=15): 50 x + y ; x != x | y * ; 0 + x = x. [para(8(a,1),22(a,1,2))]. given #80 (T,wt=7): 414 1 * * ; 0 = 0. [para(399(a,1),50(a,1,2)),rewrite(16(3),7(10),127(10)),xx(a)]. given #81 (T,wt=8): 417 1 * * * ; 0 = 0. [para(414(a,1),50(a,1,2)),rewrite(16(3),7(11),127(11)),xx(a)]. given #82 (T,wt=9): 391 0 != x | x * ; x = 0. [para(341(a,1),49(a,1,2)),rewrite(33(2),7(6),33(6)),flip(a)]. given #83 (T,wt=9): 400 0 != x | 1 * ; x = 0. [back_rewrite(178),rewrite(393(4))]. given #84 (A,wt=27): 51 x + (y + (z ; (x + y) + u)) != x + y | z * ; u + (x + y) = x + y. [para(10(a,1),22(a,1))]. given #85 (T,wt=9): 419 1 * * * * ; 0 = 0. [para(417(a,1),50(a,1,2)),rewrite(16(3),7(12),127(12)),xx(a)]. given #86 (T,wt=10): 392 x + c2 != c2 | c2 + x = c2. [back_rewrite(376),rewrite(379(8))]. given #87 (T,wt=10): 398 0 != x | 1 * * ; x = 0. [back_rewrite(234),rewrite(393(4))]. given #88 (T,wt=10): 408 x ^ + x * ; 0 = x ^. [para(23(a,1),50(a,1,2)),rewrite(16(3),7(8)),xx(a)]. given #89 (A,wt=15): 52 1 + (x + y) != 1 | 1 + x * ; y = 1. [para(11(a,1),22(a,1,2,1)),rewrite(7(9))]. given #90 (T,wt=8): 456 1 + 1 * ; c2 = 1. [para(29(a,1),52(a,1,2)),rewrite(16(3)),xx(a)]. given #91 (T,wt=8): 489 c2 != 1 | 1 * * = c2. [para(456(a,1),49(a,1,2)),rewrite(7(3),29(3),11(8),7(8),139(8)),flip(a)]. given #92 (T,wt=9): 465 x + 1 != 1 | x * = 1. [para(38(a,1),52(a,1)),rewrite(11(8),122(7))]. given #93 (T,wt=4): 490 1 * = 1. [hyper(465,a,16,a)]. given #94 (A,wt=21): 54 x + (y ; (z ; x) + u) != x | (y ; z) * ; u + x = x. [para(14(a,1),22(a,1,2,1))]. given #95 (T,wt=9): 491 1 + x != 1 | x * = 1. [para(7(a,1),465(a,1))]. given #96 (T,wt=9): 493 1 ^ != 1 | 1 ^ * = 1. [para(91(a,1),465(a,1))]. given #97 (T,wt=9): 523 x * != 1 | x * * = 1. [para(122(a,1),491(a,1))]. given #98 (T,wt=11): 102 x + (c2 ; x + y) = x + y. [para(79(a,1),10(a,1,1)),flip(a)]. given #99 (A,wt=17): 56 x + y ; x != x | x + y * ; (y ; x) = x. [para(16(a,1),22(a,1,2)),rewrite(7(7))]. given #100 (T,wt=8): 549 x * ; x ^ = x ^. [para(23(a,1),56(a,1,2)),rewrite(16(3),23(7),127(8)),xx(a)]. given #101 (T,wt=9): 538 x + c2 ; (x ; c2) = x. [para(146(a,1),102(a,1,2)),rewrite(79(3),14(4)),flip(a)]. given #102 (T,wt=9): 542 x + c2 ; (x ; 0) = x. [para(341(a,1),102(a,1,2)),rewrite(79(3),14(4)),flip(a)]. given #103 (T,wt=9): 554 x * * ; x * = x *. [para(382(a,1),56(a,1,2)),rewrite(16(3),382(9),127(9)),xx(a)]. given #104 (A,wt=23): 57 x + (y ; x + (z ; x + u)) != x | (y + z) * ; u + x = x. [para(17(a,1),22(a,1,2,1)),rewrite(10(4))]. given #105 (T,wt=9): 561 x * * ; x ^ = x ^. [para(549(a,1),56(a,1,2)),rewrite(16(3),549(9),127(9)),xx(a)]. given #106 (T,wt=10): 551 x * ; x ^ ^ = x ^ ^. [para(244(a,1),56(a,1,2)),rewrite(16(5),244(11),127(12)),xx(a)]. given #107 (T,wt=10): 552 x ^ * * ; x ^ = x ^. [para(298(a,1),56(a,1,2)),rewrite(16(3),298(11),127(10)),xx(a)]. given #108 (T,wt=10): 596 x * * * ; x * = x *. [para(554(a,1),56(a,1,2)),rewrite(16(3),554(11),127(10)),xx(a)]. given #109 (A,wt=13): 59 x ; (y ; (x ; y) ^) = (x ; y) ^. [para(23(a,1),14(a,1)),flip(a)]. given #110 (T,wt=8): 679 (x ; 0) ^ = x ; 0. [para(15(a,1),59(a,1,2)),flip(a)]. given #111 (T,wt=10): 650 x * * * ; x ^ = x ^. [para(561(a,1),56(a,1,2)),rewrite(16(3),561(11),127(10)),xx(a)]. given #112 (T,wt=10): 687 c2 ^ + (c2 ; x) ^ = c2 ^. [para(59(a,1),171(a,1,1)),rewrite(7(6))]. given #113 (T,wt=11): 109 x + (y + c2 ; x) = y + x. [para(79(a,1),35(a,1,2)),flip(a)]. given #114 (A,wt=18): 61 x ; (x + y) ^ + y ; (x + y) ^ = (x + y) ^. [para(23(a,1),17(a,1)),flip(a)]. given #115 (T,wt=11): 112 c2 + (c2 ^ + x) = c2 ^ + x. [para(84(a,1),10(a,1,1)),flip(a)]. given #116 (T,wt=11): 114 c2 + (x + c2 ^) = x + c2 ^. [para(84(a,1),35(a,1,2)),flip(a)]. given #117 (T,wt=11): 125 x + x ; y * = x ; y *. [hyper(19,a,122,a),rewrite(11(2))]. given #118 (T,wt=8): 799 x ^ ; y * = x ^. [para(125(a,1),246(a,1))]. given #119 (A,wt=17): 62 x ^ + y != x ^ | x ^ + x * ; y = x ^. [para(23(a,1),22(a,1,2,1)),rewrite(36(4),7(8))]. given #120 (T,wt=8): 811 x ^ * = 1 + x ^. [para(799(a,1),20(a,1,2)),flip(a)]. given #121 (T,wt=8): 857 (1 + x ^) ^ = 1 ^. [para(811(a,1),301(a,1,1))]. given #122 (T,wt=6): 865 1 ^ ^ = 1 ^. [para(74(a,1),857(a,1,1))]. given #123 (T,wt=8): 866 1 ^ ; 1 ^ = 1 ^. [para(865(a,1),23(a,1,2)),rewrite(865(8))]. given #124 (A,wt=30): 63 x ; y + z != y + (z + x ; y) | y + (x ^ + x * ; z) = x ^ + x * ; z. [para(7(a,1),25(a,1,2)),flip(a)]. given #125 (T,wt=9): 806 x * + x * * = x *. [para(554(a,1),125(a,1,2)),rewrite(7(4),554(8))]. given #126 (T,wt=10): 808 x * + x * * * = x *. [para(596(a,1),125(a,1,2)),rewrite(7(5),596(10))]. given #127 (T,wt=10): 864 x ^ ; (1 + y ^) = x ^. [para(811(a,1),799(a,1,2))]. given #128 (T,wt=8): 911 x ^ ; 1 ^ = x ^. [para(74(a,1),864(a,1,2))]. given #129 (A,wt=30): 64 x + y ; z != z + (y ; z + x) | z + (y ^ + y * ; x) = y ^ + y * ; x. [para(7(a,1),25(a,2)),flip(a)]. given #130 (T,wt=10): 905 x * != 1 | x * * * = 1. [para(808(a,1),52(a,1,2)),rewrite(122(3),20(11))]. given #131 (T,wt=11): 126 1 + (x * + y) = x * + y. [para(122(a,1),10(a,1,1)),flip(a)]. given #132 (T,wt=11): 127 x + y * ; x = y * ; x. [para(122(a,1),17(a,1,1)),rewrite(12(4)),flip(a)]. given #133 (T,wt=10): 955 x * ; x * * = x * *. [para(127(a,1),133(a,1))]. given #134 (A,wt=38): 66 x + (y + (z ; (x + y) + u)) != z ; (x + y) + u | x + (y + (z ^ + z * ; u)) = z ^ + z * ; u. [para(10(a,1),25(a,1)),rewrite(10(15))]. given #135 (T,wt=6): 976 x * * = x *. [para(955(a,1),125(a,1,2)),rewrite(806(4),955(5)),flip(a)]. given #136 (T,wt=10): 977 (1 + x ^) * = 1 + x ^. [para(811(a,1),955(a,1,1)),rewrite(811(5),17(8),12(6),799(10),7(6),896(6),811(5)),flip(a)]. given #137 (T,wt=11): 128 1 + (x + y *) = x + y *. [para(122(a,1),35(a,1,2)),flip(a)]. given #138 (T,wt=11): 142 c2 + (x * + y) = x * + y. [para(139(a,1),10(a,1,1)),flip(a)]. given #139 (A,wt=26): 67 1 + (x + y) != x + y | 1 + (x ^ + x * ; y) = x ^ + x * ; y. [para(11(a,1),25(a,1,2,1)),rewrite(11(5))]. given #140 (T,wt=11): 144 c2 + (x + y *) = x + y *. [para(139(a,1),35(a,1,2)),flip(a)]. given #141 (T,wt=11): 159 x + (x ; c2 + y) = x + y. [para(146(a,1),10(a,1,1)),flip(a)]. given #142 (T,wt=11): 164 x + (y + x ; c2) = y + x. [para(146(a,1),35(a,1,2)),flip(a)]. given #143 (T,wt=11): 167 1 + x ; c2 != c2 | x * = c2. [para(78(a,1),22(a,1)),rewrite(7(4),11(9),7(9),139(9))]. given #144 (A,wt=42): 69 x + (y ; (z ; x) + u) != y ; (z ; x) + u | x + ((y ; z) ^ + (y ; z) * ; u) = (y ; z) ^ + (y ; z) * ; u. [para(14(a,1),25(a,1,2,1)),rewrite(14(6))]. given #145 (T,wt=11): 262 x ; x ^ ^ ^ = x ^ ^ ^. [para(244(a,1),58(a,1,2)),rewrite(244(9))]. given #146 (T,wt=11): 276 x ^ + x ^ ^ ; y = x ^. [para(58(a,1),246(a,1,2))]. given #147 (T,wt=11): 288 x ; (x * ; 0) = x * ; 0. [para(46(a,1),33(a,1)),flip(a)]. given #148 (T,wt=11): 325 (1 + x ; (y ; 0)) ^ = 1 ^. [para(14(a,1),305(a,1,1,2))]. given #149 (A,wt=30): 70 x + y ; x != y ; x | x + (y ^ + y * ; (y ; x)) = y ^ + y * ; (y ; x). [para(16(a,1),25(a,1,2)),rewrite(16(5))]. given #150 (T,wt=11): 339 x ; y + x ; 0 = x ; y. [para(85(a,1),7(a,1)),flip(a)]. given #151 (T,wt=9): 1220 x ; 0 + x * = x *. [para(339(a,1),42(a,1,2)),rewrite(20(4),7(5)),flip(a)]. given #152 (T,wt=11): 348 x ; 0 + x ^ ^ = x ^ ^. [para(244(a,1),85(a,1,2)),rewrite(244(8))]. given #153 (T,wt=11): 354 x + (x ; 0 + y) = x + y. [para(341(a,1),10(a,1,1)),flip(a)]. given #154 (A,wt=46): 71 x + (y ; x + (z ; x + u)) != y ; x + (z ; x + u) | x + ((y + z) ^ + (y + z) * ; u) = (y + z) ^ + (y + z) * ; u. [para(17(a,1),25(a,1,2,1)),rewrite(10(4),17(7),10(9))]. given #155 (T,wt=11): 359 x + (y + x ; 0) = y + x. [para(341(a,1),35(a,1,2)),flip(a)]. given #156 (T,wt=11): 409 x ; 0 != 0 | x * ; 0 = 0. [para(33(a,1),50(a,1)),rewrite(7(9),127(9))]. given #157 (T,wt=11): 520 x * != 1 | (x ; x *) * = 1. [para(20(a,1),491(a,1))]. given #158 (T,wt=11): 522 1 + x != 1 | (1 + x) * = 1. [para(36(a,1),491(a,1))]. given #159 (A,wt=24): 72 x + (y + z ; (x + y)) != z ; (x + y) | x + (y + z ^) = z ^. [para(10(a,1),27(a,1)),rewrite(10(10))]. given #160 (T,wt=11): 524 x + 1 != 1 | (x + 1) * = 1. [para(38(a,1),491(a,1))]. given #161 (T,wt=11): 525 1 + x != 1 | (c2 + x) * = 1. [para(77(a,1),491(a,1))]. given #162 (T,wt=11): 526 x + 1 != 1 | (x + c2) * = 1. [para(100(a,1),491(a,1))]. given #163 (T,wt=11): 536 c2 ; x + (y + x) = y + x. [para(38(a,1),102(a,2)),rewrite(132(5))]. given #164 (A,wt=12): 73 1 + x != x | 1 + x ^ = x ^. [para(11(a,1),27(a,1,2)),rewrite(11(4))]. given #165 (T,wt=10): 1435 c2 != 1 | 1 + c2 ^ = c2 ^. [para(29(a,1),73(a,1)),flip(a)]. given #166 (T,wt=11): 586 c2 ; (x ; 0) + x * = x *. [para(542(a,1),47(a,1,2,1,2,1)),rewrite(542(12),14(9),14(8),15(7),7(8),96(9),542(11))]. given #167 (T,wt=11): 686 c2 ; (c2 ; x) ^ = (c2 ; x) ^. [para(59(a,1),81(a,1,2)),rewrite(59(11))]. given #168 (T,wt=11): 689 x ^ + (x ^ ; y) ^ = x ^. [para(59(a,1),246(a,1,2))]. given #169 (A,wt=24): 75 x + y ; (z ; x) != y ; (z ; x) | x + (y ; z) ^ = (y ; z) ^. [para(14(a,1),27(a,1,2)),rewrite(14(5))]. given #170 (T,wt=11): 722 c2 ^ + (c2 ; x) ^ ^ = c2 ^. [para(59(a,1),687(a,1,2,1))]. given #171 (T,wt=11): 767 c2 ; (x ; 0) + x ^ = x ^. [para(542(a,1),61(a,1,1,2,1)),rewrite(23(2),542(10),14(7),14(6),15(5),7(6),542(11))]. given #172 (T,wt=11): 817 x ^ ; (1 + y ; 0) = x ^. [para(249(a,1),799(a,1,2))]. given #173 (T,wt=11): 921 1 ^ != x ^ | x ^ ^ = 1 ^. [para(911(a,1),27(a,1,2)),rewrite(91(4),911(6),91(9)),flip(b)]. given #174 (A,wt=28): 76 x + (y ; x + z ; x) != y ; x + z ; x | x + (y + z) ^ = (y + z) ^. [para(17(a,1),27(a,1,2)),rewrite(17(6))]. given #175 (T,wt=8): 1554 (x * + y) ^ = 1 ^. [para(290(a,1),76(a,1,2,1)),rewrite(91(8),16(5),290(6),91(8),91(11)),flip(b),xx(a)]. given #176 (T,wt=7): 1574 (1 + x) ^ = 1 ^. [para(45(a,1),1554(a,1,1,1))]. given #177 (T,wt=7): 1577 (x + 1) ^ = 1 ^. [para(7(a,1),1574(a,1,1))]. given #178 (T,wt=8): 1555 (x + y *) ^ = 1 ^. [para(290(a,1),76(a,1,2,2)),rewrite(7(8),91(8),16(5),290(9),7(8),91(8),91(11)),flip(b),xx(a)]. given #179 (A,wt=13): 86 x ; 0 + y != 0 | x * ; y = 0. [para(33(a,1),22(a,1)),rewrite(7(9),33(9))]. given #180 (T,wt=9): 1576 (x * ; y *) ^ = 1 ^. [para(46(a,1),1554(a,1,1))]. given #181 (T,wt=9): 1578 (x + (1 + y)) ^ = 1 ^. [para(35(a,1),1574(a,1,1))]. given #182 (T,wt=9): 1579 (x + (y + 1)) ^ = 1 ^. [para(10(a,1),1577(a,1,1))]. given #183 (T,wt=10): 1575 (x + (y * + z)) ^ = 1 ^. [para(35(a,1),1554(a,1,1))]. given #184 (A,wt=13): 90 x ; y + x ; 1 ^ = x ; 1 ^. [hyper(19,a,74,a)]. given #185 (T,wt=10): 1580 (x + (y + z *)) ^ = 1 ^. [para(10(a,1),1555(a,1,1))]. given #186 (T,wt=11): 1077 x ; c2 + (y + x) = y + x. [para(38(a,1),159(a,2)),rewrite(132(5))]. given #187 (T,wt=11): 1173 x ^ + x ^ ^ ^ ^ = x ^. [para(262(a,1),246(a,1,2))]. given #188 (T,wt=11): 1253 x ; 0 + (y + x) = y + x. [para(38(a,1),354(a,2)),rewrite(132(5))]. given #189 (A,wt=13): 92 x ; y + 1 ^ ; y = 1 ^ ; y. [para(74(a,1),17(a,1,1)),flip(a)]. given #190 (T,wt=11): 1366 x + 1 != 1 | (1 + x) * = 1. [para(7(a,1),522(a,1))]. given #191 (T,wt=11): 1380 1 + x != 1 | (x + 1) * = 1. [para(7(a,1),524(a,1))]. given #192 (T,wt=11): 1382 x + 1 != 1 | (c2 + x) * = 1. [para(7(a,1),525(a,1))]. given #193 (T,wt=11): 1388 1 + x != 1 | (x + c2) * = 1. [para(7(a,1),526(a,1))]. given #194 (A,wt=24): 95 x + (y + z) != x + z | u ; y + u ; (x + z) = u ; (x + z). [para(35(a,1),19(a,1))]. given #195 (T,wt=11): 1403 x ^ + c2 ; x ^ ^ = x ^. [para(261(a,1),536(a,1,2)),rewrite(7(6),261(10))]. given #196 (T,wt=11): 1545 c2 + (c2 + x) ^ = (c2 + x) ^. [para(30(a,1),76(a,1,2,1)),rewrite(36(6),30(7)),xx(a)]. given #197 (T,wt=9): 1786 c2 + c2 ^ ^ = c2 ^ ^. [para(84(a,1),1545(a,1,2,1)),rewrite(84(9))]. given #198 (T,wt=11): 1546 c2 + (x + c2) ^ = (x + c2) ^. [para(30(a,1),76(a,1,2,2)),rewrite(7(5),36(6),30(9),7(8)),xx(a)]. given #199 (A,wt=13): 96 1 + (x + y ; y *) = x + y *. [para(20(a,1),35(a,1,2)),flip(a)]. given #200 (T,wt=7): 1823 x + x * = x *. [para(125(a,1),96(a,1,2)),rewrite(20(4)),flip(a)]. given #201 (T,wt=9): 1842 c2 ; x + x * = x *. [para(1823(a,1),102(a,2)),rewrite(1836(5))]. given #202 (T,wt=9): 1845 x ; c2 + x * = x *. [para(1823(a,1),159(a,2)),rewrite(1836(5))]. given #203 (T,wt=11): 1590 (x * ; (1 + y ^)) ^ = 1 ^. [para(811(a,1),1576(a,1,1,2))]. given #204 (A,wt=21): 97 x + (y + (z ; x + u)) != x | z * ; (y + u) + x = x. [para(35(a,1),22(a,1,2))]. given #205 (T,wt=11): 1591 (x + (y + (1 + z))) ^ = 1 ^. [para(10(a,1),1578(a,1,1))]. given #206 (T,wt=11): 1592 (x + (y + (z + 1))) ^ = 1 ^. [para(10(a,1),1579(a,1,1,2))]. given #207 (T,wt=11): 1594 (x + y * ; z *) ^ = 1 ^. [para(46(a,1),1575(a,1,1,2))]. given #208 (T,wt=11): 1598 x + x ; 1 ^ = x ; 1 ^. [para(11(a,1),90(a,1,1))]. given #209 (A,wt=38): 98 x ; y + (z + u) != y + (z + (x ; y + u)) | y + (x ^ + x * ; (z + u)) = x ^ + x * ; (z + u). [para(35(a,1),25(a,1,2)),flip(a)]. given #210 (T,wt=11): 1686 x + 1 ^ ; x = 1 ^ ; x. [para(12(a,1),92(a,1,1))]. given #211 (T,wt=11): 1804 c2 + c2 ^ ^ ^ = c2 ^ ^ ^. [para(1786(a,1),1545(a,1,2,1)),rewrite(1786(11))]. given #212 (T,wt=11): 1831 x + (x * + y) = x * + y. [para(1823(a,1),10(a,1,1)),flip(a)]. given #213 (T,wt=11): 1836 x + (y + x *) = y + x *. [para(1823(a,1),35(a,1,2)),flip(a)]. given #214 (A,wt=38): 99 x + (y ; z + u) != z + (y ; z + (x + u)) | z + (y ^ + y * ; (x + u)) = y ^ + y * ; (x + u). [para(35(a,1),25(a,2)),flip(a)]. given #215 (T,wt=11): 1929 (x * ; y * + z) ^ = 1 ^. [para(7(a,1),1594(a,1,1))]. given #216 (T,wt=12): 107 c2 ; x != x | x + c2 ^ = c2 ^. [para(79(a,1),27(a,1)),flip(a)]. given #217 (T,wt=12): 118 x ; 1 ^ != 1 ^ | 1 ^ = x ^. [para(91(a,1),27(a,1)),rewrite(91(10)),flip(a)]. given #218 (T,wt=12): 150 c2 ^ != c2 | x ; c2 ^ = x ; c2. [para(84(a,1),39(a,1)),rewrite(7(10),111(10))]. given #219 (A,wt=13): 103 x + (y + c2 ; (x + y)) = x + y. [para(79(a,1),10(a,1)),flip(a)]. given #220 (T,wt=12): 155 x * != c2 | y ; x * = y ; c2. [para(139(a,1),39(a,1)),rewrite(7(8),141(8))]. given #221 (T,wt=12): 228 x * + c2 ; (x ; x *) = x *. [para(79(a,1),42(a,1,2)),rewrite(20(4)),flip(a)]. given #222 (T,wt=12): 230 x * + x ; (x * ; c2) = x *. [para(146(a,1),42(a,1,2)),rewrite(20(4),14(6)),flip(a)]. given #223 (T,wt=12): 299 x * ; (1 ^ ; y) = 1 ^ ; y. [para(290(a,1),14(a,1,1)),flip(a)]. given #224 (A,wt=19): 105 x + y ; x != x | x + y * ; (c2 ; (y ; x)) = x. [para(79(a,1),22(a,1,2)),rewrite(7(9))]. given #225 (T,wt=12): 401 x * ; (x * ; y) = x * ; y. [para(382(a,1),14(a,1,1)),flip(a)]. given #226 (T,wt=12): 411 x ^ ^ + x * ; 0 = x ^ ^. [para(244(a,1),50(a,1,2)),rewrite(16(5),7(11)),xx(a)]. given #227 (T,wt=12): 550 x * ; (x ^ ; y) = x ^ ; y. [para(58(a,1),56(a,1,2)),rewrite(16(5),58(11),127(12)),xx(a)]. given #228 (T,wt=12): 701 x * ; x ^ ^ ^ = x ^ ^ ^. [para(551(a,1),59(a,1,2,2,1)),rewrite(23(7),551(9))]. given #229 (A,wt=34): 106 x + y ; x != y ; x | x + (y ^ + y * ; (c2 ; (y ; x))) = y ^ + y * ; (c2 ; (y ; x)). [para(79(a,1),25(a,1,2)),rewrite(79(7))]. given #230 (T,wt=12): 703 (x ; (y ; 0)) ^ = x ; (y ; 0). [para(14(a,1),679(a,1,1)),rewrite(14(7))]. given #231 (T,wt=12): 760 x ^ + x ; (c2 ; x ^) = x ^. [para(146(a,1),61(a,1,1,2,1)),rewrite(23(2),146(6),14(5),146(9))]. given #232 (T,wt=12): 810 x ^ ; (y * ; z) = x ^ ; z. [para(799(a,1),14(a,1,1)),flip(a)]. given #233 (T,wt=12): 816 (x ; y ^) * = 1 + x ; y ^. [para(799(a,1),44(a,1,2,2)),flip(a)]. given #234 (A,wt=13): 111 x ; c2 + x ; c2 ^ = x ; c2 ^. [hyper(19,a,84,a)]. given #235 (T,wt=12): 840 1 ^ != 1 | 1 + 1 ^ ; x = 1. [back_rewrite(460),rewrite(811(8),74(9))]. given #236 (T,wt=12): 919 x ^ ; (1 ^ ; y) = x ^ ; y. [para(911(a,1),14(a,1,1)),flip(a)]. given #237 (T,wt=12): 965 1 + x * ; (x ; x *) = x *. [back_rewrite(547),rewrite(956(6))]. given #238 (T,wt=12): 969 (1 + x ; 0) * = 1 + x ; 0. [para(249(a,1),955(a,1,1)),rewrite(249(7),17(10),12(7),14(13),15(12),7(8),895(8),249(7)),flip(a)]. given #239 (A,wt=13): 113 c2 ; x + c2 ^ ; x = c2 ^ ; x. [para(84(a,1),17(a,1,1)),flip(a)]. given #240 (T,wt=8): 2380 c2 ^ ; c2 ^ = c2 ^. [para(23(a,1),113(a,1,1)),rewrite(246(8)),flip(a)]. given #241 (T,wt=6): 2403 c2 ^ ^ = c2 ^. [para(2380(a,1),27(a,1,2)),rewrite(16(5),2380(7),261(11)),flip(b),xx(a)]. given #242 (T,wt=11): 2382 c2 + c2 ^ ; c2 = c2 ^ ; c2. [para(30(a,1),113(a,1,1))]. given #243 (T,wt=12): 1188 x ^ + x ^ ^ ^ ; y = x ^. [para(58(a,1),276(a,1,2))]. given #244 (A,wt=13): 115 1 ^ ; x + y ; x = 1 ^ ; x. [para(91(a,1),17(a,1,1)),flip(a)]. given #245 (T,wt=12): 1190 x ^ + (x ^ ^ ; y) ^ = x ^. [para(59(a,1),276(a,1,2))]. given #246 (T,wt=12): 1191 x ^ + x ^ ^ ^ ^ ^ = x ^. [para(262(a,1),276(a,1,2))]. given #247 (T,wt=12): 1195 x ^ ; (x ^ ; 0) = x ^ ; 0. [para(288(a,1),58(a,1,2)),rewrite(811(2),17(5),12(3),33(5),58(4),811(6),17(9),12(7),33(9)),flip(a)]. given #248 (T,wt=12): 1358 x + 1 != x | 1 + x ^ = x ^. [para(359(a,1),67(a,1)),rewrite(12(5),8(4),12(9),408(9),12(11),408(11))]. given #249 (A,wt=19): 117 x ; 1 ^ + y != 1 ^ | x ^ + x * ; y = 1 ^. [para(91(a,1),25(a,1)),rewrite(91(14)),flip(a),flip(b)]. given #250 (T,wt=12): 1404 x ^ + c2 ; (x ^ ; y) = x ^. [para(246(a,1),536(a,1,2)),rewrite(7(6),246(10))]. given #251 (T,wt=11): 2528 x ^ + (c2 ; x ^) ^ = x ^. [para(59(a,1),1404(a,1,2))]. given #252 (T,wt=12): 1407 x ^ + c2 ; x ^ ^ ^ = x ^. [para(277(a,1),536(a,1,2)),rewrite(7(7),277(12))]. given #253 (T,wt=12): 1409 x ^ + c2 ; (x * ; 0) = x ^. [para(408(a,1),536(a,1,2)),rewrite(7(7),408(12))]. given #254 (A,wt=15): 119 x ; y + x ; (y + z) = x ; (y + z). [hyper(19,a,36,a)]. given #255 (T,wt=10): 2611 c2 ^ ; (c2 ^ + x) = c2 ^. [para(2380(a,1),119(a,1,1)),rewrite(246(9)),flip(a)]. given #256 (T,wt=9): 2640 c2 ; (c2 ^ + x) = c2 ^. [para(2611(a,1),113(a,1,2)),rewrite(7(8),2569(8),2611(11))]. given #257 (T,wt=7): 2643 c2 ^ = c2 ; 1 ^. [para(74(a,1),2640(a,1,2)),flip(a)]. given #258 (T,wt=10): 2718 (c2 ; 1 ^) ^ = c2 ; 1 ^. [back_rewrite(2403),rewrite(2643(2),2643(7))]. given #259 (A,wt=13): 121 x + (y + (x + z)) = y + (x + z). [para(36(a,1),10(a,2,2)),rewrite(35(3),10(2))]. given #260 (T,wt=11): 2604 (x * ; (y * + z)) ^ = 1 ^. [para(119(a,1),1929(a,1,1))]. given #261 (T,wt=10): 2862 (x * ; (1 + y)) ^ = 1 ^. [para(45(a,1),2604(a,1,1,2,1))]. given #262 (T,wt=10): 2864 (x * ; (y + 1)) ^ = 1 ^. [para(7(a,1),2862(a,1,1,2))]. given #263 (T,wt=11): 2861 (x * ; (y + z *)) ^ = 1 ^. [para(7(a,1),2604(a,1,1,2))]. given #264 (A,wt=21): 123 x + (y ; x + z) != x | x + y * ; (y ; x + z) = x. [para(36(a,1),22(a,1,2)),rewrite(7(9))]. given #265 (T,wt=12): 1468 x ^ + (x ^ ; y) ^ ^ = x ^. [para(59(a,1),689(a,1,2,1))]. given #266 (T,wt=12): 1543 x ^ + (x + y) ^ = (x + y) ^. [para(23(a,1),76(a,1,2,1)),rewrite(36(6),23(6)),xx(a)]. given #267 (T,wt=12): 1544 x ^ + (y + x) ^ = (y + x) ^. [para(23(a,1),76(a,1,2,2)),rewrite(7(5),36(6),23(8),7(8)),xx(a)]. given #268 (T,wt=10): 2956 x ^ + (c2 ; x) ^ = x ^. [para(79(a,1),1544(a,1,2,1)),rewrite(7(5),79(8))]. given #269 (A,wt=38): 124 x + (y ; x + z) != y ; x + z | x + (y ^ + y * ; (y ; x + z)) = y ^ + y * ; (y ; x + z). [para(36(a,1),25(a,1,2)),rewrite(36(7))]. given #270 (T,wt=10): 2958 x ^ + (x ; c2) ^ = x ^. [para(146(a,1),1544(a,1,2,1)),rewrite(7(5),146(8))]. ============================== PROOF ================================= % Proof 1 at 1.01 (+ 0.01) seconds. % Length of proof is 29. % Level of proof is 7. % Maximum clause weight is 28. % Given clauses 270. 1 x ; 1 = x & 1 ; x = x # label(non_clause). [assumption]. 2 x + y = y -> z ; x + z ; y = z ; y # label(non_clause). [assumption]. 5 y + x ; y = x ; y -> y + x ^ = x ^ # label(non_clause). [assumption]. 6 (all p (p + 1 = 1 & p ; p = p -> (p ; x) ^ + (p ; x ; p) ^ = (p ; x) ^)) # label(goal). [goal]. 7 x + y = y + x. [assumption]. 9 x + (y + z) = x + y + z. [assumption]. 10 x + y + z = x + (y + z). [copy(9),flip(a)]. 11 x ; 1 = x. [clausify(1)]. 13 x ; (y ; z) = x ; y ; z. [assumption]. 14 x ; y ; z = x ; (y ; z). [copy(13),flip(a)]. 16 x + x = x. [assumption]. 17 (x + y) ; z = x ; z + y ; z. [assumption]. 18 x + y != y | z ; y = z ; x + z ; y. [clausify(2)]. 19 x + y != y | z ; x + z ; y = z ; y. [copy(18),flip(b)]. 23 x ; x ^ = x ^. [assumption]. 26 x ; y != y + x ; y | x ^ = y + x ^. [clausify(5)]. 27 x + y ; x != y ; x | x + y ^ = y ^. [copy(26),flip(a),flip(b)]. 28 c2 + 1 = 1. [deny(6)]. 29 1 + c2 = 1. [copy(28),rewrite(7(3))]. 31 (c2 ; c1) ^ != (c2 ; c1) ^ + (c2 ; c1 ; c2) ^. [deny(6)]. 32 (c2 ; c1) ^ + (c2 ; (c1 ; c2)) ^ != (c2 ; c1) ^. [copy(31),rewrite(14(13)),flip(a)]. 36 x + (x + y) = x + y. [para(16(a,1),10(a,1,1)),flip(a)]. 39 x + y != x | z ; y + z ; x = z ; x. [para(7(a,1),19(a,1))]. 76 x + (y ; x + z ; x) != y ; x + z ; x | x + (y + z) ^ = (y + z) ^. [para(17(a,1),27(a,1,2)),rewrite(17(6))]. 146 x + x ; c2 = x. [hyper(39,a,29,a),rewrite(11(4),7(3),11(5))]. 1544 x ^ + (y + x) ^ = (y + x) ^. [para(23(a,1),76(a,1,2,2)),rewrite(7(5),36(6),23(8),7(8)),xx(a)]. 2958 x ^ + (x ; c2) ^ = x ^. [para(146(a,1),1544(a,1,2,1)),rewrite(7(5),146(8))]. 3032 (x ; y) ^ + (x ; (y ; c2)) ^ = (x ; y) ^. [para(14(a,1),2958(a,1,2,1))]. 3033 $F. [resolve(3032,a,32,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=270. Generated=18919. Kept=3018. proofs=1. Usable=214. Sos=2213. Demods=902. Limbo=3, Disabled=605. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=15901. Back_subsumed=82. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1208 (3 lex), Back_demodulated=504. Back_unit_deleted=0. Demod_attempts=388722. Demod_rewrites=63459. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=111991. Nonunit_bsub_feature_tests=41227. Megabytes=3.68. User_CPU=1.01, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 14728 exit (max_proofs) Fri Sep 21 17:40:11 2007