============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11353 was started by mccune on cleo.thornwood, Sat Aug 12 20:59:51 2006 The command was "/home/mccune/bin/prover9 -f cs.in DA.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 DA.in formulas(sos). (x @ z) * (y @ z) = x * y @ z. end_of_list. formulas(sos). (A @ B) @ C != D @ (F @ G) # answer(A). 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 != D @ (F @ G) # answer(A). [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, D, F, G, *, @ ]). 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 != D @ (F @ G) # answer(A). [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=11): 7 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. given #7 (F,wt=15): 18 ((A @ B) @ C) * x != (D @ (F @ G)) * x # answer(A). [ur(2,b,7,a)]. given #8 (F,wt=15): 19 x * ((A @ B) @ C) != x * (D @ (F @ G)) # answer(A). [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): 24 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=19): 20 x * ((A @ B) @ C) * y != x * (D @ (F @ G)) * y # answer(A). [ur(1,b,18,a)]. given #13 (F,wt=19): 23 x * y * ((A @ B) @ C) != x * y * (D @ (F @ G)) # answer(A). [ur(1,b,19,a)]. given #14 (T,wt=10): 25 x * (y @ y) != y | y = x. [para(10(a,1),2(a,1)),flip(a)]. given #15 (T,wt=10): 26 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=17): 42 C * (A @ B) * (D @ (F @ G)) != (A @ B) * C # answer(A). [para(4(a,1),23(a,1)),flip(a)]. given #18 (F,wt=17): 43 (F @ G) * D * ((A @ B) @ C) != D * (F @ G) # answer(A). [para(4(a,1),23(a,2))]. given #19 (T,wt=11): 27 x * (x @ x) * y = x * y. [para(10(a,1),3(a,1,1)),flip(a)]. given #20 (T,wt=7): 58 (x @ x) * y = y. [hyper(8,a,27,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=21): 52 C * (A @ B) * (D @ (F @ G)) * x != (A @ B) * C * x # answer(A). [ur(9,b,42,a),rewrite(3(11),3(18))]. given #23 (F,wt=21): 54 x * C * (A @ B) * (D @ (F @ G)) != x * (A @ B) * C # answer(A). [ur(1,b,42,a)]. given #24 (T,wt=6): 77 x != y | y = x. [para(10(a,1),11(a,2)),rewrite(58(2),66(4),10(3))]. given #25 (T,wt=9): 65 x * ((y @ y) @ x) = x. [para(58(a,1),4(a,1,2)),rewrite(58(5))]. 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=21): 55 (F @ G) * D * ((A @ B) @ C) * x != D * (F @ G) * x # answer(A). [ur(9,b,43,a),rewrite(3(11),3(18))]. given #28 (F,wt=21): 57 x * (F @ G) * D * ((A @ B) @ C) != x * D * (F @ G) # answer(A). [ur(1,b,43,a)]. given #29 (T,wt=9): 72 x * (x @ x * x) = x. [hyper(11,a,3,a)]. given #30 (T,wt=9): 83 (x @ x) @ y = y @ y. [hyper(24,a,65,a),flip(a)]. 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=21): 82 C * (A @ B) * (D @ (F @ G)) * (C @ C) != (A @ B) * C # answer(A). [para(10(a,1),52(a,2,2))]. given #33 (F,wt=21): 90 (D @ (F @ G)) * ((x @ x) @ ((A @ B) @ C)) != (A @ B) @ C # answer(A). [para(65(a,1),18(a,1)),flip(a)]. given #34 (T,wt=9): 111 x @ x * x = x @ x. [hyper(24,a,72,a),flip(a)]. given #35 (T,wt=9): 115 ((x @ x) @ y) * z = z. [para(83(a,2),58(a,1,1))]. 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=21): 91 ((A @ B) @ C) * ((x @ x) @ (D @ (F @ G))) != D @ (F @ G) # answer(A). [para(65(a,1),18(a,2))]. given #38 (F,wt=23): 21 (D @ (F @ G)) * x * (x @ ((A @ B) @ C)) != x * ((A @ B) @ C) # answer(A). [para(4(a,1),18(a,1)),flip(a)]. given #39 (T,wt=10): 64 x * y != y | z @ z = x. [para(58(a,1),2(a,1)),flip(a)]. NOTE: New constant: x @ x = c_0. [new_symbol(160)]. NOTE: New Function symbol precedence: lex([ A, B, C, D, F, G, c_0, *, @ ]). given #40 (T,wt=5): 163 x @ x = c_0. [new_symbol(160)]. 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=23): 22 ((A @ B) @ C) * x * (x @ (D @ (F @ G))) != x * (D @ (F @ G)) # answer(A). [para(4(a,1),18(a,2))]. given #43 (F,wt=23): 34 x * y * z * ((A @ B) @ C) != x * y * z * (D @ (F @ G)) # answer(A). [ur(8,b,19,a)]. given #44 (T,wt=5): 166 c_0 @ x = c_0. [back_rewrite(159),rewrite(163(1),163(3))]. given #45 (T,wt=5): 172 c_0 * x = x. [back_rewrite(135),rewrite(163(1),166(2),166(2))]. 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=23): 35 x * y * ((A @ B) @ C) * z != x * y * (D @ (F @ G)) * z # answer(A). [ur(8,b,18,a)]. given #48 (F,wt=23): 40 x * (D @ (F @ G)) * (((A @ B) @ C) @ x) != ((A @ B) @ C) * x # answer(A). [para(4(a,1),20(a,1)),flip(a)]. given #49 (T,wt=5): 181 x * c_0 = x. [back_rewrite(116),rewrite(163(1),166(2),166(2))]. given #50 (T,wt=7): 184 x @ x * x = c_0. [back_rewrite(111),rewrite(163(3))]. 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=19): 205 (D @ (F @ G)) * (((A @ B) @ C) @ c_0) != (A @ B) @ C # answer(A). [para(172(a,1),40(a,1)),rewrite(181(20))]. given #53 (F,wt=21): 213 (B @ C) * (A @ C) * (D @ (F @ G)) != (A @ C) * (B @ C) # answer(A). [para(17(a,1),23(a,1)),flip(a)]. given #54 (T,wt=7): 187 x * (x @ c_0) = x. [back_rewrite(179),rewrite(181(5))]. given #55 (T,wt=8): 175 x * y != x | c_0 = y. [back_rewrite(131),rewrite(163(3),166(4),166(4))]. given #56 (A,wt=18): 36 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=23): 41 x * ((A @ B) @ C) * ((D @ (F @ G)) @ x) != (D @ (F @ G)) * x # answer(A). [para(4(a,1),20(a,2))]. given #58 (F,wt=23): 81 C * (A @ B) * (D @ (F @ G)) * (C @ (A @ B)) != C * (A @ B) # answer(A). [para(4(a,1),52(a,2))]. given #59 (T,wt=5): 243 x @ c_0 = c_0. [hyper(175,a,187,a),flip(a)]. given #60 (T,wt=8): 178 x * y != y | c_0 = x. [back_rewrite(125),rewrite(163(3),166(4))]. given #61 (A,wt=18): 37 x * y * z != x * u * y | u * (u @ y) = z. [para(4(a,1),8(a,1,2)),flip(a)]. given #62 (F,wt=23): 108 (F @ G) * D * ((A @ B) @ C) * ((F @ G) @ D) != (F @ G) * D # answer(A). [para(4(a,1),55(a,2))]. given #63 (F,wt=25): 53 x * y * C * (A @ B) * (D @ (F @ G)) != x * y * (A @ B) * C # answer(A). [ur(8,b,42,a)]. given #64 (T,wt=10): 103 x * y != y * y | y = x. [para(10(a,1),12(a,1,2))]. given #65 (T,wt=10): 265 x * y != x * z | z = y. [para(172(a,1),37(a,1,2)),rewrite(181(3),243(5),181(5))]. given #66 (A,wt=14): 38 x * y * z != y * x | y @ x = z. [para(4(a,1),8(a,1)),flip(a)]. given #67 (F,wt=21): 267 B * A * C * (A @ B) * (D @ (F @ G)) != A * B * C # answer(A). [para(14(a,1),53(a,2))]. given #68 (F,wt=25): 56 x * y * (F @ G) * D * ((A @ B) @ C) != x * y * D * (F @ G) # answer(A). [ur(8,b,43,a)]. given #69 (T,wt=12): 173 x * (x @ y) != x * y | c_0 = y. [back_rewrite(134),rewrite(163(5),166(6))]. given #70 (T,wt=12): 176 x * y * z != z | x * y = c_0. [back_rewrite(130),rewrite(163(4),166(5)),flip(b)]. given #71 (A,wt=18): 46 x * y * z * u != v * u | x * y * z = v. [para(3(a,1),9(a,1,2))]. given #72 (F,wt=21): 279 F * G * D * ((A @ B) @ C) != G * F * D * (F @ G) # answer(A). [para(14(a,1),56(a,1))]. given #73 (F,wt=25): 79 x * C * (A @ B) * (D @ (F @ G)) * y != x * (A @ B) * C * y # answer(A). [ur(1,b,52,a)]. given #74 (T,wt=12): 185 x * y != y | x * (x @ y) = c_0. [back_rewrite(98),rewrite(163(3),166(4)),flip(b)]. given #75 (T,wt=12): 186 x * y * z != x * y | c_0 = z. [back_rewrite(92),rewrite(163(5),166(6))]. given #76 (A,wt=18): 47 x * y * z != u * v * z | x * y = u * v. [para(3(a,1),9(a,2))]. given #77 (F,wt=25): 80 C * (A @ B) * (D @ (F @ G)) * x * (x @ C) != (A @ B) * x * C # answer(A). [para(4(a,1),52(a,2,2))]. given #78 (F,wt=25): 106 x * (F @ G) * D * ((A @ B) @ C) * y != x * D * (F @ G) * y # answer(A). [ur(1,b,55,a)]. given #79 (T,wt=12): 276 x * y != y * x | y @ x = c_0. [para(181(a,1),38(a,1,2))]. given #80 (T,wt=12): 283 x @ y != x * y | y * x = c_0. [para(4(a,1),176(a,1)),flip(a)]. given #81 (A,wt=18): 48 x * y * (y @ z) != u * y * z | u * z = x. [para(4(a,1),9(a,1,2)),flip(a)]. given #82 (F,wt=25): 107 D * (F @ G) * (((A @ B) @ C) @ D) != (F @ G) * ((A @ B) @ C) * D # answer(A). [para(4(a,1),55(a,1,2)),flip(a)]. given #83 (F,wt=25): 199 (F @ G) * ((A @ B) @ C) * D * (D @ (D @ (F @ G))) != D * (F @ G) # answer(A). [ur(11,b,22,a(flip))]. given #84 (T,wt=10): 324 x * y != z * y | z = x. [para(181(a,1),48(a,2,2)),rewrite(243(2),181(2),181(5))]. given #85 (T,wt=12): 302 x * y != y * x | x @ y = c_0. [para(4(a,1),186(a,1)),flip(b)]. given #86 (A,wt=14): 49 x * (y @ z) != y * z | z * y = x. [para(4(a,1),9(a,1)),flip(a)]. given #87 (F,wt=25): 220 x * (B @ C) * (A @ C) * (D @ (F @ G)) != x * (A @ C) * (B @ C) # answer(A). [para(17(a,1),34(a,1,2)),flip(a)]. given #88 (F,wt=25): 226 (B @ C) * (A @ C) * (D @ (F @ G)) * x != (A @ C) * (B @ C) * x # answer(A). [ur(9,b,213,a),rewrite(3(13),3(22))]. given #89 (T,wt=13): 183 (x @ x * y) * (y @ x * y) = c_0. [back_rewrite(112),rewrite(163(1),166(3)),flip(a)]. given #90 (T,wt=13): 217 (x @ y) * ((x @ y) @ y) = x @ y. [para(163(a,1),17(a,1,1)),rewrite(172(6),163(6),181(7))]. given #91 (A,wt=18): 50 x * y * z * (z @ u) != z * u | x * y = u. [para(4(a,1),9(a,2))]. given #92 (F,wt=25): 277 x * B * A * C * (A @ B) * (D @ (F @ G)) != x * A * B * C # answer(A). [ur(265,b,267,a),flip(a)]. given #93 (F,wt=25): 278 B * A * C * (A @ B) * (D @ (F @ G)) * x != A * B * C * x # answer(A). [ur(9,b,267,a),rewrite(3(15),3(14),3(13),3(22),3(21))]. given #94 (T,wt=7): 346 (x @ y) @ y = c_0. [hyper(175,a,217,a),flip(a)]. given #95 (T,wt=11): 347 (x @ y) * y = y * (x @ y). [para(217(a,1),4(a,1,2)),flip(a)]. given #96 (A,wt=15): 68 (x @ x * y) * (y @ x * y) * z = z. [para(6(a,1),58(a,1,1)),rewrite(3(6))]. given #97 (F,wt=15): 371 C * ((A @ B) @ C) != (D @ (F @ G)) * C # answer(A). [para(347(a,1),18(a,1))]. given #98 (F,wt=19): 372 ((A @ B) @ C) * (F @ G) != (F @ G) * (D @ (F @ G)) # answer(A). [para(347(a,1),18(a,2))]. given #99 (T,wt=7): 367 x @ (y @ x) = c_0. [hyper(276,a,347,a)]. given #100 (T,wt=9): 416 (x @ y) @ y * x = c_0. [para(68(a,1),17(a,1)),rewrite(404(8))]. given #101 (A,wt=20): 73 x * y * z != u * x * y | u * (u @ x * y) = z. [para(3(a,1),11(a,1))]. given #102 (F,wt=19): 377 x * C * ((A @ B) @ C) != x * (D @ (F @ G)) * C # answer(A). [para(347(a,1),20(a,1,2))]. given #103 (F,wt=19): 426 C * ((A @ B) @ C) * x != (D @ (F @ G)) * C * x # answer(A). [ur(324,b,371,a),rewrite(3(8),3(16)),flip(a)]. given #104 (T,wt=9): 435 (x @ y) @ x * y = c_0. [para(4(a,1),416(a,1,2)),rewrite(6(3),346(3),181(3))]. given #105 (T,wt=11): 424 x * (y @ x) * y = y * x. [back_rewrite(365),rewrite(416(3),181(2)),flip(a)]. given #106 (A,wt=22): 74 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 #107 (F,wt=17): 470 C * (D @ (F @ G)) * (A @ B) != (A @ B) * C # answer(A). [para(424(a,1),20(a,1)),flip(a)]. given #108 (F,wt=17): 471 (F @ G) * ((A @ B) @ C) * D != D * (F @ G) # answer(A). [para(424(a,1),20(a,2))]. given #109 (T,wt=11): 430 x @ (y @ x) * (z @ x) = c_0. [para(6(a,1),367(a,1,2))]. given #110 (T,wt=11): 446 (x @ (y @ y * z)) @ x = c_0. [para(68(a,1),416(a,1,2)),rewrite(6(6),405(5),172(5))]. given #111 (A,wt=18): 75 x * y != z * y | z * (z @ y) = x * (x @ y). [para(4(a,1),11(a,1))]. given #112 (F,wt=17): 494 (D @ (F @ G)) * C * (A @ B) != (A @ B) * C # answer(A). [para(424(a,1),426(a,1)),flip(a)]. given #113 (F,wt=19): 452 C * C * ((A @ B) @ C) != (D @ (F @ G)) * C * C # answer(A). [para(347(a,1),426(a,1,2))]. given #114 (T,wt=11): 466 (x @ y) * x = x * (x @ y). [hyper(11,a,424,a),flip(a)]. given #115 (T,wt=7): 529 (x @ y) @ x = c_0. [hyper(302,a,466,a)]. given #116 (A,wt=22): 76 x * (x @ y) * z != x * y | y * (y @ x * (x @ y)) = z. [para(4(a,1),11(a,2)),rewrite(3(3))]. given #117 (F,wt=15): 538 ((A @ B) @ C) * D != D * (D @ (F @ G)) # answer(A). [para(466(a,1),18(a,2))]. given #118 (F,wt=19): 537 (A @ B) * ((A @ B) @ C) != (D @ (F @ G)) * (A @ B) # answer(A). [para(466(a,1),18(a,1))]. given #119 (T,wt=7): 530 x @ (x @ y) = c_0. [hyper(276,a,466,a)]. given #120 (T,wt=12): 389 x * (y @ x) != x | y @ x = c_0. [para(347(a,1),178(a,1)),flip(b)]. given #121 (A,wt=22): 101 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 #122 (F,wt=19): 542 x * ((A @ B) @ C) * D != x * D * (D @ (F @ G)) # answer(A). [para(466(a,1),20(a,2,2))]. given #123 (F,wt=19): 585 ((A @ B) @ C) * D * x != D * (D @ (F @ G)) * x # answer(A). [ur(324,b,538,a),rewrite(3(8),3(16)),flip(a)]. given #124 (T,wt=12): 485 x * (y @ x) != y * x | c_0 = y. [para(424(a,1),38(a,1)),rewrite(347(3),346(6)),flip(a)]. given #125 (T,wt=12): 486 x * y != x | y * (x @ y) = c_0. [para(424(a,1),176(a,1))]. given #126 (A,wt=22): 102 x * y * (y @ z * (z @ y)) != z * y | z * (z @ y) = x. [para(4(a,1),12(a,2))]. given #127 (F,wt=19): 609 ((A @ B) @ C) * D * D != D * D * (D @ (F @ G)) # answer(A). [para(466(a,1),585(a,2,2))]. given #128 (F,wt=21): 384 (F @ G) * D * C * ((A @ B) @ C) != D * (F @ G) * C # answer(A). [para(347(a,1),55(a,1,2,2))]. given #129 (T,wt=12): 554 x * (x @ y) != x | x @ y = c_0. [para(466(a,1),178(a,1)),flip(b)]. given #130 (T,wt=13): 259 x * (x @ x * y) = x * (x @ y). [hyper(37,a,15,a),flip(a)]. given #131 (A,wt=22): 120 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 #132 (F,wt=21): 385 (F @ G) * D * ((A @ B) @ C) * G != D * G * (F @ G) # answer(A). [para(347(a,1),55(a,2,2))]. given #133 (F,wt=21): 477 x * C * (D @ (F @ G)) * (A @ B) != x * (A @ B) * C # answer(A). [para(424(a,1),35(a,1,2)),flip(a)]. given #134 (T,wt=9): 620 x @ x * y = x @ y. [hyper(265,a,259,a),flip(a)]. given #135 (T,wt=11): 630 (x @ y) @ x * (x @ y) = c_0. [para(259(a,1),183(a,1,1,2)),rewrite(620(3),530(2),620(3),620(4),172(6))]. given #136 (A,wt=18): 137 x * y * z != y * u | x * (x @ y) * z = u. [para(14(a,1),1(a,1))]. given #137 (F,wt=21): 478 x * (F @ G) * ((A @ B) @ C) * D != x * D * (F @ G) # answer(A). [para(424(a,1),35(a,2,2))]. given #138 (F,wt=21): 499 F * G * D * ((A @ B) @ C) * (D @ G) != F * D * G # answer(A). [ur(74,b,106,a(flip)),rewrite(14(24)),flip(a)]. given #139 (T,wt=11): 638 x * (y @ x) * (x @ y) = x. [back_rewrite(572),rewrite(620(2),357(4))]. given #140 (T,wt=9): 734 (x @ y) * (y @ x) = c_0. [hyper(175,a,638,a),flip(a)]. given #141 (A,wt=18): 138 x * y * (y @ z) * u != y * z * u | z = x. [para(14(a,1),2(a,1)),flip(a)]. given #142 (F,wt=13): 767 (D @ (F @ G)) * (C @ (A @ B)) != c_0 # answer(A). [para(734(a,1),18(a,1)),flip(a)]. given #143 (F,wt=13): 768 ((A @ B) @ C) * ((F @ G) @ D) != c_0 # answer(A). [para(734(a,1),18(a,2))]. given #144 (T,wt=9): 808 (x @ y) @ (y @ x) = c_0. [para(734(a,1),276(a,1)),rewrite(734(4)),xx(a)]. given #145 (T,wt=10): 791 x @ y != c_0 | y @ x = c_0. [para(734(a,1),175(a,1)),flip(a),flip(b)]. given #146 (A,wt=18): 139 x * y * (y @ z) * u != y * z * u | x = z. [para(14(a,1),2(a,2))]. given #147 (F,wt=13): 769 (C @ (A @ B)) * (D @ (F @ G)) != c_0 # answer(A). [para(734(a,1),19(a,1)),flip(a)]. given #148 (F,wt=13): 770 ((F @ G) @ D) * ((A @ B) @ C) != c_0 # answer(A). [para(734(a,1),19(a,2))]. given #149 (T,wt=11): 653 (x @ y * x) @ (y @ x) = c_0. [back_rewrite(405),rewrite(620(4))]. given #150 (T,wt=11): 654 (x @ y * x) * (y @ x) = c_0. [back_rewrite(404),rewrite(620(4))]. given #151 (A,wt=21): 140 x * y * z * (z @ x * y) * u = z * x * y * u. [para(14(a,1),3(a,1)),rewrite(3(2)),flip(a)]. given #152 (F,wt=15): 757 (D @ (F @ G)) * C * (C @ (A @ B)) != C # answer(A). [para(638(a,1),426(a,1)),flip(a)]. given #153 (F,wt=15): 772 x * (D @ (F @ G)) * (C @ (A @ B)) != x # answer(A). [para(734(a,1),20(a,1,2)),rewrite(181(2)),flip(a)]. given #154 (T,wt=11): 674 (x @ y) * (y @ x * y) = c_0. [back_rewrite(183),rewrite(620(2))]. given #155 (T,wt=11): 702 (x @ y) @ y * (x @ y) = c_0. [para(346(a,1),620(a,2)),rewrite(347(3))]. given #156 (A,wt=23): 141 x * y * z * (y @ x) * (z @ x) * u = y * z * x * u. [para(3(a,1),14(a,1,2)),rewrite(6(2),3(4),3(10))]. given #157 (F,wt=15): 773 x * ((A @ B) @ C) * ((F @ G) @ D) != x # answer(A). [para(734(a,1),20(a,2,2)),rewrite(181(14))]. given #158 (F,wt=15): 774 x * (C @ (A @ B)) * (D @ (F @ G)) != x # answer(A). [para(734(a,1),23(a,1,2)),rewrite(181(2)),flip(a)]. given #159 (T,wt=11): 703 (x @ y) @ x * y * x = c_0. [para(620(a,1),416(a,1,1)),rewrite(3(3))]. given #160 (T,wt=11): 704 (x @ y) @ x * x * y = c_0. [para(620(a,1),435(a,1,1))]. given #161 (A,wt=21): 142 x * y * z * (z @ (x @ y)) = y * x * z * (x @ y). [para(4(a,1),14(a,1,2,2)),flip(a)]. given #162 (F,wt=15): 775 x * ((F @ G) @ D) * ((A @ B) @ C) != x # answer(A). [para(734(a,1),23(a,2,2)),rewrite(181(14))]. given #163 (F,wt=15): 816 ((A @ B) @ C) * D * ((F @ G) @ D) != D # answer(A). [para(734(a,1),585(a,2,2)),rewrite(181(16))]. given #164 (T,wt=11): 763 (x @ y) * (y @ x) * z = z. [para(734(a,1),3(a,1,1)),rewrite(172(2)),flip(a)]. given #165 (T,wt=9): 1080 x @ y * x = x @ y. [para(674(a,1),763(a,1,2)),rewrite(181(3)),flip(a)]. given #166 (A,wt=22): 146 x * y * z * u != x * z * v | y * (y @ z) * u = v. [para(14(a,1),8(a,1,2))]. given #167 (F,wt=11): 1124 D @ (G @ F) != C @ (A @ B) # answer(A). [back_rewrite(1079),rewrite(1116(5))]. given #168 (F,wt=11): 1241 D @ (F @ G) != C @ (B @ A) # answer(A). [back_rewrite(7),rewrite(1116(5)),flip(a)]. given #169 (T,wt=11): 895 x @ (x @ y) * (x @ y) = c_0. [para(630(a,1),654(a,1,2)),rewrite(534(6),6(7),620(5),713(10),181(6),181(6))]. given #170 (T,wt=11): 1096 x @ y * (y @ x) = x @ y. [back_rewrite(694),rewrite(1080(5))]. given #171 (A,wt=18): 147 x * y * z != y * x * u | (x @ y) * z = u. [para(14(a,1),8(a,1))]. given #172 (F,wt=13): 1170 (D @ (G @ F)) * (C @ (B @ A)) != c_0 # answer(A). [back_rewrite(770),rewrite(1116(5),1116(10))]. given #173 (F,wt=13): 1171 (C @ (B @ A)) * (D @ (G @ F)) != c_0 # answer(A). [back_rewrite(768),rewrite(1116(5),1116(10))]. given #174 (T,wt=11): 1116 (x @ y) @ z = z @ (y @ x). [para(763(a,1),1080(a,1,2)),rewrite(6(3),163(3),181(4),6(6),808(5),172(6))]. given #175 (T,wt=11): 1121 (x @ y) @ (x @ y * y) = c_0. [back_rewrite(868),rewrite(1099(3),1116(4,R))]. given #176 (A,wt=18): 148 x * y * z != y * x * u | (y @ x) * u = z. [para(14(a,1),8(a,2)),flip(b)]. given #177 (F,wt=15): 831 (D @ (F @ G)) * (C @ (A @ B)) * x != x # answer(A). [ur(324,b,767,a),rewrite(172(2),3(12)),flip(a)]. given #178 (F,wt=15): 850 (C @ (A @ B)) * (D @ (F @ G)) * x != x # answer(A). [ur(324,b,769,a),rewrite(172(2),3(12)),flip(a)]. given #179 (T,wt=11): 1310 (x @ y) @ ((y @ x) @ z) = c_0. [para(1116(a,2),367(a,1,2))]. given #180 (T,wt=11): 1317 (x @ y) @ (z @ (y @ x)) = c_0. [para(1116(a,1),530(a,1,2))]. given #181 (A,wt=22): 149 x * y * (y @ z) * u != v * y * z * u | v * z = x. [para(14(a,1),9(a,1,2)),flip(a)]. given #182 (F,wt=15): 1068 (C @ (A @ B)) * D * (D @ (F @ G)) != D # answer(A). [para(763(a,1),542(a,1)),flip(a)]. given #183 (F,wt=15): 1126 (D @ (G @ F)) * C * (C @ (B @ A)) != C # answer(A). [back_rewrite(1065),rewrite(1116(5),1116(11))]. given #184 (T,wt=12): 761 (x @ y) * z != c_0 | y @ x = z. [para(734(a,1),1(a,1)),flip(a)]. given #185 (T,wt=12): 762 x * (y @ z) != c_0 | z @ y = x. [para(734(a,1),2(a,1)),flip(a)]. given #186 (A,wt=18): 150 x * (y @ z) * u != y * z * u | z * y = x. [para(14(a,1),9(a,1)),flip(a)]. given #187 (F,wt=15): 1153 (D @ (G @ F)) * (C @ (B @ A)) * x != x # answer(A). [back_rewrite(854),rewrite(1116(5),1116(10))]. given #188 (F,wt=15): 1158 (C @ (B @ A)) * (D @ (G @ F)) * x != x # answer(A). [back_rewrite(835),rewrite(1116(5),1116(10))]. given #189 (T,wt=12): 799 x @ y != z | z * (y @ x) = c_0. [para(734(a,1),176(a,1,2)),rewrite(181(2)),flip(a)]. given #190 (T,wt=12): 804 x * (y @ z) != x | z @ y = c_0. [para(734(a,1),186(a,1,2)),rewrite(181(2)),flip(a),flip(b)]. given #191 (A,wt=22): 151 x * y * z * (z @ u) * v != z * u * v | x * y = u. [para(14(a,1),9(a,2))]. given #192 (F,wt=15): 1159 (C @ (B @ A)) * D * (D @ (G @ F)) != D # answer(A). [back_rewrite(816),rewrite(1116(5),1116(11))]. given #193 (F,wt=15): 1168 x * (D @ (G @ F)) * (C @ (B @ A)) != x # answer(A). [back_rewrite(775),rewrite(1116(5),1116(10))]. given #194 (T,wt=12): 809 x * y != c_0 | y @ x = y * x. [para(734(a,1),49(a,1)),flip(a),flip(b)]. given #195 (T,wt=12): 1029 x @ y != z | (y @ x) * z = c_0. [para(763(a,1),175(a,1)),flip(a),flip(b)]. given #196 (A,wt=22): 153 x * y * z != u * y | u * (u @ y) = x * (x @ y) * z. [para(14(a,1),11(a,1))]. given #197 (F,wt=15): 1169 x * (C @ (B @ A)) * (D @ (G @ F)) != x # answer(A). [back_rewrite(773),rewrite(1116(5),1116(10))]. given #198 (F,wt=15): 1194 D * (D @ (F @ G)) != (C @ (B @ A)) * D # answer(A). [back_rewrite(538),rewrite(1116(5)),flip(a)]. given #199 (T,wt=12): 1031 (x @ y) * z != z | y @ x = c_0. [para(763(a,1),178(a,1)),flip(a),flip(b)]. given #200 (T,wt=12): 1398 c_0 != x | (y @ z) * x = y @ z. [para(763(a,1),761(a,1)),flip(a),flip(b)]. given #201 (A,wt=25): 156 x * y * z * (z @ (x @ y)) * u = y * x * z * (x @ y) * u. [para(14(a,1),14(a,1,2,2)),flip(a)]. given #202 (F,wt=15): 1219 (D @ (F @ G)) * C != C * (C @ (B @ A)) # answer(A). [back_rewrite(371),rewrite(1116(6)),flip(a)]. given #203 (F,wt=15): 1239 x * (D @ (F @ G)) != x * (C @ (B @ A)) # answer(A). [back_rewrite(19),rewrite(1116(5)),flip(a)]. given #204 (T,wt=12): 1459 (x @ y) * z != z | x @ y = c_0. [para(763(a,1),1031(a,1)),flip(a)]. given #205 (T,wt=13): 269 (x @ y) @ (z @ y) = (x @ z) @ y. [hyper(38,a,17,a)]. ============================== PROOF ================================= % Proof 1 at 0.35 (+ 0.01) seconds: A. % Length of proof is 73. % Level of proof is 24. % Maximum clause weight is 23. % Given clauses 205. 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 != D @ (F @ G) # answer(A). [assumption]. 8 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite(3(4))]. 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)]. 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) * x != (D @ (F @ G)) * x # answer(A). [ur(2,b,7,a)]. 20 x * ((A @ B) @ C) * y != x * (D @ (F @ G)) * y # answer(A). [ur(1,b,18,a)]. 24 x * y != x | x @ x = y. [para(10(a,1),1(a,1)),flip(a)]. 27 x * (x @ x) * y = x * y. [para(10(a,1),3(a,1,1)),flip(a)]. 37 x * y * z != x * u * y | u * (u @ y) = z. [para(4(a,1),8(a,1,2)),flip(a)]. 38 x * y * z != y * x | y @ x = z. [para(4(a,1),8(a,1)),flip(a)]. 40 x * (D @ (F @ G)) * (((A @ B) @ C) @ x) != ((A @ B) @ C) * x # answer(A). [para(4(a,1),20(a,1)),flip(a)]. 58 (x @ x) * y = y. [hyper(8,a,27,a)]. 64 x * y != y | z @ z = x. [para(58(a,1),2(a,1)),flip(a)]. 65 x * ((y @ y) @ x) = x. [para(58(a,1),4(a,1,2)),rewrite(58(5))]. 68 (x @ x * y) * (y @ x * y) * z = z. [para(6(a,1),58(a,1,1)),rewrite(3(6))]. 73 x * y * z != u * x * y | u * (u @ x * y) = z. [para(3(a,1),11(a,1))]. 83 (x @ x) @ y = y @ y. [hyper(24,a,65,a),flip(a)]. 112 (x @ x) @ y * z = (y @ y * z) * (z @ y * z). [para(83(a,2),6(a,1))]. 115 ((x @ x) @ y) * z = z. [para(83(a,2),58(a,1,1))]. 116 x * (((y @ y) @ z) @ x) = x. [para(83(a,2),65(a,1,2,1))]. 124 x * (x @ ((y @ y) @ z)) = x * ((y @ y) @ z). [hyper(11,a,115,a)]. 131 x * y != x | ((z @ z) @ u) @ x = y. [para(115(a,1),11(a,2)),rewrite(115(8))]. 135 (((x @ x) @ y) @ z) * u = u. [para(83(a,2),115(a,1,1,1))]. 159 (x @ x) @ y = z @ z. [hyper(64,a,115,a),flip(a)]. 160 x @ x = y @ y. [hyper(64,a,58,a)]. 163 x @ x = c_0. [new_symbol(160)]. 166 c_0 @ x = c_0. [back_rewrite(159),rewrite(163(1),163(3))]. 172 c_0 * x = x. [back_rewrite(135),rewrite(163(1),166(2),166(2))]. 175 x * y != x | c_0 = y. [back_rewrite(131),rewrite(163(3),166(4),166(4))]. 179 x * (x @ c_0) = x * c_0. [back_rewrite(124),rewrite(163(1),166(2),163(4),166(5))]. 181 x * c_0 = x. [back_rewrite(116),rewrite(163(1),166(2),166(2))]. 183 (x @ x * y) * (y @ x * y) = c_0. [back_rewrite(112),rewrite(163(1),166(3)),flip(a)]. 187 x * (x @ c_0) = x. [back_rewrite(179),rewrite(181(5))]. 198 x * y * ((x @ y) @ y * x) = (x @ y) * y * x. [para(15(a,1),14(a,1)),flip(a)]. 217 (x @ y) * ((x @ y) @ y) = x @ y. [para(163(a,1),17(a,1,1)),rewrite(172(6),163(6),181(7))]. 243 x @ c_0 = c_0. [hyper(175,a,187,a),flip(a)]. 259 x * (x @ x * y) = x * (x @ y). [hyper(37,a,15,a),flip(a)]. 265 x * y != x * z | z = y. [para(172(a,1),37(a,1,2)),rewrite(181(3),243(5),181(5))]. 269 (x @ y) @ (z @ y) = (x @ z) @ y. [hyper(38,a,17,a)]. 276 x * y != y * x | y @ x = c_0. [para(181(a,1),38(a,1,2))]. 346 (x @ y) @ y = c_0. [hyper(175,a,217,a),flip(a)]. 347 (x @ y) * y = y * (x @ y). [para(217(a,1),4(a,1,2)),flip(a)]. 357 (x @ y) * y * z = y * (x @ y) * z. [para(346(a,1),14(a,1,2,2,1)),rewrite(172(3)),flip(a)]. 365 x * y * ((x @ y) @ y * x) = y * (x @ y) * x. [back_rewrite(198),rewrite(357(8))]. 367 x @ (y @ x) = c_0. [hyper(276,a,347,a)]. 404 (x @ y * x) * (y @ y * x) = c_0. [hyper(175,a,68,a),flip(a)]. 416 (x @ y) @ y * x = c_0. [para(68(a,1),17(a,1)),rewrite(404(8))]. 424 x * (y @ x) * y = y * x. [back_rewrite(365),rewrite(416(3),181(2)),flip(a)]. 448 x * (x @ y * x) = (x @ y) * x. [hyper(73,a,14,a)]. 466 (x @ y) * x = x * (x @ y). [hyper(11,a,424,a),flip(a)]. 495 x * (x @ y * x) = x * (x @ y). [back_rewrite(448),rewrite(466(5))]. 572 (x @ x * y) * y * (y @ x) = y. [para(466(a,1),68(a,1,2)),rewrite(495(5))]. 620 x @ x * y = x @ y. [hyper(265,a,259,a),flip(a)]. 638 x * (y @ x) * (x @ y) = x. [back_rewrite(572),rewrite(620(2),357(4))]. 674 (x @ y) * (y @ x * y) = c_0. [back_rewrite(183),rewrite(620(2))]. 734 (x @ y) * (y @ x) = c_0. [hyper(175,a,638,a),flip(a)]. 763 (x @ y) * (y @ x) * z = z. [para(734(a,1),3(a,1,1)),rewrite(172(2)),flip(a)]. 808 (x @ y) @ (y @ x) = c_0. [para(734(a,1),276(a,1)),rewrite(734(4)),xx(a)]. 1080 x @ y * x = x @ y. [para(674(a,1),763(a,1,2)),rewrite(181(3)),flip(a)]. 1116 (x @ y) @ z = z @ (y @ x). [para(763(a,1),1080(a,1,2)),rewrite(6(3),163(3),181(4),6(6),808(5),172(6))]. 1232 x * (D @ (F @ G)) * ((C @ (B @ A)) @ x) != (C @ (B @ A)) * x # answer(A). [back_rewrite(40),rewrite(1116(10),1116(18))]. 1500 (x @ y) @ (z @ y) = c_0. [para(367(a,1),269(a,1,2)),rewrite(243(4)),flip(a)]. 1514 x @ (y @ z) = c_0. [para(269(a,2),734(a,1,1)),rewrite(1500(3),172(4))]. 1553 $F # answer(A). [back_rewrite(1232),rewrite(1514(5),1514(6),166(3),181(3),181(2),1514(5),172(2)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=205. Generated=12211. Kept=1551. proofs=1. Usable=117. Sos=647. Demods=121. Limbo=44, Disabled=749. Hints=0. Weight_deleted=4209. Literals_deleted=0. Forward_subsumed=6450. Back_subsumed=103. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=379 (2 lex), Back_demodulated=640. Back_unit_deleted=0. Demod_attempts=236586. Demod_rewrites=23678. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=47712. Nonunit_bsub_feature_tests=12521. Megabytes=1.15. User_CPU=0.35, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11353 exit (max_proofs) Sat Aug 12 20:59:51 2006