Prover9 Manual		Version 2009-02A

Output Files

• The output shows how equalities are oriented; different term ordering parameters may give better or more intuitive orientations.
• If Prover9 focused the search on uninteresting clauses (see the sequence of given clauses), different inference rules, a different pick_given_ratio, or a specialized weighting function can be used.
• If Prover9 ran out of time or memory with a huge sos list and small usable list (i.e., few given clauses were used), the sos_limit should be reduced.

Basic Structure of Output Files

============================== Prover9 ===============================
    Version, date, host computer, command.
============================== end of head ===========================

============================== INPUT =================================
    Echo of the input.  Everything in this section that is not
    in the input is commented with "%", so copy-and-paste can be
    done on this section to create a new input file.
============================== end of input ==========================

============================== PROCESS GOALS =========================
    The search is always by refutation, and this section shows
    how goals are negated in preparation for the search.
============================== end of process goals ==================

============================== PROCESS INITIAL CLAUSES ===============
    This section shows the starting clauses (after Skomemization,
    if applicable) and then some of what Prover9 does in preparation
    for the search.  This includes predicate_elim, term ordering
    decisions, and auto_inference settings.  At this stage, clauses
    may be deleted by subsumption and equations may be copied to the
    list demodulators.  See the flag process_initial_sos.
============================== end of process initial clauses ========

============================== CLAUSES FOR SEARCH ====================
    This section shows the clauses just before the start of the
    search, that is, just before selection of the first given clause.
    
============================== end of clauses for search =============

============================== SEARCH ================================
    This section typically shows the sequence of given clauses,
    and it may also include PROOF and STATISTICS sections.

============================== PROOF =================================
    A proof in standard form.
============================== end of proof ==========================

============================== STATISTICS ============================
    We encourage users to look at statistics!
============================== end of statistics =====================

============================== end of search =========================

• assumption -- input formula.
• clausify -- from CNF translation of a non-clausal assumption.
• goal -- input formula.
• deny -- from CNF translation of the negation of a goal.
• resolve(59,b,47,c) -- resolve the second literal of clause 59 with the third literal of clause 47.
• hyper(59, b,47,a, c,38,a) -- hyperresolution; interpret the list as a clause ID followed by a sequence of triples, <literal,clause-ID,literal> the inference is presented as a sequence of binary resolution steps. In the example shown, start with clause 59; then resolve literal b with clause 47 on literal a; with the result of the first step, resolve literal c with clause 38 on literal a. The special case "xx" means resolution with x=x.
• ur(39, a,48,a, b,88,a, c,87,a, d,86,a) -- unit-resulting resolution; the list is interpreted as in hyperresolution.
• para(47(a,1),28(a,1,2,2,1)) -- paramodulate from the clause 47 into clause 28 at the positions shown.
• copy(59) -- copy clause 59.
• back_rewite(59) -- copy clause 59.
• back_unit_del(59) -- copy clause 59.
• new_symbol(59) -- introduce a new constant (see parameter new_constants).
• factor(59,b,c) -- factor clause 59 by unifying the second and third literals.
• xx_res(59,b) -- resolve the second literal of clause 59 with x=x.
• propositional -- not used in standard proofs.
• instantiate -- not used in standard proofs.
• ivy -- not used in standard proofs.

Secondary Steps (each assumes a working clause, which is either the result of a primary step or a previous secondary step).

• rewrite([38(5,R),47(5),59(6,R)]) -- rewriting (demodulation) with equations 38, 47, then 59; the arguments (5), (5), and (6) identify the positions of the rewritten subterms (in an obscure way), and the argument R indicates that the demodulator is used backward (right-to-left).
• flip(c) -- the third literal is an equality that has been flipped by the term ordering. This does not necessarily mean that the equality is orientable by the primary term ordering, e.g., KBO.
• merge(d) -- the fourth literal has been removed because it was identical to a preceding literal.
• unit_del(b,38) -- the second literal has been removed because it was an instance of the negation clause 38 (which is a unit clause).
• xx(b) -- the second literal has been removed because it was an instance of x!=x.

Standard Proofs

Options That Say What Goes To the Output File

set(echo_input).    % default set
clear(echo_input).

set(quiet).
clear(quiet).    % default clear

Setting this flag causes most messages to the standard error file (usually the user's screen) to be suppressed. These messages include notifications about proofs and statistics reports, and warnings about demodulation limits. Setting this flag also suppresses several messages to the ordinary output file, and it clears the bell flag.

set(print_initial_clauses).    % default set
clear(print_initial_clauses).

set(print_given).    % default set
clear(print_given).

set(print_gen).
clear(print_gen).    % default clear

set(print_kept).
clear(print_kept).    % default clear

set(print_labeled).
clear(print_labeled).    % default clear

Setting this flag causes kept clauses containing label attributes to be printed, even when the flag print_kept is clear. This flag is useful when using the hints strategy, because when a clause matches a hint containing a label, the label is copied to the clause. That is, clauses matching labeled hints will be printed.

set(print_clause_properties).
clear(print_clause_properties).    % default clear

set(print_proofs).    % default set
clear(print_proofs).

Clearing this flag prevents proofs from being printed to the output file. The proof message still goes to the standard error file (usually the user's screen), unless the flag quiet has been set.

set(default_output).    % default set
clear(default_output).

assign(report, n).  % default n=-1, range [-1 .. INT_MAX]

assign(stats, string).  % default string=lots, range [none,some,lots,all]

set(clocks).
clear(clocks).    % default clear

set(bell).    % default set
clear(bell).