Implementing an ATP System

This simple Prolog implementation of the ANL loop with binary resolution for clauses forms a very weak and broken ATP system. Missing features, in decreasing order of importance, include:

Full resolution or Factoring (binary is not enough)
Heuristics (gotta make it more powerful)
Subsumption (you can't live without it)
Proof output (do you trust a system that just says "yes"?)
Equality reasoning (those axioms will kill you)

Take this simple implementation, and implement the missing features. You should aim to produce an ATP system that can solve (and output proofs for) as many of the TPTP problems listed below as possible, with a 60 second time limit per problem.

I might update this list in the next week or two

   Satisfiable
KRS005-1 NLP043-1 SET777-1 SWV010-1 SYN059-1    Easy
PUZ001-1 PUZ011-1 SYN003-1.006 SYN009-3 SYN068-1    Moderate
COM003-2 KRS002-1 MGT036-3 SWV292-2 SYN328-1    Harder
ALG002-1 GRP001-5 FLD001-3 LCL064-1 PUZ031-1    Equality
COM004-1 LCL171-3 PUZ020-1 SET845-2 SWV307-2

Here is a .tgz of all the problems with the include directives expanded.
Here is a program you can run in SWI to test your ATP system on all the problems (the equality problems with axioms are used).

You must email the source code of your program to me by 4th December (AoE). Your submission will be graded according to the following (all testing will use a 60s CPU time limit). It is worth 25% of the subject's assessment.

No refutations for satisfiable sets - 0%, but prerequisite to any marks for finding solutions
Solution of Easy problems - 5% (solve all 5)
Solution of Moderate problems - 4% (solve any 4)
Solution of Harder problems - 3% (solve any 3)
Solution of Equality problems - 3% (solve any 3) (you can add axioms of equality, if you want)
Quality of proof output - 3%
Quality of Prolog code - 2%

Please review the policies on assessment in the administration document.