============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13127 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:40 2006 The command was "/home/mccune/bin/prover9 -f cs.in ED.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 ED.in clauses(sos). x * y * z * y * x = y * x * z * x * y. end_of_list. clauses(sos). (A @ C) * (B @ C) != A * B @ C # answer(D). 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 = y * x * z * x * y. [input]. 6 (A @ C) * (B @ C) != A * B @ C # answer(D). [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 * y * x = y * x * z * x * y. [input]. 12 A * B @ C != (A @ C) * (B @ C) # answer(D). [copy(6),flip(a)]. end_of_list. clauses(demodulators). 9 (x * y) * z = x * y * z. [input]. 10 x * y * (y @ x) = y * x. [input]. 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=19): 11 x * y * z * y * x = y * x * z * x * y. [input]. given #6 (I,wt=13): 12 A * B @ C != (A @ C) * (B @ C) # answer(D). [copy(6),flip(a)]. given #7 (F,wt=17): 29 (A * B @ C) * x != (A @ C) * (B @ C) * x # answer(D). [ur(8,b,12,a),demod(9(14))]. given #8 (F,wt=17): 30 x * (A * B @ C) != x * (A @ C) * (B @ C) # answer(D). [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): 36 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=21): 31 x * (A * B @ C) * y != x * (A @ C) * (B @ C) * y # answer(D). [ur(7,b,29,a)]. given #13 (F,wt=21): 34 (A * B @ C) * ((B @ C) @ (A @ C)) != (B @ C) * (A @ C) # answer(D). [para(10(a,1),29(a,2))]. given #14 (T,wt=10): 37 x * (y @ y) != y | y = x. [para(15(a,1),8(a,1)),flip(a)]. given #15 (T,wt=10): 38 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=21): 35 x * y * (A * B @ C) != x * y * (A @ C) * (B @ C) # answer(D). [ur(7,b,30,a)]. given #18 (F,wt=19): 66 C * A * B * (A @ C) * (B @ C) != A * B * C # answer(D). [para(10(a,1),35(a,1)),demod(9(5),9(17)),flip(a)]. given #19 (T,wt=11): 39 x * (x @ x) * y = x * y. [para(15(a,1),9(a,1,1)),flip(a)]. given #20 (T,wt=7): 69 (x @ x) * y = y. [hyper(13,a,39,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): 43 (A * B @ C) * ((B @ C) @ (B @ C)) != (A @ C) * (B @ C) # answer(D). [para(15(a,1),29(a,2,2))]. given #23 (F,wt=23): 33 (A * B @ C) * x * (x @ (B @ C)) != (A @ C) * x * (B @ C) # answer(D). [para(10(a,1),29(a,2,2))]. given #24 (T,wt=6): 90 x != y | y = x. [para(15(a,1),16(a,2)),demod(69(2),79(4),15(3))]. given #25 (T,wt=9): 78 x * ((y @ y) @ x) = x. [para(69(a,1),10(a,1,2)),demod(69(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): 92 (A * B @ C) * ((x @ x) @ (B @ C)) != (A @ C) * (B @ C) # answer(D). [para(69(a,1),33(a,1,2)),demod(69(19))]. given #28 (F,wt=23): 67 C * A * B * (A @ C) * (B @ C) * x != A * B * C * x # answer(D). [ur(14,b,66,a),demod(9(13),9(12),9(11),9(20),9(19))]. given #29 (T,wt=9): 84 x * (x @ x * x) = x. [hyper(16,a,9,a)]. given #30 (T,wt=9): 93 (x @ x) @ y = y @ y. [hyper(36,a,78,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=23): 68 x * C * A * B * (A @ C) * (B @ C) != x * A * B * C # answer(D). [ur(7,b,66,a)]. given #33 (F,wt=23): 99 (A @ C) * (B @ C) * ((x @ x) @ (A * B @ C)) != A * B @ C # answer(D). [para(78(a,1),29(a,1)),flip(a)]. given #34 (T,wt=9): 117 x @ x * x = x @ x. [hyper(36,a,84,a),flip(a)]. given #35 (T,wt=9): 119 ((x @ x) @ y) * z = z. [para(93(a,2),69(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=17): 157 C * A * (A * B @ C) != A * C * (B @ C) # answer(D). [para(19(a,1),35(a,2))]. given #38 (F,wt=21): 164 C * A * (A * B @ C) * x != A * C * (B @ C) * x # answer(D). [ur(14,b,157,a),demod(9(9),9(18),9(17))]. given #39 (T,wt=10): 77 x * y != y | z @ z = x. [para(69(a,1),8(a,1)),flip(a)]. NOTE: New constant: 0 x @ x = c_0. [new_symbol(175)]. NOTE: New Function symbol precedence: lex([ A, B, C, c_0, *, @ ]). given #40 (T,wt=5): 179 x @ x = c_0. [new_symbol(175)]. 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=21): 166 x * C * A * (A * B @ C) != x * A * C * (B @ C) # answer(D). [ur(7,b,157,a)]. given #43 (F,wt=23): 113 C * A * B * (A @ C) * (B @ C) * (C @ B) != A * C * B # answer(D). [para(10(a,1),67(a,2,2))]. given #44 (T,wt=5): 183 c_0 @ x = c_0. [back_demod(174),demod(179(1),179(3))]. given #45 (T,wt=5): 189 c_0 * x = x. [back_demod(139),demod(179(1),183(2),183(2))]. given #46 (A,wt=17): 21 x * y * z * (y * z @ x) = y * z * x. [para(9(a,1),10(a,1,2)),demod(9(7))]. given #47 (F,wt=23): 114 A * B * C * (A @ C) * B != A * B * C * B * (A @ C) # answer(D). [para(11(a,1),67(a,1,2,2)),demod(19(19),19(14)),flip(a)]. given #48 (F,wt=23): 169 C * A * (A * B @ C) * ((B @ C) @ C) != A * (B @ C) * C # answer(D). [para(10(a,1),164(a,2,2))]. given #49 (T,wt=5): 199 x * c_0 = x. [back_demod(120),demod(179(1),183(2),183(2))]. given #50 (T,wt=7): 200 x @ x * x = c_0. [back_demod(117),demod(179(3))]. given #51 (A,wt=22): 22 x * y * z * y * x != y * u | x * z * x * y = u. [para(11(a,1),7(a,1))]. given #52 (F,wt=25): 32 (A @ C) * (B @ C) * x * (x @ (A * B @ C)) != x * (A * B @ C) # answer(D). [para(10(a,1),29(a,1)),flip(a)]. given #53 (F,wt=25): 47 x * y * z * (A * B @ C) != x * y * z * (A @ C) * (B @ C) # answer(D). [ur(13,b,30,a)]. given #54 (T,wt=7): 204 x * (x @ c_0) = x. [back_demod(196),demod(199(5))]. given #55 (T,wt=8): 192 x * y != x | c_0 = y. [back_demod(135),demod(179(3),183(4),183(4))]. given #56 (A,wt=22): 23 x * y * z * y * u != y * u * z * u * y | u = x. [para(11(a,1),8(a,1)),flip(a)]. given #57 (F,wt=25): 48 x * y * (A * B @ C) * z != x * y * (A @ C) * (B @ C) * z # answer(D). [ur(13,b,29,a)]. given #58 (F,wt=25): 54 x * (A @ C) * (B @ C) * ((A * B @ C) @ x) != (A * B @ C) * x # answer(D). [para(10(a,1),31(a,1)),flip(a)]. given #59 (T,wt=5): 257 x @ c_0 = c_0. [hyper(192,a,204,a),flip(a)]. given #60 (T,wt=8): 195 x * y != y | c_0 = x. [back_demod(130),demod(179(3),183(4))]. given #61 (A,wt=22): 24 x * y * z * y * u != y * u * z * u * y | x = u. [para(11(a,1),8(a,2))]. given #62 (F,wt=25): 55 x * (A * B @ C) * ((B @ C) @ (A @ C)) != x * (B @ C) * (A @ C) # answer(D). [para(10(a,1),31(a,2,2))]. given #63 (F,wt=25): 57 (A * B @ C) * ((B @ C) @ (A @ C)) * x != (B @ C) * (A @ C) * x # answer(D). [ur(8,b,34,a),demod(9(14),9(22))]. given #64 (T,wt=9): 219 x * (x * x @ x) = x. [hyper(13,a,21,a)]. given #65 (T,wt=7): 269 x * x @ x = c_0. [hyper(192,a,219,a),flip(a)]. given #66 (A,wt=23): 25 x * y * z * y * x * u = y * x * z * x * y * u. [para(11(a,1),9(a,1,1)),demod(9(5),9(4),9(3),9(2),9(9),9(8),9(7))]. given #67 (F,wt=25): 165 x * y * C * A * (A * B @ C) != x * y * A * C * (B @ C) # answer(D). [ur(13,b,157,a)]. given #68 (F,wt=25): 167 x * C * A * (A * B @ C) * y != x * A * C * (B @ C) * y # answer(D). [ur(7,b,164,a)]. given #69 (T,wt=10): 109 x * y != y * y | y = x. [para(15(a,1),17(a,1,2))]. given #70 (T,wt=12): 190 x * (x @ y) != x * y | c_0 = y. [back_demod(138),demod(179(5),183(6))]. given #71 (A,wt=23): 26 x * y * z * u * z * y = x * z * y * u * y * z. [para(11(a,1),9(a,2,2)),demod(9(5))]. given #72 (F,wt=25): 168 A * C * (B @ C) * ((A * B @ C) @ A) != C * (A * B @ C) * A # answer(D). [para(10(a,1),164(a,1,2)),flip(a)]. given #73 (F,wt=25): 170 A * C * (A * B @ C) * C * A != A * C * (B @ C) * A * C # answer(D). [para(11(a,1),164(a,1))]. given #74 (T,wt=12): 193 x * y * z != z | x * y = c_0. [back_demod(134),demod(179(4),183(5)),flip(b)]. given #75 (T,wt=12): 201 x * y != y | x * (x @ y) = c_0. [back_demod(105),demod(179(3),183(4)),flip(b)]. given #76 (A,wt=23): 27 x * y * z * u * y * x = y * x * z * u * x * y. [para(9(a,1),11(a,1,2,2)),demod(9(8))]. given #77 (F,wt=25): 171 C * A * (A * B @ C) * C * A != C * A * (B @ C) * A * C # answer(D). [para(11(a,1),164(a,2))]. given #78 (F,wt=25): 215 C * A * B * (A @ C) * (B @ C) * (C @ A * B) != C * A * B # answer(D). [para(20(a,1),67(a,2))]. given #79 (T,wt=12): 202 x * y * z != x * y | c_0 = z. [back_demod(100),demod(179(5),183(6))]. given #80 (T,wt=12): 286 x @ y != x * y | y * x = c_0. [para(10(a,1),193(a,1)),flip(a)]. given #81 (A,wt=23): 28 x * (x @ y) * y * (x @ y) * x = (x @ y) * x * x * y. [para(10(a,1),11(a,1,2,2)),flip(a)]. given #82 (F,wt=25): 218 C * A * (A * B @ C) * ((B @ C) @ A * C) != (B @ C) * A * C # answer(D). [para(20(a,1),164(a,2))]. given #83 (F,wt=25): 227 A * B * C * ((A @ C) * (B @ C) @ B) != A * C * (B @ C) * B # answer(D). [para(21(a,1),67(a,1,2,2)),demod(19(13)),flip(a)]. given #84 (T,wt=12): 304 x * y != y * x | x @ y = c_0. [para(10(a,1),202(a,1)),flip(b)]. given #85 (T,wt=13): 85 x * y * (x * y @ x) = y * x. [hyper(16,a,9,a(flip)),demod(9(4))]. given #86 (A,wt=18): 49 x * y * z * u != x * y * z * v | u = v. [para(9(a,1),13(a,1,2)),demod(9(5))]. given #87 (F,wt=25): 228 C * A * B * (A @ C) * (B @ C) * (B * C @ A) != B * C * A # answer(D). [para(21(a,1),67(a,2))]. given #88 (F,wt=25): 231 C * A * (A * B @ C) * (C * (B @ C) @ A) != C * (B @ C) * A # answer(D). [para(21(a,1),164(a,2))]. given #89 (T,wt=13): 197 x * y @ x * y * x * y = c_0. [back_demod(127),demod(179(8))]. given #90 (T,wt=13): 205 x * y * (y @ y * x) = y * x. [hyper(7,a,20,a)]. given #91 (A,wt=18): 50 x * y * z != x * u * y | u * (u @ y) = z. [para(10(a,1),13(a,1,2)),flip(a)]. given #92 (F,wt=25): 330 (A * B @ C) * ((A @ C) * (B @ C) @ (A @ C)) != (B @ C) * (A @ C) # answer(D). [para(85(a,1),29(a,2))]. given #93 (F,wt=25): 333 C * A * B * (A @ C) * (B @ C) * (B * C @ B) != A * C * B # answer(D). [para(85(a,1),67(a,2,2))]. given #94 (T,wt=10): 376 x * y != x * z | z = y. [para(189(a,1),50(a,1,2)),demod(199(3),257(5),199(5))]. given #95 (T,wt=13): 271 x * y * x * y @ x * y = c_0. [para(9(a,1),269(a,1,1))]. given #96 (A,wt=14): 51 x * y * z != y * x | y @ x = z. [para(10(a,1),13(a,1)),flip(a)]. given #97 (F,wt=25): 336 C * A * (A * B @ C) * (C * (B @ C) @ C) != A * (B @ C) * C # answer(D). [para(85(a,1),164(a,2,2))]. given #98 (F,wt=25): 358 (A * B @ C) * ((B @ C) @ (B @ C) * (A @ C)) != (B @ C) * (A @ C) # answer(D). [para(205(a,1),29(a,2))]. given #99 (T,wt=12): 388 x * y != y * x | y @ x = c_0. [para(199(a,1),51(a,1,2))]. given #100 (T,wt=13): 326 x * (y * x @ y) = x * (x @ y). [hyper(16,a,85,a),flip(a)]. given #101 (A,wt=22): 52 x * y * z * y * x != y * x * u | z * x * y = u. [para(11(a,1),13(a,1))]. given #102 (F,wt=25): 361 C * A * B * (A @ C) * (B @ C) * (C @ C * B) != A * C * B # answer(D). [para(205(a,1),67(a,2,2))]. given #103 (F,wt=9): 389 x * y @ x = y @ x. [hyper(376,a,326,a),flip(a)]. given #104 (T,wt=11): 400 (x @ y) * y * x = x * y. [hyper(52,a,19,a)]. given #105 (T,wt=9): 462 (x @ y) @ y * x = c_0. [para(400(a,1),304(a,1)),demod(9(4),10(4)),xx(a)]. given #106 (A,wt=18): 59 x * y * z * u != v * u | x * y * z = v. [para(9(a,1),14(a,1,2))]. given #107 (F,wt=17): 424 (A * B @ C) * C * B != (A @ C) * B * C # answer(D). [para(400(a,1),29(a,2,2))]. given #108 (F,wt=19): 423 (A @ C) * (B @ C) * C * A * B != A * B * C # answer(D). [para(400(a,1),29(a,1)),demod(9(5)),flip(a)]. given #109 (T,wt=9): 463 y * x @ (x @ y) = c_0. [para(400(a,1),304(a,2)),demod(9(3),10(3)),xx(a)]. given #110 (T,wt=9): 474 x * y @ (x @ y) = c_0. [para(400(a,1),389(a,1,1)),demod(463(6))]. given #111 (A,wt=18): 60 x * y * z != u * v * z | x * y = u * v. [para(9(a,1),14(a,2))]. given #112 (F,wt=21): 425 ((B @ C) @ (A @ C)) * (A * B @ C) != (B @ C) * (A @ C) # answer(D). [para(400(a,1),30(a,2))]. given #113 (F,wt=21): 431 x * (A * B @ C) * C * B != x * (A @ C) * B * C # answer(D). [para(400(a,1),31(a,2,2,2))]. given #114 (T,wt=9): 483 x * y @ y * x = c_0. [para(462(a,1),389(a,2)),demod(9(3),10(3))]. given #115 (T,wt=11): 476 (x * y @ y) @ x * y = c_0. [para(10(a,1),462(a,1,2)),demod(405(3))]. given #116 (A,wt=18): 61 x * y * (y @ z) != u * y * z | u * z = x. [para(10(a,1),14(a,1,2)),flip(a)]. given #117 (F,wt=21): 446 C * A * (A * B @ C) * C * B != A * C * B * C # answer(D). [para(400(a,1),164(a,2,2,2))]. given #118 (F,wt=21): 500 (A * B @ C) * C * B * x != (A @ C) * B * C * x # answer(D). [ur(59,b,424,a),demod(9(18),9(17))]. given #119 (T,wt=10): 577 x * y != z * y | z = x. [para(199(a,1),61(a,2,2)),demod(257(2),199(2),199(5))]. given #120 (T,wt=11): 484 (x @ y) @ y * y * x = c_0. [para(389(a,1),462(a,1,1))]. given #121 (A,wt=14): 62 x * (y @ z) != y * z | z * y = x. [para(10(a,1),14(a,1)),flip(a)]. given #122 (F,wt=21): 517 (A * B @ C) * B * C != (A @ C) * B * C * (B @ C) # answer(D). [para(474(a,1),33(a,1,2,2)),demod(199(10),9(19))]. given #123 (F,wt=21): 587 (A * B @ C) * C * B * (C @ B) != (A @ C) * C * B # answer(D). [para(10(a,1),500(a,2,2))]. given #124 (T,wt=11): 505 x * y @ (x * y @ y) = c_0. [para(10(a,1),463(a,1,1)),demod(405(4))]. given #125 (T,wt=11): 512 x * x * y @ (y @ x) = c_0. [para(389(a,1),463(a,1,2))]. given #126 (A,wt=18): 63 x * y * z * (z @ u) != z * u | x * y = u. [para(10(a,1),14(a,2))]. given #127 (F,wt=21): 616 (A * B @ C) * C * C * B != (A @ C) * C * B * C # answer(D). [para(512(a,1),33(a,1,2,2)),demod(199(12),9(23),9(22),10(22))]. given #128 (F,wt=23): 429 x * (A @ C) * (B @ C) * C * A * B != x * A * B * C # answer(D). [para(400(a,1),31(a,1,2)),demod(9(5)),flip(a)]. given #129 (T,wt=11): 530 x * y * x @ (y @ x) = c_0. [para(389(a,1),474(a,1,2)),demod(9(2))]. given #130 (T,wt=11): 644 x * y * y @ (x @ y) = c_0. [para(530(a,1),389(a,2)),demod(420(4))]. given #131 (A,wt=22): 64 x * y * z * y * x != u * z * x * y | y * x = u. [para(11(a,1),14(a,1))]. given #132 (F,wt=23): 441 C * A * B * (A @ C) * B * C != A * B * C * C * B # answer(D). [para(400(a,1),67(a,1,2,2,2,2))]. given #133 (F,wt=23): 445 A * C * (B @ C) * C * A * B != C * A * A * B * C # answer(D). [para(400(a,1),164(a,1,2,2)),demod(9(7)),flip(a)]. given #134 (T,wt=12): 396 x * (x @ y) != x | x @ y = c_0. [para(326(a,1),192(a,1)),demod(389(6)),flip(b)]. given #135 (T,wt=12): 455 x * y != x | (x @ y) * y = c_0. [para(400(a,1),193(a,1))]. given #136 (A,wt=15): 73 x * y * y * x = y * x * x * y. [para(39(a,1),11(a,1,2)),demod(69(6))]. given #137 (F,wt=23): 503 (A @ C) * (B @ C) * C * A * B * x != A * B * C * x # answer(D). [ur(59,b,423,a),demod(9(12),9(11),9(20),9(19))]. given #138 (F,wt=19): 716 A * B * C * (B @ A) != (A @ C) * B * C * A # answer(D). [para(10(a,1),503(a,1,2,2,2)),demod(420(12)),flip(a)]. given #139 (T,wt=12): 460 (x @ y) * y != x * y | c_0 = x. [para(400(a,1),202(a,1)),flip(a)]. given #140 (T,wt=13): 355 x * (x @ x * y) = x * (x @ y). [hyper(16,a,205,a),flip(a)]. given #141 (A,wt=20): 86 x * y * z != u * x * y | u * (u @ x * y) = z. [para(9(a,1),16(a,1))]. given #142 (F,wt=23): 619 (A @ C) * (B @ C) * C * C * A * B != C * A * B * C # answer(D). [para(512(a,1),32(a,1,2,2,2)),demod(199(15),9(28),9(27),9(26),21(27))]. given #143 (F,wt=23): 661 C * A * (B @ C) * A * C * B != C * A * A * B * C # answer(D). [para(25(a,1),445(a,1))]. given #144 (T,wt=9): 731 x @ x * y = x @ y. [hyper(376,a,355,a),flip(a)]. given #145 (T,wt=9): 771 (x @ y) @ x * y = c_0. [para(400(a,1),731(a,1,2)),demod(462(6))]. given #146 (A,wt=20): 87 x * y * z != z * u | x * y * (x * y @ z) = u. [para(9(a,1),16(a,2)),demod(9(8)),flip(a)]. given #147 (F,wt=23): 670 C * A * B * (A @ C) * B * C != A * C * B * B * C # answer(D). [para(73(a,1),67(a,2,2)),demod(400(13))]. given #148 (F,wt=23): 717 (A @ C) * (B @ C) * C * A * B * (C @ B) != A * C * B # answer(D). [para(10(a,1),503(a,2,2))]. given #149 (T,wt=11): 772 (x @ y) @ x * y * x = c_0. [para(731(a,1),462(a,1,1)),demod(9(3))]. given #150 (T,wt=11): 773 x * y * x @ (x @ y) = c_0. [para(731(a,1),463(a,1,2)),demod(9(2))]. given #151 (A,wt=18): 88 x * y != z * y | z * (z @ y) = x * (x @ y). [para(10(a,1),16(a,1))]. given #152 (F,wt=21): 829 (A * B @ C) * B * C * B != (A @ C) * B * B * C # answer(D). [para(773(a,1),33(a,1,2,2)),demod(199(12),9(23),9(22),10(22))]. given #153 (F,wt=23): 718 A * B * C * (B @ A) * x != (A @ C) * B * C * A * x # answer(D). [para(19(a,1),503(a,1,2,2,2)),demod(420(13)),flip(a)]. given #154 (T,wt=11): 774 x * x * y @ (x @ y) = c_0. [para(731(a,1),474(a,1,2))]. given #155 (T,wt=11): 787 x * y @ (y @ x * y) = c_0. [back_demod(515),demod(760(4))]. given #156 (A,wt=20): 107 x * y * z * (y * z @ u) != y * z * u | u = x. [para(9(a,1),17(a,1,2)),demod(9(7))]. given #157 (F,wt=21): 841 (A @ C) * B * C * A * ((B @ A) @ C) != B * A * C # answer(D). [para(10(a,1),718(a,1,2,2)),demod(19(9)),flip(a)]. given #158 (F,wt=21): 845 A * B * C * (B @ A) * (C * A @ B) != A * C * B # answer(D). [para(21(a,1),718(a,2,2)),demod(420(24))]. given #159 (T,wt=11): 797 (x @ y * x) @ y * x = c_0. [para(10(a,1),771(a,1,2)),demod(760(3))]. given #160 (T,wt=11): 806 (x @ y) @ y * x * y = c_0. [para(389(a,1),771(a,1,1)),demod(9(3))]. given #161 (A,wt=20): 125 x * y * z * (y * z @ u) != y * z * u | x = u. [para(9(a,1),18(a,1,2)),demod(9(7))]. given #162 (F,wt=21): 888 A * B * C * ((A @ C) * (B @ C) @ B) != A * B * C # answer(D). [back_demod(227),demod(871(23))]. given #163 (F,wt=23): 722 (A @ C) * B * C * A * A * B != A * B * C * B * A # answer(D). [para(73(a,1),503(a,1,2,2,2)),demod(420(16))]. given #164 (T,wt=11): 810 (x @ y) @ x * x * y = c_0. [para(731(a,1),771(a,1,1))]. given #165 (T,wt=11): 871 x * (y @ x) * y = y * x. [para(787(a,1),10(a,1,2,2)),demod(199(5),531(4),9(5),749(4)),flip(a)]. given #166 (A,wt=18): 141 x * y * z != y * u | x * (x @ y) * z = u. [para(19(a,1),7(a,1))]. given #167 (F,wt=17): 941 C * A * (A * B @ C) * B != A * B * C # answer(D). [para(871(a,1),164(a,2,2))]. given #168 (F,wt=19): 936 C * (A @ C) * (B @ C) * A * B != A * B * C # answer(D). [para(871(a,1),31(a,1)),demod(9(5)),flip(a)]. given #169 (T,wt=11): 879 x * y @ (x @ y * x) = c_0. [para(787(a,1),389(a,2)),demod(531(4))]. given #170 (T,wt=11): 904 (x @ y * x) @ x * y = c_0. [para(797(a,1),731(a,2)),demod(531(6))]. given #171 (A,wt=18): 142 x * y * (y @ z) * u != y * z * u | z = x. [para(19(a,1),8(a,1)),flip(a)]. given #172 (F,wt=21): 948 x * C * A * (A * B @ C) * B != x * A * B * C # answer(D). [para(871(a,1),167(a,2,2,2))]. given #173 (F,wt=21): 994 C * A * (A * B @ C) * B * x != A * B * C * x # answer(D). [ur(577,b,941,a),demod(9(6),9(5),9(18),9(17),9(16)),flip(a)]. given #174 (T,wt=11): 916 (x @ y) @ x * y * y = c_0. [para(806(a,1),731(a,2)),demod(420(5))]. given #175 (T,wt=11): 932 (x @ y) * x = x * (x @ y). [hyper(16,a,871,a),flip(a)]. given #176 (A,wt=18): 143 x * y * (y @ z) * u != y * z * u | x = z. [para(19(a,1),8(a,2))]. given #177 (F,wt=17): 1066 (A * B @ C) * B != (A @ C) * B * (B @ C) # answer(D). [para(932(a,1),29(a,2,2))]. given #178 (F,wt=19): 1044 A * B * C * (B @ (A * B @ C)) != A * B * C # answer(D). [para(10(a,1),994(a,1,2,2)),demod(21(11)),flip(a)]. given #179 (T,wt=7): 1059 x @ (x @ y) = c_0. [hyper(388,a,932,a)]. given #180 (T,wt=7): 1060 (x @ y) @ x = c_0. [hyper(304,a,932,a)]. given #181 (A,wt=21): 144 x * y * z * (z @ x * y) * u = z * x * y * u. [para(19(a,1),9(a,1)),demod(9(2)),flip(a)]. given #182 (F,wt=21): 1046 C * A * (A * B @ C) * B * (C @ B) != A * C * B # answer(D). [para(10(a,1),994(a,2,2))]. given #183 (F,wt=21): 1065 A * B * (A * B @ C) != (A @ C) * (B @ C) * A * B # answer(D). [para(932(a,1),29(a,1)),demod(9(9))]. given #184 (T,wt=11): 984 x * (x @ y) * (y @ x) = x. [hyper(141,a,10,a)]. given #185 (T,wt=9): 1170 (x @ y) * (y @ x) = c_0. [hyper(192,a,984,a),flip(a)]. given #186 (A,wt=21): 145 x * y * z * (y * z @ x) * u = y * z * x * u. [para(9(a,1),19(a,1,2)),demod(9(9))]. given #187 (F,wt=13): 1205 (A * B @ C) * (C @ B) != A @ C # answer(D). [para(1170(a,1),29(a,2,2)),demod(199(14))]. given #188 (F,wt=15): 1200 C * A * B * (A @ C) != A * C * B # answer(D). [back_demod(113),demod(1170(13),199(8))]. given #189 (T,wt=9): 1232 (x @ y) @ (y @ x) = c_0. [para(1170(a,1),304(a,1)),demod(1170(4)),xx(a)]. given #190 (T,wt=10): 1221 x @ y != c_0 | y @ x = c_0. [para(1170(a,1),192(a,1)),flip(a),flip(b)]. given #191 (A,wt=21): 146 x * y * z * (z @ (x @ y)) = y * x * z * (x @ y). [para(10(a,1),19(a,1,2,2)),flip(a)]. given #192 (F,wt=15): 1204 (A @ C) * (B @ C) * (C @ A * B) != c_0 # answer(D). [para(1170(a,1),29(a,1)),flip(a)]. given #193 (F,wt=15): 1206 (C @ A * B) * (A @ C) * (B @ C) != c_0 # answer(D). [para(1170(a,1),30(a,1)),flip(a)]. given #194 (T,wt=11): 1090 x * (x @ y) @ (x @ y) = c_0. [para(932(a,1),389(a,1,1)),demod(1059(6))]. given #195 (T,wt=11): 1095 (x @ y) @ x * (x @ y) = c_0. [para(932(a,1),731(a,1,2)),demod(1060(6))]. given #196 (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 #197 (F,wt=17): 1208 x * (A @ C) * (B @ C) * (C @ A * B) != x # answer(D). [para(1170(a,1),31(a,1,2)),demod(199(2)),flip(a)]. given #198 (F,wt=17): 1209 x * (A * B @ C) * (C @ B) != x * (A @ C) # answer(D). [para(1170(a,1),31(a,2,2,2)),demod(199(15))]. given #199 (T,wt=11): 1203 (x @ y) * (y @ x) * z = z. [para(1170(a,1),9(a,1,1)),demod(189(2)),flip(a)]. given #200 (T,wt=9): 1403 ((x @ y) @ z) @ z = c_0. [para(1203(a,1),771(a,1,2)),demod(1402(4))]. given #201 (A,wt=18): 152 x * y * z != y * x * u | (x @ y) * z = u. [para(19(a,1),13(a,1))]. ============================== PROOF ================================= % Proof 1 at 0.36 (+ 0.01) seconds: D. % Length of proof is 27. % Level of proof is 8. % Maximum clause weight is 23. % Given clauses 201. 6 (A @ C) * (B @ C) != A * B @ C # answer(D). [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 * y * x = y * x * z * x * y. [input]. 12 A * B @ C != (A @ C) * (B @ C) # answer(D). [copy(6),flip(a)]. 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)]. 19 x * y * (y @ x) * z = y * x * z. [para(10(a,1),9(a,1,1)),demod(9(2),9(5)),flip(a)]. 25 x * y * z * y * x * u = y * x * z * x * y * u. [para(11(a,1),9(a,1,1)),demod(9(5),9(4),9(3),9(2),9(9),9(8),9(7))]. 29 (A * B @ C) * x != (A @ C) * (B @ C) * x # answer(D). [ur(8,b,12,a),demod(9(14))]. 39 x * (x @ x) * y = x * y. [para(15(a,1),9(a,1,1)),flip(a)]. 52 x * y * z * y * x != y * x * u | z * x * y = u. [para(11(a,1),13(a,1))]. 59 x * y * z * u != v * u | x * y * z = v. [para(9(a,1),14(a,1,2))]. 69 (x @ x) * y = y. [hyper(13,a,39,a)]. 73 x * y * y * x = y * x * x * y. [para(39(a,1),11(a,1,2)),demod(69(6))]. 152 x * y * z != y * x * u | (x @ y) * z = u. [para(19(a,1),13(a,1))]. 400 (x @ y) * y * x = x * y. [hyper(52,a,19,a)]. 420 (x @ y) * y * x * z = x * y * z. [para(400(a,1),9(a,1,1)),demod(9(2),9(5)),flip(a)]. 423 (A @ C) * (B @ C) * C * A * B != A * B * C # answer(D). [para(400(a,1),29(a,1)),demod(9(5)),flip(a)]. 503 (A @ C) * (B @ C) * C * A * B * x != A * B * C * x # answer(D). [ur(59,b,423,a),demod(9(12),9(11),9(20),9(19))]. 722 (A @ C) * B * C * A * A * B != A * B * C * B * A # answer(D). [para(73(a,1),503(a,1,2,2,2)),demod(420(16))]. 921 (A @ C) * B * C * A * A * B != B * A * C * A * B # answer(D). [para(11(a,1),722(a,2))]. 1442 (x @ y) * z * y * x * u = z * x * y * u. [hyper(152,a,25,a)]. 1443 $F # answer(D). [resolve(1442,a,921,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=201. Generated=13334. Kept=1436. proofs=1. Usable=159. Sos=876. Demods=321. Denials=0. Limbo=2, Disabled=404. Hints=0. Weight_deleted=5987. Literals_deleted=0. Forward_subsumed=5911. Back_subsumed=52. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=484 (0 lex), Back_demodulated=346. Back_unit_deleted=0. Demod_attempts=301581. Demod_rewrites=32663. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=44723. Nonunit_bsub_feature_tests=11381. Megabytes=1.21. User_CPU=0.36, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13127 exit (max_proofs) Mon Jun 19 16:41:41 2006