in('string_predicates').
 out('string_predicates.o').


 in(queue_lemmas),storeTheory(queue_lemmas).
| ?- prove(thy(queue_lemmas) => del_min_complete_induction).
| ?- prove(thy(queue_lemmas) => del_min_correct_induction).
| ?-
| ?-


in(l1),storeTheory(ba).


prove(thy(l1) =>  main_lemma_create).


restore('/HG/local/provers/saturate/bin/sat6')


 prove(thy(queue_lemmas)=>del_min_correct_induction,[option(search_depth(0))]).

prove(thy(l1) =>  main_lemma_create,[option(search_depth(1))]).




in('easy_lemmas').
prove(thy(easy_lemmas) => lm2,[option(search_depth(1))]).

in('tmp1').
prove(thy(tmp1) => lmm).
prove(thy(tmp1) => lmm,[option(search_depth(1))]).

in('induction_step').
prove(thy(induction_step) => induction_step_create).
prove(thy(induction_step) => induction_step_insert).
prove(thy(induction_step) => induction_step_delete).