Implementing an ATP System

This simple Prolog implementation of the ANL loop with full resolution for clauses forms a very weak and broken ATP system. Missing features include:

Proof output (do you trust a system that just says "yes"?)
Heuristics (gotta make it more powerful)
Doing subsumption on-the-fly (wot's this batch processing?)
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.

   Satisfiable
KRS005-1
NLP043-1
SET777-1
SWV010-1
SYN059-1
   Easiest
MGT003-1
MGT036-3
PUZ001-1
PUZ011-1
SYN068-1
   Moderate
COM003-2
FLD039-1
KRS002-1
SYN349-1
TOP004-1
   Harder
ALG002-1
COM001-1
FLD001-3
PUZ031-1
SYN729-1
   Equality
COM004-1
LCL171-3
PUZ020-1
SET845-2
SWV307-2

You must email the source code of your program to me by 29th April. Your submission will be graded according to the following.

No refutations for satisfiable sets - 0%, but prerequisite for any marks for finding solutions
Solution of Easy problems with Proof output - 3% (solve any 3)
Solution of Moderate problems with Proof output - 3% (solve any 3)
Solution of Harder problems with Proof output - 3% (solve any 3)
Solution of Equality problems with Proof output - 3% (solve any 3) (you can add axioms of equality, if you want)
Quality of proof output - 3%
Subsumption on-the-fly - 3%
Quality of Prolog code - 2%

It is worth 20% of the subject's assessment. Please review the policies on assessment in the administration document.