1. mprover: count mace4 search in max_seconds?

2. compress all clauses?  DONE (I hope)

3. get_given_clause: SOS1, SOS2: fix in case one isn't being used.  ??

4. KBO weights, auto and manual.  DONE

5. RPO working??  DONE

6. expand_eq_defs  (by arity)  DONE

7. output default order  DONE

8. free (instead of compress) disabled clauses ??  used_flag??

9. cannot introduce constants in forked search. DONE?

10. xproof fails with new_constant if secondary justifications (c0!=c1). DONE?

11. FOF reduction: before starting subproblems, check for $c or $f symbols.

12. If lex command, don't do inverse_order, unfold_eq_defs.

13. If lex command without all symbols, put unspecified ones at start. DONE

14. RPO orients: (x*y)*z = E*(x*(E*(x*(E*(y*(E*(x*(E*(x*(E*z)))))))))). OK

15. check in_use clause flag and clause compression. DONE

16. proof from predicate elim not reported; DONE.

17. p & -p not proved without process_initial_sos.  DONE.

18. Check for more than one unary func when explicit kb weight 0.

=========================================================

19. Auto_denials: give warning if denials share constants.  DONE

20. Auto_denials: maybe check if all get proved.

21. Auto_denials: maybe check if some get subsumed.

22. Clean up Clause/Tformula.  DONE

23. Non-clausal goals with actions: actions don't always get copied to denial.

24. cac_redundancy: allow all wt=11?  Check efficiency.

=========================================================

25. Memory leak in isofilter??  (when most are isomorphic)  DONE (zap_interp)

26. Interpformat option to output only specified operations.

27. Prover9: Level message when part added to breadth-first. DONE

28. Too many op commands generated by prooftrans. DONE.

29. Separate term ordering stuff (eq_defs, inverse_order) from auto_inference.

30. Give message for auto_denials with non-Horn. DONE

31. Check binary factoring.  See factor.in.

================================ ADAM-2007

32. Isofilter: quiet option, which removes "1000 interps" messages.  DONE

33. Prover9: automatic disabling of back subsumption at 500 given clauses
	can cause problems; make it an option?  DONE

34. LADR: give users the option of redeclaring built-in operations,
	e.g., redeclare(conjuntion, and) changes conjunction from
	the default "&" to "and".  DONE

35. Interpformat: New format so that models can be easily parsed
	by python, perl, etc.  DONE

36. Package manual and examples for offline Windows users.

37. Prover9: Rethink hints processing w.r.t. redundant hints.

38. Prover9: Predicate elimination can multiple proofs with multiple goals.