============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3322 was started by mccune on cleo.thornwood, Wed Nov 22 11:22:14 2006 The command was "/home/mccune/bin/prover9 -f qg1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file qg1.in formulas(sos). x * (x \ y) = y. x \ (x * y) = y. (x / y) * y = x. (x * y) / y = x. x * (y * (y * x)) = y * x. end_of_list. formulas(goals). y * (y * x) = x * y. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 y * (y * x) = x * y # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x * (x \ y) = y. [assumption]. x \ (x * y) = y. [assumption]. (x / y) * y = x. [assumption]. (x * y) / y = x. [assumption]. x * (y * (y * x)) = y * x. [assumption]. c1 * (c1 * c2) != c2 * c1. [deny(1)]. 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([ c1, c2, *, /, \ ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 x * (x \ y) = y. [assumption]. 3 x \ (x * y) = y. [assumption]. 4 (x / y) * y = x. [assumption]. 5 (x * y) / y = x. [assumption]. 6 x * (y * (y * x)) = y * x. [assumption]. 8 c2 * c1 != c1 * (c1 * c2). [copy(7),flip(a)]. end_of_list. formulas(demodulators). 2 x * (x \ y) = y. [assumption]. 3 x \ (x * y) = y. [assumption]. 4 (x / y) * y = x. [assumption]. 5 (x * y) / y = x. [assumption]. 6 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=7): 2 x * (x \ y) = y. [assumption]. given #2 (I,wt=7): 3 x \ (x * y) = y. [assumption]. given #3 (I,wt=7): 4 (x / y) * y = x. [assumption]. given #4 (I,wt=7): 5 (x * y) / y = x. [assumption]. given #5 (I,wt=11): 6 x * (y * (y * x)) = y * x. [assumption]. given #6 (I,wt=9): 8 c2 * c1 != c1 * (c1 * c2). [copy(7),flip(a)]. given #7 (F,wt=7): 9 (x / y) \ x = y. [para(4(a,1),3(a,1,2))]. given #8 (F,wt=7): 10 x / (y \ x) = y. [para(2(a,1),5(a,1,1))]. given #9 (T,wt=9): 11 (x \ y) * (x * y) = y. [para(2(a,1),6(a,1,2,2)),rewrite(2(5))]. given #10 (T,wt=9): 13 x * ((y / x) * y) = y. [para(4(a,1),6(a,1,2,2)),rewrite(4(5))]. given #11 (A,wt=11): 14 (x * y) / (x * (x * y)) = y. [para(6(a,1),5(a,1,1))]. given #12 (F,wt=5): 27 x * x = x. [para(4(a,1),13(a,1,2))]. given #13 (F,wt=5): 29 x / x = x. [para(6(a,1),14(a,1,2)),rewrite(27(1),27(1),27(1),27(2))]. given #14 (T,wt=9): 31 (x / (x / y)) * x = y. [back_rewrite(25),rewrite(30(3))]. given #15 (T,wt=9): 32 x \ y = (y / x) * y. [back_rewrite(20),rewrite(30(3))]. given #16 (A,wt=15): 15 (x * (x * y)) * (y * (x * y)) = x * y. [para(6(a,1),6(a,1,2,2)),rewrite(6(8))]. given #17 (F,wt=9): 34 x / (x / y) = y / x. [para(31(a,1),5(a,1,1)),flip(a)]. given #18 (F,wt=9): 40 (x / y) * (y / x) = y. [para(34(a,1),4(a,1,1))]. given #19 (T,wt=11): 28 ((x / y) * x) * (y * x) = x. [para(13(a,1),6(a,1,2,2)),rewrite(13(7))]. given #20 (T,wt=11): 30 x / (y * x) = (x / y) * x. [para(13(a,1),14(a,1,1)),rewrite(13(3))]. given #21 (A,wt=11): 35 x * ((x / (x / y)) * y) = y. [para(31(a,1),6(a,1,2,2)),rewrite(31(7))]. given #22 (F,wt=11): 41 (x * y) / x = (y / x) * y. [para(5(a,1),34(a,1,2)),rewrite(30(4))]. given #23 (F,wt=11): 42 (x / (y / x)) * x = x / y. [para(34(a,1),31(a,1,1,2))]. given #24 (T,wt=11): 46 (x / y) / x = x / (y / x). [para(34(a,1),34(a,1,2)),flip(a)]. given #25 (T,wt=11): 47 x / (y / (y / x)) = y / x. [para(34(a,2),34(a,1,2))]. given #26 (A,wt=19): 36 (x * (y * x)) * ((y * (y * x)) * (y * x)) = y * x. [para(15(a,1),6(a,1,2,2)),rewrite(15(12))]. given #27 (F,wt=11): 49 ((x / y) * x) * y = y * x. [para(5(a,1),40(a,1,2)),rewrite(30(2))]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 27. % Level of proof is 12. % Maximum clause weight is 15. % Given clauses 27. 1 y * (y * x) = x * y # label(goal). [goal]. 2 x * (x \ y) = y. [assumption]. 3 x \ (x * y) = y. [assumption]. 4 (x / y) * y = x. [assumption]. 5 (x * y) / y = x. [assumption]. 6 x * (y * (y * x)) = y * x. [assumption]. 7 c1 * (c1 * c2) != c2 * c1. [deny(1)]. 8 c2 * c1 != c1 * (c1 * c2). [copy(7),flip(a)]. 9 (x / y) \ x = y. [para(4(a,1),3(a,1,2))]. 11 (x \ y) * (x * y) = y. [para(2(a,1),6(a,1,2,2)),rewrite(2(5))]. 13 x * ((y / x) * y) = y. [para(4(a,1),6(a,1,2,2)),rewrite(4(5))]. 14 (x * y) / (x * (x * y)) = y. [para(6(a,1),5(a,1,1))]. 15 (x * (x * y)) * (y * (x * y)) = x * y. [para(6(a,1),6(a,1,2,2)),rewrite(6(8))]. 20 x \ y = y / (x * y). [para(11(a,1),5(a,1,1)),flip(a)]. 25 x / ((x / y) * x) = y. [back_rewrite(9),rewrite(20(2))]. 28 ((x / y) * x) * (y * x) = x. [para(13(a,1),6(a,1,2,2)),rewrite(13(7))]. 30 x / (y * x) = (x / y) * x. [para(13(a,1),14(a,1,1)),rewrite(13(3))]. 31 (x / (x / y)) * x = y. [back_rewrite(25),rewrite(30(3))]. 34 x / (x / y) = y / x. [para(31(a,1),5(a,1,1)),flip(a)]. 40 (x / y) * (y / x) = y. [para(34(a,1),4(a,1,1))]. 41 (x * y) / x = (y / x) * y. [para(5(a,1),34(a,1,2)),rewrite(30(4))]. 49 ((x / y) * x) * y = y * x. [para(5(a,1),40(a,1,2)),rewrite(30(2))]. 94 (x / y) * x = y * (x / y). [para(31(a,1),49(a,1,1)),flip(a)]. 97 (x * (y / x)) * x = x * y. [para(49(a,1),15(a,2)),rewrite(94(2),94(4),94(8),15(11))]. 100 (x * (y / x)) * (x * y) = y. [para(28(a,1),49(a,2)),rewrite(94(3),94(6),94(9),97(10))]. 104 x * (x * y) = y * x. [para(41(a,1),49(a,1,1,1)),rewrite(94(2),100(4)),flip(a)]. 105 $F. [resolve(104,a,8,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=27. Generated=484. Kept=102. proofs=1. Usable=21. Sos=39. Demods=65. Limbo=11, Disabled=36. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=382. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=95 (0 lex), Back_demodulated=29. Back_unit_deleted=0. Demod_attempts=4638. Demod_rewrites=1041. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.11. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3322 exit (max_proofs) Wed Nov 22 11:22:14 2006