mirror of
https://github.com/RAIRLab/Spectra.git
synced 2024-11-13 21:07:30 -05:00
56 lines
1.5 KiB
Text
56 lines
1.5 KiB
Text
|
#! /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
|
||
|
|
|