An example script for provers

#!/usr/bin/python3
# -*- coding: utf-8 -*-
#
# Runs prover on problems, collects results
#
# Call on the command line 


import sys, csv
import datetime
import subprocess

# ====== configuration globals ======

# problems.csv should contain problem names, 
# one per line, without a folder and without the .p suffix, like this (remove #):
# NUM847+1 
# CSR028+3 
# NUM304+1
# ...


problems_filename="problems.csv" 

# the Problems folder of TPTP:

problem_path="/opt/TPTP/Problems/"

# summary results of running on problems:

# NB! if you stop the runner and restart, it will continue
# from the last problem NOT in the outfile.
# I.e. to run again from scratch, remove outfile

outfile="example_result.txt"

# folder for storing problem running logs:

log_folder="/tmp/"

# time in seconds per problem:

timeout=20

# ====== globals set in code =========

problem_list=[] 


# ====== top level =========

def main():
  global problems_list
  problem_list=read_problems()
  solved=read_solved()  
  #print(problem_list)
  i=0 
  of=open(outfile,"a")
  while i<len(problem_list):    
    problem=problem_list[i]
    if not solved:
      pass
    elif solved and problem!=solved:
      i+=1
      continue
    else:
      solved=False
      i=i+1 
      problem=problem_list[i]
    #print(problem)
    res=runone(problem)
    if res[0]:
      of.write(problem+",Proved,"+res[1]+","+res[2]+","+res[3]+"\n")
    else:
      of.write(problem+",Failed,"+res[1]+","+res[2]+","+str(timeout)+"\n")        
    of.flush()    
    i+=1
  of.close()  

def runone(problem):  
  global timeout
  proved=False
  timeline=""
  pref=problem[:3]
  runnr=0
  timeline1=""
  timeline2=""
  path=problem_path+pref+"/"+problem+".p"
  cmd="timeout "+str(timeout)+" ../gkc_41 "+path  
  print(path)
  outfile=log_folder+problem
  of=open(outfile,"w")
  of.write(cmd+"\n")
  of.write(str(datetime.datetime.now())+"\n")
  p = subprocess.Popen(cmd, shell=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
  for line in p.stdout.readlines():
    #print("!!"+str(line))
    line=line.decode("utf-8")
    of.write(line)
    if line.startswith("**** run "):
      try:
        tmp=line.split()
        runnr=tmp[2]
      except:
        continue        
    elif line.startswith("this run seconds:"):
      try:
        tmp=line.split()
        timeline1=tmp[3]
      except:
        timeline1=" "        
    elif line.startswith("total seconds:"):
      try:
        tmp=line.split()
        timeline2=tmp[2]  
      except:
        timeline2=" "        
    elif line.startswith("result: proof found"):
      proved=True
      #print("Proved,"+str(runnr))      
    elif "maxresident)k" in line:
      line=line.replace("user ",",")
      line=line.replace("system ",",")
      line=line.replace("elapsed ",",")
      line=line.replace("%CPU ",","+str(datetime.datetime.now())+",")
      timeline=line  
  if proved:    
    print("Proved,"+str(runnr)+","+timeline1+","+timeline2)
  else:
    print("Failed,"+str(runnr)+","+timeline1+","+str(timeout))
  retval = p.wait()  
  of.close()
  return (proved,str(runnr),timeline1,timeline2)
        

def read_problems():   
  pfname=problems_filename
  problems=[]
  # --- read problems file ---
  try:
    csvfile=open(pfname)
    freader = csv.reader(csvfile)
    for row in freader:   
      niceprob=row[0].strip()
      if niceprob and len(niceprob)>6 and \
         niceprob[0].isupper() and niceprob[1].isupper() and niceprob[2].isupper():         
        problems.append(niceprob)
    csvfile.close()   
  except Exception as e:
    print("Could not open or read the input file "+problems)
    return []
  return problems      


def read_solved():   
  pfname=outfile
  solved=[]
  last=""
  try: 
    csvfile=open(pfname)
    freader = csv.reader(csvfile)  
  except:
    print("no solved file found")  
    return None  
  # --- read problems file ---
  try:
    csvfile=open(pfname)
    freader = csv.reader(csvfile)
    for row in freader:
      if not row: continue
      niceprob=row[0].strip()
      if niceprob and len(niceprob)>6 and \
         niceprob[0].isupper() and niceprob[1].isupper() and niceprob[2].isupper():         
        solved.append(niceprob) 
        last=niceprob
    csvfile.close()   
  except Exception as e:
    print("Could not open or read the solved file "+pfname)
    return None
  return last  

# ---- run top level ----

main()