THORN 16 - increase in performance wrt equality

[dr.mt...@gmail.com]

THORN 16 evolved from THORN 15 while working on program verification.

Equality was added late in the development of THORN but it turns out to be 

heavily used in the formalisation of Shen programs.  There I found THORN 15 lagged

in performance (not inference speed, but problem solving speed).  The following

was timed.

(<-kb [eq [append [append [] %30798] %30856] [append [] [append %30798 %30856]]])

run time: 767.4219970703125 secs
356877005 inferences

true : boolean

given  axioms wrt append detailing types etc.

The solution turned out to be term ordering wrt compilation of equality clauses whereby

complex terms are written to simpler ones.   This produced an interesting result.

(<-kb [eq [append [append [] %30798] %30856] [append [] [append %30798 %30856]]])

run time: 0.0 secs
3624 inferences
true

which is more like it.   Five orders of magnitude.  

Mark