FTP 35 vs FTP 34

[Mark Tarver]

I got some of the figures wrong here, but on one problem

FTP 35 solved it in 20,000 inferences vs FTP 34 of over

500,000 inferences.   

The reason I got the figure wrong is that I disabled the

proof construction in SBCL in order to avoid a crash.  

In fact it takes as many inferences to reconstruct the

proof as it does to find it (finding it 9,764 inferences).

That tells you that the proof process for the set theory problems

is highly deterministic and very efficient with very little

search under FTP 35.

The new system comes into its own when the axiom set

contains many definitions which in logic are generally 

expressed as equivalences.  These generate many logic

clauses.  FTP 35 has a special facility for handling these.

Mark