Extending the hol2fol to capture ground and normalized 
schema terms. An instance of a proof schema
now can be transformed to a proof which contains FOL expressions
only. The indexed variables are transformed to a fol-functions. 








git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1517 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
The indexed-first-order variable was not correctly
mapped to a first-order variable. Now it is mapped correctly.






git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1518 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
The clause set of an instance of a proof schema was 
transformed to a first-order clause-set which was
refuted by Prover9 and the obtained proof was
transformed to an LKProof. The next step is to 
plug the projections and construct the ACNF.











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