============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13017 was started by mccune on cleo.thornwood, Mon Jun 19 16:40:19 2006 The command was "/home/mccune/bin/prover9 -f qg1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file qg1.in clauses(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. clauses(goals). x * (x * y) = y * x. end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). c2 * c1 != c1 * (c1 * c2). end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x * (x \ y) = y. [input]. 2 x \ (x * y) = y. [input]. 3 (x / y) * y = x. [input]. 4 (x * y) / y = x. [input]. 5 x * (y * (y * x)) = y * x. [input]. 6 c2 * c1 != c1 * (c1 * c2). [clausify]. 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([ c1, c2, *, /, \ ]). After inverse_order: Function symbol precedence: lex([ c1, c2, *, /, \ ]). 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: clauses(usable). end_of_list. clauses(sos). 7 x * (x \ y) = y. [input]. 8 x \ (x * y) = y. [input]. 9 (x / y) * y = x. [input]. 10 (x * y) / y = x. [input]. 11 x * (y * (y * x)) = y * x. [input]. 12 c2 * c1 != c1 * (c1 * c2). [clausify]. end_of_list. clauses(demodulators). 7 x * (x \ y) = y. [input]. 8 x \ (x * y) = y. [input]. 9 (x / y) * y = x. [input]. 10 (x * y) / y = x. [input]. 11 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=7): 7 x * (x \ y) = y. [input]. given #2 (I,wt=7): 8 x \ (x * y) = y. [input]. given #3 (I,wt=7): 9 (x / y) * y = x. [input]. given #4 (I,wt=7): 10 (x * y) / y = x. [input]. given #5 (I,wt=11): 11 x * (y * (y * x)) = y * x. [input]. given #6 (I,wt=9): 12 c2 * c1 != c1 * (c1 * c2). [clausify]. given #7 (F,wt=7): 13 (x / y) \ x = y. [para(9(a,1),8(a,1,2))]. given #8 (F,wt=7): 14 x / (y \ x) = y. [para(7(a,1),10(a,1,1))]. given #9 (T,wt=9): 15 (x \ y) * (x * y) = y. [para(7(a,1),11(a,1,2,2)),demod(7(5))]. given #10 (T,wt=9): 17 x * ((y / x) * y) = y. [para(9(a,1),11(a,1,2,2)),demod(9(5))]. given #11 (A,wt=11): 18 (x * y) / (x * (x * y)) = y. [para(11(a,1),10(a,1,1))]. given #12 (F,wt=5): 31 x * x = x. [para(9(a,1),17(a,1,2))]. given #13 (F,wt=5): 33 x / x = x. [para(11(a,1),18(a,1,2)),demod(31(1),31(1),31(1),31(2))]. given #14 (T,wt=9): 35 (x / (x / y)) * x = y. [back_demod(29),demod(34(3))]. given #15 (T,wt=9): 36 x \ y = (y / x) * y. [back_demod(24),demod(34(3))]. given #16 (A,wt=15): 19 (x * (x * y)) * (y * (x * y)) = x * y. [para(11(a,1),11(a,1,2,2)),demod(11(8))]. given #17 (F,wt=9): 38 x / (x / y) = y / x. [para(35(a,1),10(a,1,1)),flip(a)]. given #18 (F,wt=9): 44 (x / y) * (y / x) = y. [para(38(a,1),9(a,1,1))]. given #19 (T,wt=11): 32 ((x / y) * x) * (y * x) = x. [para(17(a,1),11(a,1,2,2)),demod(17(7))]. given #20 (T,wt=11): 34 x / (y * x) = (x / y) * x. [para(17(a,1),18(a,1,1)),demod(17(3))]. given #21 (A,wt=11): 39 x * ((x / (x / y)) * y) = y. [para(35(a,1),11(a,1,2,2)),demod(35(7))]. given #22 (F,wt=11): 45 (x * y) / x = (y / x) * y. [para(10(a,1),38(a,1,2)),demod(34(4))]. given #23 (F,wt=11): 46 (x / (y / x)) * x = x / y. [para(38(a,1),35(a,1,1,2))]. given #24 (T,wt=11): 50 (x / y) / x = x / (y / x). [para(38(a,1),38(a,1,2)),flip(a)]. given #25 (T,wt=11): 51 x / (y / (y / x)) = y / x. [para(38(a,2),38(a,1,2))]. given #26 (A,wt=19): 40 (x * (y * x)) * ((y * (y * x)) * (y * x)) = y * x. [para(19(a,1),11(a,1,2,2)),demod(19(12))]. given #27 (F,wt=11): 53 ((x / y) * x) * y = y * x. [para(10(a,1),44(a,1,2)),demod(34(2))]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 25. % Level of proof is 12. % Maximum clause weight is 15. % Given clauses 27. 7 x * (x \ y) = y. [input]. 8 x \ (x * y) = y. [input]. 9 (x / y) * y = x. [input]. 10 (x * y) / y = x. [input]. 11 x * (y * (y * x)) = y * x. [input]. 12 c2 * c1 != c1 * (c1 * c2). [clausify]. 13 (x / y) \ x = y. [para(9(a,1),8(a,1,2))]. 15 (x \ y) * (x * y) = y. [para(7(a,1),11(a,1,2,2)),demod(7(5))]. 17 x * ((y / x) * y) = y. [para(9(a,1),11(a,1,2,2)),demod(9(5))]. 18 (x * y) / (x * (x * y)) = y. [para(11(a,1),10(a,1,1))]. 19 (x * (x * y)) * (y * (x * y)) = x * y. [para(11(a,1),11(a,1,2,2)),demod(11(8))]. 24 x \ y = y / (x * y). [para(15(a,1),10(a,1,1)),flip(a)]. 29 x / ((x / y) * x) = y. [back_demod(13),demod(24(2))]. 32 ((x / y) * x) * (y * x) = x. [para(17(a,1),11(a,1,2,2)),demod(17(7))]. 34 x / (y * x) = (x / y) * x. [para(17(a,1),18(a,1,1)),demod(17(3))]. 35 (x / (x / y)) * x = y. [back_demod(29),demod(34(3))]. 38 x / (x / y) = y / x. [para(35(a,1),10(a,1,1)),flip(a)]. 44 (x / y) * (y / x) = y. [para(38(a,1),9(a,1,1))]. 45 (x * y) / x = (y / x) * y. [para(10(a,1),38(a,1,2)),demod(34(4))]. 53 ((x / y) * x) * y = y * x. [para(10(a,1),44(a,1,2)),demod(34(2))]. 98 (x / y) * x = y * (x / y). [para(35(a,1),53(a,1,1)),flip(a)]. 101 (x * (y / x)) * x = x * y. [para(53(a,1),19(a,2)),demod(98(2),98(4),98(8),19(11))]. 104 (x * (y / x)) * (x * y) = y. [para(32(a,1),53(a,2)),demod(98(3),98(6),98(9),101(10))]. 108 x * (x * y) = y * x. [para(45(a,1),53(a,1,1,1)),demod(98(2),104(4)),flip(a)]. 109 $F. [resolve(108,a,12,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=27. Generated=484. Kept=102. proofs=1. Usable=21. Sos=39. Demods=65. Denials=0. 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=4615. 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 13017 exit (max_proofs) Mon Jun 19 16:40:19 2006