============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 26455 was started by mccune on cleo, Fri Apr 13 09:14:38 2007 The command was "/home/mccune/bin/prover9 -f qg1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file qg1.in assign(max_seconds,30). 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 (A,wt=7): 9 (x / y) \ x = y. [para(4(a,1),3(a,1,2))]. given #8 (T,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 (T,wt=5): 27 x * x = x. [para(4(a,1),13(a,1,2))]. given #12 (A,wt=11): 14 (x * y) / (x * (x * y)) = y. [para(6(a,1),5(a,1,1))]. given #13 (T,wt=5): 29 x / x = x. [para(27(a,1),5(a,1,1))]. 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 (T,wt=9): 34 x / (x / y) = y / x. [para(31(a,1),5(a,1,1)),flip(a)]. given #17 (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 #18 (T,wt=9): 36 (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 (T,wt=11): 35 x * ((x / (x / y)) * y) = y. [para(31(a,1),6(a,1,2,2)),rewrite(31(7))]. given #22 (A,wt=11): 37 (x * y) / x = (y / x) * y. [para(5(a,1),34(a,1,2)),rewrite(30(4))]. given #23 (T,wt=11): 38 (x / (y / x)) * x = x / y. [para(34(a,1),31(a,1,1,2))]. given #24 (T,wt=11): 42 (x / y) / x = x / (y / x). [para(34(a,1),34(a,1,2)),flip(a)]. given #25 (T,wt=11): 43 x / (y / (y / x)) = y / x. [para(34(a,2),34(a,1,2))]. given #26 (T,wt=11): 49 ((x / y) * x) * y = y * x. [para(5(a,1),36(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 26. 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)]. 36 (x / y) * (y / x) = y. [para(34(a,1),4(a,1,1))]. 37 (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),36(a,1,2)),rewrite(30(2))]. 87 (x / y) * x = y * (x / y). [para(31(a,1),49(a,1,1)),flip(a)]. 91 (x * (y / x)) * x = x * y. [para(49(a,1),15(a,2)),rewrite(87(2),87(4),87(8),15(11))]. 93 (x * (y / x)) * (x * y) = y. [para(28(a,1),49(a,2)),rewrite(87(3),87(6),87(9),91(10))]. 97 x * (x * y) = y * x. [para(37(a,1),49(a,1,1,1)),rewrite(87(2),93(4)),flip(a)]. 98 $F. [resolve(97,a,8,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=26. Generated=420. Kept=95. proofs=1. Usable=20. Sos=34. Demods=59. Limbo=11, Disabled=35. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=325. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=88 (0 lex), Back_demodulated=28. Back_unit_deleted=0. Demod_attempts=3322. Demod_rewrites=734. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.10. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 26455 exit (max_proofs) Fri Apr 13 09:14:38 2007