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
28
29
30
31
32
33
34
35
36
37
|
#! /usr/local/bin/tcsh -f
echo "# Starting bootstrap " > protokoll_bootstrap
foreach time (10 20 50 100 200 500)
echo "# New time: $time" >> protokoll_bootstrap
set new = 1;
set count = 0;
while($new)
set new = 0;
set count = `expr $count + 1`;
foreach problem (/home/schulz/EPROVER/TPTP/ROB/*.lop)
echo $problem " " $time " " $count
nice +10 /home/schulz/EPROVER/TESTRUNS_BOOTSTRAP/eprover \
-l4 --soft-cpu-limit=$time \
-H'(10*TSMWeight(ConstPrio,2,1,5,rec,/home/schulz/EPROVER/TESTRUNS_BOOTSTRAP/E_KNOWLEDGE_ROB,4000,1,100,Flat, IndexIdentity, 0,-40,40,-2,-1,0,1,-1))' \
-WSelectLargestNegLit --delete-bad-limit=1000000 \
-o /tmp/e_tmp_file $problem;
nice +10 /home/schulz/EPROVER/TESTRUNS_BOOTSTRAP/ekb_ginsert \
/tmp/e_tmp_file -n `basename $problem`\_$time\_$count\
-k /home/schulz/EPROVER/TESTRUNS_BOOTSTRAP/E_KNOWLEDGE_ROB;
if( { grep "# Proof found" /tmp/e_tmp_file>/dev/null }) then
echo Success
echo `basename $problem` " T" >> protokoll_bootstrap
if( { grep `basename $problem`" T" protokoll_bootstrap }) then
echo "No new proof"
else
set new = 1;
endif
else
echo Failure
echo `basename $problem` " F" >> protokoll_bootstrap
endif
rm /tmp/e_tmp_file;
end
end
end
|
