forked from sneeuwballen/zipperposition
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathpoly_test.sh
27 lines (22 loc) · 1.27 KB
/
poly_test.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
touch "$1"
for filename in ../tptp_benchmarks/poly_problems/TF1/*.p; do
# with monomorphisation e at 0.0
printf "\n\nwith monomorphisation, call point 0.0\n" >> "$1"
timeout 45\
./zipperposition.exe --mode best --try-e "./eprover-ho" --e-timeout 30 --e-max-derived 100000 --e-call-point 0.0 --output none "$filename" --timeout 30 >> "$1"
# with monomorphisation e at 0.05
printf "\n\nwith monomorphisation, call point 0.05\n" >> "$1"
timeout 45\
./zipperposition.exe --mode best --try-e "./eprover-ho" --e-timeout 30 --e-max-derived 100000 --e-call-point 0.05 --output none "$filename" --timeout 30 >> "$1"
# with monomorphisation e at 0.1
printf "\n\nwith monomorphisation, call point 0.1\n" >> "$1"
timeout 45\
./zipperposition.exe --mode best --try-e "./eprover-ho" --e-timeout 30 --e-max-derived 100000 --e-call-point 0.1 --output none "$filename" --timeout 30 >> "$1"
# without monomorphisation
printf "\n\nwithout monomorphisation (or e)\n" >> "$1"
timeout 45\
./zipperposition.exe --mode best --output none "$filename" --timeout 30 >> "$1"
printf "\n\n ------------------------------------------------------------------------------- \n\n" >> "$1"
printf "$filename done\n" >> "$1"
printf "$filename done\n"
done