============================== Prover9 =============================== Prover9 (32) version 2009-02A, February 2009. Process 11137 was started by mccune on cleo, Wed Feb 25 09:31:05 2009 The command was "/home/mccune/bin/prover9 -f cancel2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file cancel2.in assign(max_seconds,30). formulas(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). x * y = z * y -> x = z. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x * y = z * y -> x = z # 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 * e) * x = x. [assumption]. x * (x * y) = y. [assumption]. (x * y) * (z * u) = (x * z) * (y * u). [assumption]. ((x * x) * x) * x = e. [assumption]. c3 * c2 = c1 * c2. [deny(1)]. c3 != 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([ e, c1, c2, c3, * ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). kept: 2 (x * e) * x = x. [assumption]. kept: 3 x * (x * y) = y. [assumption]. kept: 4 (x * y) * (z * u) = (x * z) * (y * u). [assumption]. kept: 5 ((x * x) * x) * x = e. [assumption]. kept: 6 c3 * c2 = c1 * c2. [deny(1)]. kept: 7 c3 != c1. [deny(1)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 (x * e) * x = x. [assumption]. 3 x * (x * y) = y. [assumption]. 4 (x * y) * (z * u) = (x * z) * (y * u). [assumption]. 5 ((x * x) * x) * x = e. [assumption]. 6 c3 * c2 = c1 * c2. [deny(1)]. 7 c3 != c1. [deny(1)]. end_of_list. formulas(demodulators). 2 (x * e) * x = x. [assumption]. 3 x * (x * y) = y. [assumption]. 5 ((x * x) * x) * x = e. [assumption]. 6 c3 * c2 = c1 * c2. [deny(1)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=7): 2 (x * e) * x = x. [assumption]. given #2 (I,wt=7): 3 x * (x * y) = y. [assumption]. given #3 (I,wt=15): 4 (x * y) * (z * u) = (x * z) * (y * u). [assumption]. given #4 (I,wt=9): 5 ((x * x) * x) * x = e. [assumption]. given #5 (I,wt=7): 6 c3 * c2 = c1 * c2. [deny(1)]. given #6 (I,wt=3): 7 c3 != c1. [deny(1)]. given #7 (A,wt=5): 8 e * e = e. [para(2(a,1),2(a,1,1)),rewrite([3(5)]),flip(a)]. given #8 (T,wt=7): 23 c3 * (c1 * c2) = c2. [para(6(a,1),3(a,1,2))]. given #9 (T,wt=9): 17 ((x * x) * x) * e = x. [para(5(a,1),3(a,1,2))]. given #10 (T,wt=13): 9 ((x * y) * x) * (e * y) = x * y. [para(4(a,1),2(a,1))]. given #11 (T,wt=11): 36 (x * y) * (e * (y * x)) = x. [para(3(a,1),9(a,1,1,1)),rewrite([3(7)])]. given #12 (A,wt=15): 10 ((x * e) * y) * (x * z) = x * (y * z). [para(2(a,1),4(a,1,1)),flip(a)]. given #13 (T,wt=9): 50 e * ((x * x) * e) = x. [para(5(a,1),36(a,1,2,2)),rewrite([44(2),49(4),8(6),44(5)])]. given #14 (T,wt=9): 53 (x * x) * (e * x) = e. [para(17(a,1),36(a,1,2,2)),rewrite([44(3),3(5)])]. given #15 (T,wt=9): 67 (e * (x * x)) * x = e. [back_rewrite(5),rewrite([44(2)])]. given #16 (T,wt=9): 79 (x * x) * e = e * x. [para(50(a,1),3(a,1,2)),flip(a)]. given #17 (A,wt=15): 11 (x * (y * e)) * (z * y) = (x * z) * y. [para(2(a,1),4(a,1,2)),flip(a)]. given #18 (T,wt=9): 83 (x * e) * (x * x) = e. [para(53(a,1),4(a,1)),flip(a)]. given #19 (T,wt=9): 123 (x * e) * e = x * x. [para(83(a,1),3(a,1,2))]. given #20 (T,wt=11): 43 (c2 * c3) * (e * (c1 * c2)) = c2. [para(23(a,1),9(a,1,1,1)),rewrite([23(14)])]. given #21 (T,wt=11): 44 (x * y) * x = e * (y * x). [para(36(a,1),3(a,1,2))]. given #22 (A,wt=15): 12 (x * y) * ((x * z) * (y * u)) = z * u. [para(4(a,1),3(a,1,2))]. given #23 (T,wt=11): 51 (c1 * c2) * (e * (c2 * c3)) = c3. [para(6(a,1),36(a,1,1))]. given #24 (T,wt=7): 194 (c1 * e) * c3 = c3. [para(51(a,1),4(a,1)),rewrite([3(9)]),flip(a)]. given #25 (T,wt=11): 85 (e * x) * (x * x) = x * x. [para(53(a,1),36(a,1,1)),rewrite([3(8)])]. given #26 (T,wt=11): 114 (x * e) * (x * e) = e * x. [para(11(a,2),79(a,1)),rewrite([8(3)])]. given #27 (A,wt=15): 13 (x * y) * ((x * z) * u) = z * (y * u). [para(3(a,1),4(a,1,1)),flip(a)]. given #28 (T,wt=7): 359 c3 * (c1 * c1) = c3. [back_rewrite(201),rewrite([257(9),249(6),3(7)])]. given #29 (T,wt=7): 361 c3 * c3 = c1 * c1. [para(359(a,1),3(a,1,2))]. ============================== PROOF ================================= % Proof 1 at 0.03 (+ 0.00) seconds. % Length of proof is 26. % Level of proof is 11. % Maximum clause weight is 15. % Given clauses 29. 1 x * y = z * y -> x = z # label(non_clause) # label(goal). [goal]. 2 (x * e) * x = x. [assumption]. 3 x * (x * y) = y. [assumption]. 4 (x * y) * (z * u) = (x * z) * (y * u). [assumption]. 5 ((x * x) * x) * x = e. [assumption]. 6 c3 * c2 = c1 * c2. [deny(1)]. 7 c3 != c1. [deny(1)]. 8 e * e = e. [para(2(a,1),2(a,1,1)),rewrite([3(5)]),flip(a)]. 9 ((x * y) * x) * (e * y) = x * y. [para(4(a,1),2(a,1))]. 13 (x * y) * ((x * z) * u) = z * (y * u). [para(3(a,1),4(a,1,1)),flip(a)]. 17 ((x * x) * x) * e = x. [para(5(a,1),3(a,1,2))]. 36 (x * y) * (e * (y * x)) = x. [para(3(a,1),9(a,1,1,1)),rewrite([3(7)])]. 44 (x * y) * x = e * (y * x). [para(36(a,1),3(a,1,2))]. 49 x * (e * (x * x)) = e * (x * x). [para(5(a,1),36(a,1,1)),rewrite([44(4),3(8),44(6)])]. 50 e * ((x * x) * e) = x. [para(5(a,1),36(a,1,2,2)),rewrite([44(2),49(4),8(6),44(5)])]. 51 (c1 * c2) * (e * (c2 * c3)) = c3. [para(6(a,1),36(a,1,1))]. 53 (x * x) * (e * x) = e. [para(17(a,1),36(a,1,2,2)),rewrite([44(3),3(5)])]. 79 (x * x) * e = e * x. [para(50(a,1),3(a,1,2)),flip(a)]. 194 (c1 * e) * c3 = c3. [para(51(a,1),4(a,1)),rewrite([3(9)]),flip(a)]. 201 (c3 * (c1 * e)) * (e * c3) = c3. [para(194(a,1),36(a,1,2,2))]. 249 (x * y) * e = x * (y * (e * x)). [para(53(a,1),13(a,1,2))]. 257 (x * y) * (e * x) = x * (y * e). [para(79(a,1),13(a,1,2))]. 359 c3 * (c1 * c1) = c3. [back_rewrite(201),rewrite([257(9),249(6),3(7)])]. 361 c3 * c3 = c1 * c1. [para(359(a,1),3(a,1,2))]. 375 c3 = c1. [para(361(a,1),36(a,1,1)),rewrite([361(7),36(9)]),flip(a)]. 376 $F. [resolve(375,a,7,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=29. Generated=940. Kept=374. proofs=1. Usable=18. Sos=263. Demods=157. Limbo=1, Disabled=97. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=566. Back_subsumed=2. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=230 (0 lex), Back_demodulated=89. Back_unit_deleted=0. Demod_attempts=11924. Demod_rewrites=1264. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.35. User_CPU=0.04, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11137 exit (max_proofs) Wed Feb 25 09:31:05 2009