# max 400 Kb, max 5 min.
# memtime -m 400000 -c 300 ../h1.opt
# si on explose la mémoire, h1 s'arrete sur NoMem.
# si on explose le temps, h1 s'arrete sur Killed [9]
FILES=`(cd tptp; find . -name '*.h1.p' -print)`
export EXT=h1
for i in $FILES
do
  TMP=tptp/${i%.h1.p}.bench.$EXT
  echo "Benching h1 on $i" | tee $TMP
  memtime -m 400000 -c 300 h1.opt -no-log -progress tptp/$i 2>&1 | tee -a $TMP
  h1mon h1.pgr >>$TMP
done
find tptp -name '*.bench.'$EXT -exec grep -q Killed {} \; -print | wc -l
#12
find tptp -name '*.bench.'$EXT -exec grep -q NoMem {} \; -print | wc -l
#4
for i in tptp/*
do
  echo $i: `grep -l Killed $i/*.bench.$EXT | wc -l` killed, `grep -l NoMem $i/*.bench.$EXT | wc -l` nomem, `ls $i/*.h1.p | wc -l` files
done
#tptp/COM: 1 killed, 0 nomem, 7 files
#tptp/FLD: 0 killed, 0 nomem, 279 files
#tptp/KRS: 0 killed, 0 nomem, 17 files
#tptp/LCL: 0 killed, 0 nomem, 297 files
#tptp/MGT: 0 killed, 0 nomem, 22 files
#tptp/MSC: 0 killed, 0 nomem, 12 files
#tptp/NLP: 0 killed, 0 nomem, 103 files
#tptp/PUZ: 11 killed, 4 nomem, 71 files

./statbench $EXT

### On teste -no-alternation
export EXT=h1-no-alt
for i in $FILES
do
  TMP=tptp/${i%.h1.p}.bench.$EXT
  echo "Benching h1 on $i" | tee $TMP
  memtime -m 400000 -c 300 h1.opt -no-log -progress -no-alternation tptp/$i 2>&1 | tee -a $TMP
  h1mon h1.pgr >>$TMP
done
find tptp -name '*.bench'.$EXT -exec grep -q Killed {} \; -print | wc -l
#9
find tptp -name '*.bench'.$EXT -exec grep -q NoMem {} \; -print | wc -l
#13
for i in tptp/*
do
  echo $i: `grep -l Killed $i/*.bench.$EXT | wc -l` killed, `grep -l NoMem $i/*.bench.$EXT | wc -l` nomem, `ls $i/*.h1.p | wc -l` files
done
#tptp/COM: 0 killed, 0 nomem, 7 files
#tptp/FLD: 0 killed, 0 nomem, 279 files
#tptp/KRS: 0 killed, 0 nomem, 17 files
#tptp/LCL: 0 killed, 0 nomem, 297 files
#tptp/MGT: 0 killed, 0 nomem, 22 files
#tptp/MSC: 0 killed, 0 nomem, 12 files
#tptp/NLP: 0 killed, 7 nomem, 103 files
#tptp/PUZ: 9 killed, 6 nomem, 71 files

#Note: tptp/COM/COM006-1 is Killed by standard h1, immediate refutation with -no-alternation.

./statbench $EXT

### On teste quand il n'y a plus l'approx des skeleta (-path-refine 0)
export EXT=h1-no-skel
for i in $FILES
do
  TMP=tptp/${i%.h1.p}.bench.$EXT
  echo "Benching h1 on $i" | tee $TMP
  memtime -m 400000 -c 300 h1.opt -no-log -progress -path-refine 0 tptp/$i 2>&1 | tee -a $TMP
  h1mon h1.pgr >>$TMP
done
find tptp -name '*.bench.'$EXT -exec grep -q Killed {} \; -print | wc -l
#11
find tptp -name '*.bench.'$EXT -exec grep -q NoMem {} \; -print | wc -l
#5
for i in tptp/*
do
  echo $i: `grep -l Killed $i/*.bench.$EXT | wc -l` killed, `grep -l NoMem $i/*.bench.$EXT | wc -l` nomem, `ls $i/*.h1.p | wc -l` files
done
#tptp/COM: 1 killed, 0 nomem, 7 files
#tptp/FLD: 0 killed, 0 nomem, 279 files
#tptp/KRS: 0 killed, 0 nomem, 17 files
#tptp/LCL: 0 killed, 0 nomem, 297 files
#tptp/MGT: 0 killed, 0 nomem, 22 files
#tptp/MSC: 0 killed, 0 nomem, 12 files
#tptp/NLP: 0 killed, 0 nomem, 103 files
#tptp/PUZ: 10 killed, 5 nomem, 71 files

./statbench $EXT

### On teste le monadic-proxy
export EXT=h1-monadic-proxy
for i in $FILES
do
  TMP=tptp/${i%.h1.p}.bench.$EXT
  echo "Benching h1 on $i" | tee $TMP
  memtime -m 400000 -c 300 h1.opt -no-log -progress -monadic-proxy tptp/$i 2>&1 | tee -a $TMP
  h1mon h1.pgr >>$TMP
done
find tptp -name '*.bench'.$EXT -exec grep -q Killed {} \; -print | wc -l
#11
find tptp -name '*.bench'.$EXT -exec grep -q NoMem {} \; -print | wc -l
#5
for i in tptp/*
do
  echo $i: `grep -l Killed $i/*.bench.$EXT | wc -l` killed, `grep -l NoMem $i/*.bench.$EXT | wc -l` nomem, `ls $i/*.h1.p | wc -l` files
done
#tptp/COM: 1 killed, 0 nomem, 7 files
#tptp/FLD: 0 killed, 0 nomem, 279 files
#tptp/KRS: 0 killed, 0 nomem, 17 files
#tptp/LCL: 0 killed, 0 nomem, 297 files
#tptp/MGT: 0 killed, 0 nomem, 22 files
#tptp/MSC: 0 killed, 0 nomem, 12 files
#tptp/NLP: 0 killed, 0 nomem, 103 files
#tptp/PUZ: 10 killed, 5 nomem, 71 files

# Les NoMem de PUZ: (obsolete) 37-3, 52-1, 53-1; for h1, c'était 37-1, 37-2, 37-3, 53-1.

./statbench $EXT

# On teste le -no-deep-abbrv
export EXT=h1-noda
for i in $FILES
do
  TMP=tptp/${i%.h1.p}.bench.$EXT
  echo "Benching h1 on $i" | tee $TMP
  memtime -m 400000 -c 300 h1.opt -no-log -progress -no-deep-abbrv tptp/$i 2>&1 | tee -a $TMP
  h1mon h1.pgr >>$TMP
done
find tptp -name '*.bench.'$EXT -exec grep -q Killed {} \; -print | wc -l
#10
find tptp -name '*.bench.'$EXT -exec grep -q NoMem {} \; -print | wc -l
#5
for i in tptp/*
do
  echo $i: `grep -l Killed $i/*.bench.$EXT | wc -l` killed, `grep -l NoMem $i/*.bench.$EXT | wc -l` nomem, `ls $i/*.h1.p | wc -l` files
done
#tptp/COM: 1 killed, 0 nomem, 7 files
#tptp/FLD: 0 killed, 0 nomem, 279 files
#tptp/KRS: 0 killed, 0 nomem, 17 files
#tptp/LCL: 0 killed, 0 nomem, 297 files
#tptp/MGT: 0 killed, 0 nomem, 22 files
#tptp/MSC: 0 killed, 0 nomem, 12 files
#tptp/NLP: 0 killed, 0 nomem, 103 files
#tptp/PUZ: 9 killed, 5 nomem, 71 files

# Obsolete:
# Les NoMem de PUZ: 17-1,       37-2, 37-3, 52-1, 53-1;
#       ceux de h1:       37-1, 37-2, 37-3, 53-1.
# Les Killed de PUZ: 15-3, 36-1.005,       39-1, 40-1, 41-1, 42-1, 48-1, 49-1, 50-1;
#        ceux de h1: 15-3, 36-1.005, 38-1, 39-1, 40-1, 41-1, 42-1, 48-1, 49-1, 50-1, 52-1

./statbench $EXT

# On teste le -no-sort-simplify
export EXT=h1-noss
for i in $FILES
do
  TMP=tptp/${i%.h1.p}.bench.$EXT
  echo "Benching h1 on $i" | tee $TMP
  memtime -m 400000 -c 300 h1.opt -no-log -progress -no-sort-simplify tptp/$i 2>&1 | tee -a $TMP
  h1mon h1.pgr >>$TMP
done
find tptp -name '*.bench.'$EXT -exec grep -q Killed {} \; -print | wc -l
#11
find tptp -name '*.bench.'$EXT -exec grep -q NoMem {} \; -print | wc -l
#5
for i in tptp/*
do
  echo $i: `grep -l Killed $i/*.bench.$EXT | wc -l` killed, `grep -l NoMem $i/*.bench.$EXT | wc -l` nomem, `ls $i/*.h1.p | wc -l` files
done
#tptp/COM: 1 killed, 0 nomem, 7 files
#tptp/FLD: 0 killed, 0 nomem, 279 files
#tptp/KRS: 0 killed, 0 nomem, 17 files
#tptp/LCL: 0 killed, 0 nomem, 297 files
#tptp/MGT: 0 killed, 0 nomem, 22 files
#tptp/MSC: 0 killed, 0 nomem, 12 files
#tptp/NLP: 0 killed, 0 nomem, 103 files
#tptp/PUZ: 10 killed, 5 nomem, 71 files

./statbench $EXT