A proof schema was instantiated to a HOL LK proof. 
The clause set was extracted and refuted by Prover9. 
The resolution proof was converted to a first-order LK proof. 
The projections of the instantiated HOL proof were computed.
A small problem is the application of the ground substitution
which was obtained by the resolution refutation. We have to 
discuss this issue.
The first-order LK proof which contains only cuts was transformed
to a HOL LK proof which serves as a skeleton of the ACNF.
We can consider that the usual CERES method is now 
available in GAPT. Soon I will integrate the functionality also
in the cli.







git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1521 85d21ef8-add0-11de-ae77-5bfb9c5a3f34