equal
deleted
inserted
replaced
8 |
8 |
9 Use the "mesonlog" shell script to process logs. |
9 Use the "mesonlog" shell script to process logs. |
10 |
10 |
11 show_hyps := false; |
11 show_hyps := false; |
12 |
12 |
13 keep_derivs := MinDeriv; |
13 proofs := 0; |
14 by (rtac ccontr 1); |
14 by (rtac ccontr 1); |
15 val [prem] = gethyps 1; |
15 val [prem] = gethyps 1; |
16 val nnf = make_nnf prem; |
16 val nnf = make_nnf prem; |
17 val xsko = skolemize nnf; |
17 val xsko = skolemize nnf; |
18 by (cut_facts_tac [xsko] 1 THEN REPEAT (etac exE 1)); |
18 by (cut_facts_tac [xsko] 1 THEN REPEAT (etac exE 1)); |
21 val horns = make_horns clauses; |
21 val horns = make_horns clauses; |
22 val goes = gocls clauses; |
22 val goes = gocls clauses; |
23 |
23 |
24 Goal "False"; |
24 Goal "False"; |
25 by (resolve_tac goes 1); |
25 by (resolve_tac goes 1); |
26 keep_derivs := FullDeriv; |
26 proofs := 2; |
27 |
27 |
28 by (prolog_step_tac horns 1); |
28 by (prolog_step_tac horns 1); |
29 by (iter_deepen_prolog_tac horns); |
29 by (iter_deepen_prolog_tac horns); |
30 by (depth_prolog_tac horns); |
30 by (depth_prolog_tac horns); |
31 by (best_prolog_tac size_of_subgoals horns); |
31 by (best_prolog_tac size_of_subgoals horns); |