OTTER settings

include(quiet).

set(unit_deletion).           %
set(ur_res).                  % 
set(para_into).               %   
set(para_from).               %  cancelled at one point
set(back_demod).              %
assign(pick_given_ratio,3).
assign(max_weight,1000).
assign(max_proofs,1).

set(interactive_given).

set(control_memory).

In a first attempt at a proof I generally used the above options as my default settings for OTTER. I always turned off the interactive selection of given clauses by entering 0 immediately. If the search failed, I used interactive_given to help me debug the input file and the search options. All of the final proofs in this document were obtained with no human intervention in the selection of given clauses.

The included file quiet contains the following commands:

clear(print_kept).
clear(print_new_demod).
clear(print_back_sub).
clear(print_back_demod).
assign(max_mem,24000).
set(bird_print).

These prevent the output file from being too big, limit the main memory usage, and cause the output to be printed in an easier-to-read standard notation for combinatory logic.

Various combinations of the following "emergency measures" were tried whenever the first attempt at proof failed.

Emergency measures

up show outline