============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3870 was started by mccune on cleo.thornwood, Wed Nov 22 11:24:23 2006 The command was "/home/mccune/bin/prover9 -f cs.in EN.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 EN.in formulas(sos). x * y * z * y * x = y * x * z * x * y. end_of_list. formulas(sos). (A @ B) * C != C * (A @ B) # answer(N). 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 = y * x * z * x * y. [assumption]. (A @ B) * C != C * (A @ B) # answer(N). [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]. 5 x * y * z * y * x = y * x * z * x * y. [assumption]. 6 (A @ B) * C != C * (A @ B) # answer(N). [assumption]. end_of_list. formulas(demodulators). 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. 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=19): 5 x * y * z * y * x = y * x * z * x * y. [assumption]. given #6 (I,wt=11): 6 (A @ B) * C != C * (A @ B) # answer(N). [assumption]. given #7 (F,wt=15): 23 (A @ B) * C * x != C * (A @ B) * x # answer(N). [ur(2,b,6,a),rewrite(3(6),3(12))]. given #8 (F,wt=15): 24 x * (A @ B) * C != x * C * (A @ B) # answer(N). [ur(1,b,6,a)]. given #9 (T,wt=7): 9 x * (x @ x) = x. [hyper(1,a,4,a)]. given #10 (T,wt=10): 31 x * y != x | x @ x = y. [para(9(a,1),1(a,1)),flip(a)]. given #11 (A,wt=14): 7 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite(3(4))]. given #12 (F,wt=15): 37 C * (A @ B) * (C @ C) != (A @ B) * C # answer(N). [para(9(a,1),23(a,1,2)),flip(a)]. given #13 (F,wt=17): 27 C * (A @ B) * (C @ (A @ B)) != C * (A @ B) # answer(N). [para(4(a,1),23(a,1)),flip(a)]. given #14 (T,wt=10): 32 x * (y @ y) != y | y = x. [para(9(a,1),2(a,1)),flip(a)]. given #15 (T,wt=10): 33 x * (y @ y) != y | x = y. [para(9(a,1),2(a,2))]. given #16 (A,wt=14): 8 x * y * z != u * z | x * y = u. [para(3(a,1),2(a,1))]. given #17 (F,wt=17): 29 (A @ B) * C * ((A @ B) @ C) != (A @ B) * C # answer(N). [para(4(a,1),23(a,2))]. given #18 (F,wt=19): 25 x * (A @ B) * C * y != x * C * (A @ B) * y # answer(N). [ur(1,b,23,a)]. given #19 (T,wt=11): 34 x * (x @ x) * y = x * y. [para(9(a,1),3(a,1,1)),flip(a)]. given #20 (T,wt=7): 72 (x @ x) * y = y. [hyper(7,a,34,a)]. given #21 (A,wt=14): 10 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. given #22 (F,wt=19): 26 C * (A @ B) * x * (x @ C) != (A @ B) * x * C # answer(N). [para(4(a,1),23(a,1,2)),flip(a)]. given #23 (F,wt=17): 97 C * (A @ B) * ((x @ x) @ C) != (A @ B) * C # answer(N). [para(72(a,1),26(a,1,2,2)),rewrite(72(15))]. given #24 (T,wt=6): 93 x != y | y = x. [para(9(a,1),10(a,2)),rewrite(72(2),82(4),9(3))]. given #25 (T,wt=9): 81 x * ((y @ y) @ x) = x. [para(72(a,1),4(a,1,2)),rewrite(72(5))]. given #26 (A,wt=14): 11 x * y * (y @ z) != y * z | z = x. [para(4(a,1),2(a,1)),flip(a)]. given #27 (F,wt=19): 30 x * y * (A @ B) * C != x * y * C * (A @ B) # answer(N). [ur(1,b,24,a)]. given #28 (F,wt=19): 38 (A @ B) * C * ((A @ B) @ (A @ B)) != C * (A @ B) # answer(N). [para(9(a,1),23(a,2,2))]. given #29 (T,wt=9): 87 x * (x @ x * x) = x. [hyper(10,a,3,a)]. given #30 (T,wt=9): 101 (x @ x) @ y = y @ y. [hyper(31,a,81,a),flip(a)]. given #31 (A,wt=14): 12 x * y * (y @ z) != y * z | x = z. [para(4(a,1),2(a,2))]. given #32 (F,wt=19): 51 x * C * (A @ B) * (C @ C) != x * (A @ B) * C # answer(N). [ur(1,b,37,a)]. given #33 (F,wt=19): 107 (A @ B) * C * ((x @ x) @ (A @ B)) != C * (A @ B) # answer(N). [para(81(a,1),23(a,2,2))]. given #34 (T,wt=9): 122 x @ x * x = x @ x. [hyper(31,a,87,a),flip(a)]. given #35 (T,wt=9): 124 ((x @ x) @ y) * z = z. [para(101(a,2),72(a,1,1))]. given #36 (A,wt=15): 13 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=15): 169 B * A * C * (A @ B) != A * B * C # answer(N). [para(13(a,1),30(a,1)),flip(a)]. given #38 (F,wt=19): 125 C * (A @ B) * (((x @ x) @ y) @ C) != (A @ B) * C # answer(N). [para(101(a,2),97(a,1,2,2,1))]. given #39 (T,wt=10): 80 x * y != y | z @ z = x. [para(72(a,1),2(a,1)),flip(a)]. NOTE: New constant: x @ x = c_0. [new_symbol(179)]. NOTE: New Function symbol precedence: lex([ A, B, C, c_0, *, @ ]). given #40 (T,wt=5): 183 x @ x = c_0. [new_symbol(179)]. given #41 (A,wt=17): 14 x * y * z * (z @ x * y) = z * x * y. [para(4(a,1),3(a,1)),flip(a)]. given #42 (F,wt=19): 173 B * A * C * (A @ B) * x != A * B * C * x # answer(N). [ur(8,b,169,a),rewrite(3(9),3(8),3(16),3(15))]. given #43 (F,wt=17): 226 A * B * C * ((A @ B) @ C) != A * B * C # answer(N). [para(4(a,1),173(a,1,2,2)),rewrite(13(9)),flip(a)]. given #44 (T,wt=5): 187 c_0 @ x = c_0. [back_rewrite(178),rewrite(183(1),183(3))]. given #45 (T,wt=5): 194 c_0 * x = x. [back_rewrite(144),rewrite(183(1),187(2),187(2))]. given #46 (A,wt=17): 15 x * y * z * (y * z @ x) = y * z * x. [para(3(a,1),4(a,1,2)),rewrite(3(7))]. given #47 (F,wt=19): 175 x * B * A * C * (A @ B) != x * A * B * C # answer(N). [ur(1,b,169,a)]. given #48 (F,wt=19): 228 B * A * C * (A @ B) * (C @ B) != A * C * B # answer(N). [para(4(a,1),173(a,2,2))]. given #49 (T,wt=5): 203 x * c_0 = x. [back_rewrite(126),rewrite(183(1),187(2),187(2))]. given #50 (T,wt=7): 204 x @ x * x = c_0. [back_rewrite(122),rewrite(183(3))]. given #51 (A,wt=22): 16 x * y * z * y * x != y * u | x * z * x * y = u. [para(5(a,1),1(a,1))]. given #52 (F,wt=21): 28 (A @ B) * C * x * (x @ (A @ B)) != C * x * (A @ B) # answer(N). [para(4(a,1),23(a,2,2))]. given #53 (F,wt=21): 53 C * (A @ B) * (C @ (A @ B)) * x != C * (A @ B) * x # answer(N). [ur(2,b,27,a),rewrite(3(12),3(11),3(18))]. given #54 (T,wt=7): 208 x * (x @ c_0) = x. [back_rewrite(201),rewrite(203(5))]. given #55 (T,wt=8): 197 x * y != x | c_0 = y. [back_rewrite(140),rewrite(183(3),187(4),187(4))]. given #56 (A,wt=22): 17 x * y * z * y * u != y * u * z * u * y | u = x. [para(5(a,1),2(a,1)),flip(a)]. given #57 (F,wt=21): 54 x * C * (A @ B) * (C @ (A @ B)) != x * C * (A @ B) # answer(N). [ur(1,b,27,a)]. given #58 (F,wt=21): 65 (A @ B) * C * ((A @ B) @ C) * x != (A @ B) * C * x # answer(N). [ur(8,b,29,a),rewrite(3(11),3(18))]. given #59 (T,wt=5): 284 x @ c_0 = c_0. [hyper(197,a,208,a),flip(a)]. given #60 (T,wt=8): 200 x * y != y | c_0 = x. [back_rewrite(135),rewrite(183(3),187(4))]. given #61 (A,wt=22): 18 x * y * z * y * u != y * u * z * u * y | x = u. [para(5(a,1),2(a,2))]. given #62 (F,wt=21): 67 x * (A @ B) * C * ((A @ B) @ C) != x * (A @ B) * C # answer(N). [ur(1,b,29,a)]. given #63 (F,wt=21): 231 A * B * C * ((A @ B) @ C) * x != A * B * C * x # answer(N). [para(13(a,1),173(a,1,2,2)),rewrite(13(10)),flip(a)]. given #64 (T,wt=9): 238 x * (x * x @ x) = x. [hyper(7,a,15,a)]. given #65 (T,wt=7): 307 x * x @ x = c_0. [hyper(197,a,238,a),flip(a)]. given #66 (A,wt=23): 19 x * y * z * y * x * u = y * x * z * x * y * u. [para(5(a,1),3(a,1,1)),rewrite(3(5),3(4),3(3),3(2),3(9),3(8),3(7))]. given #67 (F,wt=21): 235 B * A * C * (A @ B) * (C @ A * B) != C * A * B # answer(N). [para(14(a,1),173(a,2))]. given #68 (F,wt=21): 237 x * A * B * C * ((A @ B) @ C) != x * A * B * C # answer(N). [ur(1,b,226,a)]. given #69 (T,wt=10): 119 x * y != y * y | y = x. [para(9(a,1),11(a,1,2))]. given #70 (T,wt=12): 195 x * (x @ y) != x * y | c_0 = y. [back_rewrite(143),rewrite(183(5),187(6))]. given #71 (A,wt=23): 20 x * y * z * u * z * y = x * z * y * u * y * z. [para(5(a,1),3(a,2,2)),rewrite(3(5))]. given #72 (F,wt=21): 255 B * A * C * (A @ B) * (B * C @ A) != B * C * A # answer(N). [para(15(a,1),173(a,2))]. given #73 (F,wt=21): 301 A * B * C * ((A @ B) @ C) * (C @ B) != A * C * B # answer(N). [para(4(a,1),231(a,2,2))]. given #74 (T,wt=12): 198 x * y * z != z | x * y = c_0. [back_rewrite(139),rewrite(183(4),187(5)),flip(b)]. given #75 (T,wt=12): 205 x * y != y | x * (x @ y) = c_0. [back_rewrite(113),rewrite(183(3),187(4)),flip(b)]. given #76 (A,wt=23): 21 x * y * z * u * y * x = y * x * z * u * x * y. [para(3(a,1),5(a,1,2,2)),rewrite(3(8))]. given #77 (F,wt=23): 42 x * y * z * (A @ B) * C != x * y * z * C * (A @ B) # answer(N). [ur(7,b,24,a)]. given #78 (F,wt=23): 43 x * y * (A @ B) * C * z != x * y * C * (A @ B) * z # answer(N). [ur(7,b,23,a)]. given #79 (T,wt=12): 206 x * y * z != x * y | c_0 = z. [back_rewrite(108),rewrite(183(5),187(6))]. given #80 (T,wt=12): 330 x @ y != x * y | y * x = c_0. [para(4(a,1),198(a,1)),flip(a)]. given #81 (A,wt=23): 22 x * (x @ y) * y * (x @ y) * x = (x @ y) * x * x * y. [para(4(a,1),5(a,1,2,2)),flip(a)]. given #82 (F,wt=23): 68 x * C * (A @ B) * y * (y @ C) != x * (A @ B) * y * C # answer(N). [para(4(a,1),25(a,1,2,2)),flip(a)]. given #83 (F,wt=23): 70 C * x * (A @ B) * x * C != x * (A @ B) * C * C * x # answer(N). [para(5(a,1),25(a,2)),flip(a)]. given #84 (T,wt=12): 350 x * y != y * x | x @ y = c_0. [para(4(a,1),206(a,1)),flip(b)]. given #85 (T,wt=13): 88 x * y * (x * y @ x) = y * x. [hyper(10,a,3,a(flip)),rewrite(3(4))]. given #86 (A,wt=18): 44 x * y * z * u != x * y * z * v | u = v. [para(3(a,1),7(a,1,2)),rewrite(3(5))]. given #87 (F,wt=19): 377 (A @ B) * C * (C * (A @ B) @ C) != (A @ B) * C # answer(N). [para(88(a,1),23(a,2))]. given #88 (F,wt=19): 386 A * B * C * (C * (A @ B) @ C) != A * B * C # answer(N). [para(88(a,1),173(a,1,2,2)),rewrite(13(9)),flip(a)]. given #89 (T,wt=13): 202 x * y @ x * y * x * y = c_0. [back_rewrite(132),rewrite(183(8))]. given #90 (T,wt=13): 209 x * y * (y @ y * x) = y * x. [hyper(1,a,14,a)]. given #91 (A,wt=18): 45 x * y * z != x * u * y | u * (u @ y) = z. [para(4(a,1),7(a,1,2)),flip(a)]. given #92 (F,wt=19): 412 C * (A @ B) * (C @ C * (A @ B)) != C * (A @ B) # answer(N). [para(209(a,1),23(a,1)),flip(a)]. given #93 (F,wt=21): 376 C * (A @ B) * ((A @ B) * C @ (A @ B)) != C * (A @ B) # answer(N). [para(88(a,1),23(a,1)),flip(a)]. given #94 (T,wt=10): 436 x * y != x * z | z = y. [para(194(a,1),45(a,1,2)),rewrite(203(3),284(5),203(5))]. given #95 (T,wt=13): 309 x * y * x * y @ x * y = c_0. [para(3(a,1),307(a,1,1))]. given #96 (A,wt=14): 46 x * y * z != y * x | y @ x = z. [para(4(a,1),7(a,1)),flip(a)]. given #97 (F,wt=21): 387 B * A * C * (A @ B) * (B * C @ B) != A * C * B # answer(N). [para(88(a,1),173(a,2,2))]. given #98 (F,wt=21): 413 (A @ B) * C * ((A @ B) @ (A @ B) * C) != (A @ B) * C # answer(N). [para(209(a,1),23(a,2))]. given #99 (T,wt=12): 450 x * y != y * x | y @ x = c_0. [para(203(a,1),46(a,1,2))]. given #100 (T,wt=13): 372 x * (y * x @ y) = x * (x @ y). [hyper(10,a,88,a),flip(a)]. given #101 (A,wt=22): 47 x * y * z * y * x != y * x * u | z * x * y = u. [para(5(a,1),7(a,1))]. ============================== PROOF ================================= % Proof 1 at 0.10 (+ 0.00) seconds: N. % Length of proof is 18. % Level of proof is 6. % Maximum clause weight is 23. % Given clauses 101. 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 = y * x * z * x * y. [assumption]. 6 (A @ B) * C != C * (A @ B) # answer(N). [assumption]. 7 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite(3(4))]. 8 x * y * z != u * z | x * y = u. [para(3(a,1),2(a,1))]. 13 x * y * (y @ x) * z = y * x * z. [para(4(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)]. 21 x * y * z * u * y * x = y * x * z * u * x * y. [para(3(a,1),5(a,1,2,2)),rewrite(3(8))]. 24 x * (A @ B) * C != x * C * (A @ B) # answer(N). [ur(1,b,6,a)]. 30 x * y * (A @ B) * C != x * y * C * (A @ B) # answer(N). [ur(1,b,24,a)]. 47 x * y * z * y * x != y * x * u | z * x * y = u. [para(5(a,1),7(a,1))]. 169 B * A * C * (A @ B) != A * B * C # answer(N). [para(13(a,1),30(a,1)),flip(a)]. 173 B * A * C * (A @ B) * x != A * B * C * x # answer(N). [ur(8,b,169,a),rewrite(3(9),3(8),3(16),3(15))]. 343 A * B * C * (A @ B) * B * A != A * B * C * A * B # answer(N). [para(21(a,1),173(a,1))]. 465 (x @ y) * y * x = x * y. [hyper(47,a,13,a)]. 468 $F # answer(N). [back_rewrite(343),rewrite(465(10)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=101. Generated=4273. Kept=467. proofs=1. Usable=73. Sos=238. Demods=52. Limbo=3, Disabled=159. Hints=0. Weight_deleted=1855. Literals_deleted=0. Forward_subsumed=1950. Back_subsumed=5. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=100 (0 lex), Back_demodulated=148. Back_unit_deleted=0. Demod_attempts=88195. Demod_rewrites=9044. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=7061. Nonunit_bsub_feature_tests=2362. Megabytes=0.49. User_CPU=0.10, System_CPU=0.00, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3870 exit (max_proofs) Wed Nov 22 11:24:24 2006