|Prover9 Manual||Version 2009-11A|
============================== 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 =========================
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.
Secondary Steps (each assumes a working clause, which is either the result of a primary step or a previous secondary step).
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.