STANDARD.TXT           2001 January 7

The STANDARD.IN file is our starting point for proving most theorems.
To use it, we have to do the following steps:

1. Replace the sos list with the negation of the statement of the
   theorem to be proved.

2. Unblock terms expected to occur in the proof by reducing their
   weights from 100 to something less, often 1, or else increase
   max_weight to something greater than 100.  The latter approach
   works only for rather simple theorems.  

3. One may need to adjust the inference rules and assignments.
   For some theorems one may need to use binary_res, or one
   may need to assign a nonzero value to max_distinct_vars.
   One often needs to adjust the value of max_weight. Starting 
   with sos_queue makes it easy to monitor the number of kept
   clauses on each level. When these grow too rapidly, one may 
   need to take action to cope with combinatorial explosion; 
   examining the clause dump in the output file often helps. 
  
4. One occasionally needs to block demodulators that interfere
   with the proof by remarking out an include statement.

I am sometimes not completely satisfied with the first proof that Otter
finds. After Otter finds a proof one can sometimes quickly find a
shorter proof by adjusting max_weight. I often use the Perl script
MAXWT.PL to find out what is the highest weight in the first proof
found, and then try lowering the assignment for max_weight to be less
than that to see if a less complicated proof can be found.  Sometimes
a non-minimal value for max_weight yields a shorter proof. Blocking
terms that observed not to occur in the first proof can dramatically
reduce run time and the size of the output file, thereby encouraging
further experimentation. Other techniques for shortening proofs include
assigning a low value to max_literals, or using pick_given_ratio instead
of sos_queue. Larry Wos suggests many more techniques in his writings.
Go read his books and papers!