Prover9 Manual Version 2009-11A

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.

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.

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

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