#!/bin/bash

CVC5=~/bin/cvc5-Linux


# echo collapsed2 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed2.smt2) &>> logfile; 
# echo >> logfile; echo collapsed2

# echo collapsed6 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed6.smt2) &>> logfile; 
# echo >> logfile; echo collapsed6

# echo collapsed7 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed7.smt2) &>> logfile; 
# echo >> logfile; echo collapsed7

# echo collapsed10 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed10.smt2) &>> logfile; 
# echo >> logfile; echo collapsed10

# echo collapsed11 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed11.smt2) &>> logfile; 
# echo >> logfile; echo collapsed11

# echo collapsed13 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed13.smt2) &>> logfile; 
# echo >> logfile; echo collapsed13

# echo collapsed14 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed14.smt2) &>> logfile; 
# echo >> logfile; echo collapsed14

# echo collapsed15 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed15.smt2) &>> logfile; 
# echo >> logfile; echo collapsed15

# echo collapsed16 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed16.smt2) &>> logfile; 
# echo >> logfile; echo collapsed16

# echo collapsed17 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed17.smt2) &>> logfile; 
# echo >> logfile; echo collapsed17

# echo collapsed18 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed18.smt2) &>> logfile; 
# echo >> logfile; echo collapsed18

# echo collapsed19 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed19.smt2) &>> logfile; 
# echo >> logfile; echo collapsed19

# echo collapsed20 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed20.smt2) &>> logfile; 
# echo >> logfile; echo collapsed20

# echo collapsed21 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed21.smt2) &>> logfile; 
# echo >> logfile; echo collapsed21

# echo collapsed22 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed22.smt2) &>> logfile; 
# echo >> logfile; echo collapsed22

# echo collapsed23 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed23.smt2) &>> logfile; 
# echo >> logfile; echo collapsed23

# echo collapsed24 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed24.smt2) &>> logfile; 
# echo >> logfile; echo collapsed24

# echo collapsed25 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed25.smt2) &>> logfile; 
# echo >> logfile; echo collapsed25

# echo collapsed3 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed3.smt2) &>> logfile; 
# echo >> logfile; echo collapsed3

# echo collapsed26 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed26.smt2) &>> logfile; 
# echo >> logfile;	 echo collapsed26


echo collapsed27 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed27.smt2) &>> logfile; 
echo >> logfile;	 echo collapsed27

echo collapsed28 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed28.smt2) &>> logfile; 
echo >> logfile;	 echo collapsed28

echo collapsed29 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed29.smt2) &>> logfile; 
echo >> logfile;	 echo collapsed29

echo collapsed30 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed30.smt2) &>> logfile; 
echo >> logfile;	 echo collapsed30

echo collapsed31 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed31.smt2) &>> logfile; 
echo >> logfile;	 echo collapsed31

echo collapsed32 >> logfile; (time timeout -s 9 3600 $CVC5 --lang=sygus2 collapsed32.smt2) &>> logfile; 
echo >> logfile;	 echo collapsed32

