============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 12986 was started by mccune on cleo.thornwood, Mon Jun 19 16:39:37 2006 The command was "/home/mccune/bin/prover9 -f x3-ring.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file x3-ring.in assign(order,kbo). clauses(sos). x + 0 = x. x + - x = 0. (x + y) + z = x + (y + z). x + y = y + x. x * (y + z) = (x * y) + (x * z). (x + y) * z = (x * z) + (y * z). (x * y) * z = x * (y * z). x * (x * x) = x. A * B != B * A. end_of_list. ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x + 0 = x. [input]. 2 x + - x = 0. [input]. 3 (x + y) + z = x + (y + z). [input]. 4 x + y = y + x. [input]. 5 x * (y + z) = (x * y) + (x * z). [input]. 6 (x + y) * z = (x * z) + (y * z). [input]. 7 (x * y) * z = x * (y * z). [input]. 8 x * (x * x) = x. [input]. 9 A * B != B * A. [input]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: no changes. Term ordering decisions: % Assigning unary symbol - kb_weight 0 and highest precedence (7). Function symbol KB weights: 0=1. A=1. B=1. *=1. +=1. -=0. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ 0, A, B, *, +, - ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: no changes. % Operation + is associative-commutative; redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 10 x + 0 = x. [input]. 11 x + - x = 0. [input]. 12 (x + y) + z = x + (y + z). [input]. 13 x + y = y + x. [input]. 14 (x * y) + (x * z) = x * (y + z). [copy(5),flip(a)]. 15 (x * y) + (z * y) = (x + z) * y. [copy(6),flip(a)]. 16 (x * y) * z = x * (y * z). [input]. 17 x * (x * x) = x. [input]. 18 B * A != A * B. [copy(9),flip(a)]. end_of_list. clauses(demodulators). 10 x + 0 = x. [input]. 11 x + - x = 0. [input]. 12 (x + y) + z = x + (y + z). [input]. 13 x + y = y + x. [input]. % (lex-dep) 14 (x * y) + (x * z) = x * (y + z). [copy(5),flip(a)]. 15 (x * y) + (z * y) = (x + z) * y. [copy(6),flip(a)]. 16 (x * y) * z = x * (y * z). [input]. 17 x * (x * x) = x. [input]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=5): 10 x + 0 = x. [input]. given #2 (I,wt=6): 11 x + - x = 0. [input]. given #3 (I,wt=11): 12 (x + y) + z = x + (y + z). [input]. given #4 (I,wt=7): 13 x + y = y + x. [input]. given #5 (I,wt=13): 14 (x * y) + (x * z) = x * (y + z). [copy(5),flip(a)]. given #6 (I,wt=13): 15 (x * y) + (z * y) = (x + z) * y. [copy(6),flip(a)]. given #7 (I,wt=11): 16 (x * y) * z = x * (y * z). [input]. given #8 (I,wt=7): 17 x * (x * x) = x. [input]. given #9 (I,wt=7): 18 B * A != A * B. [copy(9),flip(a)]. given #10 (T,wt=5): 24 0 + x = x. [para(13(a,1),10(a,1))]. given #11 (A,wt=10): 21 x + (y + - (x + y)) = 0. [para(12(a,1),11(a,1))]. given #12 (F,wt=4): 37 - 0 = 0. [para(24(a,1),11(a,1))]. given #13 (F,wt=8): 23 - x + (y + x) = y. [para(11(a,1),12(a,2,2)),demod(13(3),10(5))]. given #14 (T,wt=5): 41 - - x = x. [para(11(a,1),23(a,1,2)),demod(10(4))]. given #15 (T,wt=8): 26 x + (- x + y) = y. [back_demod(22),demod(24(5))]. given #16 (A,wt=11): 25 x + (y + z) = y + (x + z). [para(13(a,1),12(a,1,1)),demod(12(2))]. given #17 (F,wt=8): 48 x + (y + - x) = y. [para(41(a,1),23(a,1,1))]. given #18 (F,wt=9): 46 - (x + - (y + x)) = y. [para(21(a,1),23(a,1,2)),demod(13(6),24(6))]. given #19 (T,wt=9): 47 x + - (x + y) = - y. [para(23(a,1),23(a,1,2)),demod(13(3))]. given #20 (T,wt=10): 68 - (x + y) = - y + - x. [para(23(a,1),47(a,1,2,1)),flip(a)]. given #21 (A,wt=17): 27 (x * y) + ((x * z) + u) = (x * (y + z)) + u. [para(14(a,1),12(a,1,1)),flip(a)]. given #22 (F,wt=11): 29 (x + x) * y = x * (y + y). [para(15(a,1),14(a,1))]. given #23 (F,wt=9): 76 0 * (x + x) = 0 * x. [para(10(a,1),29(a,1,1)),flip(a)]. given #24 (T,wt=9): 77 (x + x) * 0 = x * 0. [para(10(a,1),29(a,2,2))]. given #25 (T,wt=11): 35 x * (x * (x * y)) = x * y. [para(17(a,1),16(a,1,1)),demod(16(3)),flip(a)]. given #26 (A,wt=17): 28 (x * y) + ((z * y) + u) = ((x + z) * y) + u. [para(15(a,1),12(a,1,1)),flip(a)]. given #27 (F,wt=12): 42 - x + (y + (x + z)) = y + z. [para(23(a,1),12(a,1,1)),demod(12(4)),flip(a)]. given #28 (F,wt=12): 43 - x + (y + (z + x)) = y + z. [para(12(a,1),23(a,1,2))]. given #29 (T,wt=12): 55 x + (y + (- x + z)) = y + z. [para(25(a,1),26(a,1,2))]. given #30 (T,wt=12): 57 x + (y + (z + - x)) = y + z. [para(12(a,1),48(a,1,2))]. given #31 (A,wt=17): 30 (x * (y * z)) + (u * z) = ((x * y) + u) * z. [para(16(a,1),15(a,1,1))]. given #32 (F,wt=13): 32 x * ((x * x) + y) = x + (x * y). [para(17(a,1),14(a,1,1)),flip(a)]. given #33 (F,wt=7): 182 x + (x * 0) = x. [para(10(a,1),32(a,1,2)),demod(17(2)),flip(a)]. given #34 (T,wt=5): 214 0 * 0 = 0. [para(182(a,1),24(a,1)),flip(a)]. given #35 (T,wt=5): 222 x * 0 = 0. [para(214(a,1),15(a,1,1)),demod(220(4),24(3)),flip(a)]. given #36 (A,wt=17): 31 (x * y) + (z * (u * y)) = (x + (z * u)) * y. [para(16(a,1),15(a,1,2))]. given #37 (F,wt=9): 226 x * (0 * y) = 0 * y. [para(222(a,1),16(a,1,1)),flip(a)]. given #38 (F,wt=10): 224 x + (x * - (x * x)) = 0. [back_demod(183),demod(222(6))]. given #39 (T,wt=9): 259 - (x * - (x * x)) = x. [para(224(a,1),23(a,1,2)),demod(13(6),24(6))]. given #40 (T,wt=9): 272 x * - (x * x) = - x. [para(259(a,1),41(a,1,1)),flip(a)]. given #41 (A,wt=13): 33 x * (y + (x * x)) = x + (x * y). [para(17(a,1),14(a,1,2)),demod(13(2)),flip(a)]. given #42 (F,wt=9): 285 x * (x * - x) = - x. [para(272(a,1),35(a,1,2,2)),demod(272(6))]. given #43 (F,wt=9): 313 - x * (- x * x) = x. [para(41(a,1),285(a,1,2,2)),demod(41(6))]. given #44 (T,wt=11): 191 x * (x * (x + x)) = x + x. [para(17(a,1),32(a,2,2)),demod(14(3))]. given #45 (T,wt=11): 196 (x + x) * (x * x) = x + x. [para(32(a,1),29(a,2)),demod(17(5))]. given #46 (A,wt=15): 34 x + (y * (x * x)) = (x + y) * (x * x). [para(17(a,1),15(a,1,1))]. given #47 (F,wt=11): 213 x * (y + (0 * y)) = x * y. [para(182(a,1),15(a,2,1)),demod(16(4),14(5))]. given #48 (F,wt=7): 397 x + (0 * x) = x. [para(213(a,1),17(a,1,2)),demod(396(8),228(5),13(3),24(3),16(2),17(2)),flip(a)]. given #49 (T,wt=6): 401 0 * - x = 0. [para(397(a,1),26(a,1,2)),demod(11(2)),flip(a)]. given #50 (T,wt=5): 416 0 * x = 0. [para(41(a,1),401(a,1,2))]. given #51 (A,wt=15): 36 x * (y * (x * (y * (x * y)))) = x * y. [para(17(a,1),16(a,1)),demod(16(4)),flip(a)]. given #52 (F,wt=12): 418 x * (y + (- (x * x) * y)) = 0. [back_demod(257),demod(416(7))]. given #53 (F,wt=13): 163 ((x * x) + y) * x = x + (y * x). [para(17(a,1),30(a,1,1)),flip(a)]. given #54 (T,wt=10): 448 x + (- (x * x) * x) = 0. [para(11(a,1),163(a,1,1)),demod(416(2)),flip(a)]. given #55 (T,wt=9): 478 - (- (x * x) * x) = x. [para(448(a,1),23(a,1,2)),demod(13(6),24(6))]. given #56 (A,wt=14): 44 - (x * y) + (x * (z + y)) = x * z. [para(14(a,1),23(a,1,2))]. given #57 (F,wt=9): 498 - (x * y) = x * - y. [para(23(a,1),44(a,1,2,2)),demod(13(5),66(5))]. given #58 (F,wt=9): 507 - x * - y = x * y. [para(418(a,1),44(a,1,2)),demod(498(2),16(3),311(4),498(3),13(5),24(5))]. given #59 (T,wt=9): 578 - x * y = x * - y. [para(41(a,1),507(a,1,1)),flip(a)]. given #60 (T,wt=13): 229 (x + (y * y)) * y = y + (x * y). [para(17(a,1),31(a,1,2)),demod(13(2)),flip(a)]. given #61 (A,wt=17): 50 (x * y) + (z + (x * u)) = z + (x * (y + u)). [para(14(a,1),25(a,1,2)),flip(a)]. given #62 (F,wt=14): 571 (x + x) * (x * - x) = - x + - x. [para(196(a,1),498(a,1,1)),demod(68(2),498(6)),flip(a)]. given #63 (F,wt=14): 596 x * ((y + (x * (x * - y))) * z) = 0. [back_demod(535),demod(578(2))]. given #64 (T,wt=12): 689 (x + (y * (y * - x))) * y = 0. [para(596(a,1),36(a,1,2,2,2)),demod(222(10),222(6),222(6)),flip(a)]. given #65 (T,wt=13): 701 (x + (y * (y * - x))) * - y = 0. [para(41(a,1),689(a,1,1,2,2,2)),demod(614(5),498(3),498(2))]. given #66 (A,wt=17): 51 (x * y) + (z + (u * y)) = z + ((x + u) * y). [para(15(a,1),25(a,1,2)),flip(a)]. given #67 (F,wt=14): 614 (- x + y) * z = (x + - y) * - z. [para(578(a,1),15(a,1,1)),demod(575(4)),flip(a)]. given #68 (F,wt=14): 625 (x + x) * ((x + (x + x)) * - x) = 0. [back_demod(520),demod(614(7),68(5),41(3),41(3))]. given #69 (T,wt=13): 797 (x + x) * ((x + (x + x)) * x) = 0. [para(41(a,1),625(a,1,2,2)),demod(614(9),68(7),41(5),41(5),614(8),41(2),498(6),41(5))]. given #70 (T,wt=13): 809 x * ((x + (x + x)) * (x + x)) = 0. [para(797(a,1),15(a,2)),demod(14(9),14(7))]. given #71 (A,wt=19): 71 (x * (y + z)) + (u * z) = (x * y) + ((x + u) * z). [para(15(a,1),27(a,1,2)),flip(a)]. given #72 (F,wt=11): 835 (x + (x + x)) * (x + x) = 0. [para(809(a,1),163(a,2,2)),demod(16(9),822(8),809(7),222(4),24(2),809(5),13(7),24(7)),flip(a)]. given #73 (F,wt=13): 960 (x + (x + x)) * ((x + x) * y) = 0. [para(835(a,1),16(a,1,1)),demod(416(2)),flip(a)]. given #74 (T,wt=11): 981 (x + x) * (x + (x + x)) = 0. [para(960(a,1),36(a,1,2,2,2)),demod(222(6),222(5),222(3)),flip(a)]. given #75 (T,wt=13): 966 (x + (x + x)) * (- x + - x) = 0. [para(835(a,1),498(a,1,1)),demod(37(2),68(5)),flip(a)]. given #76 (A,wt=21): 73 (x * y) + (z + ((x * u) + v)) = z + ((x * (y + u)) + v). [para(27(a,1),25(a,1,2)),flip(a)]. given #77 (F,wt=13): 977 (x + (x + x)) * (x * (y + y)) = 0. [para(29(a,1),960(a,1,2))]. given #78 (F,wt=13): 993 (x + x) * ((x + (x + x)) * y) = 0. [para(981(a,1),16(a,1,1)),demod(416(2)),flip(a)]. given #79 (T,wt=13): 1060 x + (x + (x + (x + (x + x)))) = 0. [para(977(a,1),34(a,2)),demod(25(4),13(3),973(8),1005(5),25(5),25(4),25(3),13(2))]. given #80 (T,wt=11): 1085 (x + (x + x)) * (y + y) = 0. [para(28(a,1),1060(a,1,2,2)),demod(14(7),81(7),27(7),15(6))]. given #81 (A,wt=17): 78 (x + (y + (x + y))) * z = (x + y) * (z + z). [para(12(a,1),29(a,1,1))]. given #82 (F,wt=13): 1089 x + (x + (x + x)) = - x + - x. [back_demod(315),demod(1088(8),1064(4))]. given #83 (F,wt=13): 1107 (x + (x + x)) * (y * (z + z)) = 0. [para(14(a,1),1085(a,1,2))]. given #84 (T,wt=13): 1110 (x + (x + x)) * ((y + y) * z) = 0. [para(15(a,1),1085(a,1,2))]. given #85 (T,wt=11): 1276 (x + x) * (y + (y + y)) = 0. [para(1110(a,1),36(a,1,2,2,2)),demod(222(6),222(5),222(3)),flip(a)]. given #86 (A,wt=17): 79 (x + x) * (y + z) = x * (y + (z + (y + z))). [para(12(a,1),29(a,2,2))]. given #87 (F,wt=13): 1283 (x + x) * (y * (z + (z + z))) = 0. [para(14(a,1),1276(a,1,2,2)),demod(14(5))]. given #88 (F,wt=13): 1286 (x + x) * ((y + (y + y)) * z) = 0. [para(15(a,1),1276(a,1,2,2)),demod(15(5))]. given #89 (T,wt=14): 698 (x * y) + (y * (y * (x * - y))) = 0. [para(689(a,1),15(a,2)),demod(16(5),16(4),578(3))]. given #90 (T,wt=11): 1411 x * (x * (y * x)) = y * x. [para(698(a,1),23(a,1,2)),demod(498(5),498(4),498(3),41(2),13(5),24(5))]. given #91 (A,wt=19): 80 (x * (y + y)) + ((x + x) * z) = (x + x) * (y + z). [para(29(a,1),14(a,1,1))]. given #92 (F,wt=13): 1461 x * (x * (y * - x)) = y * - x. [para(1411(a,1),498(a,1,1)),demod(498(2),498(5),498(4)),flip(a)]. given #93 (F,wt=14): 699 (x + (y * (y * - x))) * (y * z) = 0. [para(689(a,1),16(a,1,1)),demod(416(2)),flip(a)]. given #94 (T,wt=14): 712 (x + (y * (y + (y * - x)))) * y = y. [para(689(a,1),163(a,2,2)),demod(50(6),10(8))]. given #95 (T,wt=14): 771 (x + - y) * - z = (y + - x) * z. [para(13(a,1),614(a,1,1)),flip(a)]. given #96 (A,wt=19): 81 ((x + x) * y) + (x * (z + z)) = (x + x) * (y + z). [para(29(a,1),14(a,1,2))]. given #97 (F,wt=14): 1237 - x + (- x + - x) = x + (x + x). [para(1089(a,1),26(a,1,2)),demod(41(2),41(2)),flip(a)]. given #98 (F,wt=14): 1462 x * (y * (z + (x * (x * - z)))) = 0. [para(1411(a,1),596(a,1,2))]. given #99 (T,wt=14): 1538 x * (y * (- z + (x * (x * z)))) = 0. [para(1461(a,1),596(a,1,2)),demod(68(5),498(4),498(3),41(2),13(4))]. given #100 (T,wt=14): 1575 (x + (y * (y * - x))) * (z * y) = 0. [para(1411(a,1),699(a,1,2))]. given #101 (A,wt=17): 82 x * (y + (y + z)) = ((x + x) * y) + (x * z). [para(29(a,2),14(a,1,1)),demod(12(6)),flip(a)]. given #102 (F,wt=15): 84 x * ((y + y) * z) = x * (y * (z + z)). [para(14(a,1),29(a,1,1)),demod(16(3),16(6))]. given #103 (F,wt=15): 85 (x + x) * (y * z) = x * (y * (z + z)). [para(14(a,1),29(a,2,2))]. given #104 (T,wt=15): 90 (x + x) * (y * z) = x * ((y + y) * z). [para(15(a,1),29(a,2,2))]. given #105 (T,wt=15): 99 ((x + x) * y) + z = (x * (y + y)) + z. [para(29(a,2),27(a,2,1)),demod(27(4)),flip(a)]. given #106 (A,wt=17): 83 x * (y + (z + z)) = (x * y) + ((x + x) * z). [para(29(a,2),14(a,1,2)),flip(a)]. given #107 (F,wt=15): 114 x * ((x * (x * y)) + z) = x * (y + z). [para(35(a,1),14(a,1,1)),demod(14(3)),flip(a)]. given #108 (F,wt=15): 115 x * (y + (x * (x * z))) = x * (y + z). [para(35(a,1),14(a,1,2)),demod(14(3)),flip(a)]. given #109 (T,wt=15): 159 (x + (x * y)) * z = x * (z + (y * z)). [para(30(a,1),14(a,1)),demod(13(2),13(5))]. given #110 (T,wt=15): 185 x + (x * (x * y)) = x * (x * (x + y)). [para(14(a,1),32(a,1,2)),flip(a)]. given #111 (A,wt=17): 86 (x + (x + y)) * z = (x * (z + z)) + (y * z). [para(29(a,1),15(a,1,1)),demod(12(6)),flip(a)]. given #112 (F,wt=15): 187 x + (x * (y * x)) = x * ((x + y) * x). [para(15(a,1),32(a,1,2)),flip(a)]. given #113 (F,wt=15): 307 x * ((x * - x) + y) = - x + (x * y). [para(285(a,1),14(a,1,1)),flip(a)]. given #114 (T,wt=15): 308 x * (y + (x * - x)) = - x + (x * y). [para(285(a,1),14(a,1,2)),demod(13(3)),flip(a)]. given #115 (T,wt=15): 340 x * (x * ((x + x) * y)) = (x + x) * y. [para(191(a,1),16(a,1,1)),demod(16(5)),flip(a)]. given #116 (A,wt=17): 87 (x + (y + y)) * z = (x * z) + (y * (z + z)). [para(29(a,1),15(a,1,2)),flip(a)]. given #117 (F,wt=15): 348 x * (x * (x + (x + x))) = x + (x + x). [para(191(a,1),32(a,2,2)),demod(14(4))]. given #118 (F,wt=15): 355 (x + x) * (x * (x * y)) = (x + x) * y. [para(196(a,1),16(a,1,1)),demod(16(5)),flip(a)]. given #119 (T,wt=15): 392 (x + (x + x)) * (x * x) = x + (x + x). [para(196(a,1),34(a,1,2)),flip(a)]. given #120 (T,wt=15): 570 x * (x * (- x + - x)) = - x + - x. [para(191(a,1),498(a,1,1)),demod(68(2),498(6),68(5)),flip(a)]. given #121 (A,wt=19): 88 ((x + x) * y) + (z * (y + y)) = (x + z) * (y + y). [para(29(a,2),15(a,1,1))]. given #122 (F,wt=15): 620 (x * y) + (z * - y) = (x + - z) * y. [back_demod(574),demod(614(8),41(8))]. given #123 (F,wt=15): 627 (x + y) * ((x + y) * (y + x)) = y + x. [back_demod(327),demod(614(8),41(5),68(6),614(9),41(2),498(7),68(6),41(4),41(4))]. given #124 (T,wt=15): 649 x + ((y + y) * z) = x + (y * (z + z)). [para(29(a,2),50(a,2,2)),demod(50(4)),flip(a)]. given #125 (T,wt=15): 963 x * ((x + (x + x)) * x) = x + (x + x). [para(835(a,1),32(a,2,2)),demod(953(7),13(7),12(7),953(8),807(6),13(8),24(8))]. given #126 (A,wt=19): 89 (x * (y + y)) + ((z + z) * y) = (x + z) * (y + y). [para(29(a,2),15(a,1,2))]. given #127 (F,wt=15): 1093 (x + x) * (y + (x * ((x + x) * y))) = 0. [back_demod(622),demod(1089(4),614(6),41(3),41(4))]. given #128 (F,wt=15): 1104 (x + (x + x)) * (y + (z + (y + z))) = 0. [para(12(a,1),1085(a,1,2))]. given #129 (T,wt=15): 1240 (x + x) * (y + y) = x * (- y + - y). [para(1089(a,1),28(a,1)),demod(498(2),498(4),14(5),14(9),81(9)),flip(a)]. given #130 (T,wt=15): 1246 (x + (y * (y * (x + x)))) * (y + y) = 0. [back_demod(704),demod(1240(5),41(2),41(2))]. given #131 (A,wt=23): 94 (x * (y + y)) + (((x + x) * z) + u) = ((x + x) * (y + z)) + u. [para(29(a,1),27(a,1,1))]. given #132 (F,wt=15): 1257 (x + (x + x)) * (y * (z * (u + u))) = 0. [para(14(a,1),1107(a,1,2,2))]. given #133 (F,wt=15): 1260 (x + (x + x)) * (y * ((z + z) * u)) = 0. [para(15(a,1),1107(a,1,2,2))]. given #134 (T,wt=15): 1279 (x + (y + (x + y))) * (z + (z + z)) = 0. [para(12(a,1),1276(a,1,1))]. given #135 (T,wt=15): 1390 (x + x) * (y * (z * (u + (u + u)))) = 0. [para(14(a,1),1283(a,1,2,2,2)),demod(14(5))]. given #136 (A,wt=23): 95 ((x + x) * y) + ((x * (z + z)) + u) = ((x + x) * (y + z)) + u. [para(29(a,1),27(a,1,2,1))]. given #137 (F,wt=15): 1393 (x + x) * (y * ((z + (z + z)) * u)) = 0. [para(15(a,1),1283(a,1,2,2,2)),demod(15(5))]. given #138 (F,wt=15): 1415 (x + ((y + y) * (y * x))) * (y + y) = 0. [para(29(a,1),698(a,1,2,2)),demod(68(5),68(9),14(12),25(10),13(9),1237(9),25(7),25(6),13(5),11(5),10(5),227(8))]. given #139 (T,wt=15): 1416 (x + (y * ((y + y) * x))) * (y + y) = 0. [para(29(a,1),698(a,1,2)),demod(68(5),68(11),14(15),14(12),25(10),13(9),1237(9),25(7),25(6),13(5),11(5),10(5),227(8))]. given #140 (T,wt=15): 1443 x * (x * (y * (x * z))) = y * (x * z). [para(1411(a,1),16(a,1,1)),demod(16(2),16(5),16(4)),flip(a)]. given #141 (A,wt=21): 96 ((x + x) * y) + ((x * z) + u) = (x * (y + (y + z))) + u. [para(29(a,2),27(a,1,1)),demod(12(7))]. given #142 (F,wt=15): 1445 x * (x * (y * (z * x))) = y * (z * x). [para(16(a,1),1411(a,1,2,2)),demod(16(6))]. given #143 (F,wt=15): 1454 x * (x * (x + (y * x))) = x + (y * x). [para(1411(a,1),32(a,2,2)),demod(14(4))]. given #144 (T,wt=15): 1459 x * (y * (x * (y * (y * x)))) = y * x. [para(36(a,1),1411(a,1,2,2)),demod(16(10),16(9),16(8),16(7),36(9),16(7),16(6),16(5),16(4),1411(3),36(10))]. given #145 (T,wt=15): 1576 (x + (y * (y * - x))) * (z * - y) = 0. [para(1461(a,1),699(a,1,2))]. given #146 (A,wt=21): 97 (x * (y + (z + z))) + u = (x * y) + (((x + x) * z) + u). [para(29(a,2),27(a,1,2,1)),flip(a)]. given #147 (F,wt=15): 1664 (x + (y * - y)) * y = - y + (x * y). [para(771(a,1),163(a,1)),demod(578(3),41(2),498(2),578(8),41(7))]. given #148 (F,wt=15): 1756 (x + (x + x)) * y = x * (y + (y + y)). [para(15(a,1),1237(a,2,2)),demod(498(2),498(4),498(6),14(7),14(7),1237(5),15(7)),flip(a)]. given #149 (T,wt=15): 2092 x * (x * (y * (x + x))) = y * (x + x). [back_demod(1446),demod(2007(6),41(2),41(2))]. given #150 (T,wt=15): 2323 (x * (y + y)) + z = z + ((x + x) * y). [para(99(a,1),13(a,1))]. given #151 (A,wt=21): 98 ((x + x) * (y + z)) + u = (x * (y + (z + (y + z)))) + u. [para(29(a,1),27(a,2,1)),demod(27(6),25(7),13(6))]. given #152 (F,wt=15): 2324 ((x + x) * y) + z = z + (x * (y + y)). [para(99(a,2),13(a,1))]. given #153 (F,wt=15): 2381 x * ((x + x) * (x * y)) = (x + x) * y. [back_demod(2228),demod(2374(6),41(3))]. given #154 (T,wt=15): 2914 x * ((x + (x * y)) * x) = x + (y * x). [para(185(a,1),163(a,1,1)),demod(16(5),32(4),16(5),2608(4),32(3),16(4),16(7),16(8),35(7),16(7),16(6),1411(7))]. given #155 (T,wt=15): 3413 x * ((x + x) * (y * x)) = y * (x + x). [back_demod(2183),demod(3401(6),498(4),41(3))]. given #156 (A,wt=19): 117 x * (y * (x * (y * (x * (y * z))))) = x * (y * z). [para(35(a,1),16(a,1)),demod(16(2),16(5),16(6)),flip(a)]. given #157 (F,wt=15): 3720 (x + (x + x)) * (y + (x * (x * y))) = 0. [para(392(a,1),159(a,1,1,2)),demod(25(5),13(4),25(4),25(3),13(2),1089(3),48(4),11(2),416(2),16(5)),flip(a)]. given #158 (F,wt=15): 3974 (x + y) * ((y + x) * (x + y)) = x + y. [para(13(a,1),627(a,1,1))]. given #159 (T,wt=15): 3975 (x + y) * ((y + x) * (y + x)) = y + x. [para(13(a,1),627(a,1,2,1))]. given #160 (T,wt=15): 4232 (x + (x + x)) * (y + (z + (z + y))) = 0. [para(13(a,1),1104(a,1,2,2,2))]. given #161 (A,wt=19): 123 ((x + y) * z) + (y * u) = (x * z) + (y * (z + u)). [para(14(a,1),28(a,1,2)),flip(a)]. given #162 (F,wt=15): 4429 (x + (y + (y + x))) * (z + (z + z)) = 0. [para(13(a,1),1279(a,1,1,2,2))]. given #163 (F,wt=15): 4634 x * (y * (x * (y * x))) = y * (y * x). [para(36(a,1),1443(a,1,2)),flip(a)]. given #164 (T,wt=15): 5176 x * (y * (x * (x * y))) = y * (x * y). [para(1411(a,1),1459(a,1,2,2,2)),demod(16(4),4634(5),16(4))]. given #165 (T,wt=15): 6327 (x + x) * (x * (y * x)) = y * (x + x). [para(1411(a,1),2381(a,1,2,2)),demod(3413(4)),flip(a)]. given #166 (A,wt=21): 124 (x * (y * z)) + ((u * z) + v) = (((x * y) + u) * z) + v. [para(16(a,1),28(a,1,1))]. given #167 (F,wt=15): 7450 x * (y * (y * x)) = y * (x * (y * x)). [para(4634(a,1),1443(a,1,2))]. given #168 (F,wt=16): 141 - x + (y + (z + (x + u))) = y + (z + u). [para(12(a,1),42(a,1,2)),demod(12(7))]. given #169 (T,wt=16): 146 - x + (y + (z + (u + x))) = y + (z + u). [para(12(a,1),43(a,1,2,2))]. given #170 (T,wt=16): 149 x + (y + (z + (- x + u))) = y + (z + u). [para(12(a,1),55(a,1,2)),demod(12(7))]. given #171 (A,wt=21): 125 (x * y) + ((z * (u * y)) + v) = ((x + (z * u)) * y) + v. [para(16(a,1),28(a,1,2,1))]. given #172 (F,wt=16): 154 x + (y + (z + (u + - x))) = y + (z + u). [para(12(a,1),57(a,1,2,2))]. given #173 (F,wt=16): 319 ((x * x) + y) * - x = - x + (y * - x). [para(285(a,1),30(a,1,1)),flip(a)]. given #174 (T,wt=16): 322 (x + (y * y)) * - y = - y + (x * - y). [para(285(a,1),31(a,1,2)),demod(13(4)),flip(a)]. given #175 (T,wt=16): 575 (x * - y) + (z * y) = (x + - z) * - y. [para(507(a,1),15(a,1,2))]. given #176 (A,wt=19): 126 ((x + y) * (x * x)) + z = x + ((y * (x * x)) + z). [para(17(a,1),28(a,1,1)),flip(a)]. given #177 (F,wt=16): 696 (x + ((y * (y * - x)) + z)) * y = z * y. [para(689(a,1),15(a,1,1)),demod(24(3),12(6)),flip(a)]. given #178 (F,wt=15): 8803 ((x * (x * y)) + z) * x = (y + z) * x. [para(26(a,1),696(a,1,1,2)),demod(498(6),498(5),41(4)),flip(a)]. given #179 (T,wt=15): 8805 (x + (y * (y * z))) * y = (z + x) * y. [para(48(a,1),696(a,1,1,2)),demod(498(6),498(5),41(4)),flip(a)]. given #180 (T,wt=16): 784 (x + (y * - y)) * - y = y + (x * - y). [para(614(a,1),229(a,1)),demod(498(2),578(7))]. given #181 (A,wt=19): 127 ((x + y) * (y * y)) + z = y + ((x * (y * y)) + z). [para(17(a,1),28(a,1,2,1)),demod(25(4)),flip(a)]. given #182 (F,wt=16): 1557 (x + (y * (y * - x))) * ((y + y) * z) = 0. [para(29(a,2),699(a,1,2))]. given #183 (F,wt=16): 1755 (x + (x + x)) * - y = (x + (x + x)) * y. [para(1237(a,1),15(a,2,1)),demod(578(2),614(6),41(4),15(6))]. given #184 (T,wt=16): 1769 x * (y * ((z + (x * (x * - z))) * u)) = 0. [para(1462(a,1),16(a,1,1)),demod(416(2),16(7)),flip(a)]. given #185 (T,wt=16): 1771 x * (y * (z * (u + (x * (x * - u))))) = 0. [para(16(a,1),1462(a,1,2))]. given #186 (A,wt=21): 129 (x * y) + (z + ((u * y) + v)) = z + (((x + u) * y) + v). [para(28(a,1),25(a,1,2)),flip(a)]. given #187 (F,wt=16): 1777 x * (y + (y * (x * (x * (y * - y))))) = 0. [para(32(a,1),1462(a,1,2)),demod(498(2))]. given #188 (F,wt=14): 9675 (x * y) + (y * (x * (y * - y))) = 0. [para(1777(a,1),14(a,2)),demod(7491(7))]. given #189 (T,wt=11): 9721 x * (y * (x * x)) = y * x. [para(9675(a,1),23(a,1,2)),demod(498(5),498(4),498(3),41(2),13(5),24(5))]. given #190 (T,wt=11): 9838 x * (y * y) = y * (x * y). [para(9721(a,1),1443(a,1,2)),flip(a)]. given #191 (A,wt=23): 132 (x * (y + z)) + ((u * z) + v) = (x * y) + (((x + u) * z) + v). [para(28(a,1),27(a,1,2)),flip(a)]. given #192 (F,wt=12): 9730 (x + (y * (x * - y))) * y = 0. [para(163(a,1),9675(a,1,1)),demod(179(7),12(8),618(7),68(3),498(2),13(4),658(8),26(5))]. given #193 (F,wt=12): 10332 ((x * y) + (y * - x)) * x = 0. [para(14(a,1),9730(a,1,1)),demod(16(3),1518(5))]. given #194 (T,wt=12): 10474 ((x * y) + (y * - x)) * y = 0. [para(123(a,1),10332(a,1,1)),demod(68(3),26(5),10401(6))]. given #195 (T,wt=12): 10488 (x + (x * (y * - y))) * y = 0. [para(10332(a,1),9721(a,1,2)),demod(222(2),16(3),498(5),8803(8)),flip(a)]. given #196 (A,wt=23): 133 ((x + y) * z) + ((y * u) + v) = (x * z) + ((y * (z + u)) + v). [para(27(a,1),28(a,1,2)),flip(a)]. given #197 (F,wt=13): 9774 (x + (y * (x * - y))) * - y = 0. [para(319(a,1),9675(a,1,1)),demod(41(10),578(9),179(10),578(10),498(9),41(8),12(9),586(8),68(4),498(3),13(5),8468(10),26(5))]. given #198 (F,wt=13): 9798 x * (y * (x * - x)) = y * - x. [para(9721(a,1),498(a,1,1)),demod(498(2),498(5),498(4)),flip(a)]. given #199 (T,wt=13): 10045 x * (y * - y) = y * (x * - y). [para(9838(a,1),498(a,1,1)),demod(498(3),498(2),498(5)),flip(a)]. given #200 (T,wt=13): 10575 (x + (x * (y * - y))) * - y = 0. [para(15(a,1),10488(a,1,1)),demod(16(8),16(7),578(6),285(7))]. given #201 (A,wt=21): 134 ((x + (x + y)) * z) + u = (x * (z + z)) + ((y * z) + u). [para(29(a,1),28(a,1,1)),demod(12(7)),flip(a)]. given #202 (F,wt=14): 10335 (x + (y * (x * - y))) * (y * z) = 0. [para(9730(a,1),16(a,1,1)),demod(416(2)),flip(a)]. given #203 (F,wt=10): 11135 (x * y) + (y * - x) = 0. [para(10335(a,1),1411(a,1,2)),demod(222(6),1518(6)),flip(a)]. % Operation * is associative-commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 1 at 3.98 (+ 0.06) seconds. % Length of proof is 78. % Level of proof is 26. % Maximum clause weight is 20. % Given clauses 203. 5 x * (y + z) = (x * y) + (x * z). [input]. 6 (x + y) * z = (x * z) + (y * z). [input]. 9 A * B != B * A. [input]. 10 x + 0 = x. [input]. 11 x + - x = 0. [input]. 12 (x + y) + z = x + (y + z). [input]. 13 x + y = y + x. [input]. 14 (x * y) + (x * z) = x * (y + z). [copy(5),flip(a)]. 15 (x * y) + (z * y) = (x + z) * y. [copy(6),flip(a)]. 16 (x * y) * z = x * (y * z). [input]. 17 x * (x * x) = x. [input]. 18 B * A != A * B. [copy(9),flip(a)]. 22 x + (- x + y) = 0 + y. [para(11(a,1),12(a,1,1)),flip(a)]. 23 - x + (y + x) = y. [para(11(a,1),12(a,2,2)),demod(13(3),10(5))]. 24 0 + x = x. [para(13(a,1),10(a,1))]. 25 x + (y + z) = y + (x + z). [para(13(a,1),12(a,1,1)),demod(12(2))]. 26 x + (- x + y) = y. [back_demod(22),demod(24(5))]. 30 (x * (y * z)) + (u * z) = ((x * y) + u) * z. [para(16(a,1),15(a,1,1))]. 31 (x * y) + (z * (u * y)) = (x + (z * u)) * y. [para(16(a,1),15(a,1,2))]. 32 x * ((x * x) + y) = x + (x * y). [para(17(a,1),14(a,1,1)),flip(a)]. 35 x * (x * (x * y)) = x * y. [para(17(a,1),16(a,1,1)),demod(16(3)),flip(a)]. 36 x * (y * (x * (y * (x * y)))) = x * y. [para(17(a,1),16(a,1)),demod(16(4)),flip(a)]. 41 - - x = x. [para(11(a,1),23(a,1,2)),demod(10(4))]. 42 - x + (y + (x + z)) = y + z. [para(23(a,1),12(a,1,1)),demod(12(4)),flip(a)]. 44 - (x * y) + (x * (z + y)) = x * z. [para(14(a,1),23(a,1,2))]. 47 x + - (x + y) = - y. [para(23(a,1),23(a,1,2)),demod(13(3))]. 50 (x * y) + (z + (x * u)) = z + (x * (y + u)). [para(14(a,1),25(a,1,2)),flip(a)]. 66 (x * y) + - (x * (y + z)) = - (x * z). [para(14(a,1),47(a,1,2,1))]. 68 - (x + y) = - y + - x. [para(23(a,1),47(a,1,2,1)),flip(a)]. 163 ((x * x) + y) * x = x + (y * x). [para(17(a,1),30(a,1,1)),flip(a)]. 179 ((x * x) + y) * (x * z) = (x + (y * x)) * z. [para(35(a,1),30(a,1,1)),demod(31(4)),flip(a)]. 182 x + (x * 0) = x. [para(10(a,1),32(a,1,2)),demod(17(2)),flip(a)]. 183 x + (x * - (x * x)) = x * 0. [para(11(a,1),32(a,1,2)),flip(a)]. 213 x * (y + (0 * y)) = x * y. [para(182(a,1),15(a,2,1)),demod(16(4),14(5))]. 214 0 * 0 = 0. [para(182(a,1),24(a,1)),flip(a)]. 220 x + (y * 0) = x. [para(182(a,1),42(a,1,2,2)),demod(23(3)),flip(a)]. 222 x * 0 = 0. [para(214(a,1),15(a,1,1)),demod(220(4),24(3)),flip(a)]. 224 x + (x * - (x * x)) = 0. [back_demod(183),demod(222(6))]. 228 (x + (y * z)) * (z * z) = ((x * z) + y) * z. [para(17(a,1),31(a,1,2,2)),demod(30(4)),flip(a)]. 257 x * (y + (- (x * x) * y)) = 0 * y. [para(224(a,1),15(a,2,1)),demod(16(5),14(6))]. 259 - (x * - (x * x)) = x. [para(224(a,1),23(a,1,2)),demod(13(6),24(6))]. 272 x * - (x * x) = - x. [para(259(a,1),41(a,1,1)),flip(a)]. 285 x * (x * - x) = - x. [para(272(a,1),35(a,1,2,2)),demod(272(6))]. 311 x * (x * (- x * y)) = - x * y. [para(285(a,1),16(a,1,1)),demod(16(5)),flip(a)]. 396 x * ((y + (0 * y)) * z) = x * (y * z). [para(213(a,1),16(a,1,1)),demod(16(2)),flip(a)]. 397 x + (0 * x) = x. [para(213(a,1),17(a,1,2)),demod(396(8),228(5),13(3),24(3),16(2),17(2)),flip(a)]. 401 0 * - x = 0. [para(397(a,1),26(a,1,2)),demod(11(2)),flip(a)]. 416 0 * x = 0. [para(41(a,1),401(a,1,2))]. 418 x * (y + (- (x * x) * y)) = 0. [back_demod(257),demod(416(7))]. 437 x * ((y + (- (x * x) * y)) * z) = 0. [para(418(a,1),16(a,1,1)),demod(416(2)),flip(a)]. 498 - (x * y) = x * - y. [para(23(a,1),44(a,1,2,2)),demod(13(5),66(5))]. 507 - x * - y = x * y. [para(418(a,1),44(a,1,2)),demod(498(2),16(3),311(4),498(3),13(5),24(5))]. 535 x * ((y + (x * (- x * y))) * z) = 0. [back_demod(437),demod(498(2),16(3))]. 575 (x * - y) + (z * y) = (x + - z) * - y. [para(507(a,1),15(a,1,2))]. 578 - x * y = x * - y. [para(41(a,1),507(a,1,1)),flip(a)]. 585 (x * y) + (z * (u * - y)) = (- x + (z * u)) * - y. [para(507(a,1),31(a,1,1))]. 596 x * ((y + (x * (x * - y))) * z) = 0. [back_demod(535),demod(578(2))]. 614 (- x + y) * z = (x + - y) * - z. [para(578(a,1),15(a,1,1)),demod(575(4)),flip(a)]. 618 (x * y) + (z * (u * - y)) = (x + (z * - u)) * y. [back_demod(585),demod(614(10),498(7),41(10))]. 658 x + ((y + (x * z)) * x) = (y + (x * (x + z))) * x. [para(50(a,1),163(a,1,1)),flip(a)]. 689 (x + (y * (y * - x))) * y = 0. [para(596(a,1),36(a,1,2,2,2)),demod(222(10),222(6),222(6)),flip(a)]. 698 (x * y) + (y * (y * (x * - y))) = 0. [para(689(a,1),15(a,2)),demod(16(5),16(4),578(3))]. 1411 x * (x * (y * x)) = y * x. [para(698(a,1),23(a,1,2)),demod(498(5),498(4),498(3),41(2),13(5),24(5))]. 1443 x * (x * (y * (x * z))) = y * (x * z). [para(1411(a,1),16(a,1,1)),demod(16(2),16(5),16(4)),flip(a)]. 1459 x * (y * (x * (y * (y * x)))) = y * x. [para(36(a,1),1411(a,1,2,2)),demod(16(10),16(9),16(8),16(7),36(9),16(7),16(6),16(5),16(4),1411(3),36(10))]. 1461 x * (x * (y * - x)) = y * - x. [para(1411(a,1),498(a,1,1)),demod(498(2),498(5),498(4)),flip(a)]. 1462 x * (y * (z + (x * (x * - z)))) = 0. [para(1411(a,1),596(a,1,2))]. 1518 x * (y + (x * (z * - x))) = (x * y) + (z * - x). [para(1461(a,1),14(a,1,2)),flip(a)]. 1777 x * (y + (y * (x * (x * (y * - y))))) = 0. [para(32(a,1),1462(a,1,2)),demod(498(2))]. 4634 x * (y * (x * (y * x))) = y * (y * x). [para(36(a,1),1443(a,1,2)),flip(a)]. 5176 x * (y * (x * (x * y))) = y * (x * y). [para(1411(a,1),1459(a,1,2,2,2)),demod(16(4),4634(5),16(4))]. 7491 x * (y * (x * (x * (y * z)))) = y * (x * (y * z)). [para(5176(a,1),16(a,1,1)),demod(16(3),16(2),16(7),16(6),16(5)),flip(a)]. 9675 (x * y) + (y * (x * (y * - y))) = 0. [para(1777(a,1),14(a,2)),demod(7491(7))]. 9730 (x + (y * (x * - y))) * y = 0. [para(163(a,1),9675(a,1,1)),demod(179(7),12(8),618(7),68(3),498(2),13(4),658(8),26(5))]. 10335 (x + (y * (x * - y))) * (y * z) = 0. [para(9730(a,1),16(a,1,1)),demod(416(2)),flip(a)]. 11135 (x * y) + (y * - x) = 0. [para(10335(a,1),1411(a,1,2)),demod(222(6),1518(6)),flip(a)]. 11191 x * y = y * x. [para(11135(a,1),23(a,1,2)),demod(498(3),41(2),13(3),24(3))]. 11192 $F. [resolve(11191,a,18,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=203. Generated=45677. Kept=11182. proofs=1. Usable=141. Sos=8386. Demods=5101. Denials=0. Limbo=5, Disabled=2658. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=31894. Back_subsumed=231. Sos_limit_deleted=2601. Sos_displaced=0. Sos_removed=0. New_demodulators=7212 (4 lex), Back_demodulated=2418. Back_unit_deleted=0. Demod_attempts=1125774. Demod_rewrites=237712. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=12.60. User_CPU=3.98, System_CPU=0.06, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 12986 exit (max_proofs) Mon Jun 19 16:39:41 2006