#! /bin/tcsh

# this is Geoff's run-snark script for SystemOnTPTP as of 2012-08-21

if (! -f $1) then
    echo "Missing filename"
    exit
endif
echo $1
if ($2 == "") then
  set runtimelimit = nil
else
  set runtimelimit = $2
endif

set this_directory=`dirname $0`
$this_directory/snark << ENDOFSTDIN 
#+sbcl (sb-ext:disable-debugger)
(in-package :snark-user)

(defvar snark-tptp-options)
(setf snark-tptp-options
      '(
        (agenda-length-limit nil)
        (agenda-length-before-simplification-limit nil)
        (use-hyperresolution t)
        (use-ur-resolution t)
        (use-paramodulation t)
        (use-factoring :pos)
        (use-literal-ordering-with-hyperresolution 'literal-ordering-p)
        (use-literal-ordering-with-paramodulation  'literal-ordering-p)
        (ordering-functions>constants t)
        (assert-context :current)
        (run-time-limit $runtimelimit)
        (listen-for-commands nil)
        (use-closure-when-satisfiable t)
        (print-rows-when-given nil)
        (print-rows-when-derived nil)
        (print-unorientable-rows nil)
        (print-row-wffs-prettily nil)
        (print-final-rows :tptp)                ;System on TPTP uses value :tptp
        (print-options-when-starting nil)       ;System on TPTP uses this
        (use-variable-name-sorts nil)
        (use-purity-test t)
        (use-relevance-test t)
        (declare-tptp-symbols1)
        (declare-tptp-symbols2)
        ))

(setf *tptp-environment-variable* "$TPTP")
(refute-file "$1" :options snark-tptp-options :format :tptp)

(quit)
ENDOFSTDIN