set(print_subproblems). % default set
clear(print_subproblems).
This flag is consulted when the FOF reduction procedure is in use.
If the flag is set, each subproblem is printed just before
search starts on that subproblem.
An Example of FOF Reduction
This example was given by Peter Andrews as a challenge problem for resolution
systems in the 1970s. Prover9's miniscope procedure reduces it to 32
trivial subproblems. (More powerful miniscope methods can solve the problem
by reducing it to 0 subproblems.)
prover9 -f andrews.in > andrews.out
Here is the same problem without FOF reduction.
prover9 -f andrews2.in > andrews2.out
The preceding example is artificial and seems tailor-made for FOF reduction.
Other, more realistic examples can be found in the