#!/usr/bin/php
<?php 
require_once("TarskiTheorems.php");
require_once("GenerateInputFiles.php");
require_once("FinalResults.php");

 
$chapter = "11";
$check_results = true;   // if true, only tries so-far-unproved theormems
$diagrams = true; 
$hints = false;
$cases = false;

$sos = false;
$directory = "SubformulaInputs";
 

$settings = array(
"set(hyper_res).",
"set(para_into).",
"set(para_from).",
"set(binary_res).",
"set(ur_res).",
"set(order_history).",
"assign(max_seconds,3600).",
"assign(max_mem,2000000).",
"clear(print_kept).",
"set(input_sos_first).",
"set(back_sub).",
"assign(bsub_hint_wt,-1).",
"set(keep_hint_subsumers).",
"assign(max_weight,16).",
"assign(max_distinct_vars,4).",
"assign(pick_given_ratio,4).",
"assign(max_proofs,1)."
);

$theorems = TheoremsByChapter($chapter);
foreach($theorems as $t)
	{  $results = $TarskiFinalResults[$t->name];
	   if(is_numeric($results))
			continue;  // already proved this result automatically without hints
	   if(is_array($results) && $results[1] == "diagram")
			continue;  // already proved this result automatically without hints
	   if(is_array($results) && $results[1] == "subformula")
			continue;  // already proved this theorem, don't try it again
	   if(!$check_results || $TarskiFinalResults[$t->name]===false)
		 {  WriteInputFile($t, $directory, $diagrams, $settings, $sos, $cases);
			$theorem_name = $t->name;
			InsertSubformulaHintsIntoInputFile($t, $directory);
			$infile = $directory . "/" . $theorem_name . ".in";
			$outfile = $directory . "/" . $theorem_name . ".out";
			
			echo "Trying to prove $theorem_name with subformula strategy";
			exec( "otter < $infile > $outfile");
		 }
	}
?>