Prover9 Manual |  | Version 2009-02A

# Output Files

Even when Prover9 fails to find a proof, its output file usually has lots of valuable information about the search. The output file can suggest many ways of improving the search for subsequent jobs as in the following examples.

- 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 output files are divided into sections and subsections so the users (people and programs) can find what they are looking for. The delimiters are self-explanatory. A few comments about the sections are given here. For a specific example, see the output file subset_trans.out.

    ============================== 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 =========================

## Clause Justifications

After the initial stage of the output, each clause in the file has an integer identifier (ID) and a justification that may refer to IDs of other clauses. A justification is a list consisting of one primary step and some number of secondary steps. Most primary steps are inference rules applied to given clauses, and most secondary steps consist of simplification, rewriting, or orienting equalities.

Many of the types of step refer to positions of literals or terms in the parent clauses. Literals are identified by the characters 'a' (first literal), 'b' (second literal), etc. Terms are identified by the literal identifier followed by a sequence of integers giving the position of the term within the literal. For example, the position 'c,1,3,2' means third literal, first argument, third argument, second argument. Negation signs on literals are not included in the sequence.

Primary Steps.

- `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

Prover9 proofs may be transformed by separate programs, e.g., by Prooftrans.

## Options That Say What Goes To the Output File

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

> Clearing this flag suppresses printing of clauses, formulas, weighting rules (and everything else that ends with `end_of_list`) that would ordinarily appear in the `INPUT` section of the output file.

    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).

> If this flag is set, clauses are printed in the `PROCESS INITIAL CLAUSES` and `CLAUSES FOR SEARCH` sections of the output file.

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

> Clearing this flag prevents given clauses from being printed to the output file.

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

> Setting this flag causes all generated clauses to be printed to the the output file. In addition, some other information about the processing of each generated clause is printed. This flag can be output files to be really huge.

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

> Setting this flag causes all kept clauses to be printed to the the output file. In addition, some other information on the processing of kept clauses is printed.

    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

> Setting this flag causes several properties of clauses to be printed as "props" attributes on the clauses. The properties include which literals are maximal (counting from 1), which literals are maximal among literals of the same sign, and which literals are selected for application of inference rules.

    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).

> Setting this flag restores most of the output flags and parameters to their default values. Clearing this flag does nothing.

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

> If n > 0, statistics are sent to the output file approximately every n seconds. (On Unix-like systems, one can also tell Prover9 to print statistics to the output file by sending the signal `USR1` to a running Prover9 process, e.g., `kill -USR1 4223`.)

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

> This parameter determines how many statistics are sent to the output file.

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

> If this flag is set, various operations during the Prover9 job are timed (e.g., inference, demodulation, and subsumption), and timing reports are sent to the output file.

> Timing the operations can be expensive, especially in Solaris and Macintosh systems. On Linux systems, `set(clocks)` typically adds 5% -- 10% to the run time.

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

> If this flag is set, Prover9 beeps when important things happen, such as proofs and warnings. Some users run searches that find hundreds of proofs, and they clear this flag to prevent all of the beeping.

Next Section: Weighting