============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5093 was started by mccune on cleo, Tue Nov 3 09:41:53 2009 The command was "/home/mccune/LADR/bin/prover9 -f cs.in AE.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file cs.in assign(max_seconds,30). 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 @ (w @ v5). [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: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ A, B, C, *, @ ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 2). % (nonunit Horn with equality) Auto_process settings: (no changes). kept: 1 x * y != x * z | y = z. [assumption]. kept: 2 x * y != z * y | x = z. [assumption]. kept: 3 (x * y) * z = x * y * z. [assumption]. kept: 4 x * y * (y @ x) = y * x. [assumption]. kept: 5 (x @ y) @ z = u @ (w @ v5). [assumption]. kept: 6 A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. ============================== 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 @ (w @ v5). [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.01 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 @ (w @ v5). [assumption]. given #6 (I,wt=19): 6 A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. given #7 (A,wt=14): 7 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite([3(4)])]. given #8 (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 #9 (F,wt=23): 21 x * A * B * C * B * A != x * B * A * C * A * B # answer(E). [ur(1,b,6,a)]. given #10 (F,wt=23): 25 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 #11 (F,wt=23): 26 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 #12 (T,wt=7): 9 x * (x @ x) = x. [hyper(1,a,4,a)]. given #13 (T,wt=10): 27 x * y != x | x @ x = y. [para(9(a,1),1(a,1)),flip(a)]. given #14 (T,wt=10): 28 x * (y @ y) != y | y = x. [para(9(a,1),2(a,1)),flip(a)]. given #15 (T,wt=10): 29 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): 35 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): 36 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 @ (w @ v5). [para(5(a,1),5(a,1))]. given #20 (T,wt=11): 19 (x @ y) @ z = (u @ w) @ v5. [para(5(a,2),5(a,2))]. given #21 (T,wt=11): 30 x * (x @ x) * y = x * y. [para(9(a,1),3(a,1,1)),flip(a)]. given #22 (T,wt=7): 50 (x @ x) * y = y. [hyper(7,a,30,a)]. given #23 (A,wt=14): 10 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. given #24 (T,wt=6): 71 x != y | y = x. [para(9(a,1),10(a,2)),rewrite([50(2),59(4),9(3)])]. given #25 (T,wt=9): 58 x * ((y @ y) @ x) = x. [para(50(a,1),4(a,1,2)),rewrite([50(5)])]. given #26 (T,wt=7): 88 x * (y @ y) = x. [back_rewrite(59),rewrite([78(3)]),flip(a)]. NOTE: New constant: x @ x = c_0. [new_symbol(89)]. NOTE: New Function symbol precedence: function_order([ A, B, C, c_0, *, @ ]). given #27 (T,wt=5): 93 x @ x = c_0. [new_symbol(89)]. given #28 (A,wt=14): 11 x * y * (y @ z) != y * z | z = x. [para(4(a,1),2(a,1)),flip(a)]. given #29 (T,wt=5): 97 x * c_0 = x. [back_rewrite(88),rewrite([93(1)])]. given #30 (T,wt=5): 100 c_0 @ x = c_0. [back_rewrite(73),rewrite([93(1),93(3)])]. given #31 (T,wt=5): 103 c_0 * x = x. [back_rewrite(50),rewrite([93(1)])]. given #32 (T,wt=5): 107 x @ c_0 = c_0. [para(93(a,1),18(a,1,2)),rewrite([104(4)])]. given #33 (A,wt=14): 12 x * y * (y @ z) != y * z | x = z. [para(4(a,1),2(a,2))]. given #34 (T,wt=7): 104 x @ (y @ z) = c_0. [para(93(a,1),5(a,1,1)),rewrite([100(2)]),flip(a)]. given #35 (T,wt=7): 106 (x @ y) @ z = c_0. [para(93(a,1),5(a,2))]. given #36 (T,wt=8): 96 x * y != x | c_0 = y. [back_rewrite(90),rewrite([93(3)])]. given #37 (T,wt=8): 102 x * y != y | c_0 = x. [back_rewrite(57),rewrite([93(3)])]. given #38 (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 #39 (T,wt=9): 65 x * (x @ x * x) = x. [hyper(10,a,3,a)]. given #40 (T,wt=7): 134 x @ x * x = c_0. [hyper(96,a,65,a),flip(a)]. given #41 (T,wt=10): 110 x * y != y * y | y = x. [para(93(a,1),11(a,1,2,2)),rewrite([97(2)])]. given #42 (T,wt=11): 37 (x @ y) * z = z * (x @ y). [back_rewrite(16),rewrite([32(6)])]. given #43 (A,wt=17): 14 x * y * z * (z @ x * y) = z * x * y. [para(4(a,1),3(a,1)),flip(a)]. given #44 (F,wt=25): 164 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 #45 (F,wt=25): 165 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 #46 (T,wt=12): 94 x * y != y | x * (x @ y) = c_0. [back_rewrite(92),rewrite([93(3)]),flip(b)]. given #47 (T,wt=12): 95 x * y * z != x * y | c_0 = z. [back_rewrite(91),rewrite([93(5)])]. given #48 (T,wt=12): 101 x * y * z != z | x * y = c_0. [back_rewrite(64),rewrite([93(4)]),flip(b)]. given #49 (T,wt=12): 111 x * (x @ y) != x * y | c_0 = y. [para(103(a,1),11(a,1)),flip(b)]. given #50 (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 #51 (F,wt=25): 203 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 #52 (F,wt=25): 204 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 #53 (T,wt=9): 199 x * (x * x @ x) = x. [hyper(7,a,15,a)]. given #54 (T,wt=7): 218 x * x @ x = c_0. [hyper(96,a,199,a),flip(a)]. given #55 (T,wt=12): 154 (x @ y) * z != z | x @ y = c_0. [para(37(a,2),96(a,1)),flip(b)]. given #56 (T,wt=12): 155 x * (y @ z) != x | y @ z = c_0. [para(37(a,1),102(a,1)),flip(b)]. given #57 (A,wt=18): 22 x * y * z * u != x * y * z * w | u = w. [para(3(a,1),7(a,1,2)),rewrite([3(5)])]. given #58 (T,wt=12): 178 x * y != y * x | x @ y = c_0. [para(4(a,1),95(a,1)),flip(b)]. given #59 (T,wt=12): 189 x @ y != x * y | y * x = c_0. [para(4(a,1),101(a,1)),flip(a)]. given #60 (T,wt=13): 66 x * y * (x * y @ x) = y * x. [hyper(10,a,3,a(flip)),rewrite([3(4)])]. given #61 (T,wt=13): 136 x * y @ x * y * x * y = c_0. [para(3(a,1),134(a,1,2))]. given #62 (A,wt=18): 23 x * y * z != x * u * y | u * (u @ y) = z. [para(4(a,1),7(a,1,2)),flip(a)]. given #63 (F,wt=25): 254 B * A * C * A * B * (B * A @ B) != A * B * C * A * B # answer(E). [para(66(a,1),20(a,1,2,2,2)),flip(a)]. given #64 (F,wt=25): 255 A * B * C * B * A * (A * B @ A) != B * A * C * B * A # answer(E). [para(66(a,1),20(a,2,2,2,2))]. given #65 (T,wt=10): 279 x * y != x * z | z = y. [para(97(a,1),23(a,2,2)),rewrite([103(2),107(5),97(5)])]. given #66 (T,wt=13): 220 x * y * x * y @ x * y = c_0. [para(3(a,1),218(a,1,1))]. given #67 (T,wt=13): 248 x * (y * x @ y) = x * (x @ y). [hyper(10,a,66,a),flip(a)]. given #68 (T,wt=9): 297 x * y @ x = y @ x. [hyper(279,a,248,a),flip(a)]. given #69 (A,wt=14): 24 x * y * z != y * x | y @ x = z. [para(4(a,1),7(a,1)),flip(a)]. given #70 (T,wt=9): 310 (x @ y) * z @ z = c_0. [para(37(a,2),297(a,1,1)),rewrite([106(5)])]. given #71 (T,wt=12): 319 x * y != y * x | y @ x = c_0. [para(97(a,1),24(a,1,2))]. given #72 (T,wt=13): 275 x * (x @ x * y) = x * (x @ y). [hyper(23,a,14,a),flip(a)]. given #73 (T,wt=9): 334 x @ x * y = x @ y. [hyper(279,a,275,a),flip(a)]. given #74 (A,wt=18): 43 x * y * z * u != w * u | x * y * z = w. [para(3(a,1),8(a,1,2))]. given #75 (T,wt=9): 348 x @ (y @ z) * x = c_0. [para(37(a,2),334(a,1,2)),rewrite([104(5)])]. given #76 (T,wt=13): 307 x * (x @ y) @ y = x * y @ y. [para(4(a,1),297(a,1,1)),flip(a)]. given #77 (T,wt=11): 382 (x @ y) * z * z @ z = c_0. [para(310(a,1),307(a,1,1,2)),rewrite([97(4),310(3),3(4)]),flip(a)]. given #78 (T,wt=13): 315 (x @ y) * z @ z * (x @ y) = c_0. [back_rewrite(293),rewrite([306(8)])]. given #79 (A,wt=18): 44 x * y * z != u * w * z | x * y = u * w. [para(3(a,1),8(a,2))]. given #80 (T,wt=13): 316 x * (y @ z) @ (y @ z) * x = c_0. [back_rewrite(291),rewrite([306(8)])]. given #81 (T,wt=13): 329 x * (y @ z) * u @ x * u = c_0. [para(13(a,1),310(a,1,1)),rewrite([104(5),103(5)])]. given #82 (T,wt=13): 346 x @ y * (y @ x) = x @ y * x. [para(4(a,1),334(a,1,2)),flip(a)]. given #83 (T,wt=11): 434 x @ (y @ z) * x * x = c_0. [para(310(a,1),346(a,1,2,2)),rewrite([97(4),348(3),3(4)]),flip(a)]. given #84 (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 #85 (T,wt=10): 452 x * y != z * y | z = x. [para(97(a,1),45(a,2,2)),rewrite([107(2),97(2),97(5)])]. given #86 (T,wt=13): 372 x * y @ x * (z @ u) * y = c_0. [para(13(a,1),348(a,1,2)),rewrite([104(2),103(2)])]. given #87 (T,wt=13): 391 (x @ y) * z * z * z @ z = c_0. [para(382(a,1),307(a,1,1,2)),rewrite([97(5),382(4),3(5),3(4)]),flip(a)]. given #88 (T,wt=13): 437 x @ (y @ z) * x * x * x = c_0. [para(382(a,1),346(a,1,2,2)),rewrite([97(5),434(4),3(5),3(4)]),flip(a)]. given #89 (A,wt=14): 46 x * (y @ z) != y * z | z * y = x. [para(4(a,1),8(a,1)),flip(a)]. given #90 (T,wt=14): 113 x * (y @ z) != u * x | y @ z = u. [para(104(a,1),11(a,1,2,2)),rewrite([97(2)]),flip(a)]. given #91 (T,wt=14): 114 (x @ y) * z != u * (x @ y) | z = u. [para(106(a,1),11(a,1,2,2)),rewrite([97(3)]),flip(a)]. given #92 (T,wt=14): 115 (x @ y) * z != u * (x @ y) | u = z. [para(106(a,1),12(a,1,2,2)),rewrite([97(3)]),flip(a)]. given #93 (T,wt=14): 137 (x @ y) * z != z * u | x @ y = u. [para(37(a,2),1(a,1))]. given #94 (A,wt=18): 47 x * y * z * (z @ u) != z * u | x * y = u. [para(4(a,1),8(a,2))]. given #95 (T,wt=14): 278 x * (y @ x) * z != y * x | y = z. [para(4(a,1),23(a,2)),rewrite([104(7),97(7)])]. given #96 (T,wt=12): 511 x * (y @ x) != y * x | c_0 = y. [para(4(a,1),278(a,1)),rewrite([37(2),106(6)]),flip(b)]. given #97 (T,wt=14): 288 x * y * z != x * y * u | u = z. [para(3(a,1),279(a,1)),rewrite([3(4)])]. given #98 (T,wt=14): 449 x * y * z != y * z | x * z = z. [para(4(a,1),45(a,1)),flip(a)]. given #99 (A,wt=20): 67 x * y * z != u * x * y | u * (u @ x * y) = z. [para(3(a,1),10(a,1))]. given #100 (T,wt=13): 542 x * (x @ y * x) = x * (x @ y). [hyper(67,a,13,a),rewrite([37(5)])]. given #101 (T,wt=9): 554 x @ y * x = x @ y. [hyper(279,a,542,a),flip(a)]. given #102 (T,wt=9): 583 x * y @ y = x @ y. [para(4(a,1),554(a,1,2)),rewrite([581(4),307(4)]),flip(a)]. given #103 (T,wt=11): 580 x @ y * (y @ x) = x @ y. [back_rewrite(346),rewrite([554(5)])]. given #104 (A,wt=20): 68 x * y * z != z * u | x * y * (x * y @ z) = u. [para(3(a,1),10(a,2)),rewrite([3(8)]),flip(a)]. given #105 (T,wt=11): 597 x * (x @ y) @ y = x @ y. [back_rewrite(307),rewrite([583(5)])]. given #106 (T,wt=13): 573 x * y @ x * (x @ y) = y @ x. [back_rewrite(435),rewrite([554(8),297(6)])]. given #107 (T,wt=13): 581 x * (x @ y) @ x * y = x @ y. [back_rewrite(384),rewrite([568(8)])]. given #108 (T,wt=13): 582 x @ y * z * x = x @ y * z. [para(3(a,1),554(a,1,2))]. given #109 (A,wt=18): 69 x * y != z * y | z * (z @ y) = x * (x @ y). [para(4(a,1),10(a,1))]. given #110 (T,wt=13): 591 x * y @ y * (y @ x) = x @ y. [back_rewrite(562),rewrite([583(6)])]. given #111 (T,wt=13): 592 x * (x @ y) @ y * x = x @ y. [back_rewrite(560),rewrite([583(8),554(6)])]. given #112 (T,wt=13): 600 x * y * z @ z = x * y @ z. [para(3(a,1),583(a,1,1))]. given #113 (T,wt=13): 642 x * x * y @ y * x = x @ y. [para(573(a,1),573(a,1,2,2)),rewrite([3(4),4(3),3(5),4(5),581(8)])]. given #114 (A,wt=20): 108 x * y * z * (y * z @ u) != y * z * u | u = x. [para(3(a,1),11(a,1,2)),rewrite([3(7)])]. given #115 (T,wt=13): 656 x * y @ y * y * x = x @ y. [para(573(a,1),581(a,1,1,2)),rewrite([3(3),4(3),3(5),4(4),573(8)])]. given #116 (T,wt=14): 451 x * y != z * x | y * (x @ y) = z. [para(4(a,1),45(a,2)),rewrite([104(2),97(2)]),flip(a)]. given #117 (T,wt=11): 772 x * (x @ y) * (y @ x) = x. [hyper(451,a,4,a),rewrite([580(5),3(4)])]. given #118 (T,wt=9): 780 (x @ y) * (y @ x) = c_0. [hyper(96,a,772,a),flip(a)]. given #119 (A,wt=20): 112 x * y * z * (y * z @ u) != y * z * u | x = u. [para(3(a,1),12(a,1,2)),rewrite([3(7)])]. given #120 (T,wt=10): 804 x @ y != c_0 | y @ x = c_0. [para(780(a,1),96(a,1)),flip(a),flip(b)]. given #121 (T,wt=10): 817 x * y != y | y @ x = x. [para(780(a,1),278(a,1,2)),rewrite([97(2)]),flip(a),flip(b)]. given #122 (T,wt=11): 800 (x @ y) * (y @ x) * z = z. [para(780(a,1),3(a,1,1)),rewrite([103(2)]),flip(a)]. given #123 (T,wt=11): 805 (x @ y) * z * (y @ x) = z. [para(780(a,1),13(a,2,2)),rewrite([104(3),103(4),97(6)])]. given #124 (A,wt=18): 116 x * y * z != y * u | x * (x @ y) * z = u. [para(13(a,1),1(a,1))]. given #125 (T,wt=10): 861 x * y != x | y @ x = y. [para(805(a,1),11(a,1)),flip(a),flip(b)]. given #126 (T,wt=12): 776 x * y != x | y * (x @ y) = c_0. [para(103(a,1),451(a,2))]. given #127 (T,wt=12): 779 x * x * y != x | x * y = c_0. [back_rewrite(636),rewrite([772(4)]),flip(a)]. given #128 (T,wt=12): 798 (x @ y) * z != c_0 | y @ x = z. [para(780(a,1),1(a,1)),flip(a)]. given #129 (A,wt=18): 117 x * y * (y @ z) * u != y * z * u | z = x. [para(13(a,1),2(a,1)),flip(a)]. given #130 (T,wt=12): 799 x * (y @ z) != c_0 | z @ y = x. [para(780(a,1),2(a,1)),flip(a)]. given #131 (T,wt=12): 806 x * (y @ z) != x | z @ y = c_0. [para(780(a,1),95(a,1,2)),rewrite([97(2)]),flip(a),flip(b)]. given #132 (T,wt=12): 807 x @ y != z | z * (y @ x) = c_0. [para(780(a,1),101(a,1,2)),rewrite([97(2)]),flip(a)]. given #133 (T,wt=12): 810 (x @ y) * z != z | y @ x = c_0. [para(780(a,1),24(a,1,2)),rewrite([97(2),106(5)]),flip(a),flip(b)]. given #134 (A,wt=18): 118 x * y * (y @ z) * u != y * z * u | x = z. [para(13(a,1),2(a,2))]. given #135 (T,wt=12): 814 x * y != c_0 | y @ x = y * x. [para(780(a,1),46(a,1)),flip(a),flip(b)]. given #136 (T,wt=12): 818 c_0 != x | x * (y @ z) = y @ z. [para(780(a,1),449(a,1,2)),rewrite([97(2),780(3)]),flip(a)]. given #137 (T,wt=12): 834 x @ y != z | (y @ x) * z = c_0. [para(800(a,1),96(a,1)),flip(a),flip(b)]. given #138 (T,wt=12): 899 x * y * x != x | y * x = c_0. [para(4(a,1),779(a,1,2)),rewrite([4(6)])]. given #139 (A,wt=21): 119 x * y * z * (z @ x * y) * u = z * x * y * u. [para(13(a,1),3(a,1)),rewrite([3(2)]),flip(a)]. given #140 (T,wt=12): 902 c_0 != x | (y @ z) * x = y @ z. [para(800(a,1),798(a,1)),flip(a),flip(b)]. given #141 (T,wt=14): 485 x * (y @ z) != u | (y @ z) * x = u. [para(104(a,1),46(a,1,2)),rewrite([97(2)]),flip(a)]. given #142 (T,wt=14): 486 (x @ y) * z != u | z * (x @ y) = u. [para(106(a,1),46(a,1,2)),rewrite([97(2)]),flip(a)]. given #143 (T,wt=14): 488 (x @ y) * z != x * y | y * x = z. [para(37(a,2),46(a,1))]. given #144 (A,wt=21): 120 x * y * z * (y * z @ x) * u = y * z * x * u. [para(3(a,1),13(a,1,2)),rewrite([3(9)])]. given #145 (T,wt=14): 510 x * y * (z @ x) != z * x | z = y. [para(4(a,1),278(a,1,2)),rewrite([104(7),97(7)])]. given #146 (T,wt=14): 514 (x @ y) * y * z != x * y | x = z. [para(13(a,1),278(a,1)),rewrite([106(7),103(7)])]. given #147 (T,wt=14): 750 x * y * z != z * y | z @ y = x. [para(4(a,1),108(a,2)),rewrite([104(3),97(2)])]. given #148 (T,wt=14): 801 x * (y @ z) * u != x | z @ y = u. [para(780(a,1),7(a,1,2)),rewrite([97(2)]),flip(a)]. given #149 (A,wt=15): 121 x * y * z * (y @ x) = y * x * z. [para(4(a,1),13(a,1,2,2)),rewrite([104(6),97(6)])]. ============================== PROOF ================================= % Proof 1 at 0.19 (+ 0.00) seconds: E. % Length of proof is 23. % Level of proof is 12. % Maximum clause weight is 19.000. % Given clauses 149. 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 @ (w @ v5). [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)]. 13 x * y * (y @ x) * z = y * x * z. [para(4(a,1),3(a,1,1)),rewrite([3(2),3(5)]),flip(a)]. 27 x * y != x | x @ x = y. [para(9(a,1),1(a,1)),flip(a)]. 30 x * (x @ x) * y = x * y. [para(9(a,1),3(a,1,1)),flip(a)]. 50 (x @ x) * y = y. [hyper(7,a,30,a)]. 58 x * ((y @ y) @ x) = x. [para(50(a,1),4(a,1,2)),rewrite([50(5)])]. 59 x * (x @ (y @ y)) = x * (y @ y). [para(50(a,1),4(a,1))]. 73 (x @ x) @ y = y @ y. [hyper(27,a,58,a),flip(a)]. 78 x * (y @ (z @ u)) = x. [para(5(a,1),58(a,1,2))]. 88 x * (y @ y) = x. [back_rewrite(59),rewrite([78(3)]),flip(a)]. 89 x @ x = y @ y. [hyper(27,a,88,a)]. 93 x @ x = c_0. [new_symbol(89)]. 97 x * c_0 = x. [back_rewrite(88),rewrite([93(1)])]. 100 c_0 @ x = c_0. [back_rewrite(73),rewrite([93(1),93(3)])]. 104 x @ (y @ z) = c_0. [para(93(a,1),5(a,1,1)),rewrite([100(2)]),flip(a)]. 121 x * y * z * (y @ x) = y * x * z. [para(4(a,1),13(a,1,2,2)),rewrite([104(6),97(6)])]. 1062 $F # answer(E). [para(121(a,2),6(a,1)),rewrite([3(11),3(10),4(10)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=149. Generated=7449. Kept=1061. proofs=1. Usable=112. Sos=649. Demods=220. Limbo=6, Disabled=300. Hints=0. Kept_by_rule=0, Deleted_by_rule=1260. Forward_subsumed=5127. Back_subsumed=74. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=362 (1 lex), Back_demodulated=220. Back_unit_deleted=0. Demod_attempts=106002. Demod_rewrites=16820. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=49831. Nonunit_bsub_feature_tests=15753. Megabytes=0.89. User_CPU=0.19, System_CPU=0.00, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 5093 exit (max_proofs) Tue Nov 3 09:41:54 2009