============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11355 was started by mccune on cleo.thornwood, Sat Aug 12 20:59:56 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). 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 DE.in formulas(sos). (x @ z) * (y @ z) = x * y @ z. 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 @ y) = x * z @ y. [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]. 6 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. 7 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]. 6 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. 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=13): 6 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. given #6 (I,wt=19): 7 A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. given #7 (F,wt=23): 18 A * B * C * B * A * x != B * A * C * A * B * x # answer(E). [ur(2,b,7,a),rewrite(3(10),3(9),3(8),3(7),3(20),3(19),3(18),3(17))]. given #8 (F,wt=23): 19 x * A * B * C * B * A != x * B * A * C * A * B # answer(E). [ur(1,b,7,a)]. given #9 (T,wt=7): 10 x * (x @ x) = x. [hyper(1,a,4,a)]. given #10 (T,wt=10): 22 x * y != x | x @ x = y. [para(10(a,1),1(a,1)),flip(a)]. given #11 (A,wt=14): 8 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite(3(4))]. given #12 (F,wt=23): 20 B * A * C * A * B * (A @ B) != A * B * C * A * B # answer(E). [para(4(a,1),18(a,1,2,2,2)),flip(a)]. given #13 (F,wt=23): 21 A * B * C * B * A * (B @ A) != B * A * C * B * A # answer(E). [para(4(a,1),18(a,2,2,2,2))]. given #14 (T,wt=10): 23 x * (y @ y) != y | y = x. [para(10(a,1),2(a,1)),flip(a)]. given #15 (T,wt=10): 24 x * (y @ y) != y | x = y. [para(10(a,1),2(a,2))]. given #16 (A,wt=14): 9 x * y * z != u * z | x * y = u. [para(3(a,1),2(a,1))]. given #17 (F,wt=23): 28 B * A * C * A * B * (A @ A) != A * B * C * B * A # answer(E). [para(10(a,1),18(a,1,2,2,2,2)),flip(a)]. given #18 (F,wt=23): 29 A * B * C * B * A * (B @ B) != B * A * C * A * B # answer(E). [para(10(a,1),18(a,2,2,2,2,2))]. given #19 (T,wt=11): 25 x * (x @ x) * y = x * y. [para(10(a,1),3(a,1,1)),flip(a)]. given #20 (T,wt=7): 44 (x @ x) * y = y. [hyper(8,a,25,a)]. given #21 (A,wt=14): 11 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. given #22 (F,wt=6): 63 x != y | y = x. [para(10(a,1),11(a,2)),rewrite(44(2),52(4),10(3))]. given #23 (F,wt=9): 51 x * ((y @ y) @ x) = x. [para(44(a,1),4(a,1,2)),rewrite(44(5))]. given #24 (T,wt=9): 58 x * (x @ x * x) = x. [hyper(11,a,3,a)]. given #25 (T,wt=9): 65 (x @ x) @ y = y @ y. [hyper(22,a,51,a),flip(a)]. given #26 (A,wt=14): 12 x * y * (y @ z) != y * z | z = x. [para(4(a,1),2(a,1)),flip(a)]. given #27 (F,wt=25): 72 B * A * C * A * B * ((x @ x) @ A) != A * B * C * B * A # answer(E). [para(51(a,1),18(a,1,2,2,2,2)),flip(a)]. given #28 (F,wt=25): 73 A * B * C * B * A * ((x @ x) @ B) != B * A * C * A * B # answer(E). [para(51(a,1),18(a,2,2,2,2,2))]. given #29 (T,wt=9): 80 x @ x * x = x @ x. [hyper(22,a,58,a),flip(a)]. given #30 (T,wt=9): 84 ((x @ x) @ y) * z = z. [para(65(a,2),44(a,1,1))]. given #31 (A,wt=14): 13 x * y * (y @ z) != y * z | x = z. [para(4(a,1),2(a,2))]. given #32 (F,wt=10): 50 x * y != y | z @ z = x. [para(44(a,1),2(a,1)),flip(a)]. NOTE: New constant: x @ x = c_0. [new_symbol(110)]. NOTE: New Function symbol precedence: lex([ A, B, C, c_0, *, @ ]). given #33 (F,wt=5): 112 x @ x = c_0. [new_symbol(110)]. given #34 (T,wt=5): 114 c_0 @ x = c_0. [back_rewrite(109),rewrite(112(1),112(3))]. given #35 (T,wt=5): 118 c_0 * x = x. [back_rewrite(104),rewrite(112(1),114(2),114(2))]. given #36 (A,wt=15): 14 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=5): 124 x * c_0 = x. [back_rewrite(85),rewrite(112(1),114(2),114(2))]. given #38 (F,wt=7): 127 x @ x * x = c_0. [back_rewrite(80),rewrite(112(3))]. given #39 (T,wt=7): 130 x * (x @ c_0) = x. [back_rewrite(123),rewrite(124(5))]. given #40 (T,wt=8): 119 x * y != x | c_0 = y. [back_rewrite(102),rewrite(112(3),114(4),114(4))]. given #41 (A,wt=17): 15 x * y * z * (z @ x * y) = z * x * y. [para(4(a,1),3(a,1)),flip(a)]. given #42 (F,wt=25): 170 B * A * C * A * B * (A @ C * B) != A * B * A * C * B # answer(E). [para(15(a,1),18(a,1,2,2)),flip(a)]. given #43 (F,wt=25): 171 A * B * C * B * A * (B @ C * A) != B * A * B * C * A # answer(E). [para(15(a,1),18(a,2,2,2))]. given #44 (T,wt=5): 163 x @ c_0 = c_0. [hyper(119,a,130,a),flip(a)]. given #45 (T,wt=8): 122 x * y != y | c_0 = x. [back_rewrite(96),rewrite(112(3),114(4))]. given #46 (A,wt=19): 16 x * y * z * (y @ x) * (z @ x) = y * z * x. [para(3(a,1),4(a,1,2)),rewrite(6(2),3(8))]. given #47 (F,wt=10): 91 x * y != y * y | y = x. [para(10(a,1),12(a,1,2))]. given #48 (F,wt=12): 116 x * (x @ y) != x * y | c_0 = y. [back_rewrite(106),rewrite(112(5),114(6))]. given #49 (T,wt=12): 120 x * y * z != z | x * y = c_0. [back_rewrite(101),rewrite(112(4),114(5)),flip(b)]. given #50 (T,wt=12): 128 x * y != y | x * (x @ y) = c_0. [back_rewrite(78),rewrite(112(3),114(4)),flip(b)]. given #51 (A,wt=21): 17 (x @ y) * (z @ y) * ((z @ x) @ y) = (z @ y) * (x @ y). [para(4(a,1),6(a,1,1)),rewrite(6(2),6(7)),flip(a)]. given #52 (F,wt=12): 129 x * y * z != x * y | c_0 = z. [back_rewrite(74),rewrite(112(5),114(6))]. given #53 (F,wt=12): 191 x @ y != x * y | y * x = c_0. [para(4(a,1),120(a,1)),flip(a)]. given #54 (T,wt=12): 217 x * y != y * x | x @ y = c_0. [para(4(a,1),129(a,1)),flip(b)]. given #55 (T,wt=13): 126 (x @ x * y) * (y @ x * y) = c_0. [back_rewrite(81),rewrite(112(1),114(3)),flip(a)]. given #56 (A,wt=18): 32 x * y * z * u != x * y * z * v | u = v. [para(3(a,1),8(a,1,2)),rewrite(3(5))]. given #57 (F,wt=13): 165 x * y * (y @ y * x) = y * x. [hyper(1,a,15,a)]. given #58 (F,wt=25): 255 B * A * C * A * B * (A @ A * B) != A * B * C * A * B # answer(E). [para(165(a,1),18(a,1,2,2,2)),flip(a)]. given #59 (T,wt=13): 205 (x @ y) * ((x @ y) @ y) = x @ y. [para(112(a,1),17(a,1,1)),rewrite(118(6),112(6),124(7))]. given #60 (T,wt=7): 267 (x @ y) @ y = c_0. [hyper(119,a,205,a),flip(a)]. given #61 (A,wt=18): 33 x * y * z != x * u * y | u * (u @ y) = z. [para(4(a,1),8(a,1,2)),flip(a)]. given #62 (F,wt=25): 256 A * B * C * B * A * (B @ B * A) != B * A * C * B * A # answer(E). [para(165(a,1),18(a,2,2,2,2))]. given #63 (F,wt=10): 287 x * y != x * z | z = y. [para(118(a,1),33(a,1,2)),rewrite(124(3),163(5),124(5))]. given #64 (T,wt=11): 268 (x @ y) * y = y * (x @ y). [para(205(a,1),4(a,1,2)),flip(a)]. given #65 (T,wt=7): 292 x @ (y @ x) = c_0. [hyper(217,a,268,a(flip))]. given #66 (A,wt=14): 34 x * y * z != y * x | y @ x = z. [para(4(a,1),8(a,1)),flip(a)]. given #67 (F,wt=11): 313 x @ (y @ x) * (z @ x) = c_0. [para(6(a,1),292(a,1,2))]. given #68 (F,wt=12): 304 x * (y @ x) != x | y @ x = c_0. [para(268(a,1),122(a,1)),flip(b)]. given #69 (T,wt=12): 321 x * y != y * x | y @ x = c_0. [para(124(a,1),34(a,1,2))]. given #70 (T,wt=13): 206 (x @ y) * ((y @ x) @ y) = x @ y. [para(112(a,1),17(a,1,2,1)),rewrite(118(5),112(5),118(7))]. given #71 (A,wt=18): 38 x * y * z * u != v * u | x * y * z = v. [para(3(a,1),9(a,1,2))]. given #72 (F,wt=7): 334 (x @ y) @ x = c_0. [hyper(119,a,206,a),flip(a)]. given #73 (F,wt=11): 354 (x @ y) * x = x * (x @ y). [para(334(a,1),4(a,1,2,2)),rewrite(124(3)),flip(a)]. given #74 (T,wt=7): 365 x @ (x @ y) = c_0. [hyper(321,a,354,a)]. given #75 (T,wt=12): 375 x * (x @ y) != x | x @ y = c_0. [para(354(a,1),122(a,1)),flip(b)]. given #76 (A,wt=18): 39 x * y * z != u * v * z | x * y = u * v. [para(3(a,1),9(a,2))]. given #77 (F,wt=13): 253 x * (x @ x * y) = x * (x @ y). [hyper(11,a,165,a),flip(a)]. given #78 (F,wt=9): 402 x @ x * y = x @ y. [hyper(287,a,253,a),flip(a)]. given #79 (T,wt=9): 456 (x @ y) @ x * y = c_0. [para(402(a,1),267(a,1,1))]. given #80 (T,wt=11): 411 (x @ y) @ x * (x @ y) = c_0. [para(253(a,1),126(a,1,1,2)),rewrite(402(3),365(2),402(3),402(4),118(6))]. given #81 (A,wt=18): 40 x * y * (y @ z) != u * y * z | u * z = x. [para(4(a,1),9(a,1,2)),flip(a)]. given #82 (F,wt=10): 475 x * y != z * y | z = x. [para(124(a,1),40(a,2,2)),rewrite(163(2),124(2),124(5))]. given #83 (F,wt=11): 421 (x @ y) @ (y @ x * y) = c_0. [back_rewrite(333),rewrite(402(2))]. given #84 (T,wt=11): 422 (x @ y * x) @ (y @ x) = c_0. [back_rewrite(332),rewrite(402(4))]. given #85 (T,wt=11): 424 (x @ y * x) * (y @ x) = c_0. [back_rewrite(265),rewrite(402(4))]. given #86 (A,wt=14): 41 x * (y @ z) != y * z | z * y = x. [para(4(a,1),9(a,1)),flip(a)]. given #87 (F,wt=11): 439 (x @ y) * (y @ x * y) = c_0. [back_rewrite(126),rewrite(402(2))]. given #88 (F,wt=11): 457 (x @ y) @ y * (x @ y) = c_0. [para(267(a,1),402(a,2)),rewrite(268(3))]. given #89 (T,wt=11): 469 (x @ y) @ x * x * y = c_0. [para(402(a,1),456(a,1,1))]. given #90 (T,wt=11): 510 x @ (x @ y) * (x @ y) = c_0. [para(411(a,1),424(a,1,2)),rewrite(357(6),6(7),402(5),471(10),124(6),124(6))]. given #91 (A,wt=18): 42 x * y * z * (z @ u) != z * u | x * y = u. [para(4(a,1),9(a,2))]. given #92 (F,wt=12): 429 x @ y * x != c_0 | y @ x = c_0. [back_rewrite(239),rewrite(402(6))]. given #93 (F,wt=12): 430 x @ y != c_0 | y @ x * y = c_0. [back_rewrite(238),rewrite(402(2))]. given #94 (T,wt=13): 317 (x @ y) @ (z @ y) = (x @ z) @ y. [hyper(34,a,17,a)]. given #95 (T,wt=7): 563 (y @ z) @ x = c_0. [para(317(a,2),304(a,1,2)),rewrite(558(3),124(2)),xx(a)]. given #96 (A,wt=20): 59 x * y * z != u * x * y | u * (u @ x * y) = z. [para(3(a,1),11(a,1))]. given #97 (F,wt=7): 566 x @ (y @ z) = c_0. [para(317(a,2),424(a,1,1)),rewrite(558(7),118(4))]. given #98 (F,wt=9): 567 x @ (y @ z) * x = c_0. [para(317(a,2),424(a,1,2)),rewrite(566(6),124(5))]. given #99 (T,wt=11): 575 (x @ y) * z = z * (x @ y). [back_rewrite(535),rewrite(566(4),124(3)),flip(a)]. given #100 (T,wt=11): 610 x @ (y @ z) * (u @ z) = c_0. [para(6(a,1),566(a,1,2))]. given #101 (A,wt=22): 60 x * y * z != z * u | x * y * (x @ z) * (y @ z) = u. [para(3(a,1),11(a,2)),rewrite(6(7),3(9)),flip(a)]. given #102 (F,wt=12): 612 x * (y @ z) != x | y @ z = c_0. [para(566(a,1),116(a,1,2)),rewrite(124(2)),flip(a),flip(b)]. given #103 (F,wt=12): 638 (x @ y) * z != z | x @ y = c_0. [para(575(a,2),119(a,1)),flip(b)]. given #104 (T,wt=13): 442 (x @ y) * (y @ x * y) * z = z. [back_rewrite(54),rewrite(402(2))]. given #105 (T,wt=13): 448 x @ y * (y @ x) = x @ y * x. [para(4(a,1),402(a,1,2)),flip(a)]. given #106 (A,wt=18): 61 x * y != z * y | z * (z @ y) = x * (x @ y). [para(4(a,1),11(a,1))]. given #107 (F,wt=9): 731 x @ y * x = x @ y. [para(4(a,1),448(a,2,2)),rewrite(448(5),601(5),6(5),448(3),563(6),124(4),6(6),402(4),563(6),124(5))]. given #108 (F,wt=9): 735 (x @ y) * (y @ x) = c_0. [para(448(a,1),424(a,1,2)),rewrite(4(5),6(4),402(2),563(4),124(3),731(3))]. given #109 (T,wt=10): 737 x @ y != c_0 | y @ x = c_0. [para(448(a,1),430(a,1)),rewrite(731(2),4(8),6(7),402(5),563(7),124(6))]. given #110 (T,wt=11): 740 (x @ y) * (y @ x) * z = z. [para(448(a,1),442(a,1,1)),rewrite(731(2),4(6),6(5),402(3),563(5),124(4))]. given #111 (A,wt=22): 89 x * y * z * (y @ u) * (z @ u) != y * z * u | u = x. [para(3(a,1),12(a,1,2)),rewrite(6(2),3(8))]. given #112 (F,wt=11): 768 (x @ y) * z * (y @ x) = z. [back_rewrite(588),rewrite(731(2))]. given #113 (F,wt=10): 835 x * y != x | y @ x = y. [para(768(a,1),12(a,1)),flip(a),flip(b)]. given #114 (T,wt=11): 784 x @ y * (y @ x) = x @ y. [back_rewrite(448),rewrite(731(5))]. given #115 (T,wt=12): 759 x @ y != z | (y @ x) * z = c_0. [back_rewrite(710),rewrite(731(4))]. given #116 (A,wt=22): 107 x * y * z * (y @ u) * (z @ u) != y * z * u | x = u. [para(3(a,1),13(a,1,2)),rewrite(6(2),3(8))]. given #117 (F,wt=12): 770 (x @ y) * z != z | y @ x = c_0. [back_rewrite(578),rewrite(731(5))]. given #118 (F,wt=12): 771 x * y != c_0 | y @ x = y * x. [back_rewrite(513),rewrite(731(5))]. given #119 (T,wt=12): 776 x * (y @ z) != x | z @ y = c_0. [back_rewrite(502),rewrite(731(2))]. given #120 (T,wt=12): 777 x @ y != z | z * (y @ x) = c_0. [back_rewrite(501),rewrite(731(4))]. given #121 (A,wt=18): 131 x * y * z != y * u | x * (x @ y) * z = u. [para(14(a,1),1(a,1))]. given #122 (F,wt=12): 780 (x @ y) * z != c_0 | y @ x = z. [back_rewrite(494),rewrite(731(2))]. given #123 (F,wt=12): 782 x * (y @ z) != c_0 | z @ y = x. [back_rewrite(480),rewrite(731(6))]. given #124 (T,wt=12): 884 c_0 != x | (y @ z) * x = y @ z. [para(740(a,1),780(a,1)),flip(a),flip(b)]. given #125 (T,wt=12): 885 c_0 != x | x * (y @ z) = y @ z. [para(768(a,1),780(a,1)),flip(a),flip(b)]. given #126 (A,wt=18): 132 x * y * (y @ z) * u != y * z * u | z = x. [para(14(a,1),2(a,1)),flip(a)]. given #127 (F,wt=13): 686 x @ (y @ z) * (u @ y * z) = c_0. [para(402(a,1),610(a,1,2,1))]. given #128 (F,wt=13): 687 x @ (y @ z * u) * (z @ u) = c_0. [para(402(a,1),610(a,1,2,2))]. given #129 (T,wt=13): 789 x @ y * z * x = x @ y * z. [para(3(a,1),731(a,1,2))]. given #130 (T,wt=11): 923 x @ y * z = x @ z * y. [para(14(a,1),789(a,1,2)),rewrite(6(5),563(4),789(4),118(4),6(6),563(5),118(6))]. given #131 (A,wt=18): 133 x * y * (y @ z) * u != y * z * u | x = z. [para(14(a,1),2(a,2))]. given #132 (F,wt=25): 945 A * B * C * B * A * (B @ A * C) != B * A * B * C * A # answer(E). [back_rewrite(171),rewrite(923(10))]. ============================== PROOF ================================= % Proof 1 at 0.13 (+ 0.00) seconds: E. % Length of proof is 81. % Level of proof is 22. % Maximum clause weight is 25. % Given clauses 132. 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 @ y) = x * z @ y. [assumption]. 6 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. 7 A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. 8 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite(3(4))]. 9 x * y * z != u * z | x * y = u. [para(3(a,1),2(a,1))]. 10 x * (x @ x) = x. [hyper(1,a,4,a)]. 11 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. 14 x * y * (y @ x) * z = y * x * z. [para(4(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)]. 15 x * y * z * (z @ x * y) = z * x * y. [para(4(a,1),3(a,1)),flip(a)]. 16 x * y * z * (y @ x) * (z @ x) = y * z * x. [para(3(a,1),4(a,1,2)),rewrite(6(2),3(8))]. 17 (x @ y) * (z @ y) * ((z @ x) @ y) = (z @ y) * (x @ y). [para(4(a,1),6(a,1,1)),rewrite(6(2),6(7)),flip(a)]. 18 A * B * C * B * A * x != B * A * C * A * B * x # answer(E). [ur(2,b,7,a),rewrite(3(10),3(9),3(8),3(7),3(20),3(19),3(18),3(17))]. 22 x * y != x | x @ x = y. [para(10(a,1),1(a,1)),flip(a)]. 25 x * (x @ x) * y = x * y. [para(10(a,1),3(a,1,1)),flip(a)]. 33 x * y * z != x * u * y | u * (u @ y) = z. [para(4(a,1),8(a,1,2)),flip(a)]. 34 x * y * z != y * x | y @ x = z. [para(4(a,1),8(a,1)),flip(a)]. 41 x * (y @ z) != y * z | z * y = x. [para(4(a,1),9(a,1)),flip(a)]. 44 (x @ x) * y = y. [hyper(8,a,25,a)]. 50 x * y != y | z @ z = x. [para(44(a,1),2(a,1)),flip(a)]. 51 x * ((y @ y) @ x) = x. [para(44(a,1),4(a,1,2)),rewrite(44(5))]. 54 (x @ x * y) * (y @ x * y) * z = z. [para(6(a,1),44(a,1,1)),rewrite(3(6))]. 59 x * y * z != u * x * y | u * (u @ x * y) = z. [para(3(a,1),11(a,1))]. 65 (x @ x) @ y = y @ y. [hyper(22,a,51,a),flip(a)]. 74 x * y * z != x * y | (u @ u) @ y = z. [para(51(a,1),8(a,1,2)),flip(a)]. 81 (x @ x) @ y * z = (y @ y * z) * (z @ y * z). [para(65(a,2),6(a,1))]. 84 ((x @ x) @ y) * z = z. [para(65(a,2),44(a,1,1))]. 85 x * (((y @ y) @ z) @ x) = x. [para(65(a,2),51(a,1,2,1))]. 95 x * (x @ ((y @ y) @ z)) = x * ((y @ y) @ z). [hyper(11,a,84,a)]. 96 x * y != y | (z @ z) @ u = x. [para(84(a,1),2(a,1)),flip(a)]. 102 x * y != x | ((z @ z) @ u) @ x = y. [para(84(a,1),11(a,2)),rewrite(84(8))]. 104 (((x @ x) @ y) @ z) * u = u. [para(65(a,2),84(a,1,1,1))]. 109 (x @ x) @ y = z @ z. [hyper(50,a,84,a),flip(a)]. 110 x @ x = y @ y. [hyper(50,a,44,a)]. 112 x @ x = c_0. [new_symbol(110)]. 114 c_0 @ x = c_0. [back_rewrite(109),rewrite(112(1),112(3))]. 118 c_0 * x = x. [back_rewrite(104),rewrite(112(1),114(2),114(2))]. 119 x * y != x | c_0 = y. [back_rewrite(102),rewrite(112(3),114(4),114(4))]. 122 x * y != y | c_0 = x. [back_rewrite(96),rewrite(112(3),114(4))]. 123 x * (x @ c_0) = x * c_0. [back_rewrite(95),rewrite(112(1),114(2),112(4),114(5))]. 124 x * c_0 = x. [back_rewrite(85),rewrite(112(1),114(2),114(2))]. 126 (x @ x * y) * (y @ x * y) = c_0. [back_rewrite(81),rewrite(112(1),114(3)),flip(a)]. 129 x * y * z != x * y | c_0 = z. [back_rewrite(74),rewrite(112(5),114(6))]. 130 x * (x @ c_0) = x. [back_rewrite(123),rewrite(124(5))]. 163 x @ c_0 = c_0. [hyper(119,a,130,a),flip(a)]. 165 x * y * (y @ y * x) = y * x. [hyper(1,a,15,a)]. 171 A * B * C * B * A * (B @ C * A) != B * A * B * C * A # answer(E). [para(15(a,1),18(a,2,2,2))]. 205 (x @ y) * ((x @ y) @ y) = x @ y. [para(112(a,1),17(a,1,1)),rewrite(118(6),112(6),124(7))]. 217 x * y != y * x | x @ y = c_0. [para(4(a,1),129(a,1)),flip(b)]. 253 x * (x @ x * y) = x * (x @ y). [hyper(11,a,165,a),flip(a)]. 265 (x @ y * x) * (y @ y * x) = c_0. [para(126(a,1),165(a,1,2,2,2)),rewrite(163(8),124(6),126(10))]. 268 (x @ y) * y = y * (x @ y). [para(205(a,1),4(a,1,2)),flip(a)]. 287 x * y != x * z | z = y. [para(118(a,1),33(a,1,2)),rewrite(124(3),163(5),124(5))]. 292 x @ (y @ x) = c_0. [hyper(217,a,268,a(flip))]. 304 x * (y @ x) != x | y @ x = c_0. [para(268(a,1),122(a,1)),flip(b)]. 317 (x @ y) @ (z @ y) = (x @ z) @ y. [hyper(34,a,17,a)]. 321 x * y != y * x | y @ x = c_0. [para(124(a,1),34(a,1,2))]. 332 (x @ y * x) @ (y @ y * x) = c_0. [para(126(a,1),321(a,1)),rewrite(265(6)),xx(a)]. 402 x @ x * y = x @ y. [hyper(287,a,253,a),flip(a)]. 422 (x @ y * x) @ (y @ x) = c_0. [back_rewrite(332),rewrite(402(4))]. 424 (x @ y * x) * (y @ x) = c_0. [back_rewrite(265),rewrite(402(4))]. 442 (x @ y) * (y @ x * y) * z = z. [back_rewrite(54),rewrite(402(2))]. 448 x @ y * (y @ x) = x @ y * x. [para(4(a,1),402(a,1,2)),flip(a)]. 489 (x @ y * x) * z * (y @ x) = z * (z @ (y @ x)). [para(422(a,1),16(a,1,2,2,2,1)),rewrite(118(7),442(8)),flip(a)]. 535 x * (y @ z) * ((y @ x) @ (z @ x)) = (y @ z) * x. [para(317(a,2),4(a,1,2,2))]. 558 (x @ y) @ (z @ y) = c_0. [para(292(a,1),317(a,1,2)),rewrite(163(4)),flip(a)]. 563 (y @ z) @ x = c_0. [para(317(a,2),304(a,1,2)),rewrite(558(3),124(2)),xx(a)]. 566 x @ (y @ z) = c_0. [para(317(a,2),424(a,1,1)),rewrite(558(7),118(4))]. 575 (x @ y) * z = z * (x @ y). [back_rewrite(535),rewrite(566(4),124(3)),flip(a)]. 588 (x @ y * x) * z * (y @ x) = z. [back_rewrite(489),rewrite(566(7),124(7))]. 601 x * (x @ y * x) = x * (x @ y). [hyper(59,a,14,a),rewrite(575(5))]. 731 x @ y * x = x @ y. [para(4(a,1),448(a,2,2)),rewrite(448(5),601(5),6(5),448(3),563(6),124(4),6(6),402(4),563(6),124(5))]. 768 (x @ y) * z * (y @ x) = z. [back_rewrite(588),rewrite(731(2))]. 789 x @ y * z * x = x @ y * z. [para(3(a,1),731(a,1,2))]. 831 (x @ y * z) * u * (y @ x) * (z @ x) = u. [para(6(a,1),768(a,1,2,2))]. 923 x @ y * z = x @ z * y. [para(14(a,1),789(a,1,2)),rewrite(6(5),563(4),789(4),118(4),6(6),563(5),118(6))]. 945 A * B * C * B * A * (B @ A * C) != B * A * B * C * A # answer(E). [back_rewrite(171),rewrite(923(10))]. 990 $F # answer(E). [ur(41,b,945,a(flip)),rewrite(6(24),6(25),112(21),6(24),575(26,R),118(27),3(27),3(26),3(25),3(24),3(23),831(22),4(10),3(18),3(17),3(16)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=132. Generated=6053. Kept=988. proofs=1. Usable=74. Sos=379. Demods=76. 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=83228. 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.54. User_CPU=0.14, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11355 exit (max_proofs) Sat Aug 12 20:59:56 2006