Add subdirectories to contrib for competition scripts (#3164)

25 files changed, 994 insertions, 0 deletions

diff --git a/contrib/competitions/casc/run-script-casc24-fnt b/contrib/competitions/casc/run-script-casc24-fnt
new file mode 100755
index 000000000..b10d7324a
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc24-fnt
@@ -0,0 +1,38 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+let "to = $2 - 60"
+
+file=${bench##*/}
+filename=${file%.*}
+
+# use: trywith [params..]
+# to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
+# which case this run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  (ulimit -t "$limit";$cvc4 -L tptp --szs-compliant --no-checking --no-interactive --dump-models --produce-models "$@" $bench) 2>/dev/null |
+  (read result;
+  case "$result" in
+    sat) echo "% SZS status" "Satisfiable for $filename";
+         echo "% SZS output" "start FiniteModel for $filename";
+         cat;
+         echo "% SZS output" "end FiniteModel for $filename";
+         exit 0;;
+    unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename";
+                    echo "% SZS output" "start FiniteModel for $filename";
+                    cat;
+                    echo "% SZS output" "end FiniteModel for $filename";
+                    exit 0;;
+    conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+trywith 30 --finite-model-find --uf-ss-totality
+trywith 30 --finite-model-find --decision=justification --fmf-fmc
+trywith $to --finite-model-find --decision=justification
+echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc24-fnt-no-models b/contrib/competitions/casc/run-script-casc24-fnt-no-models
new file mode 100755
index 000000000..3b4d5e320
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc24-fnt-no-models
@@ -0,0 +1,36 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+let "to = $2 - 60"
+
+file=${bench##*/}
+filename=${file%.*}
+
+# use: trywith [params..]
+# to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
+# which case this run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
+  case "$result" in
+    sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;;
+    unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;;
+  esac
+}
+function finishwith {
+  result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
+  case "$result" in
+    sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;;
+    unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;;
+  esac
+}
+
+trywith 30 --finite-model-find --uf-ss-totality
+trywith 30 --finite-model-find --decision=justification --fmf-fmc
+trywith $to --finite-model-find --decision=justification
+echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc24-fof b/contrib/competitions/casc/run-script-casc24-fof
new file mode 100755
index 000000000..b3ede0dfa
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc24-fof
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+let "to = $2 - 75"
+
+file=${bench##*/}
+filename=${file%.*}
+
+# use: trywith [params..]
+# to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
+# which case this run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
+  case "$result" in
+    sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;;
+    unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;;
+  esac
+}
+function finishwith {
+  result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
+  case "$result" in
+    sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;;
+    unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;;
+  esac
+}
+
+trywith 30
+trywith 15 --finite-model-find --fmf-inst-engine
+trywith 30 --finite-model-find --decision=justification --fmf-fmc
+trywith $to --decision=justification
+echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc25-fnt b/contrib/competitions/casc/run-script-casc25-fnt
new file mode 100755
index 000000000..7f007186c
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc25-fnt
@@ -0,0 +1,38 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fnt casc 25 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev
+trywith 20 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair
+trywith 20 --finite-model-find --decision=internal --sort-inference --uf-ss-fair
+trywith 20 --finite-model-find --uf-ss-totality --sort-inference --uf-ss-fair --mbqi=gen-ev
+trywith 60 --finite-model-find --quant-cf --sort-inference --uf-ss-fair --mbqi=abs
+finishwith --finite-model-find --sort-inference --uf-ss-fair --mbqi=abs
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc25-fof b/contrib/competitions/casc/run-script-casc25-fof
new file mode 100755
index 000000000..26c544062
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc25-fof
@@ -0,0 +1,46 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fof casc 25 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 15 --relevant-triggers --clause-split --full-saturate-quant 
+trywith 15 --clause-split --no-e-matching --full-saturate-quant 
+trywith 15 --finite-model-find --quant-cf --qcf-all-conflict --sort-inference --uf-ss-fair
+trywith 5 --trigger-sel=max --full-saturate-quant
+trywith 5 --relevant-triggers --clause-split --multi-trigger-when-single --full-saturate-quant 
+trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant 
+trywith 5 --pre-skolem-quant --no-pre-skolem-quant-nested --full-saturate-quant
+trywith 15 --relevant-triggers --decision=internal --full-saturate-quant
+trywith 15 --clause-split --no-quant-cf --full-saturate-quant
+trywith 15 --clause-split --trigger-sel=min --full-saturate-quant
+trywith 30 --prenex-quant=none --full-saturate-quant
+trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev
+finishwith --term-db-mode=relevant --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc25-tfa b/contrib/competitions/casc/run-script-casc25-tfa
new file mode 100755
index 000000000..40ed76df5
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc25-tfa
@@ -0,0 +1,41 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tfa casc 25 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+trywith 10 --cbqi2 --decision=internal --full-saturate-quant
+trywith 10 --relevant-triggers --full-saturate-quant --partial-triggers --purify-triggers
+trywith 10 --cbqi --full-saturate-quant
+trywith 10 --cbqi2 --e-matching  --partial-triggers --purify-triggers
+trywith 30 --qcf-tconstraint --full-saturate-quant
+trywith 60 --cbqi --cbqi-recurse --full-saturate-quant
+trywith 10 --full-saturate-quant --partial-triggers --purify-triggers
+trywith 10 --no-e-matching --full-saturate-quant
+trywith 10 --fmf-bound-int
+finishwith --cbqi2 --cbqi-recurse --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc25-tfn b/contrib/competitions/casc/run-script-casc25-tfn
new file mode 100755
index 000000000..6888d7b49
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc25-tfn
@@ -0,0 +1,36 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tfn casc 25 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench
+}
+
+trywith 30 --cbqi2 --decision=internal --full-saturate-quant
+trywith 30 --cbqi --full-saturate-quant
+trywith 60 --cbqi --cbqi-recurse --full-saturate-quant
+trywith 60 --fmf-bound-int --macros-quant
+finishwith --cbqi2 --cbqi-recurse --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc26-fnt b/contrib/competitions/casc/run-script-casc26-fnt
new file mode 100644
index 000000000..c89d3eb0a
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc26-fnt
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fnt casc 26 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 60 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
+trywith 30 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair
+trywith 60 --finite-model-find --decision=internal --sort-inference --uf-ss-fair
+finishwith --finite-model-find --macros-quant --macros-quant-mode=all --sort-inference --uf-ss-fair
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc26-fof b/contrib/competitions/casc/run-script-casc26-fof
new file mode 100644
index 000000000..5ec312cb7
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc26-fof
@@ -0,0 +1,50 @@
+#!/bin/bash
+
+# script is used for FOF division, also SLD division
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fof casc 26 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 20 --relational-triggers --full-saturate-quant 
+trywith 20 --no-e-matching --full-saturate-quant 
+trywith 15 --finite-model-find --uf-ss=no-minimal
+trywith 5 --multi-trigger-when-single --full-saturate-quant 
+trywith 5 --trigger-sel=max --full-saturate-quant
+trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant  
+trywith 10 --multi-trigger-cache --full-saturate-quant
+trywith 15 --prenex-quant=none --full-saturate-quant
+trywith 15 --fs-inst --decision=internal --full-saturate-quant
+trywith 15 --relevant-triggers --full-saturate-quant 
+trywith 15 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
+trywith 30 --decision=internal --full-saturate-quant
+trywith 30 --qcf-vo-exp --full-saturate-quant
+trywith 30 --no-quant-cf --full-saturate-quant 
+finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc26-tfa b/contrib/competitions/casc/run-script-casc26-tfa
new file mode 100644
index 000000000..74147e529
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc26-tfa
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tfa casc 26 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+trywith 15 --finite-model-find --decision=internal
+trywith 15 --multi-trigger-when-single --multi-trigger-priority --nl-ext-tplanes --full-saturate-quant
+trywith 15 --no-e-matching --full-saturate-quant 
+trywith 15 --cbqi-all --purify-triggers --full-saturate-quant 
+finishwith --macros-quant --macros-quant-mode=all --nl-ext-tplanes --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc27-fnt b/contrib/competitions/casc/run-script-casc27-fnt
new file mode 100755
index 000000000..301b03a2b
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc27-fnt
@@ -0,0 +1,35 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fnt casc 27 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 30 --finite-model-find --uf-ss=no-minimal --sort-inference
+finishwith --finite-model-find --macros-quant --macros-quant-mode=all --sort-inference
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc27-fof b/contrib/competitions/casc/run-script-casc27-fof
new file mode 100755
index 000000000..c95266367
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc27-fof
@@ -0,0 +1,50 @@
+#!/bin/bash
+
+# script is used for FOF division, also SLD division
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fof casc 27 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 20 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+trywith 20 --no-e-matching --full-saturate-quant
+trywith 15 --finite-model-find --uf-ss=no-minimal
+trywith 5 --multi-trigger-when-single --full-saturate-quant
+trywith 5 --trigger-sel=max --full-saturate-quant
+trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
+trywith 10 --multi-trigger-cache --full-saturate-quant
+trywith 15 --prenex-quant=none --full-saturate-quant
+trywith 15 --fs-interleave --decision=internal --full-saturate-quant
+trywith 15 --relevant-triggers --full-saturate-quant
+trywith 15 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
+trywith 30 --pre-skolem-quant --full-saturate-quant
+trywith 30 --qcf-vo-exp --full-saturate-quant
+trywith 30 --no-quant-cf --full-saturate-quant
+finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc27-tfa b/contrib/competitions/casc/run-script-casc27-tfa
new file mode 100755
index 000000000..ec4c76685
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc27-tfa
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tfa casc 27 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+trywith 15 --finite-model-find --decision=internal
+trywith 15 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+trywith 15 --no-e-matching --full-saturate-quant
+trywith 15 --cbqi-all --purify-triggers --full-saturate-quant
+finishwith --macros-quant --macros-quant-mode=all --nl-ext-tplanes --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc27-thf b/contrib/competitions/casc/run-script-casc27-thf
new file mode 100755
index 000000000..5db5527ed
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc27-thf
@@ -0,0 +1,44 @@
+#!/bin/bash
+
+# script is used for THF division
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-thf casc 27 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 20 --uf-ho --ho-elim --no-ho-elim-store-ax --full-saturate-quant
+trywith 20 --uf-ho --ho-elim --full-saturate-quant
+trywith 5  --uf-ho --ho-elim --finite-model-find --uf-ss=no-minimal
+trywith 5  --uf-ho --no-ho-matching --finite-model-find --uf-ss=no-minimal
+trywith 30 --uf-ho --no-ho-matching --full-saturate-quant --fs-interleave --ho-elim-store-ax
+trywith 20 --uf-ho --no-ho-matching --full-saturate-quant --macros-quant-mode=all
+trywith 30 --uf-ho --ho-elim --full-saturate-quant --fs-interleave
+trywith 30 --uf-ho --no-ho-matching --full-saturate-quant --ho-elim-store-ax
+finishwith  --uf-ho --ho-elim --no-ho-elim-store-ax --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-cascj7-fnt b/contrib/competitions/casc/run-script-cascj7-fnt
new file mode 100755
index 000000000..e3ad1a2ff
--- /dev/null
+++ b/contrib/competitions/casc/run-script-cascj7-fnt
@@ -0,0 +1,36 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fnt casc j7 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+trywith 30 --finite-model-find --sort-inference --uf-ss-fair
+trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=internal --sort-inference --uf-ss-fair
+trywith 15 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair
+trywith 60 --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair
+finishwith --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair --mbqi-one-inst-per-round
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-cascj7-fof b/contrib/competitions/casc/run-script-cascj7-fof
new file mode 100755
index 000000000..fb2ca33eb
--- /dev/null
+++ b/contrib/competitions/casc/run-script-cascj7-fof
@@ -0,0 +1,38 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fof casc j7 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+trywith 15 --quant-cf --pre-skolem-quant --full-saturate-quant
+trywith 30 --full-saturate-quant
+trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev
+trywith 30 --relevant-triggers --full-saturate-quant
+trywith 15 --finite-model-find --decision=justification-stoponly
+trywith 30 --pre-skolem-quant --full-saturate-quant
+finishwith --quant-cf --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-cascj7-tff b/contrib/competitions/casc/run-script-cascj7-tff
new file mode 100755
index 000000000..11350cd7e
--- /dev/null
+++ b/contrib/competitions/casc/run-script-cascj7-tff
@@ -0,0 +1,38 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tff casc j7 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench
+}
+
+trywith 15 --cbqi-recurse --full-saturate-quant
+trywith 15 --decision=internal --full-saturate-quant
+trywith 30 --quant-cf --qcf-tconstraint --full-saturate-quant
+trywith 20 --finite-model-find
+trywith 30 --fmf-bound-int
+trywith 60 --quant-cf --full-saturate-quant
+finishwith --cbqi-recurse --full-saturate-quant --pre-skolem-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-cascj8-fnt b/contrib/competitions/casc/run-script-cascj8-fnt
new file mode 100755
index 000000000..bc37180a6
--- /dev/null
+++ b/contrib/competitions/casc/run-script-cascj8-fnt
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fnt casc j8 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 60 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
+trywith 30 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair
+trywith 60 --finite-model-find --decision=internal --sort-inference --uf-ss-fair
+finishwith --finite-model-find --mbqi=abs --sort-inference --uf-ss-fair
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-cascj8-fof b/contrib/competitions/casc/run-script-cascj8-fof
new file mode 100755
index 000000000..fe18c3ed0
--- /dev/null
+++ b/contrib/competitions/casc/run-script-cascj8-fof
@@ -0,0 +1,48 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fof casc j8 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 20 --relational-triggers --full-saturate-quant 
+trywith 20 --no-e-matching --full-saturate-quant 
+trywith 15 --finite-model-find --mbqi=abs
+trywith 5 --multi-trigger-when-single --full-saturate-quant 
+trywith 5 --trigger-sel=max --full-saturate-quant
+trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant  
+trywith 10 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair
+trywith 10 --term-db-mode=relevant --full-saturate-quant
+trywith 15 --prenex-quant=none --full-saturate-quant
+trywith 15 --decision=internal --full-saturate-quant
+trywith 30 --relevant-triggers --full-saturate-quant 
+trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
+trywith 30 --fs-inst --full-saturate-quant
+trywith 30 --no-quant-cf --full-saturate-quant 
+finishwith --qcf-vo-exp --full-saturate-quant 
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-cascj8-tfa b/contrib/competitions/casc/run-script-cascj8-tfa
new file mode 100755
index 000000000..da4056466
--- /dev/null
+++ b/contrib/competitions/casc/run-script-cascj8-tfa
@@ -0,0 +1,40 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tfa casc j8 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+trywith 10 --decision=internal --full-saturate-quant
+trywith 10 --finite-model-find --decision=internal
+trywith 10 --purify-quant --full-saturate-quant
+trywith 10 --partial-triggers --full-saturate-quant
+trywith 10 --no-e-matching --full-saturate-quant
+trywith 30 --cbqi-all --purify-triggers --full-saturate-quant 
+trywith 60 --cbqi-all --fs-inst --full-saturate-quant
+finishwith --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-cascj8-tfn b/contrib/competitions/casc/run-script-cascj8-tfn
new file mode 100755
index 000000000..a6fe1e23c
--- /dev/null
+++ b/contrib/competitions/casc/run-script-cascj8-tfn
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fnt casc j8 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 60 --finite-model-find --sort-inference --uf-ss-fair
+trywith 30 --full-saturate-quant
+trywith 30 --finite-model-find --fmf-bound-int --macros-quant
+finishwith --finite-model-find --decision=internal --sort-inference --uf-ss-fair
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-cascj9-fnt b/contrib/competitions/casc/run-script-cascj9-fnt
new file mode 100755
index 000000000..4e52e8e91
--- /dev/null
+++ b/contrib/competitions/casc/run-script-cascj9-fnt
@@ -0,0 +1,35 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fnt casc j9 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 30 --finite-model-find --uf-ss=no-minimal --sort-inference
+finishwith --finite-model-find --macros-quant --macros-quant-mode=all --sort-inference
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-cascj9-fof b/contrib/competitions/casc/run-script-cascj9-fof
new file mode 100755
index 000000000..71107775a
--- /dev/null
+++ b/contrib/competitions/casc/run-script-cascj9-fof
@@ -0,0 +1,50 @@
+#!/bin/bash
+
+# script is used for FOF division, also SLD division
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fof casc j9 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 20 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+trywith 20 --no-e-matching --full-saturate-quant 
+trywith 15 --finite-model-find --uf-ss=no-minimal
+trywith 5 --multi-trigger-when-single --full-saturate-quant 
+trywith 5 --trigger-sel=max --full-saturate-quant
+trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant  
+trywith 10 --multi-trigger-cache --full-saturate-quant
+trywith 15 --prenex-quant=none --full-saturate-quant
+trywith 15 --fs-inst --decision=internal --full-saturate-quant
+trywith 15 --relevant-triggers --full-saturate-quant 
+trywith 15 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
+trywith 30 --pre-skolem-quant --full-saturate-quant
+trywith 30 --qcf-vo-exp --full-saturate-quant
+trywith 30 --no-quant-cf --full-saturate-quant 
+finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-cascj9-tfa b/contrib/competitions/casc/run-script-cascj9-tfa
new file mode 100755
index 000000000..d730db922
--- /dev/null
+++ b/contrib/competitions/casc/run-script-cascj9-tfa
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tfa casc j9 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+trywith 15 --finite-model-find --decision=internal
+trywith 15 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+trywith 15 --no-e-matching --full-saturate-quant 
+trywith 15 --cbqi-all --purify-triggers --full-saturate-quant 
+finishwith --macros-quant --macros-quant-mode=all --nl-ext-tplanes --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-cascj9-tfn-nr b/contrib/competitions/casc/run-script-cascj9-tfn-nr
new file mode 100644
index 000000000..8124fd6f9
--- /dev/null
+++ b/contrib/competitions/casc/run-script-cascj9-tfn-nr
@@ -0,0 +1,36 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tfn casc j9 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 30 --finite-model-find --decision=internal --sort-inference --macros-quant --macros-quant-mode=all
+trywith 15 --nl-ext-tplanes --full-saturate-quant --macros-quant --macros-quant-mode=all
+finishwith --finite-model-find --fmf-inst-engine --sort-inference --macros-quant --macros-quant-mode=all
+# echo "% SZS status" "GaveUp for $filename"