Modified proofs for new claset primitives. The problem is that they enforce the "most recent added rule has priority" policy more strictly now.

Modified proofs for new claset primitives. The problem is that they enforce the "most recent added rule has priority" policy more strictly now.

Recoded addSIs, etc., so that nets are built incrementally instead of from scratch each time. The old approach used excessive time (>1 sec for adding a rule to ZF_cs) and probably excessive space. Now rep_claset includes all record fields. joinrules no longer sorts the rules on number of subgoals, since it does not see the full set of them; instead the number of subgoals modifies the priority.