============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13121 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:34 2006 The command was "/home/mccune/bin/prover9 -f cs.in DE.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). clauses(sos). x * y != x * z | y = z. x * y != z * y | x = z. (x * y) * z = x * y * z. x * y * (y @ x) = y * x. end_of_list. % Reading from file DE.in clauses(sos). (x @ y) * (z @ y) = x * z @ y. end_of_list. clauses(sos). A * B * C * B * A != B * A * C * A * B # answer(E). end_of_list. ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x * y != x * z | y = z. [input]. 2 x * y != z * y | x = z. [input]. 3 (x * y) * z = x * y * z. [input]. 4 x * y * (y @ x) = y * x. [input]. 5 (x @ y) * (z @ y) = x * z @ y. [input]. 6 A * B * C * B * A != B * A * C * A * B # answer(E). [input]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: no changes. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ A, B, C, *, @ ]). After inverse_order: Function symbol precedence: lex([ A, B, C, *, @ ]). 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: clauses(usable). end_of_list. clauses(sos). 7 x * y != x * z | y = z. [input]. 8 x * y != z * y | x = z. [input]. 9 (x * y) * z = x * y * z. [input]. 10 x * y * (y @ x) = y * x. [input]. 11 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. 12 A * B * C * B * A != B * A * C * A * B # answer(E). [input]. end_of_list. clauses(demodulators). 9 (x * y) * z = x * y * z. [input]. 10 x * y * (y @ x) = y * x. [input]. 11 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=10): 7 x * y != x * z | y = z. [input]. given #2 (I,wt=10): 8 x * y != z * y | x = z. [input]. given #3 (I,wt=11): 9 (x * y) * z = x * y * z. [input]. given #4 (I,wt=11): 10 x * y * (y @ x) = y * x. [input]. given #5 (I,wt=13): 11 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. given #6 (I,wt=19): 12 A * B * C * B * A != B * A * C * A * B # answer(E). [input]. given #7 (F,wt=23): 23 A * B * C * B * A * x != B * A * C * A * B * x # answer(E). [ur(8,b,12,a),demod(9(10),9(9),9(8),9(7),9(20),9(19),9(18),9(17))]. given #8 (F,wt=23): 24 x * A * B * C * B * A != x * B * A * C * A * B # answer(E). [ur(7,b,12,a)]. given #9 (T,wt=7): 15 x * (x @ x) = x. [hyper(7,a,10,a)]. given #10 (T,wt=10): 27 x * y != x | x @ x = y. [para(15(a,1),7(a,1)),flip(a)]. given #11 (A,wt=14): 13 x * y * z != x * y * u | z = u. [para(9(a,1),7(a,1)),demod(9(4))]. given #12 (F,wt=23): 25 B * A * C * A * B * (A @ B) != A * B * C * A * B # answer(E). [para(10(a,1),23(a,1,2,2,2)),flip(a)]. given #13 (F,wt=23): 26 A * B * C * B * A * (B @ A) != B * A * C * B * A # answer(E). [para(10(a,1),23(a,2,2,2,2))]. given #14 (T,wt=10): 28 x * (y @ y) != y | y = x. [para(15(a,1),8(a,1)),flip(a)]. given #15 (T,wt=10): 29 x * (y @ y) != y | x = y. [para(15(a,1),8(a,2))]. given #16 (A,wt=14): 14 x * y * z != u * z | x * y = u. [para(9(a,1),8(a,1))]. given #17 (F,wt=23): 33 B * A * C * A * B * (A @ A) != A * B * C * B * A # answer(E). [para(15(a,1),23(a,1,2,2,2,2)),flip(a)]. given #18 (F,wt=23): 34 A * B * C * B * A * (B @ B) != B * A * C * A * B # answer(E). [para(15(a,1),23(a,2,2,2,2,2))]. given #19 (T,wt=11): 30 x * (x @ x) * y = x * y. [para(15(a,1),9(a,1,1)),flip(a)]. given #20 (T,wt=7): 49 (x @ x) * y = y. [hyper(13,a,30,a)]. given #21 (A,wt=14): 16 x * y != z * x | z * (z @ x) = y. [para(10(a,1),7(a,1)),flip(a)]. given #22 (F,wt=6): 68 x != y | y = x. [para(15(a,1),16(a,2)),demod(49(2),57(4),15(3))]. given #23 (F,wt=9): 56 x * ((y @ y) @ x) = x. [para(49(a,1),10(a,1,2)),demod(49(5))]. given #24 (T,wt=9): 63 x * (x @ x * x) = x. [hyper(16,a,9,a)]. given #25 (T,wt=9): 70 (x @ x) @ y = y @ y. [hyper(27,a,56,a),flip(a)]. given #26 (A,wt=14): 17 x * y * (y @ z) != y * z | z = x. [para(10(a,1),8(a,1)),flip(a)]. given #27 (F,wt=25): 77 B * A * C * A * B * ((x @ x) @ A) != A * B * C * B * A # answer(E). [para(56(a,1),23(a,1,2,2,2,2)),flip(a)]. given #28 (F,wt=25): 78 A * B * C * B * A * ((x @ x) @ B) != B * A * C * A * B # answer(E). [para(56(a,1),23(a,2,2,2,2,2))]. given #29 (T,wt=9): 85 x @ x * x = x @ x. [hyper(27,a,63,a),flip(a)]. given #30 (T,wt=9): 89 ((x @ x) @ y) * z = z. [para(70(a,2),49(a,1,1))]. given #31 (A,wt=14): 18 x * y * (y @ z) != y * z | x = z. [para(10(a,1),8(a,2))]. given #32 (F,wt=10): 55 x * y != y | z @ z = x. [para(49(a,1),8(a,1)),flip(a)]. NOTE: New constant: 0 x @ x = c_0. [new_symbol(115)]. NOTE: New Function symbol precedence: lex([ A, B, C, c_0, *, @ ]). given #33 (F,wt=5): 117 x @ x = c_0. [new_symbol(115)]. given #34 (T,wt=5): 119 c_0 @ x = c_0. [back_demod(114),demod(117(1),117(3))]. given #35 (T,wt=5): 123 c_0 * x = x. [back_demod(109),demod(117(1),119(2),119(2))]. given #36 (A,wt=15): 19 x * y * (y @ x) * z = y * x * z. [para(10(a,1),9(a,1,1)),demod(9(2),9(5)),flip(a)]. given #37 (F,wt=5): 129 x * c_0 = x. [back_demod(90),demod(117(1),119(2),119(2))]. given #38 (F,wt=7): 132 x @ x * x = c_0. [back_demod(85),demod(117(3))]. given #39 (T,wt=7): 135 x * (x @ c_0) = x. [back_demod(128),demod(129(5))]. given #40 (T,wt=8): 124 x * y != x | c_0 = y. [back_demod(107),demod(117(3),119(4),119(4))]. given #41 (A,wt=17): 20 x * y * z * (z @ x * y) = z * x * y. [para(10(a,1),9(a,1)),flip(a)]. given #42 (F,wt=25): 175 B * A * C * A * B * (A @ C * B) != A * B * A * C * B # answer(E). [para(20(a,1),23(a,1,2,2)),flip(a)]. given #43 (F,wt=25): 176 A * B * C * B * A * (B @ C * A) != B * A * B * C * A # answer(E). [para(20(a,1),23(a,2,2,2))]. given #44 (T,wt=5): 168 x @ c_0 = c_0. [hyper(124,a,135,a),flip(a)]. given #45 (T,wt=8): 127 x * y != y | c_0 = x. [back_demod(101),demod(117(3),119(4))]. given #46 (A,wt=19): 21 x * y * z * (y @ x) * (z @ x) = y * z * x. [para(9(a,1),10(a,1,2)),demod(11(2),9(8))]. given #47 (F,wt=10): 96 x * y != y * y | y = x. [para(15(a,1),17(a,1,2))]. given #48 (F,wt=12): 121 x * (x @ y) != x * y | c_0 = y. [back_demod(111),demod(117(5),119(6))]. given #49 (T,wt=12): 125 x * y * z != z | x * y = c_0. [back_demod(106),demod(117(4),119(5)),flip(b)]. given #50 (T,wt=12): 133 x * y != y | x * (x @ y) = c_0. [back_demod(83),demod(117(3),119(4)),flip(b)]. given #51 (A,wt=21): 22 (x @ y) * (z @ y) * ((z @ x) @ y) = (z @ y) * (x @ y). [para(10(a,1),11(a,1,1)),demod(11(2),11(7)),flip(a)]. given #52 (F,wt=12): 134 x * y * z != x * y | c_0 = z. [back_demod(79),demod(117(5),119(6))]. given #53 (F,wt=12): 196 x @ y != x * y | y * x = c_0. [para(10(a,1),125(a,1)),flip(a)]. given #54 (T,wt=12): 222 x * y != y * x | x @ y = c_0. [para(10(a,1),134(a,1)),flip(b)]. given #55 (T,wt=13): 131 (x @ x * y) * (y @ x * y) = c_0. [back_demod(86),demod(117(1),119(3)),flip(a)]. given #56 (A,wt=18): 37 x * y * z * u != x * y * z * v | u = v. [para(9(a,1),13(a,1,2)),demod(9(5))]. given #57 (F,wt=13): 170 x * y * (y @ y * x) = y * x. [hyper(7,a,20,a)]. given #58 (F,wt=25): 260 B * A * C * A * B * (A @ A * B) != A * B * C * A * B # answer(E). [para(170(a,1),23(a,1,2,2,2)),flip(a)]. given #59 (T,wt=13): 210 (x @ y) * ((x @ y) @ y) = x @ y. [para(117(a,1),22(a,1,1)),demod(123(6),117(6),129(7))]. given #60 (T,wt=7): 272 (x @ y) @ y = c_0. [hyper(124,a,210,a),flip(a)]. given #61 (A,wt=18): 38 x * y * z != x * u * y | u * (u @ y) = z. [para(10(a,1),13(a,1,2)),flip(a)]. given #62 (F,wt=25): 261 A * B * C * B * A * (B @ B * A) != B * A * C * B * A # answer(E). [para(170(a,1),23(a,2,2,2,2))]. given #63 (F,wt=10): 292 x * y != x * z | z = y. [para(123(a,1),38(a,1,2)),demod(129(3),168(5),129(5))]. given #64 (T,wt=11): 273 (x @ y) * y = y * (x @ y). [para(210(a,1),10(a,1,2)),flip(a)]. given #65 (T,wt=7): 297 x @ (y @ x) = c_0. [hyper(222,a,273,a(flip))]. given #66 (A,wt=14): 39 x * y * z != y * x | y @ x = z. [para(10(a,1),13(a,1)),flip(a)]. given #67 (F,wt=11): 318 x @ (y @ x) * (z @ x) = c_0. [para(11(a,1),297(a,1,2))]. given #68 (F,wt=12): 309 x * (y @ x) != x | y @ x = c_0. [para(273(a,1),127(a,1)),flip(b)]. given #69 (T,wt=12): 326 x * y != y * x | y @ x = c_0. [para(129(a,1),39(a,1,2))]. given #70 (T,wt=13): 211 (x @ y) * ((y @ x) @ y) = x @ y. [para(117(a,1),22(a,1,2,1)),demod(123(5),117(5),123(7))]. given #71 (A,wt=18): 43 x * y * z * u != v * u | x * y * z = v. [para(9(a,1),14(a,1,2))]. given #72 (F,wt=7): 339 (x @ y) @ x = c_0. [hyper(124,a,211,a),flip(a)]. given #73 (F,wt=11): 359 (x @ y) * x = x * (x @ y). [para(339(a,1),10(a,1,2,2)),demod(129(3)),flip(a)]. given #74 (T,wt=7): 370 x @ (x @ y) = c_0. [hyper(326,a,359,a)]. given #75 (T,wt=12): 380 x * (x @ y) != x | x @ y = c_0. [para(359(a,1),127(a,1)),flip(b)]. given #76 (A,wt=18): 44 x * y * z != u * v * z | x * y = u * v. [para(9(a,1),14(a,2))]. given #77 (F,wt=13): 258 x * (x @ x * y) = x * (x @ y). [hyper(16,a,170,a),flip(a)]. given #78 (F,wt=9): 407 x @ x * y = x @ y. [hyper(292,a,258,a),flip(a)]. given #79 (T,wt=9): 461 (x @ y) @ x * y = c_0. [para(407(a,1),272(a,1,1))]. given #80 (T,wt=11): 416 (x @ y) @ x * (x @ y) = c_0. [para(258(a,1),131(a,1,1,2)),demod(407(3),370(2),407(3),407(4),123(6))]. given #81 (A,wt=18): 45 x * y * (y @ z) != u * y * z | u * z = x. [para(10(a,1),14(a,1,2)),flip(a)]. given #82 (F,wt=10): 480 x * y != z * y | z = x. [para(129(a,1),45(a,2,2)),demod(168(2),129(2),129(5))]. given #83 (F,wt=11): 426 (x @ y) @ (y @ x * y) = c_0. [back_demod(338),demod(407(2))]. given #84 (T,wt=11): 427 (x @ y * x) @ (y @ x) = c_0. [back_demod(337),demod(407(4))]. given #85 (T,wt=11): 429 (x @ y * x) * (y @ x) = c_0. [back_demod(270),demod(407(4))]. given #86 (A,wt=14): 46 x * (y @ z) != y * z | z * y = x. [para(10(a,1),14(a,1)),flip(a)]. given #87 (F,wt=11): 444 (x @ y) * (y @ x * y) = c_0. [back_demod(131),demod(407(2))]. given #88 (F,wt=11): 462 (x @ y) @ y * (x @ y) = c_0. [para(272(a,1),407(a,2)),demod(273(3))]. given #89 (T,wt=11): 474 (x @ y) @ x * x * y = c_0. [para(407(a,1),461(a,1,1))]. given #90 (T,wt=11): 515 x @ (x @ y) * (x @ y) = c_0. [para(416(a,1),429(a,1,2)),demod(362(6),11(7),407(5),476(10),129(6),129(6))]. given #91 (A,wt=18): 47 x * y * z * (z @ u) != z * u | x * y = u. [para(10(a,1),14(a,2))]. given #92 (F,wt=12): 434 x @ y * x != c_0 | y @ x = c_0. [back_demod(244),demod(407(6))]. given #93 (F,wt=12): 435 x @ y != c_0 | y @ x * y = c_0. [back_demod(243),demod(407(2))]. given #94 (T,wt=13): 322 (x @ y) @ (z @ y) = (x @ z) @ y. [hyper(39,a,22,a)]. given #95 (T,wt=7): 568 (y @ z) @ x = c_0. [para(322(a,2),309(a,1,2)),demod(563(3),129(2)),xx(a)]. given #96 (A,wt=20): 64 x * y * z != u * x * y | u * (u @ x * y) = z. [para(9(a,1),16(a,1))]. given #97 (F,wt=7): 571 x @ (y @ z) = c_0. [para(322(a,2),429(a,1,1)),demod(563(7),123(4))]. given #98 (F,wt=9): 572 x @ (y @ z) * x = c_0. [para(322(a,2),429(a,1,2)),demod(571(6),129(5))]. given #99 (T,wt=11): 580 (x @ y) * z = z * (x @ y). [back_demod(540),demod(571(4),129(3)),flip(a)]. given #100 (T,wt=11): 615 x @ (y @ z) * (u @ z) = c_0. [para(11(a,1),571(a,1,2))]. given #101 (A,wt=22): 65 x * y * z != z * u | x * y * (x @ z) * (y @ z) = u. [para(9(a,1),16(a,2)),demod(11(7),9(9)),flip(a)]. given #102 (F,wt=12): 617 x * (y @ z) != x | y @ z = c_0. [para(571(a,1),121(a,1,2)),demod(129(2)),flip(a),flip(b)]. given #103 (F,wt=12): 643 (x @ y) * z != z | x @ y = c_0. [para(580(a,2),124(a,1)),flip(b)]. given #104 (T,wt=13): 447 (x @ y) * (y @ x * y) * z = z. [back_demod(59),demod(407(2))]. given #105 (T,wt=13): 453 x @ y * (y @ x) = x @ y * x. [para(10(a,1),407(a,1,2)),flip(a)]. given #106 (A,wt=18): 66 x * y != z * y | z * (z @ y) = x * (x @ y). [para(10(a,1),16(a,1))]. given #107 (F,wt=9): 736 x @ y * x = x @ y. [para(10(a,1),453(a,2,2)),demod(453(5),606(5),11(5),453(3),568(6),129(4),11(6),407(4),568(6),129(5))]. given #108 (F,wt=9): 740 (x @ y) * (y @ x) = c_0. [para(453(a,1),429(a,1,2)),demod(10(5),11(4),407(2),568(4),129(3),736(3))]. given #109 (T,wt=10): 742 x @ y != c_0 | y @ x = c_0. [para(453(a,1),435(a,1)),demod(736(2),10(8),11(7),407(5),568(7),129(6))]. given #110 (T,wt=11): 745 (x @ y) * (y @ x) * z = z. [para(453(a,1),447(a,1,1)),demod(736(2),10(6),11(5),407(3),568(5),129(4))]. given #111 (A,wt=22): 94 x * y * z * (y @ u) * (z @ u) != y * z * u | u = x. [para(9(a,1),17(a,1,2)),demod(11(2),9(8))]. given #112 (F,wt=11): 773 (x @ y) * z * (y @ x) = z. [back_demod(593),demod(736(2))]. given #113 (F,wt=10): 840 x * y != x | y @ x = y. [para(773(a,1),17(a,1)),flip(a),flip(b)]. given #114 (T,wt=11): 789 x @ y * (y @ x) = x @ y. [back_demod(453),demod(736(5))]. given #115 (T,wt=12): 764 x @ y != z | (y @ x) * z = c_0. [back_demod(715),demod(736(4))]. given #116 (A,wt=22): 112 x * y * z * (y @ u) * (z @ u) != y * z * u | x = u. [para(9(a,1),18(a,1,2)),demod(11(2),9(8))]. given #117 (F,wt=12): 775 (x @ y) * z != z | y @ x = c_0. [back_demod(583),demod(736(5))]. given #118 (F,wt=12): 776 x * y != c_0 | y @ x = y * x. [back_demod(518),demod(736(5))]. given #119 (T,wt=12): 781 x * (y @ z) != x | z @ y = c_0. [back_demod(507),demod(736(2))]. given #120 (T,wt=12): 782 x @ y != z | z * (y @ x) = c_0. [back_demod(506),demod(736(4))]. given #121 (A,wt=18): 136 x * y * z != y * u | x * (x @ y) * z = u. [para(19(a,1),7(a,1))]. given #122 (F,wt=12): 785 (x @ y) * z != c_0 | y @ x = z. [back_demod(499),demod(736(2))]. given #123 (F,wt=12): 787 x * (y @ z) != c_0 | z @ y = x. [back_demod(485),demod(736(6))]. given #124 (T,wt=12): 889 c_0 != x | (y @ z) * x = y @ z. [para(745(a,1),785(a,1)),flip(a),flip(b)]. given #125 (T,wt=12): 890 c_0 != x | x * (y @ z) = y @ z. [para(773(a,1),785(a,1)),flip(a),flip(b)]. given #126 (A,wt=18): 137 x * y * (y @ z) * u != y * z * u | z = x. [para(19(a,1),8(a,1)),flip(a)]. given #127 (F,wt=13): 691 x @ (y @ z) * (u @ y * z) = c_0. [para(407(a,1),615(a,1,2,1))]. given #128 (F,wt=13): 692 x @ (y @ z * u) * (z @ u) = c_0. [para(407(a,1),615(a,1,2,2))]. given #129 (T,wt=13): 794 x @ y * z * x = x @ y * z. [para(9(a,1),736(a,1,2))]. given #130 (T,wt=11): 928 x @ y * z = x @ z * y. [para(19(a,1),794(a,1,2)),demod(11(5),568(4),794(4),123(4),11(6),568(5),123(6))]. given #131 (A,wt=18): 138 x * y * (y @ z) * u != y * z * u | x = z. [para(19(a,1),8(a,2))]. given #132 (F,wt=25): 950 A * B * C * B * A * (B @ A * C) != B * A * B * C * A # answer(E). [back_demod(176),demod(928(10))]. ============================== PROOF ================================= % Proof 1 at 0.14 (+ 0.00) seconds: E. % Length of proof is 81. % Level of proof is 22. % Maximum clause weight is 25. % Given clauses 132. 5 (x @ y) * (z @ y) = x * z @ y. [input]. 7 x * y != x * z | y = z. [input]. 8 x * y != z * y | x = z. [input]. 9 (x * y) * z = x * y * z. [input]. 10 x * y * (y @ x) = y * x. [input]. 11 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. 12 A * B * C * B * A != B * A * C * A * B # answer(E). [input]. 13 x * y * z != x * y * u | z = u. [para(9(a,1),7(a,1)),demod(9(4))]. 14 x * y * z != u * z | x * y = u. [para(9(a,1),8(a,1))]. 15 x * (x @ x) = x. [hyper(7,a,10,a)]. 16 x * y != z * x | z * (z @ x) = y. [para(10(a,1),7(a,1)),flip(a)]. 19 x * y * (y @ x) * z = y * x * z. [para(10(a,1),9(a,1,1)),demod(9(2),9(5)),flip(a)]. 20 x * y * z * (z @ x * y) = z * x * y. [para(10(a,1),9(a,1)),flip(a)]. 21 x * y * z * (y @ x) * (z @ x) = y * z * x. [para(9(a,1),10(a,1,2)),demod(11(2),9(8))]. 22 (x @ y) * (z @ y) * ((z @ x) @ y) = (z @ y) * (x @ y). [para(10(a,1),11(a,1,1)),demod(11(2),11(7)),flip(a)]. 23 A * B * C * B * A * x != B * A * C * A * B * x # answer(E). [ur(8,b,12,a),demod(9(10),9(9),9(8),9(7),9(20),9(19),9(18),9(17))]. 27 x * y != x | x @ x = y. [para(15(a,1),7(a,1)),flip(a)]. 30 x * (x @ x) * y = x * y. [para(15(a,1),9(a,1,1)),flip(a)]. 38 x * y * z != x * u * y | u * (u @ y) = z. [para(10(a,1),13(a,1,2)),flip(a)]. 39 x * y * z != y * x | y @ x = z. [para(10(a,1),13(a,1)),flip(a)]. 46 x * (y @ z) != y * z | z * y = x. [para(10(a,1),14(a,1)),flip(a)]. 49 (x @ x) * y = y. [hyper(13,a,30,a)]. 55 x * y != y | z @ z = x. [para(49(a,1),8(a,1)),flip(a)]. 56 x * ((y @ y) @ x) = x. [para(49(a,1),10(a,1,2)),demod(49(5))]. 59 (x @ x * y) * (y @ x * y) * z = z. [para(11(a,1),49(a,1,1)),demod(9(6))]. 64 x * y * z != u * x * y | u * (u @ x * y) = z. [para(9(a,1),16(a,1))]. 70 (x @ x) @ y = y @ y. [hyper(27,a,56,a),flip(a)]. 79 x * y * z != x * y | (u @ u) @ y = z. [para(56(a,1),13(a,1,2)),flip(a)]. 86 (x @ x) @ y * z = (y @ y * z) * (z @ y * z). [para(70(a,2),11(a,1))]. 89 ((x @ x) @ y) * z = z. [para(70(a,2),49(a,1,1))]. 90 x * (((y @ y) @ z) @ x) = x. [para(70(a,2),56(a,1,2,1))]. 100 x * (x @ ((y @ y) @ z)) = x * ((y @ y) @ z). [hyper(16,a,89,a)]. 101 x * y != y | (z @ z) @ u = x. [para(89(a,1),8(a,1)),flip(a)]. 107 x * y != x | ((z @ z) @ u) @ x = y. [para(89(a,1),16(a,2)),demod(89(8))]. 109 (((x @ x) @ y) @ z) * u = u. [para(70(a,2),89(a,1,1,1))]. 114 (x @ x) @ y = z @ z. [hyper(55,a,89,a),flip(a)]. 115 x @ x = y @ y. [hyper(55,a,49,a)]. 117 x @ x = c_0. [new_symbol(115)]. 119 c_0 @ x = c_0. [back_demod(114),demod(117(1),117(3))]. 123 c_0 * x = x. [back_demod(109),demod(117(1),119(2),119(2))]. 124 x * y != x | c_0 = y. [back_demod(107),demod(117(3),119(4),119(4))]. 127 x * y != y | c_0 = x. [back_demod(101),demod(117(3),119(4))]. 128 x * (x @ c_0) = x * c_0. [back_demod(100),demod(117(1),119(2),117(4),119(5))]. 129 x * c_0 = x. [back_demod(90),demod(117(1),119(2),119(2))]. 131 (x @ x * y) * (y @ x * y) = c_0. [back_demod(86),demod(117(1),119(3)),flip(a)]. 134 x * y * z != x * y | c_0 = z. [back_demod(79),demod(117(5),119(6))]. 135 x * (x @ c_0) = x. [back_demod(128),demod(129(5))]. 168 x @ c_0 = c_0. [hyper(124,a,135,a),flip(a)]. 170 x * y * (y @ y * x) = y * x. [hyper(7,a,20,a)]. 176 A * B * C * B * A * (B @ C * A) != B * A * B * C * A # answer(E). [para(20(a,1),23(a,2,2,2))]. 210 (x @ y) * ((x @ y) @ y) = x @ y. [para(117(a,1),22(a,1,1)),demod(123(6),117(6),129(7))]. 222 x * y != y * x | x @ y = c_0. [para(10(a,1),134(a,1)),flip(b)]. 258 x * (x @ x * y) = x * (x @ y). [hyper(16,a,170,a),flip(a)]. 270 (x @ y * x) * (y @ y * x) = c_0. [para(131(a,1),170(a,1,2,2,2)),demod(168(8),129(6),131(10))]. 273 (x @ y) * y = y * (x @ y). [para(210(a,1),10(a,1,2)),flip(a)]. 292 x * y != x * z | z = y. [para(123(a,1),38(a,1,2)),demod(129(3),168(5),129(5))]. 297 x @ (y @ x) = c_0. [hyper(222,a,273,a(flip))]. 309 x * (y @ x) != x | y @ x = c_0. [para(273(a,1),127(a,1)),flip(b)]. 322 (x @ y) @ (z @ y) = (x @ z) @ y. [hyper(39,a,22,a)]. 326 x * y != y * x | y @ x = c_0. [para(129(a,1),39(a,1,2))]. 337 (x @ y * x) @ (y @ y * x) = c_0. [para(131(a,1),326(a,1)),demod(270(6)),xx(a)]. 407 x @ x * y = x @ y. [hyper(292,a,258,a),flip(a)]. 427 (x @ y * x) @ (y @ x) = c_0. [back_demod(337),demod(407(4))]. 429 (x @ y * x) * (y @ x) = c_0. [back_demod(270),demod(407(4))]. 447 (x @ y) * (y @ x * y) * z = z. [back_demod(59),demod(407(2))]. 453 x @ y * (y @ x) = x @ y * x. [para(10(a,1),407(a,1,2)),flip(a)]. 494 (x @ y * x) * z * (y @ x) = z * (z @ (y @ x)). [para(427(a,1),21(a,1,2,2,2,1)),demod(123(7),447(8)),flip(a)]. 540 x * (y @ z) * ((y @ x) @ (z @ x)) = (y @ z) * x. [para(322(a,2),10(a,1,2,2))]. 563 (x @ y) @ (z @ y) = c_0. [para(297(a,1),322(a,1,2)),demod(168(4)),flip(a)]. 568 (y @ z) @ x = c_0. [para(322(a,2),309(a,1,2)),demod(563(3),129(2)),xx(a)]. 571 x @ (y @ z) = c_0. [para(322(a,2),429(a,1,1)),demod(563(7),123(4))]. 580 (x @ y) * z = z * (x @ y). [back_demod(540),demod(571(4),129(3)),flip(a)]. 593 (x @ y * x) * z * (y @ x) = z. [back_demod(494),demod(571(7),129(7))]. 606 x * (x @ y * x) = x * (x @ y). [hyper(64,a,19,a),demod(580(5))]. 736 x @ y * x = x @ y. [para(10(a,1),453(a,2,2)),demod(453(5),606(5),11(5),453(3),568(6),129(4),11(6),407(4),568(6),129(5))]. 773 (x @ y) * z * (y @ x) = z. [back_demod(593),demod(736(2))]. 794 x @ y * z * x = x @ y * z. [para(9(a,1),736(a,1,2))]. 836 (x @ y * z) * u * (y @ x) * (z @ x) = u. [para(11(a,1),773(a,1,2,2))]. 928 x @ y * z = x @ z * y. [para(19(a,1),794(a,1,2)),demod(11(5),568(4),794(4),123(4),11(6),568(5),123(6))]. 950 A * B * C * B * A * (B @ A * C) != B * A * B * C * A # answer(E). [back_demod(176),demod(928(10))]. 995 $F # answer(E). [ur(46,b,950,a(flip)),demod(11(24),11(25),117(21),11(24),580(26,R),123(27),9(27),9(26),9(25),9(24),9(23),836(22),10(10),9(18),9(17),9(16)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=132. Generated=6053. Kept=988. proofs=1. Usable=74. Sos=379. Demods=76. Denials=0. Limbo=0, Disabled=541. Hints=0. Weight_deleted=942. Literals_deleted=0. Forward_subsumed=4122. Back_subsumed=138. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=307 (2 lex), Back_demodulated=397. Back_unit_deleted=0. Demod_attempts=83198. Demod_rewrites=13610. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=35943. Nonunit_bsub_feature_tests=11598. Megabytes=0.55. User_CPU=0.14, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13121 exit (max_proofs) Mon Jun 19 16:41:34 2006