============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3855 was started by mccune on cleo.thornwood, Wed Nov 22 11:24:10 2006 The command was "/home/mccune/bin/prover9 -f cs.in AE.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file cs.in op(450,infix,@). op(400,infix_right,*). assign(new_constants,1). assign(max_weight,25). formulas(sos). x * y != x * z | y = z. y * x != z * x | y = z. (x * y) * z = x * y * z. y * x * (x @ y) = x * y. end_of_list. % Reading from file AE.in formulas(sos). (x @ y) @ z = u @ (v @ w). end_of_list. formulas(sos). A * B * C * B * A != B * A * C * A * B # answer(E). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x * y != x * z | y = z. [assumption]. x * y != z * y | x = z. [assumption]. (x * y) * z = x * y * z. [assumption]. x * y * (y @ x) = y * x. [assumption]. (x @ y) @ z = u @ (v @ w). [assumption]. A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. 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([ A, B, C, *, @ ]). 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). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 x * y != x * z | y = z. [assumption]. 2 x * y != z * y | x = z. [assumption]. 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. 5 (x @ y) @ z = u @ (v @ w). [assumption]. 6 A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. end_of_list. formulas(demodulators). 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=10): 1 x * y != x * z | y = z. [assumption]. given #2 (I,wt=10): 2 x * y != z * y | x = z. [assumption]. given #3 (I,wt=11): 3 (x * y) * z = x * y * z. [assumption]. given #4 (I,wt=11): 4 x * y * (y @ x) = y * x. [assumption]. given #5 (I,wt=11): 5 (x @ y) @ z = u @ (v @ w). [assumption]. given #6 (I,wt=19): 6 A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. given #7 (F,wt=23): 20 A * B * C * B * A * x != B * A * C * A * B * x # answer(E). [ur(2,b,6,a),rewrite(3(10),3(9),3(8),3(7),3(20),3(19),3(18),3(17))]. given #8 (F,wt=23): 21 x * A * B * C * B * A != x * B * A * C * A * B # answer(E). [ur(1,b,6,a)]. given #9 (T,wt=7): 9 x * (x @ x) = x. [hyper(1,a,4,a)]. given #10 (T,wt=10): 24 x * y != x | x @ x = y. [para(9(a,1),1(a,1)),flip(a)]. given #11 (A,wt=14): 7 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite(3(4))]. given #12 (F,wt=23): 22 B * A * C * A * B * (A @ B) != A * B * C * A * B # answer(E). [para(4(a,1),20(a,1,2,2,2)),flip(a)]. given #13 (F,wt=23): 23 A * B * C * B * A * (B @ A) != B * A * C * B * A # answer(E). [para(4(a,1),20(a,2,2,2,2))]. given #14 (T,wt=10): 25 x * (y @ y) != y | y = x. [para(9(a,1),2(a,1)),flip(a)]. given #15 (T,wt=10): 26 x * (y @ y) != y | x = y. [para(9(a,1),2(a,2))]. given #16 (A,wt=14): 8 x * y * z != u * z | x * y = u. [para(3(a,1),2(a,1))]. given #17 (F,wt=23): 31 B * A * C * A * B * (A @ A) != A * B * C * B * A # answer(E). [para(9(a,1),20(a,1,2,2,2,2)),flip(a)]. given #18 (F,wt=23): 32 A * B * C * B * A * (B @ B) != B * A * C * A * B # answer(E). [para(9(a,1),20(a,2,2,2,2,2))]. given #19 (T,wt=11): 18 x @ (y @ z) = u @ (v @ w). [para(5(a,1),5(a,1))]. given #20 (T,wt=11): 19 (x @ y) @ z = (u @ v) @ w. [para(5(a,2),5(a,2))]. given #21 (A,wt=14): 10 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. given #22 (F,wt=9): 50 x * (x @ x * x) = x. [hyper(10,a,3,a)]. given #23 (F,wt=9): 57 x @ x * x = x @ x. [hyper(24,a,50,a),flip(a)]. given #24 (T,wt=11): 27 x * (x @ x) * y = x * y. [para(9(a,1),3(a,1,1)),flip(a)]. given #25 (T,wt=7): 60 (x @ x) * y = y. [hyper(7,a,27,a)]. given #26 (A,wt=14): 11 x * y * (y @ z) != y * z | z = x. [para(4(a,1),2(a,1)),flip(a)]. given #27 (F,wt=6): 77 x != y | y = x. [back_rewrite(66),rewrite(68(4),9(3))]. given #28 (F,wt=9): 70 x * ((y @ y) @ x) = x. [para(60(a,1),4(a,1,2)),rewrite(60(5))]. given #29 (T,wt=7): 102 x * (y @ y) = x. [back_rewrite(68),rewrite(90(3)),flip(a)]. NOTE: New constant: x @ x = c_0. [new_symbol(103)]. NOTE: New Function symbol precedence: lex([ A, B, C, c_0, *, @ ]). given #30 (T,wt=5): 107 x @ x = c_0. [new_symbol(103)]. given #31 (A,wt=14): 12 x * y * (y @ z) != y * z | x = z. [para(4(a,1),2(a,2))]. given #32 (F,wt=5): 111 x * c_0 = x. [back_rewrite(102),rewrite(107(1))]. given #33 (F,wt=5): 115 c_0 @ x = c_0. [back_rewrite(86),rewrite(107(1),107(3))]. given #34 (T,wt=5): 119 c_0 * x = x. [back_rewrite(60),rewrite(107(1))]. given #35 (T,wt=5): 125 x @ c_0 = c_0. [para(107(a,1),18(a,1,2)),rewrite(122(4))]. given #36 (A,wt=15): 13 x * y * (y @ x) * z = y * x * z. [para(4(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)]. given #37 (F,wt=7): 121 x @ x * x = c_0. [back_rewrite(57),rewrite(107(3))]. given #38 (F,wt=7): 122 x @ (y @ z) = c_0. [para(107(a,1),5(a,1,1)),rewrite(115(2)),flip(a)]. given #39 (T,wt=7): 124 (x @ y) @ z = c_0. [para(107(a,1),5(a,2))]. given #40 (T,wt=8): 110 x * y != x | c_0 = y. [back_rewrite(104),rewrite(107(3))]. given #41 (A,wt=17): 14 x * y * z * (z @ x * y) = z * x * y. [para(4(a,1),3(a,1)),flip(a)]. given #42 (F,wt=25): 151 B * A * C * A * B * (A @ C * B) != A * B * A * C * B # answer(E). [para(14(a,1),20(a,1,2,2)),flip(a)]. given #43 (F,wt=25): 152 A * B * C * B * A * (B @ C * A) != B * A * B * C * A # answer(E). [para(14(a,1),20(a,2,2,2))]. given #44 (T,wt=8): 118 x * y != y | c_0 = x. [back_rewrite(69),rewrite(107(3))]. given #45 (T,wt=10): 82 x * y != y * y | y = x. [para(9(a,1),11(a,1,2))]. given #46 (A,wt=17): 15 x * y * z * (y * z @ x) = y * z * x. [para(3(a,1),4(a,1,2)),rewrite(3(7))]. given #47 (F,wt=25): 164 B * A * C * A * B * (B * A @ C) != A * B * B * A * C # answer(E). [para(15(a,1),20(a,1,2,2)),flip(a)]. given #48 (F,wt=25): 165 A * B * C * B * A * (A * B @ C) != B * A * A * B * C # answer(E). [para(15(a,1),20(a,2,2,2))]. given #49 (T,wt=9): 162 x * (x * x @ x) = x. [hyper(7,a,15,a)]. given #50 (T,wt=7): 177 x * x @ x = c_0. [hyper(110,a,162,a),flip(a)]. given #51 (A,wt=11): 33 (x @ y) * z = z * (x @ y). [back_rewrite(16),rewrite(29(6))]. given #52 (F,wt=12): 108 x * y != y | x * (x @ y) = c_0. [back_rewrite(106),rewrite(107(3)),flip(b)]. given #53 (F,wt=12): 109 x * y * z != x * y | c_0 = z. [back_rewrite(105),rewrite(107(5))]. given #54 (T,wt=12): 116 x * (x @ y) != x * y | c_0 = y. [back_rewrite(85),rewrite(107(5))]. given #55 (T,wt=12): 117 x * y * z != z | x * y = c_0. [back_rewrite(75),rewrite(107(4)),flip(b)]. given #56 (A,wt=18): 36 x * y * z * u != x * y * z * v | u = v. [para(3(a,1),7(a,1,2)),rewrite(3(5))]. given #57 (F,wt=12): 198 (x @ y) * z != z | x @ y = c_0. [para(33(a,2),110(a,1)),flip(b)]. given #58 (F,wt=12): 201 x * (y @ z) != x | y @ z = c_0. [para(33(a,1),118(a,1)),flip(b)]. given #59 (T,wt=12): 207 x * y != y * x | x @ y = c_0. [para(4(a,1),109(a,1)),flip(b)]. given #60 (T,wt=12): 221 x @ y != x * y | y * x = c_0. [para(4(a,1),117(a,1)),flip(a)]. given #61 (A,wt=18): 37 x * y * z != x * u * y | u * (u @ y) = z. [para(4(a,1),7(a,1,2)),flip(a)]. given #62 (F,wt=10): 262 x * y != x * z | z = y. [para(111(a,1),37(a,2,2)),rewrite(119(2),125(5),111(5))]. given #63 (F,wt=13): 120 x * y @ x * y * x * y = c_0. [back_rewrite(59),rewrite(107(8))]. given #64 (T,wt=13): 179 x * y * x * y @ x * y = c_0. [para(3(a,1),177(a,1,1))]. given #65 (T,wt=13): 257 x * (y * x @ y) = x * (x @ y). [hyper(37,a,15,a),flip(a)]. given #66 (A,wt=14): 38 x * y * z != y * x | y @ x = z. [para(4(a,1),7(a,1)),flip(a)]. given #67 (F,wt=9): 289 x * y @ x = y @ x. [hyper(262,a,257,a),flip(a)]. given #68 (F,wt=9): 312 (x @ y) * z @ z = c_0. [para(33(a,2),289(a,1,1)),rewrite(124(5))]. given #69 (T,wt=12): 298 x * y != y * x | y @ x = c_0. [para(111(a,1),38(a,1,2))]. given #70 (T,wt=13): 258 x * (x @ x * y) = x * (x @ y). [hyper(37,a,14,a),flip(a)]. given #71 (A,wt=18): 43 x * y * z * u != v * u | x * y * z = v. [para(3(a,1),8(a,1,2))]. given #72 (F,wt=9): 326 x @ x * y = x @ y. [hyper(262,a,258,a),flip(a)]. given #73 (F,wt=9): 357 x @ (y @ z) * x = c_0. [para(33(a,2),326(a,1,2)),rewrite(122(5))]. given #74 (T,wt=13): 307 x * (x @ y) @ y = x * y @ y. [para(4(a,1),289(a,1,1)),flip(a)]. given #75 (T,wt=11): 373 (x @ y) * z * z @ z = c_0. [para(312(a,1),307(a,1,1,2)),rewrite(111(4),312(3),3(4)),flip(a)]. given #76 (A,wt=18): 44 x * y * z != u * v * z | x * y = u * v. [para(3(a,1),8(a,2))]. given #77 (F,wt=13): 315 (x @ y) * z @ z * (x @ y) = c_0. [back_rewrite(287),rewrite(306(8))]. given #78 (F,wt=13): 316 x * (y @ z) @ (y @ z) * x = c_0. [back_rewrite(285),rewrite(306(8))]. given #79 (T,wt=13): 321 x * (y @ z) * u @ x * u = c_0. [para(13(a,1),312(a,1,1)),rewrite(122(5),119(5))]. given #80 (T,wt=13): 353 x @ y * (y @ x) = x @ y * x. [para(4(a,1),326(a,1,2)),flip(a)]. given #81 (A,wt=18): 45 x * y * (y @ z) != u * y * z | u * z = x. [para(4(a,1),8(a,1,2)),flip(a)]. given #82 (F,wt=10): 436 x * y != z * y | z = x. [para(111(a,1),45(a,2,2)),rewrite(125(2),111(2),111(5))]. given #83 (F,wt=11): 425 x @ (y @ z) * x * x = c_0. [para(312(a,1),353(a,1,2,2)),rewrite(111(4),357(3),3(4)),flip(a)]. given #84 (T,wt=13): 363 x * y @ x * (z @ u) * y = c_0. [para(13(a,1),357(a,1,2)),rewrite(122(2),119(2))]. given #85 (T,wt=13): 382 (x @ y) * z * z * z @ z = c_0. [para(373(a,1),307(a,1,1,2)),rewrite(111(5),373(4),3(5),3(4)),flip(a)]. given #86 (A,wt=14): 46 x * (y @ z) != y * z | z * y = x. [para(4(a,1),8(a,1)),flip(a)]. given #87 (F,wt=13): 428 x @ (y @ z) * x * x * x = c_0. [para(373(a,1),353(a,1,2,2)),rewrite(111(5),425(4),3(5),3(4)),flip(a)]. given #88 (F,wt=14): 80 (x @ y) * z != u * (x @ y) | z = u. [para(5(a,1),11(a,1,2,2)),rewrite(29(4)),flip(a)]. given #89 (T,wt=14): 101 x * (y @ z) != u * x | y @ z = u. [back_rewrite(83),rewrite(90(5))]. given #90 (T,wt=14): 143 (x @ y) * z != u * (x @ y) | u = z. [para(124(a,1),12(a,1,2,2)),rewrite(111(3)),flip(a)]. given #91 (A,wt=18): 47 x * y * z * (z @ u) != z * u | x * y = u. [para(4(a,1),8(a,2))]. given #92 (F,wt=14): 181 (x @ y) * z != z * u | x @ y = u. [para(33(a,2),1(a,1))]. given #93 (F,wt=14): 261 x * (y @ x) * z != y * x | y = z. [para(4(a,1),37(a,2)),rewrite(122(7),111(7))]. given #94 (T,wt=12): 502 x * (y @ x) != y * x | c_0 = y. [para(4(a,1),261(a,1)),rewrite(33(2),124(6)),flip(b)]. given #95 (T,wt=14): 271 x * y * z != x * y * u | u = z. [para(3(a,1),262(a,1)),rewrite(3(4))]. given #96 (A,wt=20): 52 x * y * z != u * x * y | u * (u @ x * y) = z. [para(3(a,1),10(a,1))]. given #97 (F,wt=13): 526 x * (x @ y * x) = x * (x @ y). [hyper(52,a,13,a),rewrite(33(5))]. given #98 (F,wt=9): 538 x @ y * x = x @ y. [hyper(262,a,526,a),flip(a)]. given #99 (T,wt=9): 566 x * y @ y = x @ y. [para(4(a,1),538(a,1,2)),rewrite(564(4),307(4)),flip(a)]. given #100 (T,wt=11): 563 x @ y * (y @ x) = x @ y. [back_rewrite(353),rewrite(538(5))]. given #101 (A,wt=20): 53 x * y * z != z * u | x * y * (x * y @ z) = u. [para(3(a,1),10(a,2)),rewrite(3(8)),flip(a)]. given #102 (F,wt=11): 580 x * (x @ y) @ y = x @ y. [back_rewrite(307),rewrite(566(5))]. given #103 (F,wt=13): 557 x * y @ x * (x @ y) = y @ x. [back_rewrite(426),rewrite(538(8),289(6))]. given #104 (T,wt=13): 564 x * (x @ y) @ x * y = x @ y. [back_rewrite(375),rewrite(552(8))]. given #105 (T,wt=13): 565 x @ y * z * x = x @ y * z. [para(3(a,1),538(a,1,2))]. given #106 (A,wt=18): 54 x * y != z * y | z * (z @ y) = x * (x @ y). [para(4(a,1),10(a,1))]. given #107 (F,wt=13): 574 x * y @ y * (y @ x) = x @ y. [back_rewrite(546),rewrite(566(6))]. given #108 (F,wt=13): 575 x * (x @ y) @ y * x = x @ y. [back_rewrite(544),rewrite(566(8),538(6))]. given #109 (T,wt=13): 584 x * y * z @ z = x * y @ z. [para(3(a,1),566(a,1,1))]. given #110 (T,wt=13): 626 x * x * y @ y * x = x @ y. [para(557(a,1),557(a,1,2,2)),rewrite(3(4),4(3),3(5),4(5),564(8))]. given #111 (A,wt=20): 78 x * y * z * (y * z @ u) != y * z * u | u = x. [para(3(a,1),11(a,1,2)),rewrite(3(7))]. given #112 (F,wt=13): 640 x * y @ y * y * x = x @ y. [para(557(a,1),564(a,1,1,2)),rewrite(3(3),4(3),3(5),4(4),557(8))]. given #113 (F,wt=14): 433 x * y * z != y * z | x * z = z. [para(4(a,1),45(a,1)),flip(a)]. given #114 (T,wt=14): 435 x * y != z * x | y * (x @ y) = z. [para(4(a,1),45(a,2)),rewrite(122(2),111(2)),flip(a)]. given #115 (T,wt=11): 763 x * (x @ y) * (y @ x) = x. [hyper(435,a,4,a),rewrite(563(5),3(4))]. given #116 (A,wt=20): 126 x * y * z * (y * z @ u) != y * z * u | x = u. [para(3(a,1),12(a,1,2)),rewrite(3(7))]. given #117 (F,wt=9): 771 (x @ y) * (y @ x) = c_0. [hyper(110,a,763,a),flip(a)]. given #118 (F,wt=10): 797 x @ y != c_0 | y @ x = c_0. [para(771(a,1),110(a,1)),flip(a),flip(b)]. given #119 (T,wt=10): 809 x * y != y | y @ x = x. [para(771(a,1),261(a,1,2)),rewrite(111(2)),flip(a),flip(b)]. given #120 (T,wt=11): 792 (x @ y) * (y @ x) * z = z. [para(771(a,1),3(a,1,1)),rewrite(119(2)),flip(a)]. given #121 (A,wt=18): 127 x * y * z != y * u | x * (x @ y) * z = u. [para(13(a,1),1(a,1))]. given #122 (F,wt=11): 796 (x @ y) * z * (y @ x) = z. [para(771(a,1),13(a,2,2)),rewrite(122(3),119(4),111(6))]. given #123 (F,wt=10): 862 x * y != x | y @ x = y. [para(796(a,1),11(a,1)),flip(a),flip(b)]. given #124 (T,wt=12): 767 x * y != x | y * (x @ y) = c_0. [para(119(a,1),435(a,2))]. given #125 (T,wt=12): 770 x * x * y != x | x * y = c_0. [back_rewrite(620),rewrite(763(4)),flip(a)]. given #126 (A,wt=18): 128 x * y * (y @ z) * u != y * z * u | z = x. [para(13(a,1),2(a,1)),flip(a)]. given #127 (F,wt=12): 790 (x @ y) * z != c_0 | y @ x = z. [para(771(a,1),1(a,1)),flip(a)]. given #128 (F,wt=12): 791 x * (y @ z) != c_0 | z @ y = x. [para(771(a,1),2(a,1)),flip(a)]. given #129 (T,wt=12): 798 x * (y @ z) != x | z @ y = c_0. [para(771(a,1),109(a,1,2)),rewrite(111(2)),flip(a),flip(b)]. given #130 (T,wt=12): 799 x @ y != z | z * (y @ x) = c_0. [para(771(a,1),117(a,1,2)),rewrite(111(2)),flip(a)]. given #131 (A,wt=18): 129 x * y * (y @ z) * u != y * z * u | x = z. [para(13(a,1),2(a,2))]. given #132 (F,wt=12): 802 (x @ y) * z != z | y @ x = c_0. [para(771(a,1),38(a,1,2)),rewrite(111(2),124(5)),flip(a),flip(b)]. given #133 (F,wt=12): 806 x * y != c_0 | y @ x = y * x. [para(771(a,1),46(a,1)),flip(a),flip(b)]. given #134 (T,wt=12): 813 c_0 != x | x * (y @ z) = y @ z. [para(771(a,1),433(a,1,2)),rewrite(111(2),771(3)),flip(a)]. given #135 (T,wt=12): 826 x @ y != z | (y @ x) * z = c_0. [para(792(a,1),110(a,1)),flip(a),flip(b)]. given #136 (A,wt=21): 130 x * y * z * (z @ x * y) * u = z * x * y * u. [para(13(a,1),3(a,1)),rewrite(3(2)),flip(a)]. given #137 (F,wt=12): 890 x * y * x != x | y * x = c_0. [para(4(a,1),770(a,1,2)),rewrite(4(6))]. given #138 (F,wt=12): 912 c_0 != x | (y @ z) * x = y @ z. [para(792(a,1),790(a,1)),flip(a),flip(b)]. given #139 (T,wt=14): 471 x * (y @ z) != u | (y @ z) * x = u. [para(122(a,1),46(a,1,2)),rewrite(111(2)),flip(a)]. given #140 (T,wt=14): 472 (x @ y) * z != u | z * (x @ y) = u. [para(124(a,1),46(a,1,2)),rewrite(111(2)),flip(a)]. given #141 (A,wt=21): 131 x * y * z * (y * z @ x) * u = y * z * x * u. [para(3(a,1),13(a,1,2)),rewrite(3(9))]. given #142 (F,wt=14): 474 (x @ y) * z != x * y | y * x = z. [para(33(a,2),46(a,1))]. given #143 (F,wt=14): 501 x * y * (z @ x) != z * x | z = y. [para(4(a,1),261(a,1,2)),rewrite(122(7),111(7))]. given #144 (T,wt=14): 505 (x @ y) * y * z != x * y | x = z. [para(13(a,1),261(a,1)),rewrite(124(7),119(7))]. given #145 (T,wt=14): 734 x * y * z != z * y | z @ y = x. [para(4(a,1),78(a,2)),rewrite(122(3),111(2))]. given #146 (A,wt=15): 132 x * y * z * (y @ x) = y * x * z. [para(4(a,1),13(a,1,2,2)),rewrite(122(6),111(6))]. ============================== PROOF ================================= % Proof 1 at 0.16 (+ 0.01) seconds: E. % Length of proof is 24. % Level of proof is 12. % Maximum clause weight is 19. % Given clauses 146. 1 x * y != x * z | y = z. [assumption]. 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. 5 (x @ y) @ z = u @ (v @ w). [assumption]. 6 A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. 7 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite(3(4))]. 9 x * (x @ x) = x. [hyper(1,a,4,a)]. 10 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. 13 x * y * (y @ x) * z = y * x * z. [para(4(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)]. 24 x * y != x | x @ x = y. [para(9(a,1),1(a,1)),flip(a)]. 27 x * (x @ x) * y = x * y. [para(9(a,1),3(a,1,1)),flip(a)]. 60 (x @ x) * y = y. [hyper(7,a,27,a)]. 68 x * (x @ (y @ y)) = x * (y @ y). [hyper(10,a,60,a)]. 70 x * ((y @ y) @ x) = x. [para(60(a,1),4(a,1,2)),rewrite(60(5))]. 86 (x @ x) @ y = y @ y. [hyper(24,a,70,a),flip(a)]. 90 x * (y @ (z @ u)) = x. [para(5(a,1),70(a,1,2))]. 102 x * (y @ y) = x. [back_rewrite(68),rewrite(90(3)),flip(a)]. 103 x @ x = y @ y. [hyper(24,a,102,a)]. 107 x @ x = c_0. [new_symbol(103)]. 111 x * c_0 = x. [back_rewrite(102),rewrite(107(1))]. 115 c_0 @ x = c_0. [back_rewrite(86),rewrite(107(1),107(3))]. 122 x @ (y @ z) = c_0. [para(107(a,1),5(a,1,1)),rewrite(115(2)),flip(a)]. 132 x * y * z * (y @ x) = y * x * z. [para(4(a,1),13(a,1,2,2)),rewrite(122(6),111(6))]. 1046 $F # answer(E). [para(132(a,2),6(a,1)),rewrite(3(11),3(10),4(10)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=146. Generated=7324. Kept=1045. proofs=1. Usable=111. Sos=641. Demods=218. Limbo=6, Disabled=293. Hints=0. Weight_deleted=1224. Literals_deleted=0. Forward_subsumed=5054. Back_subsumed=74. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=353 (1 lex), Back_demodulated=213. Back_unit_deleted=0. Demod_attempts=102984. Demod_rewrites=16390. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=47724. Nonunit_bsub_feature_tests=15680. Megabytes=0.84. User_CPU=0.16, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3855 exit (max_proofs) Wed Nov 22 11:24:11 2006