Move the mouse cursor over the red justifications after the generated clauses below to highlight the corresponding parent literals (i.e. the from, into or resolved literals in the parent clauses) . "Active" literals (like the from literal in a paramodulation, or the satellites in a hyperresolution step) get a red background, the other ones a blue one. Not all justifications work and no effort is made to highlight subterms of literals.
Highlighting is "sticky" and stays around until a different justification is highlighted (so that one can scroll around large output sets)
If there is more than one clause with the same number (those will always be identical) , only the first occurence gets highlighted.
============================== Prover9 =============================== Prover9 (64) version 2009-11A, November 2009. Process 16775 was started by hlub on karawanken, Tue Aug 24 10:23:06 2010 The command was "prover9". ============================== end of head =========================== ============================== INPUT ================================= formulas(sos). e * x = x. x' * x = e. (x * y) * z = x * (y * z). x * x = e. end_of_list. formulas(goals). x * y = y * x. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x * y = y * x # 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). e * x = x. [assumption]. x' * x = e. [assumption]. (x * y) * z = x * (y * z). [assumption]. x * x = e. [assumption]. c2 * c1 != c1 * c2. [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, *, ' ]). After inverse_order: Function symbol precedence: function_order([ e, c1, c2, *, ' ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). kept: 2 e * x = x. [assumption]. kept: 3 x' * x = e. [assumption]. kept: 4 (x * y) * z = x * (y * z). [assumption]. kept: 5 x * x = e. [assumption]. kept: 6 c2 * c1 != c1 * c2. [deny(1)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 e * x = x. [assumption]. 3 x' * x = e. [assumption]. 4 (x * y) * z = x * (y * z). [assumption]. 5 x * x = e. [assumption]. 6 c2 * c1 != c1 * c2. [deny(1)]. end_of_list. formulas(demodulators). 2 e * x = x. [assumption]. 3 x' * x = e. [assumption]. 4 (x * y) * z = x * (y * z). [assumption]. 5 x * x = e. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.02 seconds. given #1 (I,wt=5): 2 e * x = x. [assumption]. given #2 (I,wt=6): 3 x' * x = e. [assumption]. given #3 (I,wt=11): 4 (x * y) * z = x * (y * z). [assumption]. given #4 (I,wt=5): 5 x * x = e. [assumption]. given #5 (I,wt=7): 6 c2 * c1 != c1 * c2. [deny(1)]. given #6 (A,wt=8): 7 x' * (x * y) = y. [para(3(a,1),4(a,1,1)), rewrite([2(2)]), flip(a)]. given #7 (T,wt=4): 15 x' = x. [back_rewrite(11), rewrite([13(4)])]. given #8 (T,wt=5): 16 x * e = x. [back_rewrite(13), rewrite([15(1)])]. given #9 (T,wt=7): 8 x * (x * y) = y. [para(5(a,1),4(a,1,1)), rewrite([2(2)]), flip(a)]. given #10 (T,wt=9): 9 x * (y * (x * y)) = e. [para(5(a,1),4(a,1)), flip(a)]. given #11 (A,wt=11): 17 x * (y * (x * (y * z))) = z. [back_rewrite(12), rewrite([15(2),4(4)])]. given #12 (T,wt=7): 19 x * (y * x) = y. [para(9(a,1),8(a,1,2)), rewrite([16(2)]), flip(a)]. % Operation * is commutative; C redundancy checks enabled. ============================== PROOF ================================= % Proof 1 at 0.02 (+ 0.00) seconds. % Length of proof is 16. % Level of proof is 7. % Maximum clause weight is 11.000. % Given clauses 12. 1 x * y = y * x # label(non_clause) # label(goal). [goal]. 2 e * x = x. [assumption]. 3 x' * x = e. [assumption]. 4 (x * y) * z = x * (y * z). [assumption]. 5 x * x = e. [assumption]. 6 c2 * c1 != c1 * c2. [deny(1)]. 7 x' * (x * y) = y. [para(3(a,1),4(a,1,1)), rewrite([2(2)]), flip(a)]. 8 x * (x * y) = y. [para(5(a,1),4(a,1,1)), rewrite([2(2)]), flip(a)]. 9 x * (y * (x * y)) = e. [para(5(a,1),4(a,1)), flip(a)]. 11 x'' * e = x. [para(3(a,1),7(a,1,2))]. 13 x' * e = x. [para(5(a,1),7(a,1,2))]. 15 x' = x. [back_rewrite(11), rewrite([13(4)])]. 16 x * e = x. [back_rewrite(13), rewrite([15(1)])]. 19 x * (y * x) = y. [para(9(a,1),8(a,1,2)), rewrite([16(2)]), flip(a)]. 24 x * y = y * x. [para(19(a,1),8(a,1,2))]. 25 $F. [resolve(24,a,6,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=12. Generated=118. Kept=23. proofs=1. Usable=8. Sos=3. Demods=12. Limbo=2, Disabled=14. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=95. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=21 (0 lex), Back_demodulated=9. Back_unit_deleted=0. Demod_attempts=702. Demod_rewrites=156. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.06. User_CPU=0.02, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 16775 exit (max_proofs) Tue Aug 24 10:23:06 2010