Update in this version:
1. Generalise is not going to have two alternatives.
Your original version makes it 

2. no separate program for parsing or proving
(1) difference in abduce new or 
(2) new nt or not?

You could avoid having new rules by k-bound; you could also limit the number of new states by state limit
 
Still need the part about prove -> 


3. Passing down the list of invented predicates.

4. Put those long positive examples after negative examples. 
After each example you tried the negative examples