============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13118 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:29 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). 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 DA.in clauses(sos). (x @ y) * (z @ y) = x * z @ y. end_of_list. clauses(sos). (A @ B) @ C != D @ (F @ G) # answer(A). 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 != D @ (F @ G) # answer(A). [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, D, F, G, *, @ ]). After inverse_order: Function symbol precedence: lex([ A, B, C, D, F, G, *, @ ]). 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 != D @ (F @ G) # answer(A). [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=11): 12 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. given #7 (F,wt=15): 23 ((A @ B) @ C) * x != (D @ (F @ G)) * x # answer(A). [ur(8,b,12,a)]. given #8 (F,wt=15): 24 x * ((A @ B) @ C) != x * (D @ (F @ G)) # answer(A). [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): 29 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=19): 25 x * ((A @ B) @ C) * y != x * (D @ (F @ G)) * y # answer(A). [ur(7,b,23,a)]. given #13 (F,wt=19): 28 x * y * ((A @ B) @ C) != x * y * (D @ (F @ G)) # answer(A). [ur(7,b,24,a)]. given #14 (T,wt=10): 30 x * (y @ y) != y | y = x. [para(15(a,1),8(a,1)),flip(a)]. given #15 (T,wt=10): 31 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=17): 47 C * (A @ B) * (D @ (F @ G)) != (A @ B) * C # answer(A). [para(10(a,1),28(a,1)),flip(a)]. given #18 (F,wt=17): 48 (F @ G) * D * ((A @ B) @ C) != D * (F @ G) # answer(A). [para(10(a,1),28(a,2))]. given #19 (T,wt=11): 32 x * (x @ x) * y = x * y. [para(15(a,1),9(a,1,1)),flip(a)]. given #20 (T,wt=7): 63 (x @ x) * y = y. [hyper(13,a,32,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=21): 57 C * (A @ B) * (D @ (F @ G)) * x != (A @ B) * C * x # answer(A). [ur(14,b,47,a),demod(9(11),9(18))]. given #23 (F,wt=21): 59 x * C * (A @ B) * (D @ (F @ G)) != x * (A @ B) * C # answer(A). [ur(7,b,47,a)]. given #24 (T,wt=6): 82 x != y | y = x. [para(15(a,1),16(a,2)),demod(63(2),71(4),15(3))]. given #25 (T,wt=9): 70 x * ((y @ y) @ x) = x. [para(63(a,1),10(a,1,2)),demod(63(5))]. 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=21): 60 (F @ G) * D * ((A @ B) @ C) * x != D * (F @ G) * x # answer(A). [ur(14,b,48,a),demod(9(11),9(18))]. given #28 (F,wt=21): 62 x * (F @ G) * D * ((A @ B) @ C) != x * D * (F @ G) # answer(A). [ur(7,b,48,a)]. given #29 (T,wt=9): 77 x * (x @ x * x) = x. [hyper(16,a,9,a)]. given #30 (T,wt=9): 88 (x @ x) @ y = y @ y. [hyper(29,a,70,a),flip(a)]. 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=21): 87 C * (A @ B) * (D @ (F @ G)) * (C @ C) != (A @ B) * C # answer(A). [para(15(a,1),57(a,2,2))]. given #33 (F,wt=21): 95 (D @ (F @ G)) * ((x @ x) @ ((A @ B) @ C)) != (A @ B) @ C # answer(A). [para(70(a,1),23(a,1)),flip(a)]. given #34 (T,wt=9): 116 x @ x * x = x @ x. [hyper(29,a,77,a),flip(a)]. given #35 (T,wt=9): 120 ((x @ x) @ y) * z = z. [para(88(a,2),63(a,1,1))]. 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=21): 96 ((A @ B) @ C) * ((x @ x) @ (D @ (F @ G))) != D @ (F @ G) # answer(A). [para(70(a,1),23(a,2))]. given #38 (F,wt=23): 26 (D @ (F @ G)) * x * (x @ ((A @ B) @ C)) != x * ((A @ B) @ C) # answer(A). [para(10(a,1),23(a,1)),flip(a)]. given #39 (T,wt=10): 69 x * y != y | z @ z = x. [para(63(a,1),8(a,1)),flip(a)]. NOTE: New constant: 0 x @ x = c_0. [new_symbol(165)]. NOTE: New Function symbol precedence: lex([ A, B, C, D, F, G, c_0, *, @ ]). given #40 (T,wt=5): 168 x @ x = c_0. [new_symbol(165)]. 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=23): 27 ((A @ B) @ C) * x * (x @ (D @ (F @ G))) != x * (D @ (F @ G)) # answer(A). [para(10(a,1),23(a,2))]. given #43 (F,wt=23): 39 x * y * z * ((A @ B) @ C) != x * y * z * (D @ (F @ G)) # answer(A). [ur(13,b,24,a)]. given #44 (T,wt=5): 171 c_0 @ x = c_0. [back_demod(164),demod(168(1),168(3))]. given #45 (T,wt=5): 177 c_0 * x = x. [back_demod(140),demod(168(1),171(2),171(2))]. 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=23): 40 x * y * ((A @ B) @ C) * z != x * y * (D @ (F @ G)) * z # answer(A). [ur(13,b,23,a)]. given #48 (F,wt=23): 45 x * (D @ (F @ G)) * (((A @ B) @ C) @ x) != ((A @ B) @ C) * x # answer(A). [para(10(a,1),25(a,1)),flip(a)]. given #49 (T,wt=5): 186 x * c_0 = x. [back_demod(121),demod(168(1),171(2),171(2))]. given #50 (T,wt=7): 189 x @ x * x = c_0. [back_demod(116),demod(168(3))]. 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=19): 210 (D @ (F @ G)) * (((A @ B) @ C) @ c_0) != (A @ B) @ C # answer(A). [para(177(a,1),45(a,1)),demod(186(20))]. given #53 (F,wt=21): 218 (B @ C) * (A @ C) * (D @ (F @ G)) != (A @ C) * (B @ C) # answer(A). [para(22(a,1),28(a,1)),flip(a)]. given #54 (T,wt=7): 192 x * (x @ c_0) = x. [back_demod(184),demod(186(5))]. given #55 (T,wt=8): 180 x * y != x | c_0 = y. [back_demod(136),demod(168(3),171(4),171(4))]. given #56 (A,wt=18): 41 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=23): 46 x * ((A @ B) @ C) * ((D @ (F @ G)) @ x) != (D @ (F @ G)) * x # answer(A). [para(10(a,1),25(a,2))]. given #58 (F,wt=23): 86 C * (A @ B) * (D @ (F @ G)) * (C @ (A @ B)) != C * (A @ B) # answer(A). [para(10(a,1),57(a,2))]. given #59 (T,wt=5): 248 x @ c_0 = c_0. [hyper(180,a,192,a),flip(a)]. given #60 (T,wt=8): 183 x * y != y | c_0 = x. [back_demod(130),demod(168(3),171(4))]. given #61 (A,wt=18): 42 x * y * z != x * u * y | u * (u @ y) = z. [para(10(a,1),13(a,1,2)),flip(a)]. given #62 (F,wt=23): 113 (F @ G) * D * ((A @ B) @ C) * ((F @ G) @ D) != (F @ G) * D # answer(A). [para(10(a,1),60(a,2))]. given #63 (F,wt=25): 58 x * y * C * (A @ B) * (D @ (F @ G)) != x * y * (A @ B) * C # answer(A). [ur(13,b,47,a)]. given #64 (T,wt=10): 108 x * y != y * y | y = x. [para(15(a,1),17(a,1,2))]. given #65 (T,wt=10): 270 x * y != x * z | z = y. [para(177(a,1),42(a,1,2)),demod(186(3),248(5),186(5))]. given #66 (A,wt=14): 43 x * y * z != y * x | y @ x = z. [para(10(a,1),13(a,1)),flip(a)]. given #67 (F,wt=21): 272 B * A * C * (A @ B) * (D @ (F @ G)) != A * B * C # answer(A). [para(19(a,1),58(a,2))]. given #68 (F,wt=25): 61 x * y * (F @ G) * D * ((A @ B) @ C) != x * y * D * (F @ G) # answer(A). [ur(13,b,48,a)]. given #69 (T,wt=12): 178 x * (x @ y) != x * y | c_0 = y. [back_demod(139),demod(168(5),171(6))]. given #70 (T,wt=12): 181 x * y * z != z | x * y = c_0. [back_demod(135),demod(168(4),171(5)),flip(b)]. given #71 (A,wt=18): 51 x * y * z * u != v * u | x * y * z = v. [para(9(a,1),14(a,1,2))]. given #72 (F,wt=21): 284 F * G * D * ((A @ B) @ C) != G * F * D * (F @ G) # answer(A). [para(19(a,1),61(a,1))]. given #73 (F,wt=25): 84 x * C * (A @ B) * (D @ (F @ G)) * y != x * (A @ B) * C * y # answer(A). [ur(7,b,57,a)]. given #74 (T,wt=12): 190 x * y != y | x * (x @ y) = c_0. [back_demod(103),demod(168(3),171(4)),flip(b)]. given #75 (T,wt=12): 191 x * y * z != x * y | c_0 = z. [back_demod(97),demod(168(5),171(6))]. given #76 (A,wt=18): 52 x * y * z != u * v * z | x * y = u * v. [para(9(a,1),14(a,2))]. given #77 (F,wt=25): 85 C * (A @ B) * (D @ (F @ G)) * x * (x @ C) != (A @ B) * x * C # answer(A). [para(10(a,1),57(a,2,2))]. given #78 (F,wt=25): 111 x * (F @ G) * D * ((A @ B) @ C) * y != x * D * (F @ G) * y # answer(A). [ur(7,b,60,a)]. given #79 (T,wt=12): 281 x * y != y * x | y @ x = c_0. [para(186(a,1),43(a,1,2))]. given #80 (T,wt=12): 288 x @ y != x * y | y * x = c_0. [para(10(a,1),181(a,1)),flip(a)]. given #81 (A,wt=18): 53 x * y * (y @ z) != u * y * z | u * z = x. [para(10(a,1),14(a,1,2)),flip(a)]. given #82 (F,wt=25): 112 D * (F @ G) * (((A @ B) @ C) @ D) != (F @ G) * ((A @ B) @ C) * D # answer(A). [para(10(a,1),60(a,1,2)),flip(a)]. given #83 (F,wt=25): 204 (F @ G) * ((A @ B) @ C) * D * (D @ (D @ (F @ G))) != D * (F @ G) # answer(A). [ur(16,b,27,a(flip))]. given #84 (T,wt=10): 329 x * y != z * y | z = x. [para(186(a,1),53(a,2,2)),demod(248(2),186(2),186(5))]. given #85 (T,wt=12): 307 x * y != y * x | x @ y = c_0. [para(10(a,1),191(a,1)),flip(b)]. given #86 (A,wt=14): 54 x * (y @ z) != y * z | z * y = x. [para(10(a,1),14(a,1)),flip(a)]. given #87 (F,wt=25): 225 x * (B @ C) * (A @ C) * (D @ (F @ G)) != x * (A @ C) * (B @ C) # answer(A). [para(22(a,1),39(a,1,2)),flip(a)]. given #88 (F,wt=25): 231 (B @ C) * (A @ C) * (D @ (F @ G)) * x != (A @ C) * (B @ C) * x # answer(A). [ur(14,b,218,a),demod(9(13),9(22))]. given #89 (T,wt=13): 188 (x @ x * y) * (y @ x * y) = c_0. [back_demod(117),demod(168(1),171(3)),flip(a)]. given #90 (T,wt=13): 222 (x @ y) * ((x @ y) @ y) = x @ y. [para(168(a,1),22(a,1,1)),demod(177(6),168(6),186(7))]. given #91 (A,wt=18): 55 x * y * z * (z @ u) != z * u | x * y = u. [para(10(a,1),14(a,2))]. given #92 (F,wt=25): 282 x * B * A * C * (A @ B) * (D @ (F @ G)) != x * A * B * C # answer(A). [ur(270,b,272,a),flip(a)]. given #93 (F,wt=25): 283 B * A * C * (A @ B) * (D @ (F @ G)) * x != A * B * C * x # answer(A). [ur(14,b,272,a),demod(9(15),9(14),9(13),9(22),9(21))]. given #94 (T,wt=7): 351 (x @ y) @ y = c_0. [hyper(180,a,222,a),flip(a)]. given #95 (T,wt=11): 352 (x @ y) * y = y * (x @ y). [para(222(a,1),10(a,1,2)),flip(a)]. given #96 (A,wt=15): 73 (x @ x * y) * (y @ x * y) * z = z. [para(11(a,1),63(a,1,1)),demod(9(6))]. given #97 (F,wt=15): 376 C * ((A @ B) @ C) != (D @ (F @ G)) * C # answer(A). [para(352(a,1),23(a,1))]. given #98 (F,wt=19): 377 ((A @ B) @ C) * (F @ G) != (F @ G) * (D @ (F @ G)) # answer(A). [para(352(a,1),23(a,2))]. given #99 (T,wt=7): 372 x @ (y @ x) = c_0. [hyper(281,a,352,a)]. given #100 (T,wt=9): 421 (x @ y) @ y * x = c_0. [para(73(a,1),22(a,1)),demod(409(8))]. given #101 (A,wt=20): 78 x * y * z != u * x * y | u * (u @ x * y) = z. [para(9(a,1),16(a,1))]. given #102 (F,wt=19): 382 x * C * ((A @ B) @ C) != x * (D @ (F @ G)) * C # answer(A). [para(352(a,1),25(a,1,2))]. given #103 (F,wt=19): 431 C * ((A @ B) @ C) * x != (D @ (F @ G)) * C * x # answer(A). [ur(329,b,376,a),demod(9(8),9(16)),flip(a)]. given #104 (T,wt=9): 440 (x @ y) @ x * y = c_0. [para(10(a,1),421(a,1,2)),demod(11(3),351(3),186(3))]. given #105 (T,wt=11): 429 x * (y @ x) * y = y * x. [back_demod(370),demod(421(3),186(2)),flip(a)]. given #106 (A,wt=22): 79 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 #107 (F,wt=17): 475 C * (D @ (F @ G)) * (A @ B) != (A @ B) * C # answer(A). [para(429(a,1),25(a,1)),flip(a)]. given #108 (F,wt=17): 476 (F @ G) * ((A @ B) @ C) * D != D * (F @ G) # answer(A). [para(429(a,1),25(a,2))]. given #109 (T,wt=11): 435 x @ (y @ x) * (z @ x) = c_0. [para(11(a,1),372(a,1,2))]. given #110 (T,wt=11): 451 (x @ (y @ y * z)) @ x = c_0. [para(73(a,1),421(a,1,2)),demod(11(6),410(5),177(5))]. given #111 (A,wt=18): 80 x * y != z * y | z * (z @ y) = x * (x @ y). [para(10(a,1),16(a,1))]. given #112 (F,wt=17): 499 (D @ (F @ G)) * C * (A @ B) != (A @ B) * C # answer(A). [para(429(a,1),431(a,1)),flip(a)]. given #113 (F,wt=19): 457 C * C * ((A @ B) @ C) != (D @ (F @ G)) * C * C # answer(A). [para(352(a,1),431(a,1,2))]. given #114 (T,wt=11): 471 (x @ y) * x = x * (x @ y). [hyper(16,a,429,a),flip(a)]. given #115 (T,wt=7): 534 (x @ y) @ x = c_0. [hyper(307,a,471,a)]. given #116 (A,wt=22): 81 x * (x @ y) * z != x * y | y * (y @ x * (x @ y)) = z. [para(10(a,1),16(a,2)),demod(9(3))]. given #117 (F,wt=15): 543 ((A @ B) @ C) * D != D * (D @ (F @ G)) # answer(A). [para(471(a,1),23(a,2))]. given #118 (F,wt=19): 542 (A @ B) * ((A @ B) @ C) != (D @ (F @ G)) * (A @ B) # answer(A). [para(471(a,1),23(a,1))]. given #119 (T,wt=7): 535 x @ (x @ y) = c_0. [hyper(281,a,471,a)]. given #120 (T,wt=12): 394 x * (y @ x) != x | y @ x = c_0. [para(352(a,1),183(a,1)),flip(b)]. given #121 (A,wt=22): 106 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 #122 (F,wt=19): 547 x * ((A @ B) @ C) * D != x * D * (D @ (F @ G)) # answer(A). [para(471(a,1),25(a,2,2))]. given #123 (F,wt=19): 590 ((A @ B) @ C) * D * x != D * (D @ (F @ G)) * x # answer(A). [ur(329,b,543,a),demod(9(8),9(16)),flip(a)]. given #124 (T,wt=12): 490 x * (y @ x) != y * x | c_0 = y. [para(429(a,1),43(a,1)),demod(352(3),351(6)),flip(a)]. given #125 (T,wt=12): 491 x * y != x | y * (x @ y) = c_0. [para(429(a,1),181(a,1))]. given #126 (A,wt=22): 107 x * y * (y @ z * (z @ y)) != z * y | z * (z @ y) = x. [para(10(a,1),17(a,2))]. given #127 (F,wt=19): 614 ((A @ B) @ C) * D * D != D * D * (D @ (F @ G)) # answer(A). [para(471(a,1),590(a,2,2))]. given #128 (F,wt=21): 389 (F @ G) * D * C * ((A @ B) @ C) != D * (F @ G) * C # answer(A). [para(352(a,1),60(a,1,2,2))]. given #129 (T,wt=12): 559 x * (x @ y) != x | x @ y = c_0. [para(471(a,1),183(a,1)),flip(b)]. given #130 (T,wt=13): 264 x * (x @ x * y) = x * (x @ y). [hyper(42,a,20,a),flip(a)]. given #131 (A,wt=22): 125 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 #132 (F,wt=21): 390 (F @ G) * D * ((A @ B) @ C) * G != D * G * (F @ G) # answer(A). [para(352(a,1),60(a,2,2))]. given #133 (F,wt=21): 482 x * C * (D @ (F @ G)) * (A @ B) != x * (A @ B) * C # answer(A). [para(429(a,1),40(a,1,2)),flip(a)]. given #134 (T,wt=9): 625 x @ x * y = x @ y. [hyper(270,a,264,a),flip(a)]. given #135 (T,wt=11): 635 (x @ y) @ x * (x @ y) = c_0. [para(264(a,1),188(a,1,1,2)),demod(625(3),535(2),625(3),625(4),177(6))]. given #136 (A,wt=18): 142 x * y * z != y * u | x * (x @ y) * z = u. [para(19(a,1),7(a,1))]. given #137 (F,wt=21): 483 x * (F @ G) * ((A @ B) @ C) * D != x * D * (F @ G) # answer(A). [para(429(a,1),40(a,2,2))]. given #138 (F,wt=21): 504 F * G * D * ((A @ B) @ C) * (D @ G) != F * D * G # answer(A). [ur(79,b,111,a(flip)),demod(19(24)),flip(a)]. given #139 (T,wt=11): 643 x * (y @ x) * (x @ y) = x. [back_demod(577),demod(625(2),362(4))]. given #140 (T,wt=9): 739 (x @ y) * (y @ x) = c_0. [hyper(180,a,643,a),flip(a)]. given #141 (A,wt=18): 143 x * y * (y @ z) * u != y * z * u | z = x. [para(19(a,1),8(a,1)),flip(a)]. given #142 (F,wt=13): 772 (D @ (F @ G)) * (C @ (A @ B)) != c_0 # answer(A). [para(739(a,1),23(a,1)),flip(a)]. given #143 (F,wt=13): 773 ((A @ B) @ C) * ((F @ G) @ D) != c_0 # answer(A). [para(739(a,1),23(a,2))]. given #144 (T,wt=9): 813 (x @ y) @ (y @ x) = c_0. [para(739(a,1),281(a,1)),demod(739(4)),xx(a)]. given #145 (T,wt=10): 796 x @ y != c_0 | y @ x = c_0. [para(739(a,1),180(a,1)),flip(a),flip(b)]. given #146 (A,wt=18): 144 x * y * (y @ z) * u != y * z * u | x = z. [para(19(a,1),8(a,2))]. given #147 (F,wt=13): 774 (C @ (A @ B)) * (D @ (F @ G)) != c_0 # answer(A). [para(739(a,1),24(a,1)),flip(a)]. given #148 (F,wt=13): 775 ((F @ G) @ D) * ((A @ B) @ C) != c_0 # answer(A). [para(739(a,1),24(a,2))]. given #149 (T,wt=11): 658 (x @ y * x) @ (y @ x) = c_0. [back_demod(410),demod(625(4))]. given #150 (T,wt=11): 659 (x @ y * x) * (y @ x) = c_0. [back_demod(409),demod(625(4))]. given #151 (A,wt=21): 145 x * y * z * (z @ x * y) * u = z * x * y * u. [para(19(a,1),9(a,1)),demod(9(2)),flip(a)]. given #152 (F,wt=15): 762 (D @ (F @ G)) * C * (C @ (A @ B)) != C # answer(A). [para(643(a,1),431(a,1)),flip(a)]. given #153 (F,wt=15): 777 x * (D @ (F @ G)) * (C @ (A @ B)) != x # answer(A). [para(739(a,1),25(a,1,2)),demod(186(2)),flip(a)]. given #154 (T,wt=11): 679 (x @ y) * (y @ x * y) = c_0. [back_demod(188),demod(625(2))]. given #155 (T,wt=11): 707 (x @ y) @ y * (x @ y) = c_0. [para(351(a,1),625(a,2)),demod(352(3))]. given #156 (A,wt=23): 146 x * y * z * (y @ x) * (z @ x) * u = y * z * x * u. [para(9(a,1),19(a,1,2)),demod(11(2),9(4),9(10))]. given #157 (F,wt=15): 778 x * ((A @ B) @ C) * ((F @ G) @ D) != x # answer(A). [para(739(a,1),25(a,2,2)),demod(186(14))]. given #158 (F,wt=15): 779 x * (C @ (A @ B)) * (D @ (F @ G)) != x # answer(A). [para(739(a,1),28(a,1,2)),demod(186(2)),flip(a)]. given #159 (T,wt=11): 708 (x @ y) @ x * y * x = c_0. [para(625(a,1),421(a,1,1)),demod(9(3))]. given #160 (T,wt=11): 709 (x @ y) @ x * x * y = c_0. [para(625(a,1),440(a,1,1))]. given #161 (A,wt=21): 147 x * y * z * (z @ (x @ y)) = y * x * z * (x @ y). [para(10(a,1),19(a,1,2,2)),flip(a)]. given #162 (F,wt=15): 780 x * ((F @ G) @ D) * ((A @ B) @ C) != x # answer(A). [para(739(a,1),28(a,2,2)),demod(186(14))]. given #163 (F,wt=15): 821 ((A @ B) @ C) * D * ((F @ G) @ D) != D # answer(A). [para(739(a,1),590(a,2,2)),demod(186(16))]. given #164 (T,wt=11): 768 (x @ y) * (y @ x) * z = z. [para(739(a,1),9(a,1,1)),demod(177(2)),flip(a)]. given #165 (T,wt=9): 1085 x @ y * x = x @ y. [para(679(a,1),768(a,1,2)),demod(186(3)),flip(a)]. given #166 (A,wt=22): 151 x * y * z * u != x * z * v | y * (y @ z) * u = v. [para(19(a,1),13(a,1,2))]. given #167 (F,wt=11): 1129 D @ (G @ F) != C @ (A @ B) # answer(A). [back_demod(1084),demod(1121(5))]. given #168 (F,wt=11): 1246 D @ (F @ G) != C @ (B @ A) # answer(A). [back_demod(12),demod(1121(5)),flip(a)]. given #169 (T,wt=11): 900 x @ (x @ y) * (x @ y) = c_0. [para(635(a,1),659(a,1,2)),demod(539(6),11(7),625(5),718(10),186(6),186(6))]. given #170 (T,wt=11): 1101 x @ y * (y @ x) = x @ y. [back_demod(699),demod(1085(5))]. given #171 (A,wt=18): 152 x * y * z != y * x * u | (x @ y) * z = u. [para(19(a,1),13(a,1))]. given #172 (F,wt=13): 1175 (D @ (G @ F)) * (C @ (B @ A)) != c_0 # answer(A). [back_demod(775),demod(1121(5),1121(10))]. given #173 (F,wt=13): 1176 (C @ (B @ A)) * (D @ (G @ F)) != c_0 # answer(A). [back_demod(773),demod(1121(5),1121(10))]. given #174 (T,wt=11): 1121 (x @ y) @ z = z @ (y @ x). [para(768(a,1),1085(a,1,2)),demod(11(3),168(3),186(4),11(6),813(5),177(6))]. given #175 (T,wt=11): 1126 (x @ y) @ (x @ y * y) = c_0. [back_demod(873),demod(1104(3),1121(4,R))]. given #176 (A,wt=18): 153 x * y * z != y * x * u | (y @ x) * u = z. [para(19(a,1),13(a,2)),flip(b)]. given #177 (F,wt=15): 836 (D @ (F @ G)) * (C @ (A @ B)) * x != x # answer(A). [ur(329,b,772,a),demod(177(2),9(12)),flip(a)]. given #178 (F,wt=15): 855 (C @ (A @ B)) * (D @ (F @ G)) * x != x # answer(A). [ur(329,b,774,a),demod(177(2),9(12)),flip(a)]. given #179 (T,wt=11): 1315 (x @ y) @ ((y @ x) @ z) = c_0. [para(1121(a,2),372(a,1,2))]. given #180 (T,wt=11): 1322 (x @ y) @ (z @ (y @ x)) = c_0. [para(1121(a,1),535(a,1,2))]. given #181 (A,wt=22): 154 x * y * (y @ z) * u != v * y * z * u | v * z = x. [para(19(a,1),14(a,1,2)),flip(a)]. given #182 (F,wt=15): 1073 (C @ (A @ B)) * D * (D @ (F @ G)) != D # answer(A). [para(768(a,1),547(a,1)),flip(a)]. given #183 (F,wt=15): 1131 (D @ (G @ F)) * C * (C @ (B @ A)) != C # answer(A). [back_demod(1070),demod(1121(5),1121(11))]. given #184 (T,wt=12): 766 (x @ y) * z != c_0 | y @ x = z. [para(739(a,1),7(a,1)),flip(a)]. given #185 (T,wt=12): 767 x * (y @ z) != c_0 | z @ y = x. [para(739(a,1),8(a,1)),flip(a)]. given #186 (A,wt=18): 155 x * (y @ z) * u != y * z * u | z * y = x. [para(19(a,1),14(a,1)),flip(a)]. given #187 (F,wt=15): 1158 (D @ (G @ F)) * (C @ (B @ A)) * x != x # answer(A). [back_demod(859),demod(1121(5),1121(10))]. given #188 (F,wt=15): 1163 (C @ (B @ A)) * (D @ (G @ F)) * x != x # answer(A). [back_demod(840),demod(1121(5),1121(10))]. given #189 (T,wt=12): 804 x @ y != z | z * (y @ x) = c_0. [para(739(a,1),181(a,1,2)),demod(186(2)),flip(a)]. given #190 (T,wt=12): 809 x * (y @ z) != x | z @ y = c_0. [para(739(a,1),191(a,1,2)),demod(186(2)),flip(a),flip(b)]. given #191 (A,wt=22): 156 x * y * z * (z @ u) * v != z * u * v | x * y = u. [para(19(a,1),14(a,2))]. given #192 (F,wt=15): 1164 (C @ (B @ A)) * D * (D @ (G @ F)) != D # answer(A). [back_demod(821),demod(1121(5),1121(11))]. given #193 (F,wt=15): 1173 x * (D @ (G @ F)) * (C @ (B @ A)) != x # answer(A). [back_demod(780),demod(1121(5),1121(10))]. given #194 (T,wt=12): 814 x * y != c_0 | y @ x = y * x. [para(739(a,1),54(a,1)),flip(a),flip(b)]. given #195 (T,wt=12): 1034 x @ y != z | (y @ x) * z = c_0. [para(768(a,1),180(a,1)),flip(a),flip(b)]. given #196 (A,wt=22): 158 x * y * z != u * y | u * (u @ y) = x * (x @ y) * z. [para(19(a,1),16(a,1))]. given #197 (F,wt=15): 1174 x * (C @ (B @ A)) * (D @ (G @ F)) != x # answer(A). [back_demod(778),demod(1121(5),1121(10))]. given #198 (F,wt=15): 1199 D * (D @ (F @ G)) != (C @ (B @ A)) * D # answer(A). [back_demod(543),demod(1121(5)),flip(a)]. given #199 (T,wt=12): 1036 (x @ y) * z != z | y @ x = c_0. [para(768(a,1),183(a,1)),flip(a),flip(b)]. given #200 (T,wt=12): 1403 c_0 != x | (y @ z) * x = y @ z. [para(768(a,1),766(a,1)),flip(a),flip(b)]. given #201 (A,wt=25): 161 x * y * z * (z @ (x @ y)) * u = y * x * z * (x @ y) * u. [para(19(a,1),19(a,1,2,2)),flip(a)]. given #202 (F,wt=15): 1224 (D @ (F @ G)) * C != C * (C @ (B @ A)) # answer(A). [back_demod(376),demod(1121(6)),flip(a)]. given #203 (F,wt=15): 1244 x * (D @ (F @ G)) != x * (C @ (B @ A)) # answer(A). [back_demod(24),demod(1121(5)),flip(a)]. given #204 (T,wt=12): 1464 (x @ y) * z != z | x @ y = c_0. [para(768(a,1),1036(a,1)),flip(a)]. given #205 (T,wt=13): 274 (x @ y) @ (z @ y) = (x @ z) @ y. [hyper(43,a,22,a)]. ============================== PROOF ================================= % Proof 1 at 0.35 (+ 0.00) seconds: A. % Length of proof is 73. % Level of proof is 24. % Maximum clause weight is 23. % Given clauses 205. 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 != D @ (F @ G) # answer(A). [input]. 13 x * y * z != x * y * u | z = u. [para(9(a,1),7(a,1)),demod(9(4))]. 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)]. 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) * x != (D @ (F @ G)) * x # answer(A). [ur(8,b,12,a)]. 25 x * ((A @ B) @ C) * y != x * (D @ (F @ G)) * y # answer(A). [ur(7,b,23,a)]. 29 x * y != x | x @ x = y. [para(15(a,1),7(a,1)),flip(a)]. 32 x * (x @ x) * y = x * y. [para(15(a,1),9(a,1,1)),flip(a)]. 42 x * y * z != x * u * y | u * (u @ y) = z. [para(10(a,1),13(a,1,2)),flip(a)]. 43 x * y * z != y * x | y @ x = z. [para(10(a,1),13(a,1)),flip(a)]. 45 x * (D @ (F @ G)) * (((A @ B) @ C) @ x) != ((A @ B) @ C) * x # answer(A). [para(10(a,1),25(a,1)),flip(a)]. 63 (x @ x) * y = y. [hyper(13,a,32,a)]. 69 x * y != y | z @ z = x. [para(63(a,1),8(a,1)),flip(a)]. 70 x * ((y @ y) @ x) = x. [para(63(a,1),10(a,1,2)),demod(63(5))]. 73 (x @ x * y) * (y @ x * y) * z = z. [para(11(a,1),63(a,1,1)),demod(9(6))]. 78 x * y * z != u * x * y | u * (u @ x * y) = z. [para(9(a,1),16(a,1))]. 88 (x @ x) @ y = y @ y. [hyper(29,a,70,a),flip(a)]. 117 (x @ x) @ y * z = (y @ y * z) * (z @ y * z). [para(88(a,2),11(a,1))]. 120 ((x @ x) @ y) * z = z. [para(88(a,2),63(a,1,1))]. 121 x * (((y @ y) @ z) @ x) = x. [para(88(a,2),70(a,1,2,1))]. 129 x * (x @ ((y @ y) @ z)) = x * ((y @ y) @ z). [hyper(16,a,120,a)]. 136 x * y != x | ((z @ z) @ u) @ x = y. [para(120(a,1),16(a,2)),demod(120(8))]. 140 (((x @ x) @ y) @ z) * u = u. [para(88(a,2),120(a,1,1,1))]. 164 (x @ x) @ y = z @ z. [hyper(69,a,120,a),flip(a)]. 165 x @ x = y @ y. [hyper(69,a,63,a)]. 168 x @ x = c_0. [new_symbol(165)]. 171 c_0 @ x = c_0. [back_demod(164),demod(168(1),168(3))]. 177 c_0 * x = x. [back_demod(140),demod(168(1),171(2),171(2))]. 180 x * y != x | c_0 = y. [back_demod(136),demod(168(3),171(4),171(4))]. 184 x * (x @ c_0) = x * c_0. [back_demod(129),demod(168(1),171(2),168(4),171(5))]. 186 x * c_0 = x. [back_demod(121),demod(168(1),171(2),171(2))]. 188 (x @ x * y) * (y @ x * y) = c_0. [back_demod(117),demod(168(1),171(3)),flip(a)]. 192 x * (x @ c_0) = x. [back_demod(184),demod(186(5))]. 203 x * y * ((x @ y) @ y * x) = (x @ y) * y * x. [para(20(a,1),19(a,1)),flip(a)]. 222 (x @ y) * ((x @ y) @ y) = x @ y. [para(168(a,1),22(a,1,1)),demod(177(6),168(6),186(7))]. 248 x @ c_0 = c_0. [hyper(180,a,192,a),flip(a)]. 264 x * (x @ x * y) = x * (x @ y). [hyper(42,a,20,a),flip(a)]. 270 x * y != x * z | z = y. [para(177(a,1),42(a,1,2)),demod(186(3),248(5),186(5))]. 274 (x @ y) @ (z @ y) = (x @ z) @ y. [hyper(43,a,22,a)]. 281 x * y != y * x | y @ x = c_0. [para(186(a,1),43(a,1,2))]. 351 (x @ y) @ y = c_0. [hyper(180,a,222,a),flip(a)]. 352 (x @ y) * y = y * (x @ y). [para(222(a,1),10(a,1,2)),flip(a)]. 362 (x @ y) * y * z = y * (x @ y) * z. [para(351(a,1),19(a,1,2,2,1)),demod(177(3)),flip(a)]. 370 x * y * ((x @ y) @ y * x) = y * (x @ y) * x. [back_demod(203),demod(362(8))]. 372 x @ (y @ x) = c_0. [hyper(281,a,352,a)]. 409 (x @ y * x) * (y @ y * x) = c_0. [hyper(180,a,73,a),flip(a)]. 421 (x @ y) @ y * x = c_0. [para(73(a,1),22(a,1)),demod(409(8))]. 429 x * (y @ x) * y = y * x. [back_demod(370),demod(421(3),186(2)),flip(a)]. 453 x * (x @ y * x) = (x @ y) * x. [hyper(78,a,19,a)]. 471 (x @ y) * x = x * (x @ y). [hyper(16,a,429,a),flip(a)]. 500 x * (x @ y * x) = x * (x @ y). [back_demod(453),demod(471(5))]. 577 (x @ x * y) * y * (y @ x) = y. [para(471(a,1),73(a,1,2)),demod(500(5))]. 625 x @ x * y = x @ y. [hyper(270,a,264,a),flip(a)]. 643 x * (y @ x) * (x @ y) = x. [back_demod(577),demod(625(2),362(4))]. 679 (x @ y) * (y @ x * y) = c_0. [back_demod(188),demod(625(2))]. 739 (x @ y) * (y @ x) = c_0. [hyper(180,a,643,a),flip(a)]. 768 (x @ y) * (y @ x) * z = z. [para(739(a,1),9(a,1,1)),demod(177(2)),flip(a)]. 813 (x @ y) @ (y @ x) = c_0. [para(739(a,1),281(a,1)),demod(739(4)),xx(a)]. 1085 x @ y * x = x @ y. [para(679(a,1),768(a,1,2)),demod(186(3)),flip(a)]. 1121 (x @ y) @ z = z @ (y @ x). [para(768(a,1),1085(a,1,2)),demod(11(3),168(3),186(4),11(6),813(5),177(6))]. 1237 x * (D @ (F @ G)) * ((C @ (B @ A)) @ x) != (C @ (B @ A)) * x # answer(A). [back_demod(45),demod(1121(10),1121(18))]. 1505 (x @ y) @ (z @ y) = c_0. [para(372(a,1),274(a,1,2)),demod(248(4)),flip(a)]. 1519 x @ (y @ z) = c_0. [para(274(a,2),739(a,1,1)),demod(1505(3),177(4))]. 1558 $F # answer(A). [back_demod(1237),demod(1519(5),1519(6),171(3),186(3),186(2),1519(5),177(2)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=205. Generated=12211. Kept=1551. proofs=1. Usable=117. Sos=647. Demods=121. Denials=0. 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=236564. 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.16. User_CPU=0.35, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13118 exit (max_proofs) Mon Jun 19 16:41:29 2006