Checkpoint and Resume
Prover9 can save its search state to disk (checkpoint) and later resume from that saved state. This is useful for:
- Long-running proofs where you want insurance against crashes or machine reboots.
- Splitting a long run across multiple sessions.
- Examining intermediate search state.
- Moving a run to a different machine.
The checkpoint captures all clause lists, indexing metadata, symbol precedence, selector state, clause justifications, and goal formulas. When resumed, the search continues as if it had never stopped. Given clause selection, kept counts, proofs, and proof content are fully deterministic across checkpoint/resume.
See also: Mace4 Checkpoint and Resume.
Setting Up for Checkpoints
Add these options to your Prover9 input file:
set(checkpoint_ancestors). % save ancestor clauses (default: on)
The checkpoint_ancestors option saves the disabled clause list, which contains ancestor clauses needed for proof reconstruction. This is on by default. If you turn it off, proofs found after resume will show [assumption] for all checkpoint-loaded clauses instead of their real derivation history.
Optionally, to have Prover9 exit immediately after writing a checkpoint:
set(checkpoint_exit). % exit after checkpoint (default: off)
Creating a Checkpoint
While Prover9 is running, send it the SIGUSR2 signal:
kill -USR2 <pid>
To find the process ID:
ps aux | grep prover9
Or, if you started Prover9 in the background:
prover9 -f input.in > output.out 2> errors.err & echo $! # prints the PID
Prover9 will write a checkpoint directory in the current working directory and print a confirmation:
Checkpoint requested at given #15919... Checkpoint written (experimental): prover9_12345_ckpt_15919 (89685 clauses, 15 MB)
The directory name includes the process ID and given clause count: prover9_<pid>_ckpt_<given>/
If checkpoint_exit is set, Prover9 exits with code 107. Otherwise, it continues searching.
What the Checkpoint Contains
The checkpoint directory contains these files:
| File | Contents |
|---|---|
| metadata.txt | Stats, timing, selector state, version info |
| sos.clauses | Set-of-support clauses |
| usable.clauses | Usable clauses |
| demods.clauses | Demodulator clauses |
| hints.clauses | Hint clauses (if any) |
| limbo.clauses | Limbo clauses (if any) |
| disabled.clauses | Ancestor clauses (if checkpoint_ancestors is set) |
| clause_data.txt | Per-clause ID, weight, and initial flag |
| options.txt | All option settings at checkpoint time |
| precedence.txt | Symbol ordering (function/relation precedence) |
| fpa_ids.txt | FPA index term IDs (for deterministic indexing) |
| justifications.txt | Clause derivation history |
| formulas.txt | Goal formulas (if any) |
| saved_input.txt | Self-contained LADR input for standalone resume |
Typical checkpoint size is about 15% of the process memory footprint. For example, a run using ~100 MB of RAM produces a ~15 MB checkpoint.
Resuming from a Checkpoint
To resume, use the -r flag with the checkpoint directory:
prover9 -r prover9_12345_ckpt_15919 -f myprob.in > resumed.out 2> resumed.err
Important: You must supply the same input file (with -f) that was used for the original run. Prover9 reads the input file to register symbols and set up parsing infrastructure, then loads the checkpoint state on top of it.
On resume, Prover9 prints restoration messages:
% Restored 24 formulas from checkpoint. % Restored justifications for 89660 clauses from checkpoint.
The search then continues exactly where it left off.
Complete Example
1. Start a long-running proof:
prover9 -f hard_problem.in > run1.out 2> run1.err &
2. After some time, create a checkpoint:
kill -USR2 $!
3. If the machine needs to restart, or you want to stop:
kill $!
4. Later, resume from the checkpoint:
prover9 -r prover9_54321_ckpt_15919 -f hard_problem.in > run2.out 2> run2.err &
5. You can checkpoint the resumed run too:
kill -USR2 $!
This creates a new checkpoint directory with a new given count.
Checkpoint-and-Exit Workflow
If you want Prover9 to save and stop (not continue running), add set(checkpoint_exit) to your input file. After receiving SIGUSR2, Prover9 writes the checkpoint and exits with code 107.
This is useful in scripts:
#!/bin/bash
prover9 -f "$1" > run.out 2> run.err &
PID=$!
sleep 3600 # run for 1 hour
kill -USR2 $PID # request checkpoint
wait $PID
EXIT=$?
if [ $EXIT -eq 107 ]; then
echo "Checkpointed successfully"
elif [ $EXIT -eq 0 ]; then
echo "Proof found before checkpoint"
else
echo "Exited with code $EXIT"
fi
Multiple Checkpoints
You can send SIGUSR2 multiple times during a run. Each checkpoint creates a new directory with the current given count in its name:
prover9_12345_ckpt_5000/ prover9_12345_ckpt_15919/ prover9_12345_ckpt_28000/
Earlier checkpoints are not overwritten. You can resume from any of them.
Periodic Automatic Checkpoints
For long-running proofs, Prover9 can create checkpoints automatically at regular intervals:
assign(checkpoint_minutes, 30). % checkpoint every 30 minutes
This uses wall-clock time (not CPU time). The timer starts when the search phase begins. The minimum interval is 15 minutes; values between 1 and 14 are clamped to 15 with a warning.
By default, only the most recent 3 automatic checkpoint directories are kept on disk. Control this with:
assign(checkpoint_keep, 5). % keep last 5 auto checkpoints
When a new periodic checkpoint would exceed the limit, the oldest automatic checkpoint is removed:
Periodic checkpoint at given #101460... Checkpoint written (experimental): prover9_54196_ckpt_101460 (141961 clauses, 200 MB) Removing old checkpoint: prover9_54196_ckpt_52668
SIGUSR2 manual checkpoints are independent of rotation. They are not counted against the checkpoint_keep limit and are never removed automatically.
Determinism Guarantees
After resuming, the following match the original (non-checkpointed) run exactly:
- Given clause count
- Kept clause count
- Number of proofs
- Proof formulas and derivation history
- Given clause selection order (same clause IDs in same order)
The Generated count may differ by ~0.5–1% because forward-subsumed intermediate clauses depend on FPA trie traversal order, which differs slightly between bulk re-indexing (resume) and incremental insertion (normal run). This does not affect which clauses are kept or which proofs are found.
Proof Output After Resume
With checkpoint_ancestors set (the default), proofs found after resume contain the full derivation history:
24 P(D(D(D(D(D(D(D(D(x))))))))). [goal]. 25 -P(D(D(D(D(D(D(D(D(x))))))))). [deny(24)]. 27 P(f(x,f(f(x,f(x,y)),y))). [hyper(3,a,17,a)].
Without checkpoint_ancestors, all checkpoint-loaded clauses appear as [assumption]. The proof is still valid, but the derivation history is lost.
Options Reference
| Option | Default | Description |
|---|---|---|
| set(checkpoint_ancestors) | on | Save disabled clauses for proof derivation history. |
| set(checkpoint_exit) | off | Exit (code 107) after writing checkpoint. |
| assign(checkpoint_minutes, N) | -1 (disabled) | Periodic checkpoint interval in minutes (wall-clock). Minimum: 15. |
| assign(checkpoint_keep, K) | 3 | Max automatic checkpoint directories to retain. Does not affect SIGUSR2 manual checkpoints. |
Exit Codes
| Code | Meaning |
|---|---|
| 0 | Proof found (max_proofs reached) |
| 2 | SOS empty (search exhausted) |
| 3 | max_megs exceeded |
| 4 | max_seconds exceeded |
| 5 | max_given exceeded |
| 6 | max_kept exceeded |
| 7 | Action exit |
| 101 | Interrupted (SIGINT / Ctrl-C) |
| 107 | Checkpoint saved (with checkpoint_exit set) |
Backward Compatibility
Checkpoints are forward-compatible. If a checkpoint is missing newer files, Prover9 proceeds gracefully:
- Without fpa_ids.txt: search is slightly less deterministic.
- Without justifications.txt: proofs show [assumption] for checkpoint-loaded clauses.
- Without formulas.txt: proofs involving goal formulas may fail during ancestor tracing.
Troubleshooting
- "get_clanc, clause with id=N not found"
- checkpoint_ancestors was not set, so ancestor clauses are missing. Re-run with set(checkpoint_ancestors) and re-checkpoint.
- Proofs show [assumption] for all clauses
- Old checkpoint format without justifications.txt, or checkpoint_ancestors was off. Re-run with current version and set(checkpoint_ancestors).
- Checkpoint directory not created
- Prover9 checks for the signal between given clauses, not during inference. Send SIGUSR2 again after a moment.
- Different Generated count after resume
- Expected (see Determinism Guarantees). The difference is typically under 1% and does not affect proofs.