============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 4311 was started by mccune on cleo, Tue Nov 3 09:38:21 2009 The command was "/home/mccune/LADR/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(non_clause) # 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: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, *, /, \ ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). kept: 2 x * (x \ y) = y. [assumption]. kept: 3 x \ (x * y) = y. [assumption]. kept: 4 (x / y) * y = x. [assumption]. kept: 5 (x * y) / y = x. [assumption]. kept: 6 x * (y * (y * x)) = y * x. [assumption]. 7 c1 * (c1 * c2) != c2 * c1. [deny(1)]. kept: 8 c2 * c1 != c1 * (c1 * c2). [copy(7),flip(a)]. ============================== 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.01 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): 44 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.02 (+ 0.00) seconds. % Length of proof is 27. % Level of proof is 12. % Maximum clause weight is 15.000. % Given clauses 26. 1 y * (y * x) = x * y # label(non_clause) # 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=409. Kept=95. proofs=1. Usable=20. Sos=34. Demods=59. Limbo=11, Disabled=35. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=314. 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=3249. Demod_rewrites=718. 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.02, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4311 exit (max_proofs) Tue Nov 3 09:38:21 2009