============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13012 was started by mccune on cleo.thornwood, Mon Jun 19 16:40:06 2006 The command was "/home/mccune/bin/prover9 -f cancel2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file cancel2.in clauses(sos). (x * e) * x = x. x * (x * y) = y. (x * y) * (z * u) = (x * z) * (y * u). ((x * x) * x) * x = e. end_of_list. formulas(goals). (all x all y all z (x * y = z * y -> x = z)). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal formula was negated; the result (to be placed in sos): clauses(negated_goals). c3 * c2 = c1 * c2. c3 != c1. end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 (x * e) * x = x. [input]. 2 x * (x * y) = y. [input]. 3 (x * y) * (z * u) = (x * z) * (y * u). [input]. 4 ((x * x) * x) * x = e. [input]. 5 c3 * c2 = c1 * c2. [clausify]. 6 c3 != c1. [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([ e, c1, c2, c3, * ]). After inverse_order: Function symbol precedence: lex([ e, c1, c2, c3, * ]). 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 * e) * x = x. [input]. 8 x * (x * y) = y. [input]. 9 (x * y) * (z * u) = (x * z) * (y * u). [input]. 10 ((x * x) * x) * x = e. [input]. 11 c3 * c2 = c1 * c2. [clausify]. 12 c3 != c1. [clausify]. end_of_list. clauses(demodulators). 7 (x * e) * x = x. [input]. 8 x * (x * y) = y. [input]. 10 ((x * x) * x) * x = e. [input]. 11 c3 * c2 = c1 * c2. [clausify]. 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 * e) * x = x. [input]. given #2 (I,wt=7): 8 x * (x * y) = y. [input]. given #3 (I,wt=15): 9 (x * y) * (z * u) = (x * z) * (y * u). [input]. given #4 (I,wt=9): 10 ((x * x) * x) * x = e. [input]. given #5 (I,wt=7): 11 c3 * c2 = c1 * c2. [clausify]. given #6 (I,wt=3): 12 c3 != c1. [clausify]. given #7 (F,wt=5): 13 e * e = e. [para(7(a,1),7(a,1,1)),demod(8(5)),flip(a)]. given #8 (F,wt=7): 28 c3 * (c1 * c2) = c2. [para(11(a,1),8(a,1,2))]. given #9 (T,wt=9): 22 ((x * x) * x) * e = x. [para(10(a,1),8(a,1,2))]. given #10 (T,wt=13): 14 ((x * y) * x) * (e * y) = x * y. [para(9(a,1),7(a,1))]. given #11 (A,wt=15): 15 ((x * e) * y) * (x * z) = x * (y * z). [para(7(a,1),9(a,1,1)),flip(a)]. given #12 (F,wt=11): 41 (x * y) * (e * (y * x)) = x. [para(8(a,1),14(a,1,1,1)),demod(8(7))]. given #13 (F,wt=9): 73 e * ((x * x) * e) = x. [para(10(a,1),41(a,1,2,2)),demod(67(2),72(4),13(6),67(5))]. given #14 (T,wt=9): 76 (x * x) * (e * x) = e. [para(22(a,1),41(a,1,2,2)),demod(67(3),8(5))]. given #15 (T,wt=9): 95 (e * (x * x)) * x = e. [back_demod(10),demod(67(2))]. given #16 (A,wt=15): 16 (x * (y * e)) * (z * y) = (x * z) * y. [para(7(a,1),9(a,1,2)),flip(a)]. given #17 (F,wt=9): 96 (x * x) * e = e * x. [para(73(a,1),8(a,1,2)),flip(a)]. given #18 (F,wt=9): 100 (x * e) * (x * x) = e. [para(76(a,1),9(a,1)),flip(a)]. given #19 (T,wt=9): 141 (x * e) * e = x * x. [para(100(a,1),8(a,1,2))]. given #20 (T,wt=11): 48 (c2 * c3) * (e * (c1 * c2)) = c2. [para(28(a,1),14(a,1,1,1)),demod(28(14))]. given #21 (A,wt=15): 17 (x * y) * ((x * z) * (y * u)) = z * u. [para(9(a,1),8(a,1,2))]. given #22 (F,wt=11): 67 (x * y) * x = e * (y * x). [para(41(a,1),8(a,1,2))]. given #23 (F,wt=11): 74 (c1 * c2) * (e * (c2 * c3)) = c3. [para(11(a,1),41(a,1,1))]. given #24 (T,wt=7): 212 (c1 * e) * c3 = c3. [para(74(a,1),9(a,1)),demod(8(9)),flip(a)]. given #25 (T,wt=11): 102 (e * x) * (x * x) = x * x. [para(76(a,1),41(a,1,1)),demod(8(8))]. given #26 (A,wt=15): 18 (x * y) * ((x * z) * u) = z * (y * u). [para(8(a,1),9(a,1,1)),flip(a)]. given #27 (F,wt=7): 358 c3 * (c1 * c1) = c3. [back_demod(219),demod(279(9),254(6),8(7))]. given #28 (F,wt=7): 361 c3 * c3 = c1 * c1. [para(358(a,1),8(a,1,2))]. ============================== PROOF ================================= % Proof 1 at 0.03 (+ 0.00) seconds. % Length of proof is 25. % Level of proof is 11. % Maximum clause weight is 15. % Given clauses 28. 7 (x * e) * x = x. [input]. 8 x * (x * y) = y. [input]. 9 (x * y) * (z * u) = (x * z) * (y * u). [input]. 10 ((x * x) * x) * x = e. [input]. 11 c3 * c2 = c1 * c2. [clausify]. 12 c3 != c1. [clausify]. 13 e * e = e. [para(7(a,1),7(a,1,1)),demod(8(5)),flip(a)]. 14 ((x * y) * x) * (e * y) = x * y. [para(9(a,1),7(a,1))]. 18 (x * y) * ((x * z) * u) = z * (y * u). [para(8(a,1),9(a,1,1)),flip(a)]. 22 ((x * x) * x) * e = x. [para(10(a,1),8(a,1,2))]. 41 (x * y) * (e * (y * x)) = x. [para(8(a,1),14(a,1,1,1)),demod(8(7))]. 67 (x * y) * x = e * (y * x). [para(41(a,1),8(a,1,2))]. 72 x * (e * (x * x)) = e * (x * x). [para(10(a,1),41(a,1,1)),demod(67(4),8(8),67(6))]. 73 e * ((x * x) * e) = x. [para(10(a,1),41(a,1,2,2)),demod(67(2),72(4),13(6),67(5))]. 74 (c1 * c2) * (e * (c2 * c3)) = c3. [para(11(a,1),41(a,1,1))]. 76 (x * x) * (e * x) = e. [para(22(a,1),41(a,1,2,2)),demod(67(3),8(5))]. 96 (x * x) * e = e * x. [para(73(a,1),8(a,1,2)),flip(a)]. 212 (c1 * e) * c3 = c3. [para(74(a,1),9(a,1)),demod(8(9)),flip(a)]. 219 (c3 * (c1 * e)) * (e * c3) = c3. [para(212(a,1),41(a,1,2,2))]. 254 (x * y) * e = x * (y * (e * x)). [para(76(a,1),18(a,1,2))]. 279 (x * y) * (e * x) = x * (y * e). [para(96(a,1),18(a,1,2))]. 358 c3 * (c1 * c1) = c3. [back_demod(219),demod(279(9),254(6),8(7))]. 361 c3 * c3 = c1 * c1. [para(358(a,1),8(a,1,2))]. 376 c3 = c1. [para(361(a,1),41(a,1,1)),demod(361(7),41(9)),flip(a)]. 377 $F. [resolve(376,a,12,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=28. Generated=977. Kept=370. proofs=1. Usable=17. Sos=252. Demods=153. Denials=0. Limbo=1, Disabled=105. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=607. Back_subsumed=2. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=229 (0 lex), Back_demodulated=97. Back_unit_deleted=0. Demod_attempts=12205. Demod_rewrites=1292. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.30. User_CPU=0.03, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13012 exit (max_proofs) Mon Jun 19 16:40:06 2006