Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL

General

This site provides supporting material for the paper Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL by Ralph Bottesch, Max W. Haslbeck, Alban Reynaud and René Thiemann.

Generated Haskell code

Archive file

The .tar.gz archive contains the generated Haskell code. The generated code doesn't have any dependencies and is compilable with an up to date Haskell environment. The archive also contains the Isabelle .thy files which were used to generate the Haskell code.

Links to Lemmas, Definitions, etc. in the Isabelle Source Code

Experimental Results

The experiments have been conducted as follows.

Testing was done on a subset of the non-incremental QF_LIA (quantifier-free linear integer arithmetic) benchmark set from SMT-LIB.
1192 benchmarks, comprising 18% of 6489 benchmarks in QF_LIA, were converted to a format that is readable by our solver. Specifically, the sub-folders 20180326-Bromberger, miplib2003, pb2010, pidgeons, prime-cone, and slacks from QF_LIA were fully converted. All solvers were tested on this set of benchmarks.
Each solver was given 60s per test on the same hardware.
Z3 version 4.4.0pre-2, CVC4 version 1.5-4, and the 2019-05-09 release of SMT-LIB were used.

Both tables display the execution times in seconds of our experiments. Satisfiable answers of the verified solvers have been converted back so that variable names of the original SMT-LIB benchmarks are used.

The first table is a selection of only those experiments where one of our verified solvers was successful, but at least one of Z3 or CVC4 failed.

input
v20_problem__011.smt2.slack (converted)	22.282s	sat	0.595s	sat	-	timeout	0.409s	sat
v25_problem_2__015.smt2.slack (converted)	-	timeout	4.092s	sat	2.186s	sat	-	timeout
v25_problem_2__030.smt2.slack (converted)	-	timeout	15.226s	sat	-	timeout	25.590s	sat
v25_problem__011.smt2.slack (converted)	-	timeout	2.148s	sat	-	timeout	0.246s	sat
v30_problem_2__009.smt2.slack (converted)	31.742s	sat	3.138s	sat	-	timeout	5.896s	sat
v30_problem_2__018.smt2.slack (converted)	-	timeout	9.358s	sat	40.857s	sat	-	timeout
v30_problem_2__019.smt2.slack (converted)	-	timeout	3.487s	sat	10.017s	sat	-	timeout
v30_problem__014.smt2.slack (converted)	-	timeout	3.598s	sat	-	timeout	8.393s	sat
v30_problem__023.smt2.slack (converted)	-	timeout	12.994s	sat	-	timeout	0.348s	sat
v35_problem_2__011.smt2.slack (converted)	-	timeout	6.472s	sat	4.625s	sat	-	timeout
v35_problem__014.smt2.slack (converted)	-	timeout	14.233s	sat	-	timeout	0.069s	sat
v40_problem_2__013.smt2.slack (converted)	-	timeout	9.229s	sat	-	timeout	-	timeout
v40_problem__014.smt2.slack (converted)	-	timeout	10.474s	sat	16.730s	sat	-	timeout
v40_problem__019.smt2.slack (converted)	-	timeout	18.158s	sat	-	timeout	0.285s	sat
v40_problem__020.smt2.slack (converted)	-	timeout	22.389s	sat	39.244s	sat	-	timeout
v45_problem_2__011.smt2.slack (converted)	-	timeout	10.436s	sat	-	timeout	7.101s	sat
v45_problem_2__012.smt2.slack (converted)	-	timeout	9.881s	sat	-	timeout	9.539s	sat
v45_problem_2__018.smt2.slack (converted)	-	timeout	17.005s	sat	35.893s	sat	-	timeout
v45_problem_2__020.smt2.slack (converted)	-	timeout	18.062s	sat	-	timeout	-	timeout
v45_problem_2__022.smt2.slack (converted)	-	timeout	31.898s	sat	46.255s	sat	-	timeout
v45_problem__012.smt2.slack (converted)	-	timeout	32.189s	sat	0.085s	sat	-	timeout
v45_problem__016.smt2.slack (converted)	-	timeout	24.553s	sat	-	timeout	-	timeout
v45_problem__018.smt2.slack (converted)	-	timeout	29.466s	sat	-	timeout	22.827s	sat
v45_problem__019.smt2.slack (converted)	-	timeout	23.478s	sat	48.825s	sat	-	timeout
v45_problem__020.smt2.slack (converted)	-	timeout	18.073s	sat	-	timeout	-	timeout
unbd-sage12 (converted)	6.702s	sat	0.202s	sat	-	timeout	0.460s	sat
unbd-sage13 (converted)	36.067s	sat	-	timeout	-	timeout	1.089s	sat
unbd-sage14 (converted)	1.129s	sat	0.221s	sat	-	timeout	0.206s	sat
unbd-sage21 (converted)	8.905s	sat	1.355s	sat	-	timeout	0.082s	sat
unbd-sage22 (converted)	33.121s	sat	-	timeout	-	timeout	0.040s	sat
unbd-sage7 (converted)	4.121s	sat	0.849s	sat	-	timeout	0.501s	sat
pigeon-hole-12 (converted)	0.241s	unsat	0.252s	unsat	0.086s	unsat	-	timeout
pigeon-hole-13 (converted)	0.352s	unsat	0.349s	unsat	0.097s	unsat	-	timeout
pigeon-hole-14 (converted)	0.468s	unsat	0.477s	unsat	0.108s	unsat	-	timeout
pigeon-hole-15 (converted)	0.642s	unsat	0.643s	unsat	0.124s	unsat	-	timeout
pigeon-hole-16 (converted)	0.826s	unsat	0.851s	unsat	0.142s	unsat	-	timeout
pigeon-hole-17 (converted)	1.082s	unsat	1.099s	unsat	0.164s	unsat	-	timeout
pigeon-hole-18 (converted)	1.395s	unsat	1.408s	unsat	0.183s	unsat	-	timeout
pigeon-hole-19 (converted)	1.806s	unsat	1.787s	unsat	0.206s	unsat	-	timeout
pigeon-hole-20 (converted)	2.309s	unsat	2.368s	unsat	0.233s	unsat	-	timeout
prime_cone_sat_15 (converted)	0.405s	sat	0.031s	sat	-	timeout	0.012s	sat
25-14.slack (converted)	-	timeout	2.136s	sat	-	timeout	0.169s	sat
30-14.slack (converted)	-	timeout	3.921s	sat	-	timeout	7.436s	sat
30-16.slack (converted)	-	timeout	5.936s	sat	-	timeout	-	timeout
35-18.slack (converted)	-	timeout	12.753s	sat	-	timeout	8.930s	sat
35-23.slack (converted)	-	timeout	21.280s	sat	-	timeout	-	timeout
40-14.slack (converted)	-	timeout	15.802s	sat	-	timeout	0.016s	sat
40-16.slack (converted)	-	timeout	18.731s	sat	-	timeout	-	timeout
40-19.slack (converted)	-	timeout	18.758s	sat	-	timeout	-	timeout
45-13.slack (converted)	-	timeout	13.350s	sat	-	timeout	7.059s	sat
45-20.slack (converted)	-	timeout	22.443s	sat	31.486s	sat	-	timeout

The second table contains all our experiments.

input
c10_problem__001.smt2.slack (converted)	0.019s	sat	0.018s	sat	0.031s	sat	0.090s	sat
c10_problem__002.smt2.slack (converted)	0.040s	unsat	0.043s	unsat	0.044s	unsat	0.024s	unsat
c10_problem__003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c10_problem__004.smt2.slack (converted)	0.630s	sat	0.148s	sat	1.320s	sat	3.674s	sat
c10_problem__005.smt2.slack (converted)	-	timeout	-	timeout	1.785s	sat	0.063s	sat
c10_problem__006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.043s	sat
c100_problem__002.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c100_problem__003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c100_problem__004.smt2.slack (converted)	-	timeout	-	timeout	2.029s	sat	0.088s	sat
c100_problem__005.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c100_problem__006.smt2.slack (converted)	0.074s	unsat	0.067s	unsat	0.058s	unsat	0.061s	unsat
c20_problem__002.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c20_problem__003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.058s	sat
c20_problem__004.smt2.slack (converted)	0.074s	unsat	0.074s	unsat	0.049s	unsat	0.061s	unsat
c20_problem__005.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.104s	sat
c20_problem__006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.100s	sat
c30_problem__002.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.103s	sat
c30_problem__003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.234s	sat
c30_problem__004.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	22.172s	sat
c30_problem__005.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c30_problem__006.smt2.slack (converted)	0.103s	unsat	0.104s	unsat	0.052s	unsat	0.055s	unsat
c40_problem__002.smt2.slack (converted)	0.090s	unsat	0.099s	unsat	0.053s	unsat	0.087s	unsat
c40_problem__003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c40_problem__004.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c40_problem__005.smt2.slack (converted)	-	timeout	-	timeout	0.197s	sat	-	timeout
c40_problem__006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c50_problem__002.smt2.slack (converted)	0.076s	unsat	0.078s	unsat	0.054s	unsat	0.054s	unsat
c50_problem__003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	5.454s	sat
c50_problem__004.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	3.113s	sat
c50_problem__005.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c50_problem__006.smt2.slack (converted)	0.089s	unsat	0.088s	unsat	0.054s	unsat	0.090s	unsat
c60_problem__002.smt2.slack (converted)	-	timeout	-	timeout	0.405s	sat	5.043s	sat
c60_problem__003.smt2.slack (converted)	-	timeout	-	timeout	1.297s	sat	-	timeout
c60_problem__004.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c60_problem__005.smt2.slack (converted)	-	timeout	-	timeout	1.092s	sat	3.671s	sat
c60_problem__006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.125s	sat
c70_problem__002.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c70_problem__003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	3.616s	sat
c70_problem__004.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
c70_problem__005.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	7.582s	sat
c70_problem__006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	7.186s	sat
c80_problem__002.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.155s	sat
c80_problem__003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.103s	sat
c80_problem__004.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	7.127s	sat
c80_problem__005.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	7.161s	sat
c80_problem__006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	6.386s	sat
c90_problem__002.smt2.slack (converted)	-	timeout	-	timeout	42.762s	sat	0.267s	sat
c90_problem__003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.253s	sat
c90_problem__004.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.067s	sat
c90_problem__005.smt2.slack (converted)	0.126s	unsat	0.124s	unsat	0.058s	unsat	0.105s	unsat
c90_problem__006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v10_problem_2__001.smt2.slack (converted)	0.018s	sat	0.019s	sat	0.026s	sat	0.010s	sat
v10_problem_2__002.smt2.slack (converted)	0.017s	sat	0.018s	sat	0.028s	sat	0.010s	sat
v10_problem_2__003.smt2.slack (converted)	0.019s	sat	0.019s	sat	0.026s	sat	0.010s	sat
v10_problem_2__004.smt2.slack (converted)	0.018s	sat	0.019s	sat	0.027s	sat	0.010s	sat
v10_problem_2__005.smt2.slack (converted)	0.019s	sat	0.019s	sat	0.028s	sat	0.010s	sat
v10_problem_2__006.smt2.slack (converted)	0.019s	sat	0.019s	sat	0.030s	sat	0.011s	sat
v10_problem_2__007.smt2.slack (converted)	0.018s	sat	0.018s	sat	0.030s	sat	0.010s	sat
v10_problem_2__008.smt2.slack (converted)	0.019s	sat	0.019s	sat	0.029s	sat	0.010s	sat
v10_problem_2__009.smt2.slack (converted)	0.027s	sat	0.017s	sat	0.031s	sat	0.011s	sat
v10_problem_2__010.smt2.slack (converted)	0.018s	sat	0.017s	sat	0.029s	sat	0.011s	sat
v10_problem_2__011.smt2.slack (converted)	0.039s	sat	0.032s	sat	0.043s	sat	0.011s	sat
v10_problem_2__012.smt2.slack (converted)	0.030s	unsat	0.018s	unsat	0.032s	unsat	0.011s	unsat
v10_problem_2__013.smt2.slack (converted)	0.028s	sat	0.027s	sat	0.034s	sat	0.010s	sat
v10_problem_2__014.smt2.slack (converted)	0.067s	sat	0.028s	sat	0.033s	sat	0.010s	sat
v10_problem_2__015.smt2.slack (converted)	0.054s	sat	0.032s	sat	0.035s	sat	0.011s	sat
v10_problem_2__016.smt2.slack (converted)	0.030s	unsat	0.030s	unsat	0.036s	unsat	0.011s	unsat
v10_problem_2__017.smt2.slack (converted)	0.054s	sat	0.031s	sat	0.034s	sat	0.012s	sat
v10_problem_2__018.smt2.slack (converted)	0.053s	sat	0.032s	sat	0.035s	sat	0.012s	sat
v10_problem_2__019.smt2.slack (converted)	0.030s	unsat	0.031s	unsat	0.036s	unsat	0.011s	unsat
v10_problem_2__020.smt2.slack (converted)	0.032s	sat	0.032s	sat	0.034s	sat	0.011s	sat
v10_problem_2__021.smt2.slack (converted)	0.043s	unsat	0.042s	unsat	0.040s	unsat	0.012s	unsat
v10_problem_2__022.smt2.slack (converted)	0.319s	sat	0.077s	sat	0.055s	sat	0.012s	sat
v10_problem_2__023.smt2.slack (converted)	0.145s	sat	0.062s	sat	0.042s	sat	0.042s	sat
v10_problem_2__024.smt2.slack (converted)	0.029s	unsat	0.029s	unsat	0.039s	unsat	0.011s	unsat
v10_problem_2__025.smt2.slack (converted)	0.032s	unsat	0.032s	unsat	0.042s	unsat	0.011s	unsat
v10_problem_2__026.smt2.slack (converted)	0.029s	unsat	0.031s	unsat	0.044s	unsat	0.012s	unsat
v10_problem_2__027.smt2.slack (converted)	0.068s	unsat	0.064s	unsat	0.058s	unsat	0.017s	unsat
v10_problem_2__028.smt2.slack (converted)	0.053s	unsat	0.051s	unsat	0.039s	unsat	0.011s	unsat
v10_problem_2__029.smt2.slack (converted)	0.032s	unsat	0.031s	unsat	0.045s	unsat	0.012s	unsat
v10_problem_2__030.smt2.slack (converted)	0.041s	unsat	0.042s	unsat	0.041s	unsat	0.011s	unsat
v10_problem_2__031.smt2.slack (converted)	0.054s	unsat	0.067s	unsat	0.042s	unsat	0.012s	unsat
v10_problem_2__032.smt2.slack (converted)	0.041s	unsat	0.042s	unsat	0.044s	unsat	0.012s	unsat
v10_problem_2__033.smt2.slack (converted)	0.077s	unsat	0.078s	unsat	0.042s	unsat	0.012s	unsat
v10_problem_2__034.smt2.slack (converted)	0.030s	unsat	0.029s	unsat	0.052s	unsat	0.015s	unsat
v10_problem_2__035.smt2.slack (converted)	0.031s	unsat	0.030s	unsat	0.049s	unsat	0.013s	unsat
v10_problem__001.smt2.slack (converted)	0.018s	sat	0.019s	sat	0.027s	sat	0.009s	sat
v10_problem__002.smt2.slack (converted)	0.018s	sat	0.018s	sat	0.028s	sat	0.010s	sat
v10_problem__003.smt2.slack (converted)	0.019s	sat	0.019s	sat	0.027s	sat	0.010s	sat
v10_problem__005.smt2.slack (converted)	0.018s	sat	0.019s	sat	0.030s	sat	0.010s	sat
v10_problem__006.smt2.slack (converted)	0.031s	sat	0.017s	sat	0.029s	sat	0.011s	sat
v10_problem__007.smt2.slack (converted)	0.017s	sat	0.019s	sat	0.031s	sat	0.010s	sat
v10_problem__008.smt2.slack (converted)	0.019s	sat	0.019s	sat	0.030s	sat	0.010s	sat
v10_problem__009.smt2.slack (converted)	0.114s	sat	0.031s	sat	0.036s	sat	0.011s	sat
v10_problem__010.smt2.slack (converted)	0.019s	sat	0.019s	sat	0.029s	sat	0.010s	sat
v10_problem__012.smt2.slack (converted)	0.160s	sat	0.042s	sat	0.034s	sat	0.011s	sat
v10_problem__013.smt2.slack (converted)	0.030s	sat	0.031s	sat	0.044s	sat	0.011s	sat
v10_problem__014.smt2.slack (converted)	0.056s	sat	0.018s	sat	0.042s	sat	0.010s	sat
v10_problem__015.smt2.slack (converted)	-	timeout	-	timeout	0.044s	sat	0.011s	sat
v10_problem__016.smt2.slack (converted)	0.030s	unsat	0.030s	unsat	0.037s	unsat	0.013s	unsat
v10_problem__017.smt2.slack (converted)	0.032s	unsat	0.029s	unsat	0.038s	unsat	0.011s	unsat
v10_problem__018.smt2.slack (converted)	0.232s	sat	0.079s	sat	0.114s	sat	0.012s	sat
v10_problem__019.smt2.slack (converted)	0.030s	sat	0.031s	sat	0.036s	sat	0.012s	sat
v10_problem__020.smt2.slack (converted)	0.052s	unsat	0.044s	unsat	0.037s	unsat	0.011s	unsat
v10_problem__021.smt2.slack (converted)	0.043s	unsat	0.041s	unsat	0.045s	unsat	0.012s	unsat
v10_problem__022.smt2.slack (converted)	0.050s	unsat	0.043s	unsat	0.039s	unsat	0.012s	unsat
v10_problem__023.smt2.slack (converted)	0.113s	sat	0.077s	sat	0.047s	sat	0.012s	sat
v10_problem__024.smt2.slack (converted)	0.043s	unsat	0.040s	unsat	0.043s	unsat	0.012s	unsat
v10_problem__025.smt2.slack (converted)	0.054s	unsat	0.053s	unsat	0.039s	unsat	0.012s	unsat
v10_problem__026.smt2.slack (converted)	0.078s	unsat	0.067s	unsat	0.045s	unsat	0.011s	unsat
v10_problem__027.smt2.slack (converted)	0.115s	unsat	0.117s	unsat	0.045s	unsat	0.011s	unsat
v10_problem__028.smt2.slack (converted)	0.053s	unsat	0.053s	unsat	0.044s	unsat	0.012s	unsat
v10_problem__029.smt2.slack (converted)	0.110s	unsat	0.111s	unsat	0.042s	unsat	0.012s	unsat
v10_problem__030.smt2.slack (converted)	0.043s	unsat	0.041s	unsat	0.052s	unsat	0.013s	unsat
v10_problem__031.smt2.slack (converted)	0.066s	unsat	0.064s	unsat	0.049s	unsat	0.013s	unsat
v10_problem__032.smt2.slack (converted)	0.098s	unsat	0.097s	unsat	0.053s	unsat	0.013s	unsat
v10_problem__034.smt2.slack (converted)	0.144s	unsat	0.135s	unsat	0.043s	unsat	0.011s	unsat
v10_problem__035.smt2.slack (converted)	0.090s	unsat	0.086s	unsat	0.045s	unsat	0.012s	unsat
v15_problem_2__001.smt2.slack (converted)	0.276s	sat	-	timeout	0.041s	sat	0.012s	sat
v15_problem_2__002.smt2.slack (converted)	0.352s	sat	0.051s	sat	0.052s	sat	0.012s	sat
v15_problem_2__003.smt2.slack (converted)	0.053s	sat	0.062s	sat	0.038s	sat	0.011s	sat
v15_problem_2__004.smt2.slack (converted)	0.054s	sat	0.148s	sat	0.037s	sat	0.012s	sat
v15_problem_2__005.smt2.slack (converted)	0.018s	sat	0.019s	sat	0.036s	sat	0.011s	sat
v15_problem_2__006.smt2.slack (converted)	-	timeout	-	timeout	0.104s	sat	0.019s	sat
v15_problem_2__007.smt2.slack (converted)	0.617s	sat	0.256s	sat	0.171s	sat	0.012s	sat
v15_problem_2__008.smt2.slack (converted)	0.220s	sat	0.207s	sat	0.040s	sat	0.012s	sat
v15_problem_2__009.smt2.slack (converted)	0.030s	sat	0.027s	sat	0.039s	sat	0.012s	sat
v15_problem_2__010.smt2.slack (converted)	0.076s	sat	0.113s	sat	0.041s	sat	0.012s	sat
v15_problem_2__011.smt2.slack (converted)	0.231s	unsat	0.235s	unsat	0.056s	unsat	0.017s	unsat
v15_problem_2__012.smt2.slack (converted)	-	timeout	-	timeout	0.044s	sat	0.012s	sat
v15_problem_2__013.smt2.slack (converted)	-	timeout	-	timeout	0.081s	sat	0.012s	sat
v15_problem_2__014.smt2.slack (converted)	1.032s	sat	0.459s	sat	0.341s	sat	0.640s	sat
v15_problem_2__015.smt2.slack (converted)	-	timeout	0.508s	sat	0.249s	sat	0.024s	sat
v15_problem_2__016.smt2.slack (converted)	10.566s	sat	0.360s	sat	0.108s	sat	0.015s	sat
v15_problem_2__017.smt2.slack (converted)	-	timeout	-	timeout	0.077s	sat	0.040s	sat
v15_problem_2__018.smt2.slack (converted)	-	timeout	-	timeout	4.172s	sat	0.206s	sat
v15_problem_2__019.smt2.slack (converted)	0.383s	unsat	0.388s	unsat	0.085s	unsat	0.016s	unsat
v15_problem_2__020.smt2.slack (converted)	0.265s	unsat	0.256s	unsat	0.067s	unsat	0.021s	unsat
v15_problem_2__021.smt2.slack (converted)	0.183s	unsat	0.178s	unsat	0.099s	unsat	0.092s	unsat
v15_problem_2__022.smt2.slack (converted)	0.341s	unsat	0.335s	unsat	0.072s	unsat	0.017s	unsat
v15_problem_2__023.smt2.slack (converted)	1.886s	sat	0.487s	sat	0.213s	sat	0.089s	sat
v15_problem_2__024.smt2.slack (converted)	0.262s	unsat	0.276s	unsat	0.093s	unsat	0.018s	unsat
v15_problem_2__025.smt2.slack (converted)	-	timeout	-	timeout	1.579s	unsat	11.770s	unsat
v15_problem__001.smt2.slack (converted)	0.764s	sat	0.132s	sat	0.036s	sat	0.011s	sat
v15_problem__002.smt2.slack (converted)	0.039s	sat	0.029s	sat	0.054s	sat	0.011s	sat
v15_problem__003.smt2.slack (converted)	0.071s	sat	0.041s	sat	0.044s	sat	0.012s	sat
v15_problem__004.smt2.slack (converted)	0.220s	sat	0.051s	sat	0.128s	sat	0.011s	sat
v15_problem__005.smt2.slack (converted)	0.113s	sat	0.103s	sat	0.035s	sat	0.010s	sat
v15_problem__006.smt2.slack (converted)	0.029s	sat	0.031s	sat	0.040s	sat	0.013s	sat
v15_problem__007.smt2.slack (converted)	1.048s	sat	0.151s	sat	0.042s	sat	0.011s	sat
v15_problem__008.smt2.slack (converted)	0.086s	sat	0.108s	sat	0.037s	sat	0.011s	sat
v15_problem__009.smt2.slack (converted)	1.835s	sat	-	timeout	0.041s	sat	0.014s	sat
v15_problem__010.smt2.slack (converted)	-	timeout	-	timeout	0.077s	sat	0.012s	sat
v15_problem__011.smt2.slack (converted)	1.132s	sat	0.525s	sat	0.957s	sat	0.383s	sat
v15_problem__012.smt2.slack (converted)	7.327s	sat	0.394s	sat	0.409s	sat	0.019s	sat
v15_problem__013.smt2.slack (converted)	2.234s	sat	0.275s	sat	0.171s	sat	0.014s	sat
v15_problem__014.smt2.slack (converted)	1.792s	sat	0.255s	sat	0.095s	sat	0.016s	sat
v15_problem__015.smt2.slack (converted)	-	timeout	0.471s	sat	0.432s	sat	0.019s	sat
v15_problem__016.smt2.slack (converted)	0.241s	unsat	0.238s	unsat	0.058s	unsat	0.015s	unsat
v15_problem__017.smt2.slack (converted)	-	timeout	-	timeout	2.783s	sat	0.794s	sat
v15_problem__018.smt2.slack (converted)	2.847s	sat	-	timeout	0.126s	sat	0.021s	sat
v15_problem__019.smt2.slack (converted)	5.832s	sat	0.577s	sat	1.184s	sat	0.025s	sat
v15_problem__020.smt2.slack (converted)	5.719s	sat	-	timeout	0.107s	sat	0.022s	sat
v15_problem__021.smt2.slack (converted)	16.876s	sat	1.022s	sat	1.235s	sat	0.026s	sat
v15_problem__022.smt2.slack (converted)	0.217s	unsat	0.223s	unsat	0.060s	unsat	0.016s	unsat
v15_problem__023.smt2.slack (converted)	0.067s	unsat	0.063s	unsat	0.060s	unsat	0.026s	unsat
v15_problem__024.smt2.slack (converted)	0.384s	unsat	0.388s	unsat	0.055s	unsat	0.022s	unsat
v15_problem__025.smt2.slack (converted)	0.277s	unsat	0.276s	unsat	0.102s	unsat	0.038s	unsat
v20_problem_2__001.smt2.slack (converted)	0.041s	sat	0.042s	sat	0.041s	sat	0.012s	sat
v20_problem_2__002.smt2.slack (converted)	3.624s	sat	0.695s	sat	0.041s	sat	0.011s	sat
v20_problem_2__003.smt2.slack (converted)	1.793s	sat	0.270s	sat	0.047s	sat	0.012s	sat
v20_problem_2__004.smt2.slack (converted)	1.404s	sat	0.359s	sat	0.055s	sat	0.012s	sat
v20_problem_2__005.smt2.slack (converted)	2.341s	sat	0.594s	sat	0.043s	sat	0.011s	sat
v20_problem_2__006.smt2.slack (converted)	3.561s	sat	0.750s	sat	1.098s	sat	0.026s	sat
v20_problem_2__007.smt2.slack (converted)	-	timeout	-	timeout	1.010s	sat	0.024s	sat
v20_problem_2__008.smt2.slack (converted)	-	timeout	0.946s	sat	0.337s	sat	0.014s	sat
v20_problem_2__009.smt2.slack (converted)	-	timeout	-	timeout	0.358s	sat	0.038s	sat
v20_problem_2__010.smt2.slack (converted)	5.704s	sat	0.628s	sat	0.051s	sat	0.647s	sat
v20_problem_2__011.smt2.slack (converted)	-	timeout	-	timeout	0.548s	sat	0.157s	sat
v20_problem_2__012.smt2.slack (converted)	7.397s	sat	-	timeout	0.051s	sat	0.013s	sat
v20_problem_2__013.smt2.slack (converted)	-	timeout	-	timeout	0.051s	sat	0.038s	sat
v20_problem_2__014.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.146s	sat
v20_problem_2__015.smt2.slack (converted)	-	timeout	-	timeout	0.931s	sat	7.179s	sat
v20_problem_2__016.smt2.slack (converted)	-	timeout	-	timeout	0.667s	sat	0.180s	sat
v20_problem_2__017.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	7.228s	sat
v20_problem_2__018.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v20_problem_2__019.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.203s	sat
v20_problem_2__020.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	7.811s	sat
v20_problem_2__021.smt2.slack (converted)	-	timeout	-	timeout	25.985s	sat	-	timeout
v20_problem_2__022.smt2.slack (converted)	-	timeout	-	timeout	33.978s	sat	0.255s	sat
v20_problem_2__023.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v20_problem_2__024.smt2.slack (converted)	-	timeout	-	timeout	0.474s	sat	7.495s	sat
v20_problem_2__025.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	30.046s	sat
v20_problem_2__026.smt2.slack (converted)	1.661s	unsat	1.672s	unsat	0.193s	unsat	0.766s	unsat
v20_problem_2__027.smt2.slack (converted)	1.106s	unsat	1.148s	unsat	0.125s	unsat	0.284s	unsat
v20_problem_2__028.smt2.slack (converted)	-	timeout	-	timeout	44.547s	sat	-	timeout
v20_problem_2__029.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.564s	sat
v20_problem_2__030.smt2.slack (converted)	0.794s	unsat	0.789s	unsat	0.097s	unsat	0.369s	unsat
v20_problem_2__031.smt2.slack (converted)	4.915s	unsat	4.939s	unsat	0.232s	unsat	1.002s	unsat
v20_problem_2__032.smt2.slack (converted)	0.874s	unsat	0.900s	unsat	0.187s	unsat	0.629s	unsat
v20_problem_2__033.smt2.slack (converted)	1.404s	unsat	1.428s	unsat	0.294s	unsat	0.645s	unsat
v20_problem_2__034.smt2.slack (converted)	2.774s	unsat	2.656s	unsat	0.268s	unsat	0.649s	unsat
v20_problem_2__035.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.915s	sat
v20_problem__001.smt2.slack (converted)	0.988s	sat	0.375s	sat	0.331s	sat	0.012s	sat
v20_problem__002.smt2.slack (converted)	3.901s	sat	0.262s	sat	0.062s	sat	0.012s	sat
v20_problem__003.smt2.slack (converted)	-	timeout	-	timeout	0.043s	sat	0.013s	sat
v20_problem__004.smt2.slack (converted)	2.664s	sat	0.369s	sat	0.147s	sat	0.012s	sat
v20_problem__005.smt2.slack (converted)	0.318s	sat	0.270s	sat	0.045s	sat	0.013s	sat
v20_problem__006.smt2.slack (converted)	-	timeout	-	timeout	5.026s	sat	0.036s	sat
v20_problem__007.smt2.slack (converted)	12.717s	sat	1.277s	sat	2.840s	sat	0.027s	sat
v20_problem__008.smt2.slack (converted)	2.529s	sat	0.527s	sat	0.046s	sat	0.014s	sat
v20_problem__009.smt2.slack (converted)	-	timeout	-	timeout	0.602s	sat	0.142s	sat
v20_problem__010.smt2.slack (converted)	7.468s	sat	0.940s	sat	0.046s	sat	0.012s	sat
v20_problem__011.smt2.slack (converted)	22.282s	sat	0.595s	sat	-	timeout	0.409s	sat
v20_problem__012.smt2.slack (converted)	-	timeout	-	timeout	0.554s	sat	0.047s	sat
v20_problem__013.smt2.slack (converted)	9.283s	sat	1.878s	sat	0.714s	sat	0.622s	sat
v20_problem__014.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v20_problem__015.smt2.slack (converted)	9.875s	sat	0.707s	sat	0.519s	sat	0.018s	sat
v20_problem__016.smt2.slack (converted)	1.238s	unsat	1.171s	unsat	0.096s	unsat	0.194s	unsat
v20_problem__017.smt2.slack (converted)	-	timeout	-	timeout	8.392s	sat	0.096s	sat
v20_problem__018.smt2.slack (converted)	0.746s	unsat	0.702s	unsat	0.105s	unsat	0.265s	unsat
v20_problem__019.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	7.603s	sat
v20_problem__020.smt2.slack (converted)	-	timeout	-	timeout	2.447s	sat	8.028s	sat
v20_problem__021.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v20_problem__022.smt2.slack (converted)	19.189s	sat	3.493s	sat	7.719s	sat	0.018s	sat
v20_problem__023.smt2.slack (converted)	1.512s	unsat	1.480s	unsat	0.158s	unsat	0.215s	unsat
v20_problem__024.smt2.slack (converted)	-	timeout	-	timeout	11.340s	sat	0.552s	sat
v20_problem__025.smt2.slack (converted)	1.234s	unsat	1.274s	unsat	0.142s	unsat	0.869s	unsat
v20_problem__026.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v20_problem__027.smt2.slack (converted)	2.828s	unsat	2.803s	unsat	0.217s	unsat	0.660s	unsat
v20_problem__028.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v20_problem__029.smt2.slack (converted)	1.786s	unsat	1.792s	unsat	0.274s	unsat	0.699s	unsat
v20_problem__030.smt2.slack (converted)	-	timeout	-	timeout	4.531s	sat	7.552s	sat
v20_problem__031.smt2.slack (converted)	2.818s	unsat	2.736s	unsat	0.168s	unsat	0.547s	unsat
v20_problem__032.smt2.slack (converted)	2.780s	unsat	2.704s	unsat	0.173s	unsat	0.427s	unsat
v20_problem__033.smt2.slack (converted)	2.917s	unsat	2.917s	unsat	0.172s	unsat	0.383s	unsat
v20_problem__034.smt2.slack (converted)	2.603s	unsat	2.562s	unsat	0.287s	unsat	0.957s	unsat
v20_problem__035.smt2.slack (converted)	2.775s	unsat	2.844s	unsat	0.159s	unsat	0.941s	unsat
v25_problem_2__001.smt2.slack (converted)	2.166s	sat	0.896s	sat	0.363s	sat	0.016s	sat
v25_problem_2__002.smt2.slack (converted)	-	timeout	0.878s	sat	0.682s	sat	1.028s	sat
v25_problem_2__003.smt2.slack (converted)	8.246s	sat	0.994s	sat	0.048s	sat	0.012s	sat
v25_problem_2__004.smt2.slack (converted)	3.351s	sat	1.175s	sat	0.047s	sat	0.012s	sat
v25_problem_2__005.smt2.slack (converted)	2.388s	sat	1.908s	sat	0.076s	sat	0.013s	sat
v25_problem_2__006.smt2.slack (converted)	-	timeout	-	timeout	1.447s	sat	0.137s	sat
v25_problem_2__007.smt2.slack (converted)	-	timeout	1.860s	sat	2.361s	sat	0.069s	sat
v25_problem_2__008.smt2.slack (converted)	8.130s	sat	1.813s	sat	0.325s	sat	0.014s	sat
v25_problem_2__009.smt2.slack (converted)	0.341s	sat	1.720s	sat	0.446s	sat	0.022s	sat
v25_problem_2__010.smt2.slack (converted)	10.160s	sat	1.358s	sat	0.100s	sat	0.015s	sat
v25_problem_2__011.smt2.slack (converted)	2.788s	sat	-	timeout	1.136s	sat	11.104s	sat
v25_problem_2__012.smt2.slack (converted)	-	timeout	-	timeout	7.101s	sat	-	timeout
v25_problem_2__013.smt2.slack (converted)	-	timeout	-	timeout	2.379s	sat	7.101s	sat
v25_problem_2__014.smt2.slack (converted)	-	timeout	3.989s	sat	1.508s	sat	0.033s	sat
v25_problem_2__015.smt2.slack (converted)	-	timeout	4.092s	sat	2.186s	sat	-	timeout
v25_problem_2__016.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem_2__017.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem_2__018.smt2.slack (converted)	-	timeout	-	timeout	18.655s	sat	7.681s	sat
v25_problem_2__019.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem_2__020.smt2.slack (converted)	-	timeout	-	timeout	3.469s	sat	1.880s	sat
v25_problem_2__021.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem_2__022.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem_2__023.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem_2__024.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem_2__025.smt2.slack (converted)	-	timeout	-	timeout	23.022s	sat	-	timeout
v25_problem_2__026.smt2.slack (converted)	-	timeout	-	timeout	15.817s	sat	-	timeout
v25_problem_2__027.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem_2__028.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	1.292s	sat
v25_problem_2__029.smt2.slack (converted)	4.327s	unsat	4.313s	unsat	0.182s	unsat	1.086s	unsat
v25_problem_2__030.smt2.slack (converted)	-	timeout	15.226s	sat	-	timeout	25.590s	sat
v25_problem_2__031.smt2.slack (converted)	6.211s	unsat	6.210s	unsat	0.311s	unsat	1.676s	unsat
v25_problem_2__032.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem_2__033.smt2.slack (converted)	5.567s	unsat	5.572s	unsat	0.267s	unsat	1.816s	unsat
v25_problem_2__034.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	26.136s	sat
v25_problem_2__035.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem__001.smt2.slack (converted)	0.981s	sat	0.645s	sat	0.817s	sat	0.015s	sat
v25_problem__002.smt2.slack (converted)	2.515s	sat	1.086s	sat	0.145s	sat	0.014s	sat
v25_problem__003.smt2.slack (converted)	3.326s	sat	0.742s	sat	0.120s	sat	0.014s	sat
v25_problem__004.smt2.slack (converted)	14.141s	sat	1.144s	sat	0.125s	sat	0.019s	sat
v25_problem__005.smt2.slack (converted)	14.345s	sat	0.926s	sat	0.051s	sat	0.015s	sat
v25_problem__006.smt2.slack (converted)	8.980s	sat	1.136s	sat	15.919s	sat	0.017s	sat
v25_problem__007.smt2.slack (converted)	-	timeout	-	timeout	6.463s	sat	0.018s	sat
v25_problem__008.smt2.slack (converted)	-	timeout	1.199s	sat	3.828s	sat	0.045s	sat
v25_problem__009.smt2.slack (converted)	15.906s	sat	1.355s	sat	1.750s	sat	0.155s	sat
v25_problem__010.smt2.slack (converted)	-	timeout	1.076s	sat	1.461s	sat	0.115s	sat
v25_problem__011.smt2.slack (converted)	-	timeout	2.148s	sat	-	timeout	0.246s	sat
v25_problem__012.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	7.235s	sat
v25_problem__013.smt2.slack (converted)	23.720s	sat	3.207s	sat	6.554s	sat	0.018s	sat
v25_problem__014.smt2.slack (converted)	-	timeout	-	timeout	0.995s	sat	0.191s	sat
v25_problem__015.smt2.slack (converted)	-	timeout	-	timeout	29.211s	sat	-	timeout
v25_problem__016.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem__017.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem__018.smt2.slack (converted)	-	timeout	-	timeout	2.448s	sat	0.024s	sat
v25_problem__019.smt2.slack (converted)	-	timeout	3.516s	sat	11.478s	sat	0.781s	sat
v25_problem__020.smt2.slack (converted)	-	timeout	4.249s	sat	6.881s	sat	0.024s	sat
v25_problem__021.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	1.546s	sat
v25_problem__022.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem__023.smt2.slack (converted)	-	timeout	-	timeout	29.516s	sat	1.077s	sat
v25_problem__024.smt2.slack (converted)	-	timeout	-	timeout	4.240s	sat	-	timeout
v25_problem__025.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem__026.smt2.slack (converted)	-	timeout	-	timeout	57.590s	sat	-	timeout
v25_problem__027.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem__028.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem__029.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem__030.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem__031.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v25_problem__032.smt2.slack (converted)	5.096s	unsat	5.111s	unsat	0.288s	unsat	1.375s	unsat
v25_problem__033.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	8.997s	sat
v25_problem__034.smt2.slack (converted)	9.361s	unsat	9.569s	unsat	0.250s	unsat	1.026s	unsat
v25_problem__035.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem_2__001.smt2.slack (converted)	41.500s	sat	2.266s	sat	0.554s	sat	0.013s	sat
v30_problem_2__002.smt2.slack (converted)	-	timeout	2.085s	sat	1.809s	sat	0.013s	sat
v30_problem_2__003.smt2.slack (converted)	15.596s	sat	2.851s	sat	0.078s	sat	0.013s	sat
v30_problem_2__004.smt2.slack (converted)	9.400s	sat	1.823s	sat	0.054s	sat	0.016s	sat
v30_problem_2__005.smt2.slack (converted)	12.396s	sat	1.393s	sat	0.220s	sat	0.016s	sat
v30_problem_2__006.smt2.slack (converted)	-	timeout	4.558s	sat	15.764s	sat	7.268s	sat
v30_problem_2__007.smt2.slack (converted)	-	timeout	-	timeout	1.944s	sat	7.133s	sat
v30_problem_2__008.smt2.slack (converted)	33.316s	sat	-	timeout	3.041s	sat	0.172s	sat
v30_problem_2__009.smt2.slack (converted)	31.742s	sat	3.138s	sat	-	timeout	5.896s	sat
v30_problem_2__010.smt2.slack (converted)	4.370s	sat	10.075s	sat	2.031s	sat	0.017s	sat
v30_problem_2__011.smt2.slack (converted)	-	timeout	3.634s	sat	0.067s	sat	0.015s	sat
v30_problem_2__012.smt2.slack (converted)	-	timeout	-	timeout	4.256s	sat	0.853s	sat
v30_problem_2__013.smt2.slack (converted)	-	timeout	-	timeout	9.799s	sat	-	timeout
v30_problem_2__014.smt2.slack (converted)	-	timeout	-	timeout	6.642s	sat	0.983s	sat
v30_problem_2__015.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem_2__016.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem_2__017.smt2.slack (converted)	-	timeout	-	timeout	23.909s	sat	1.088s	sat
v30_problem_2__018.smt2.slack (converted)	-	timeout	9.358s	sat	40.857s	sat	-	timeout
v30_problem_2__019.smt2.slack (converted)	-	timeout	3.487s	sat	10.017s	sat	-	timeout
v30_problem_2__020.smt2.slack (converted)	-	timeout	-	timeout	0.067s	sat	-	timeout
v30_problem_2__021.smt2.slack (converted)	-	timeout	-	timeout	17.178s	sat	0.016s	sat
v30_problem_2__022.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem_2__023.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem_2__024.smt2.slack (converted)	-	timeout	-	timeout	4.805s	sat	11.482s	sat
v30_problem_2__025.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem_2__026.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem_2__027.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem_2__028.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	11.980s	sat
v30_problem_2__029.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	10.372s	sat
v30_problem_2__030.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem_2__031.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem_2__032.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	1.690s	sat
v30_problem_2__033.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem_2__034.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem_2__035.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	1.828s	sat
v30_problem__001.smt2.slack (converted)	1.527s	sat	2.056s	sat	0.050s	sat	0.013s	sat
v30_problem__002.smt2.slack (converted)	-	timeout	-	timeout	0.079s	sat	0.060s	sat
v30_problem__003.smt2.slack (converted)	-	timeout	1.617s	sat	3.644s	sat	0.129s	sat
v30_problem__004.smt2.slack (converted)	11.320s	sat	2.217s	sat	0.892s	sat	0.013s	sat
v30_problem__005.smt2.slack (converted)	0.043s	sat	0.042s	sat	0.137s	sat	0.013s	sat
v30_problem__006.smt2.slack (converted)	5.849s	sat	5.015s	sat	4.478s	sat	0.037s	sat
v30_problem__007.smt2.slack (converted)	-	timeout	-	timeout	2.504s	sat	0.014s	sat
v30_problem__008.smt2.slack (converted)	41.432s	sat	-	timeout	1.707s	sat	0.017s	sat
v30_problem__009.smt2.slack (converted)	-	timeout	-	timeout	9.778s	sat	0.014s	sat
v30_problem__010.smt2.slack (converted)	41.799s	sat	2.684s	sat	23.552s	sat	0.051s	sat
v30_problem__011.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	23.470s	sat
v30_problem__012.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.277s	sat
v30_problem__013.smt2.slack (converted)	-	timeout	-	timeout	1.749s	sat	0.758s	sat
v30_problem__014.smt2.slack (converted)	-	timeout	3.598s	sat	-	timeout	8.393s	sat
v30_problem__015.smt2.slack (converted)	-	timeout	-	timeout	real	sat	-	timeout
v30_problem__016.smt2.slack (converted)	-	timeout	-	timeout	39.531s	sat	0.478s	sat
v30_problem__017.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem__018.smt2.slack (converted)	52.597s	sat	3.948s	sat	5.948s	sat	9.575s	sat
v30_problem__019.smt2.slack (converted)	-	timeout	-	timeout	17.669s	sat	7.313s	sat
v30_problem__020.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem__021.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem__022.smt2.slack (converted)	-	timeout	-	timeout	47.025s	sat	-	timeout
v30_problem__023.smt2.slack (converted)	-	timeout	12.994s	sat	-	timeout	0.348s	sat
v30_problem__024.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	9.973s	sat
v30_problem__025.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem__026.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem__027.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	1.838s	sat
v30_problem__028.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem__029.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem__030.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem__031.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem__032.smt2.slack (converted)	14.072s	unsat	13.787s	unsat	0.286s	unsat	2.366s	unsat
v30_problem__033.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem__034.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v30_problem__035.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__001.smt2.slack (converted)	0.051s	sat	0.055s	sat	1.991s	sat	0.014s	sat
v35_problem_2__002.smt2.slack (converted)	1.537s	sat	2.043s	sat	0.122s	sat	0.025s	sat
v35_problem_2__003.smt2.slack (converted)	2.855s	sat	1.842s	sat	0.055s	sat	0.013s	sat
v35_problem_2__004.smt2.slack (converted)	0.055s	sat	0.056s	sat	0.114s	sat	0.013s	sat
v35_problem_2__005.smt2.slack (converted)	15.243s	sat	-	timeout	0.054s	sat	0.014s	sat
v35_problem_2__006.smt2.slack (converted)	-	timeout	3.265s	sat	7.035s	sat	0.722s	sat
v35_problem_2__007.smt2.slack (converted)	59.781s	sat	2.501s	sat	7.203s	sat	0.463s	sat
v35_problem_2__008.smt2.slack (converted)	-	timeout	-	timeout	0.273s	sat	0.015s	sat
v35_problem_2__009.smt2.slack (converted)	-	timeout	4.366s	sat	0.066s	sat	0.014s	sat
v35_problem_2__010.smt2.slack (converted)	24.423s	sat	4.679s	sat	0.060s	sat	0.013s	sat
v35_problem_2__011.smt2.slack (converted)	-	timeout	6.472s	sat	4.625s	sat	-	timeout
v35_problem_2__012.smt2.slack (converted)	-	timeout	-	timeout	4.256s	sat	-	timeout
v35_problem_2__013.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	1.115s	sat
v35_problem_2__014.smt2.slack (converted)	-	timeout	5.352s	sat	12.093s	sat	0.015s	sat
v35_problem_2__015.smt2.slack (converted)	-	timeout	-	timeout	15.942s	sat	0.917s	sat
v35_problem_2__016.smt2.slack (converted)	-	timeout	7.533s	sat	6.827s	sat	26.867s	sat
v35_problem_2__017.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__018.smt2.slack (converted)	-	timeout	-	timeout	45.092s	sat	-	timeout
v35_problem_2__019.smt2.slack (converted)	-	timeout	-	timeout	17.864s	sat	-	timeout
v35_problem_2__020.smt2.slack (converted)	-	timeout	11.962s	sat	46.623s	sat	0.016s	sat
v35_problem_2__021.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__022.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__023.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__024.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__025.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__026.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__027.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__028.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	9.316s	sat
v35_problem_2__029.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__030.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__031.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__032.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	9.724s	sat
v35_problem_2__033.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__034.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem_2__035.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	9.615s	sat
v35_problem__001.smt2.slack (converted)	3.203s	sat	2.565s	sat	0.053s	sat	0.013s	sat
v35_problem__002.smt2.slack (converted)	38.395s	sat	3.289s	sat	0.110s	sat	0.015s	sat
v35_problem__003.smt2.slack (converted)	24.008s	sat	2.762s	sat	0.895s	sat	0.202s	sat
v35_problem__004.smt2.slack (converted)	2.019s	sat	2.233s	sat	0.056s	sat	0.013s	sat
v35_problem__005.smt2.slack (converted)	4.543s	sat	2.349s	sat	1.081s	sat	0.015s	sat
v35_problem__006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.075s	sat
v35_problem__007.smt2.slack (converted)	-	timeout	2.863s	sat	0.064s	sat	0.390s	sat
v35_problem__008.smt2.slack (converted)	-	timeout	3.629s	sat	16.456s	sat	0.079s	sat
v35_problem__009.smt2.slack (converted)	-	timeout	4.311s	sat	8.784s	sat	0.166s	sat
v35_problem__010.smt2.slack (converted)	45.322s	sat	-	timeout	4.436s	sat	0.493s	sat
v35_problem__011.smt2.slack (converted)	-	timeout	4.695s	sat	21.001s	sat	1.662s	sat
v35_problem__012.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	1.253s	sat
v35_problem__013.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	22.267s	sat
v35_problem__014.smt2.slack (converted)	-	timeout	14.233s	sat	-	timeout	0.069s	sat
v35_problem__015.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	7.871s	sat
v35_problem__016.smt2.slack (converted)	-	timeout	-	timeout	7.026s	sat	1.892s	sat
v35_problem__017.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem__018.smt2.slack (converted)	-	timeout	-	timeout	11.929s	sat	1.618s	sat
v35_problem__019.smt2.slack (converted)	-	timeout	-	timeout	25.006s	sat	0.022s	sat
v35_problem__020.smt2.slack (converted)	-	timeout	-	timeout	8.314s	sat	1.032s	sat
v35_problem__021.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem__022.smt2.slack (converted)	-	timeout	-	timeout	43.148s	sat	-	timeout
v35_problem__023.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem__024.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem__025.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem__026.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	1.141s	sat
v35_problem__027.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	9.916s	sat
v35_problem__028.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem__029.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem__030.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem__031.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem__032.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem__033.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem__034.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v35_problem__035.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__001.smt2.slack (converted)	16.701s	sat	4.381s	sat	1.159s	sat	0.015s	sat
v40_problem_2__002.smt2.slack (converted)	1.045s	sat	2.607s	sat	0.057s	sat	0.014s	sat
v40_problem_2__003.smt2.slack (converted)	7.762s	sat	3.467s	sat	0.061s	sat	0.013s	sat
v40_problem_2__004.smt2.slack (converted)	6.689s	sat	4.845s	sat	0.094s	sat	0.014s	sat
v40_problem_2__005.smt2.slack (converted)	13.414s	sat	3.412s	sat	0.740s	sat	0.029s	sat
v40_problem_2__006.smt2.slack (converted)	-	timeout	5.287s	sat	9.333s	sat	0.018s	sat
v40_problem_2__007.smt2.slack (converted)	-	timeout	5.462s	sat	0.065s	sat	0.015s	sat
v40_problem_2__008.smt2.slack (converted)	-	timeout	-	timeout	6.680s	sat	0.016s	sat
v40_problem_2__009.smt2.slack (converted)	-	timeout	-	timeout	0.381s	sat	0.015s	sat
v40_problem_2__010.smt2.slack (converted)	-	timeout	5.322s	sat	0.133s	sat	0.079s	sat
v40_problem_2__011.smt2.slack (converted)	-	timeout	-	timeout	33.338s	sat	7.833s	sat
v40_problem_2__012.smt2.slack (converted)	-	timeout	-	timeout	22.225s	sat	0.610s	sat
v40_problem_2__013.smt2.slack (converted)	-	timeout	9.229s	sat	-	timeout	-	timeout
v40_problem_2__014.smt2.slack (converted)	-	timeout	-	timeout	9.233s	sat	7.054s	sat
v40_problem_2__015.smt2.slack (converted)	-	timeout	9.397s	sat	12.838s	sat	0.022s	sat
v40_problem_2__016.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__017.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__018.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__019.smt2.slack (converted)	-	timeout	-	timeout	6.468s	sat	0.614s	sat
v40_problem_2__020.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	23.629s	sat
v40_problem_2__021.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.310s	sat
v40_problem_2__022.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.028s	sat
v40_problem_2__023.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__024.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__025.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	7.613s	sat
v40_problem_2__026.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__027.smt2.slack (converted)	-	timeout	-	timeout	11.629s	sat	-	timeout
v40_problem_2__028.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__029.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__030.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__031.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	12.066s	sat
v40_problem_2__032.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__033.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__034.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem_2__035.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem__001.smt2.slack (converted)	1.702s	sat	3.141s	sat	31.889s	sat	0.014s	sat
v40_problem__002.smt2.slack (converted)	17.037s	sat	3.234s	sat	0.206s	sat	0.015s	sat
v40_problem__003.smt2.slack (converted)	-	timeout	3.460s	sat	0.381s	sat	0.013s	sat
v40_problem__004.smt2.slack (converted)	6.544s	sat	3.020s	sat	0.059s	sat	0.013s	sat
v40_problem__005.smt2.slack (converted)	12.865s	sat	3.285s	sat	0.457s	sat	0.014s	sat
v40_problem__006.smt2.slack (converted)	-	timeout	7.553s	sat	5.810s	sat	0.014s	sat
v40_problem__007.smt2.slack (converted)	-	timeout	-	timeout	38.786s	sat	0.020s	sat
v40_problem__008.smt2.slack (converted)	-	timeout	-	timeout	11.358s	sat	0.654s	sat
v40_problem__009.smt2.slack (converted)	-	timeout	6.027s	sat	12.254s	sat	0.015s	sat
v40_problem__010.smt2.slack (converted)	-	timeout	5.924s	sat	7.109s	sat	0.015s	sat
v40_problem__011.smt2.slack (converted)	-	timeout	11.784s	sat	7.692s	sat	0.025s	sat
v40_problem__012.smt2.slack (converted)	-	timeout	-	timeout	6.781s	sat	1.766s	sat
v40_problem__013.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	8.330s	sat
v40_problem__014.smt2.slack (converted)	-	timeout	10.474s	sat	16.730s	sat	-	timeout
v40_problem__015.smt2.slack (converted)	4.714s	sat	-	timeout	13.382s	sat	9.116s	sat
v40_problem__016.smt2.slack (converted)	-	timeout	-	timeout	25.195s	sat	0.039s	sat
v40_problem__017.smt2.slack (converted)	-	timeout	14.479s	sat	40.042s	sat	0.207s	sat
v40_problem__018.smt2.slack (converted)	-	timeout	-	timeout	4.707s	sat	-	timeout
v40_problem__019.smt2.slack (converted)	-	timeout	18.158s	sat	-	timeout	0.285s	sat
v40_problem__020.smt2.slack (converted)	-	timeout	22.389s	sat	39.244s	sat	-	timeout
v40_problem__021.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem__022.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem__023.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	8.109s	sat
v40_problem__024.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	0.986s	sat
v40_problem__025.smt2.slack (converted)	-	timeout	-	timeout	11.570s	sat	10.558s	sat
v40_problem__026.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem__027.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem__028.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem__029.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem__030.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem__031.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem__032.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem__033.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	26.065s	sat
v40_problem__034.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v40_problem__035.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__001.smt2.slack (converted)	-	timeout	4.553s	sat	0.192s	sat	0.015s	sat
v45_problem_2__002.smt2.slack (converted)	-	timeout	3.457s	sat	0.660s	sat	0.016s	sat
v45_problem_2__003.smt2.slack (converted)	46.092s	sat	-	timeout	4.005s	sat	0.018s	sat
v45_problem_2__004.smt2.slack (converted)	8.041s	sat	4.470s	sat	10.210s	sat	0.017s	sat
v45_problem_2__005.smt2.slack (converted)	45.446s	sat	4.956s	sat	0.065s	sat	0.014s	sat
v45_problem_2__006.smt2.slack (converted)	-	timeout	13.927s	sat	19.532s	sat	0.015s	sat
v45_problem_2__007.smt2.slack (converted)	45.175s	sat	7.728s	sat	0.073s	sat	0.031s	sat
v45_problem_2__008.smt2.slack (converted)	43.090s	sat	6.720s	sat	0.075s	sat	7.214s	sat
v45_problem_2__009.smt2.slack (converted)	-	timeout	16.522s	sat	0.076s	sat	0.015s	sat
v45_problem_2__010.smt2.slack (converted)	-	timeout	10.463s	sat	14.464s	sat	0.963s	sat
v45_problem_2__011.smt2.slack (converted)	-	timeout	10.436s	sat	-	timeout	7.101s	sat
v45_problem_2__012.smt2.slack (converted)	-	timeout	9.881s	sat	-	timeout	9.539s	sat
v45_problem_2__013.smt2.slack (converted)	-	timeout	9.422s	sat	0.165s	sat	7.229s	sat
v45_problem_2__014.smt2.slack (converted)	-	timeout	-	timeout	13.784s	sat	-	timeout
v45_problem_2__015.smt2.slack (converted)	-	timeout	8.066s	sat	0.080s	sat	0.016s	sat
v45_problem_2__016.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__017.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__018.smt2.slack (converted)	-	timeout	17.005s	sat	35.893s	sat	-	timeout
v45_problem_2__019.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__020.smt2.slack (converted)	-	timeout	18.062s	sat	-	timeout	-	timeout
v45_problem_2__021.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__022.smt2.slack (converted)	-	timeout	31.898s	sat	46.255s	sat	-	timeout
v45_problem_2__023.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__024.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	7.954s	sat
v45_problem_2__025.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__026.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__027.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__028.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__029.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	8.575s	sat
v45_problem_2__030.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__031.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__032.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__033.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__034.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem_2__035.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__001.smt2.slack (converted)	-	timeout	4.237s	sat	0.062s	sat	0.015s	sat
v45_problem__002.smt2.slack (converted)	0.045s	sat	0.044s	sat	0.060s	sat	0.015s	sat
v45_problem__003.smt2.slack (converted)	3.034s	sat	-	timeout	0.060s	sat	0.014s	sat
v45_problem__004.smt2.slack (converted)	0.806s	sat	4.957s	sat	0.473s	sat	0.014s	sat
v45_problem__005.smt2.slack (converted)	-	timeout	5.083s	sat	0.060s	sat	0.024s	sat
v45_problem__006.smt2.slack (converted)	-	timeout	7.677s	sat	0.261s	sat	0.019s	sat
v45_problem__007.smt2.slack (converted)	-	timeout	5.553s	sat	13.053s	sat	1.217s	sat
v45_problem__008.smt2.slack (converted)	-	timeout	7.200s	sat	10.955s	sat	0.015s	sat
v45_problem__009.smt2.slack (converted)	-	timeout	6.246s	sat	5.387s	sat	0.047s	sat
v45_problem__010.smt2.slack (converted)	-	timeout	6.643s	sat	9.569s	sat	0.017s	sat
v45_problem__011.smt2.slack (converted)	-	timeout	-	timeout	13.943s	sat	-	timeout
v45_problem__012.smt2.slack (converted)	-	timeout	32.189s	sat	0.085s	sat	-	timeout
v45_problem__013.smt2.slack (converted)	-	timeout	-	timeout	26.255s	sat	0.602s	sat
v45_problem__014.smt2.slack (converted)	-	timeout	-	timeout	2.794s	sat	7.079s	sat
v45_problem__015.smt2.slack (converted)	-	timeout	11.272s	sat	1.620s	sat	0.019s	sat
v45_problem__016.smt2.slack (converted)	-	timeout	24.553s	sat	-	timeout	-	timeout
v45_problem__017.smt2.slack (converted)	-	timeout	-	timeout	27.410s	sat	-	timeout
v45_problem__018.smt2.slack (converted)	-	timeout	29.466s	sat	-	timeout	22.827s	sat
v45_problem__019.smt2.slack (converted)	-	timeout	23.478s	sat	48.825s	sat	-	timeout
v45_problem__020.smt2.slack (converted)	-	timeout	18.073s	sat	-	timeout	-	timeout
v45_problem__021.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__022.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__023.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__024.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__025.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__026.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	9.140s	sat
v45_problem__027.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__028.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__029.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__030.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__031.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__032.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	9.824s	sat
v45_problem__033.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__034.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
v45_problem__035.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_001.smt2.slack (converted)	0.019s	unsat	0.018s	unsat	0.025s	unsat	0.009s	unsat
cut_lemma_02_001.smt2.slack (converted)	0.018s	unsat	0.019s	unsat	0.030s	unsat	0.010s	unsat
cut_lemma_02_003.smt2.slack (converted)	0.017s	unsat	0.018s	unsat	0.029s	unsat	0.010s	unsat
cut_lemma_02_005.smt2.slack (converted)	0.020s	unsat	0.020s	unsat	0.031s	unsat	0.010s	unsat
cut_lemma_02_008.smt2.slack (converted)	-	timeout	-	timeout	0.217s	unsat	0.420s	unsat
cut_lemma_02_009.smt2.slack (converted)	0.019s	unsat	0.019s	unsat	0.031s	unsat	0.010s	unsat
cut_lemma_02_010.smt2.slack (converted)	0.019s	unsat	0.019s	unsat	0.029s	unsat	0.010s	unsat
cut_lemma_01_001.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	27.918s	unsat
cut_lemma_01_002.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_004.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_005.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	48.066s	unsat
cut_lemma_01_007.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_008.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	22.098s	unsat
cut_lemma_01_009.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_010.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_011.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	34.580s	unsat
cut_lemma_01_012.smt2.slack (converted)	0.040s	unsat	0.043s	unsat	0.042s	unsat	0.012s	unsat
cut_lemma_01_013.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_014.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_001.smt2.slack (converted)	0.032s	unsat	0.030s	unsat	0.037s	unsat	0.010s	unsat
cut_lemma_02_002.smt2.slack (converted)	0.032s	unsat	0.030s	unsat	0.036s	unsat	0.012s	unsat
cut_lemma_02_003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	22.058s	unsat
cut_lemma_02_004.smt2.slack (converted)	0.029s	unsat	0.030s	unsat	0.037s	unsat	0.011s	unsat
cut_lemma_02_005.smt2.slack (converted)	0.032s	unsat	0.031s	unsat	0.034s	unsat	0.011s	unsat
cut_lemma_02_006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	22.064s	unsat
cut_lemma_02_008.smt2.slack (converted)	-	timeout	-	timeout	0.783s	unsat	0.270s	unsat
cut_lemma_02_009.smt2.slack (converted)	-	timeout	-	timeout	3.465s	unsat	22.061s	unsat
cut_lemma_03_001.smt2.slack (converted)	0.042s	unsat	0.041s	unsat	0.043s	unsat	0.011s	unsat
cut_lemma_03_002.smt2.slack (converted)	-	timeout	-	timeout	1.468s	unsat	11.729s	unsat
cut_lemma_03_003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_004.smt2.slack (converted)	0.057s	unsat	0.053s	unsat	0.039s	unsat	0.011s	unsat
cut_lemma_03_005.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	27.325s	unsat
cut_lemma_03_007.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	22.099s	unsat
cut_lemma_03_008.smt2.slack (converted)	0.053s	unsat	0.055s	unsat	0.037s	unsat	0.011s	unsat
cut_lemma_03_010.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_011.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_012.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_013.smt2.slack (converted)	0.030s	unsat	0.030s	unsat	0.034s	unsat	0.010s	unsat
cut_lemma_03_014.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_001.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_002.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_004.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_005.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_007.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	24.438s	unsat
cut_lemma_01_008.smt2.slack (converted)	0.150s	unsat	0.152s	unsat	0.044s	unsat	0.012s	unsat
cut_lemma_01_009.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	28.359s	unsat
cut_lemma_01_010.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_011.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_012.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_013.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_014.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_01_015.smt2.slack (converted)	0.114s	unsat	0.113s	unsat	0.047s	unsat	0.012s	unsat
cut_lemma_01_016.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_001.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_002.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_004.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_005.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_006.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_007.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_008.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_009.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_010.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_012.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_013.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	49.580s	unsat
cut_lemma_02_014.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_015.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_02_016.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_001.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_002.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_003.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_004.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_005.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_006.smt2.slack (converted)	0.146s	unsat	0.137s	unsat	0.054s	unsat	0.016s	unsat
cut_lemma_03_007.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_008.smt2.slack (converted)	0.138s	unsat	0.145s	unsat	0.053s	unsat	0.017s	unsat
cut_lemma_03_009.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_010.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_011.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_012.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_013.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_014.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_015.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_016.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_017.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_018.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
cut_lemma_03_019.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	22.484s	unsat
cut_lemma_03_020.smt2.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage0 (converted)	-	timeout	-	timeout	-	timeout	0.067s	sat
unbd-sage1 (converted)	1.181s	sat	-	timeout	0.435s	sat	0.149s	sat
unbd-sage10 (converted)	-	timeout	-	timeout	0.087s	sat	0.424s	sat
unbd-sage11 (converted)	-	timeout	-	timeout	-	timeout	1.052s	sat
unbd-sage12 (converted)	6.702s	sat	0.202s	sat	-	timeout	0.460s	sat
unbd-sage13 (converted)	36.067s	sat	-	timeout	-	timeout	1.089s	sat
unbd-sage14 (converted)	1.129s	sat	0.221s	sat	-	timeout	0.206s	sat
unbd-sage15 (converted)	-	timeout	-	timeout	-	timeout	0.899s	sat
unbd-sage16 (converted)	-	timeout	-	timeout	-	timeout	0.620s	sat
unbd-sage17 (converted)	-	timeout	-	timeout	0.045s	sat	0.038s	sat
unbd-sage18 (converted)	-	timeout	-	timeout	-	timeout	0.884s	sat
unbd-sage19 (converted)	0.627s	sat	0.114s	sat	0.212s	sat	0.378s	sat
unbd-sage2 (converted)	-	timeout	-	timeout	-	timeout	0.173s	sat
unbd-sage20 (converted)	-	timeout	-	timeout	-	timeout	0.083s	sat
unbd-sage21 (converted)	8.905s	sat	1.355s	sat	-	timeout	0.082s	sat
unbd-sage22 (converted)	33.121s	sat	-	timeout	-	timeout	0.040s	sat
unbd-sage23 (converted)	30.312s	sat	5.272s	sat	8.204s	sat	1.198s	sat
unbd-sage24 (converted)	0.855s	sat	0.402s	sat	31.032s	sat	1.184s	sat
unbd-sage3 (converted)	-	timeout	-	timeout	1.591s	sat	0.031s	sat
unbd-sage4 (converted)	-	timeout	-	timeout	-	timeout	0.814s	sat
unbd-sage5 (converted)	0.064s	sat	-	timeout	0.077s	sat	0.195s	sat
unbd-sage6 (converted)	1.370s	sat	0.158s	sat	0.764s	sat	0.268s	sat
unbd-sage7 (converted)	4.121s	sat	0.849s	sat	-	timeout	0.501s	sat
unbd-sage8 (converted)	-	timeout	-	timeout	-	timeout	0.111s	sat
unbd-sage9 (converted)	-	timeout	-	timeout	1.802s	sat	-	timeout
unbd-sage0 (converted)	-	timeout	-	timeout	12.357s	sat	-	timeout
unbd-sage1 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage10 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage11 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage12 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage13 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage14 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage15 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage16 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage17 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage18 (converted)	-	timeout	-	timeout	46.644s	sat	-	timeout
unbd-sage19 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage2 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage20 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage21 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage22 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage23 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage24 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage3 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage4 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage5 (converted)	-	timeout	-	timeout	17.655s	sat	-	timeout
unbd-sage6 (converted)	-	timeout	-	timeout	25.942s	sat	-	timeout
unbd-sage7 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage8 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage9 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage0 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage1 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage10 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage11 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage12 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage13 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage14 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage15 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage16 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage17 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage18 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage19 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage2 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage20 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage21 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage22 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage23 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage24 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage3 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage4 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage5 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage6 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage7 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage8 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage9 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage0 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage1 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage10 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage11 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage12 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage13 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage14 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage15 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage16 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage17 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage18 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage19 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage2 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage20 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage21 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage22 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage23 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage24 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage3 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage4 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage5 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage6 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage7 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage8 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage9 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage0 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage1 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage10 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage11 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage12 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage13 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage14 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage15 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage16 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage17 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage18 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage19 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage2 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage20 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage21 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage22 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage23 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage24 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage3 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage4 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage5 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage6 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage7 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage8 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
unbd-sage9 (converted)	-	timeout	-	timeout	-	timeout	-	timeout
air04.sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
air05.sat (converted)	-	timeout	-	timeout	-	timeout	7.858s	sat
cap6000.sat (converted)	-	timeout	-	timeout	4.140s	sat	-	timeout
disctom.sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
ds.sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
fast0507.sat (converted)	-	timeout	-	timeout	33.210s	sat	3.544s	sat
harp2.sat (converted)	-	timeout	-	timeout	1.304s	sat	-	timeout
manna81.sat (converted)	-	timeout	-	timeout	2.441s	sat	0.378s	sat
mzzv11.sat (converted)	-	timeout	-	timeout	10.704s	sat	2.272s	sat
mzzv42z.sat (converted)	-	timeout	-	timeout	11.912s	sat	2.695s	sat
nw04.sat (converted)	-	timeout	-	timeout	-	timeout	36.296s	sat
p2756.sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
protfold.sat (converted)	-	timeout	-	timeout	-	timeout	3.766s	sat
seymour.sat (converted)	-	timeout	-	timeout	2.264s	sat	0.179s	sat
sp97ar.sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
stp3d.sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-1096.cudf.paranoid (converted)	0.017s	sat	0.019s	sat	0.024s	sat	0.008s	sat
normalized-j12010_10-sat (converted)	-	timeout	-	timeout	-	timeout	52.148s	sat
normalized-j12013_1-unsat (converted)	-	timeout	-	timeout	14.946s	unsat	0.700s	unsat
normalized-j12015_3-unsat (converted)	-	timeout	-	timeout	11.342s	unsat	0.468s	unsat
normalized-j12016_4-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j1201_5-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12021_4-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12022_9-sat (converted)	-	timeout	-	timeout	-	timeout	43.105s	sat
normalized-j12023_3-unsat (converted)	-	timeout	-	timeout	13.031s	unsat	0.614s	unsat
normalized-j12026_5-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12027_7-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12032_3-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12032_8-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12033_3-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12034_4-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12036_3-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12036_4-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12037_7-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12038_8-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j1203_2-sat (converted)	-	timeout	-	timeout	-	timeout	29.142s	sat
normalized-j12041_4-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12045_10-sat (converted)	-	timeout	-	timeout	-	timeout	7.116s	sat
normalized-j12047_10-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12052_5-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12056_10-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j12058_4-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j1205_1-unsat (converted)	-	timeout	-	timeout	11.578s	unsat	0.498s	unsat
normalized-j1208_10-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j1209_4-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j301_4-unsat (converted)	-	timeout	-	timeout	-	timeout	0.213s	unsat
normalized-j3020_1-sat (converted)	-	timeout	-	timeout	-	timeout	0.212s	sat
normalized-j3024_4-sat (converted)	-	timeout	-	timeout	-	timeout	0.253s	sat
normalized-j3025_1-sat (converted)	-	timeout	-	timeout	-	timeout	43.513s	sat
normalized-j3025_7-sat (converted)	-	timeout	-	timeout	-	timeout	12.566s	sat
normalized-j3027_8-sat (converted)	-	timeout	-	timeout	-	timeout	1.012s	sat
normalized-j3029_6-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j3029_8-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j3031_7-sat (converted)	-	timeout	-	timeout	-	timeout	1.106s	sat
normalized-j3037_5-sat (converted)	-	timeout	-	timeout	-	timeout	2.745s	sat
normalized-j3041_4-unsat (converted)	-	timeout	-	timeout	-	timeout	8.363s	unsat
normalized-j3046_4-unsat (converted)	-	timeout	-	timeout	-	timeout	2.477s	unsat
normalized-j3048_8-sat (converted)	-	timeout	-	timeout	3.154s	sat	0.226s	sat
normalized-j308_1-unsat (converted)	-	timeout	-	timeout	1.256s	unsat	0.058s	unsat
normalized-j308_6-sat (converted)	-	timeout	-	timeout	-	timeout	0.243s	sat
normalized-j309_10-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j309_9-sat (converted)	-	timeout	-	timeout	-	timeout	22.842s	sat
normalized-j6010_2-unsat (converted)	-	timeout	-	timeout	3.655s	unsat	0.155s	unsat
normalized-j6013_2-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j6015_4-sat (converted)	-	timeout	-	timeout	-	timeout	8.622s	sat
normalized-j6018_3-sat (converted)	-	timeout	-	timeout	-	timeout	0.932s	sat
normalized-j6022_1-sat (converted)	-	timeout	-	timeout	-	timeout	1.724s	sat
normalized-j6027_4-unsat (converted)	-	timeout	-	timeout	3.725s	unsat	0.162s	unsat
normalized-j602_7-unsat (converted)	-	timeout	-	timeout	6.869s	unsat	0.735s	unsat
normalized-j6030_9-unsat (converted)	-	timeout	-	timeout	6.323s	unsat	0.263s	unsat
normalized-j6033_2-unsat (converted)	-	timeout	-	timeout	6.732s	unsat	0.304s	unsat
normalized-j6035_10-sat (converted)	-	timeout	-	timeout	-	timeout	0.726s	sat
normalized-j603_2-unsat (converted)	-	timeout	-	timeout	4.126s	unsat	0.174s	unsat
normalized-j6040_1-sat (converted)	-	timeout	-	timeout	-	timeout	2.253s	sat
normalized-j6041_4-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j6048_4-sat (converted)	-	timeout	-	timeout	-	timeout	2.950s	sat
normalized-j605_1-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j605_10-unsat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j605_7-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j606_1-unsat (converted)	-	timeout	-	timeout	3.494s	unsat	0.151s	unsat
normalized-j9010_6-unsat (converted)	-	timeout	-	timeout	8.433s	unsat	0.374s	unsat
normalized-j9010_8-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j9012_2-unsat (converted)	-	timeout	-	timeout	6.396s	unsat	0.295s	unsat
normalized-j9012_5-sat (converted)	-	timeout	-	timeout	-	timeout	8.101s	sat
normalized-j9014_1-unsat (converted)	-	timeout	-	timeout	8.321s	unsat	0.362s	unsat
normalized-j9015_10-unsat (converted)	-	timeout	-	timeout	7.087s	unsat	0.318s	unsat
normalized-j9027_5-sat (converted)	-	timeout	-	timeout	-	timeout	11.070s	sat
normalized-j9028_2-unsat (converted)	-	timeout	-	timeout	7.315s	unsat	0.322s	unsat
normalized-j9035_1-unsat (converted)	-	timeout	-	timeout	19.815s	unsat	2.484s	unsat
normalized-j9035_5-sat (converted)	-	timeout	-	timeout	-	timeout	2.751s	sat
normalized-j9039_3-unsat (converted)	-	timeout	-	timeout	8.393s	unsat	0.389s	unsat
normalized-j903_10-unsat (converted)	-	timeout	-	timeout	5.800s	unsat	0.244s	unsat
normalized-j9042_5-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j9043_2-sat (converted)	-	timeout	-	timeout	-	timeout	17.591s	sat
normalized-j9048_1-unsat (converted)	-	timeout	-	timeout	8.681s	unsat	0.367s	unsat
normalized-j906_2-sat (converted)	-	timeout	-	timeout	-	timeout	-	timeout
normalized-j907_8-unsat (converted)	-	timeout	-	timeout	5.480s	unsat	0.231s	unsat
pigeon-hole-10 (converted)	0.124s	unsat	0.129s	unsat	0.065s	unsat	8.558s	unsat
pigeon-hole-11 (converted)	0.173s	unsat	0.175s	unsat	0.074s	unsat	59.568s	unsat
pigeon-hole-12 (converted)	0.241s	unsat	0.252s	unsat	0.086s	unsat	-	timeout
pigeon-hole-13 (converted)	0.352s	unsat	0.349s	unsat	0.097s	unsat	-	timeout
pigeon-hole-14 (converted)	0.468s	unsat	0.477s	unsat	0.108s	unsat	-	timeout
pigeon-hole-15 (converted)	0.642s	unsat	0.643s	unsat	0.124s	unsat	-	timeout
pigeon-hole-16 (converted)	0.826s	unsat	0.851s	unsat	0.142s	unsat	-	timeout
pigeon-hole-17 (converted)	1.082s	unsat	1.099s	unsat	0.164s	unsat	-	timeout
pigeon-hole-18 (converted)	1.395s	unsat	1.408s	unsat	0.183s	unsat	-	timeout
pigeon-hole-19 (converted)	1.806s	unsat	1.787s	unsat	0.206s	unsat	-	timeout
pigeon-hole-2 (converted)	0.018s	unsat	0.018s	unsat	0.028s	unsat	0.009s	unsat
pigeon-hole-20 (converted)	2.309s	unsat	2.368s	unsat	0.233s	unsat	-	timeout
pigeon-hole-3 (converted)	0.018s	unsat	0.019s	unsat	0.030s	unsat	0.008s	unsat
pigeon-hole-4 (converted)	0.018s	unsat	0.017s	unsat	0.033s	unsat	0.010s	unsat
pigeon-hole-5 (converted)	0.017s	unsat	0.017s	unsat	0.036s	unsat	0.010s	unsat
pigeon-hole-6 (converted)	0.032s	unsat	0.031s	unsat	0.041s	unsat	0.015s	unsat
pigeon-hole-7 (converted)	0.045s	unsat	0.042s	unsat	0.046s	unsat	0.115s	unsat
pigeon-hole-8 (converted)	0.055s	unsat	0.067s	unsat	0.052s	unsat	0.667s	unsat
pigeon-hole-9 (converted)	0.092s	unsat	0.086s	unsat	0.060s	unsat	3.646s	unsat
prime_cone_sat_10 (converted)	0.104s	sat	0.018s	sat	0.126s	sat	0.010s	sat
prime_cone_sat_11 (converted)	0.139s	sat	0.019s	sat	0.143s	sat	0.011s	sat
prime_cone_sat_12 (converted)	0.194s	sat	0.031s	sat	0.164s	sat	0.011s	sat
prime_cone_sat_13 (converted)	0.243s	sat	0.030s	sat	0.161s	sat	0.011s	sat
prime_cone_sat_14 (converted)	0.327s	sat	0.030s	sat	0.217s	sat	0.012s	sat
prime_cone_sat_15 (converted)	0.405s	sat	0.031s	sat	-	timeout	0.012s	sat
prime_cone_sat_16 (converted)	0.505s	sat	0.040s	sat	0.253s	sat	0.013s	sat
prime_cone_sat_17 (converted)	0.627s	sat	0.042s	sat	0.347s	sat	0.013s	sat
prime_cone_sat_18 (converted)	0.787s	sat	0.044s	sat	0.420s	sat	0.014s	sat
prime_cone_sat_19 (converted)	0.944s	sat	0.044s	sat	0.382s	sat	0.013s	sat
prime_cone_sat_2 (converted)	0.019s	sat	0.018s	sat	0.025s	sat	0.009s	sat
prime_cone_sat_20 (converted)	1.149s	sat	0.043s	sat	0.255s	sat	0.015s	sat
prime_cone_sat_3 (converted)	0.018s	sat	0.017s	sat	0.028s	sat	0.009s	sat
prime_cone_sat_4 (converted)	0.018s	sat	0.019s	sat	0.035s	sat	0.009s	sat
prime_cone_sat_5 (converted)	0.031s	sat	0.017s	sat	0.043s	sat	0.010s	sat
prime_cone_sat_6 (converted)	0.029s	sat	0.020s	sat	0.134s	sat	0.010s	sat
prime_cone_sat_7 (converted)	0.044s	sat	0.019s	sat	0.054s	sat	0.011s	sat
prime_cone_sat_8 (converted)	0.065s	sat	0.019s	sat	0.094s	sat	0.010s	sat
prime_cone_sat_9 (converted)	0.082s	sat	0.020s	sat	0.067s	sat	0.011s	sat
prime_cone_unsat_10 (converted)	0.101s	unsat	0.031s	unsat	0.128s	unsat	0.022s	unsat
prime_cone_unsat_11 (converted)	0.139s	unsat	0.031s	unsat	0.158s	unsat	0.026s	unsat
prime_cone_unsat_12 (converted)	0.184s	unsat	0.029s	unsat	0.178s	unsat	0.030s	unsat
prime_cone_unsat_13 (converted)	0.230s	unsat	0.032s	unsat	0.215s	unsat	0.041s	unsat
prime_cone_unsat_14 (converted)	0.308s	unsat	0.043s	unsat	0.241s	unsat	0.066s	unsat
prime_cone_unsat_15 (converted)	0.382s	unsat	0.041s	unsat	0.304s	unsat	0.077s	unsat
prime_cone_unsat_16 (converted)	0.480s	unsat	0.053s	unsat	0.321s	unsat	0.038s	unsat
prime_cone_unsat_17 (converted)	0.592s	unsat	0.055s	unsat	0.431s	unsat	0.081s	unsat
prime_cone_unsat_18 (converted)	0.722s	unsat	0.065s	unsat	0.525s	unsat	0.105s	unsat
prime_cone_unsat_19 (converted)	0.893s	unsat	0.063s	unsat	0.521s	unsat	0.106s	unsat
prime_cone_unsat_20 (converted)	1.101s	unsat	0.077s	unsat	0.349s	unsat	0.074s	unsat
prime_cone_unsat_3 (converted)	0.018s	unsat	0.018s	unsat	0.030s	unsat	0.010s	unsat
prime_cone_unsat_4 (converted)	0.020s	unsat	0.019s	unsat	0.038s	unsat	0.011s	unsat
prime_cone_unsat_5 (converted)	0.019s	unsat	0.019s	unsat	0.051s	unsat	0.012s	unsat
prime_cone_unsat_6 (converted)	0.029s	unsat	0.019s	unsat	0.086s	unsat	0.013s	unsat
prime_cone_unsat_7 (converted)	0.040s	unsat	0.019s	unsat	0.069s	unsat	0.015s	unsat
prime_cone_unsat_8 (converted)	0.051s	unsat	0.030s	unsat	0.097s	unsat	0.016s	unsat
prime_cone_unsat_9 (converted)	0.076s	unsat	0.029s	unsat	0.087s	unsat	0.019s	unsat
10-12.slack (converted)	0.017s	sat	0.019s	sat	0.028s	sat	0.010s	sat
10-13.slack (converted)	0.017s	sat	0.020s	sat	0.028s	sat	0.010s	sat
10-20.slack (converted)	0.019s	sat	0.019s	sat	0.027s	sat	0.011s	sat
10-21.slack (converted)	0.020s	sat	0.017s	sat	0.034s	sat	0.011s	sat
10-28.slack (converted)	0.020s	sat	0.017s	sat	0.031s	sat	0.011s	sat
10-29.slack (converted)	0.020s	sat	0.019s	sat	0.049s	sat	0.011s	sat
10-30.slack (converted)	0.081s	sat	0.029s	sat	0.031s	sat	0.010s	sat
10-31.slack (converted)	0.017s	sat	0.019s	sat	0.030s	sat	0.010s	sat
10-34.slack (converted)	0.092s	sat	0.054s	sat	0.033s	sat	0.012s	sat
10-35.slack (converted)	0.029s	sat	0.040s	sat	0.036s	sat	0.011s	sat
10-36.slack (converted)	0.018s	sat	0.029s	sat	0.032s	sat	0.011s	sat
10-37.slack (converted)	0.067s	sat	0.041s	sat	0.053s	sat	0.013s	sat
10-4.slack (converted)	0.017s	sat	0.018s	sat	0.028s	sat	0.010s	sat
10-40.slack (converted)	0.361s	sat	0.103s	sat	0.035s	sat	0.011s	sat
10-41.slack (converted)	0.170s	sat	0.041s	sat	0.035s	sat	0.011s	sat
10-45.slack (converted)	-	timeout	-	timeout	0.061s	sat	0.011s	sat
15-1.slack (converted)	0.112s	sat	0.089s	sat	0.034s	sat	0.011s	sat
15-10.slack (converted)	1.031s	sat	0.162s	sat	0.082s	sat	0.013s	sat
15-11.slack (converted)	4.051s	sat	0.432s	sat	1.650s	sat	0.457s	sat
15-12.slack (converted)	-	timeout	-	timeout	17.100s	sat	0.017s	sat
15-13.slack (converted)	1.226s	sat	0.299s	sat	0.124s	sat	0.013s	sat
15-14.slack (converted)	0.988s	sat	0.219s	sat	0.062s	sat	0.012s	sat
15-15.slack (converted)	-	timeout	-	timeout	0.058s	sat	0.014s	sat
15-17.slack (converted)	4.624s	sat	0.432s	sat	0.063s	sat	0.555s	sat
15-18.slack (converted)	-	timeout	-	timeout	0.046s	sat	0.014s	sat
15-19.slack (converted)	5.368s	sat	-	timeout	0.573s	sat	1.548s	sat
15-2.slack (converted)	0.019s	sat	0.018s	sat	0.037s	sat	0.011s	sat
15-20.slack (converted)	0.232s	sat	0.159s	sat	0.103s	sat	0.020s	sat
15-21.slack (converted)	-	timeout	0.620s	sat	0.056s	sat	0.013s	sat
15-3.slack (converted)	0.030s	sat	0.077s	sat	0.064s	sat	0.011s	sat
15-4.slack (converted)	0.189s	sat	0.091s	sat	0.045s	sat	0.012s	sat
15-5.slack (converted)	0.018s	sat	0.030s	sat	0.034s	sat	0.010s	sat
15-6.slack (converted)	2.326s	sat	0.248s	sat	0.351s	sat	0.013s	sat
15-7.slack (converted)	-	timeout	-	timeout	0.108s	sat	0.030s	sat
15-8.slack (converted)	0.814s	sat	0.054s	sat	0.035s	sat	0.011s	sat
15-9.slack (converted)	0.929s	sat	0.328s	sat	0.623s	sat	0.081s	sat
20-1.slack (converted)	0.067s	sat	0.440s	sat	0.070s	sat	0.020s	sat
20-10.slack (converted)	-	timeout	0.871s	sat	0.059s	sat	0.013s	sat
20-11.slack (converted)	-	timeout	-	timeout	58.921s	sat	9.977s	sat
20-12.slack (converted)	-	timeout	-	timeout	0.807s	sat	0.101s	sat
20-13.slack (converted)	-	timeout	1.163s	sat	0.219s	sat	0.016s	sat
20-14.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
20-15.slack (converted)	-	timeout	-	timeout	0.766s	sat	0.074s	sat
20-16.slack (converted)	-	timeout	-	timeout	3.138s	sat	22.220s	sat
20-17.slack (converted)	-	timeout	-	timeout	-	timeout	0.058s	sat
20-19.slack (converted)	-	timeout	-	timeout	3.054s	sat	-	timeout
20-2.slack (converted)	2.052s	sat	0.323s	sat	0.039s	sat	0.011s	sat
20-20.slack (converted)	-	timeout	-	timeout	0.448s	sat	0.028s	sat
20-21.slack (converted)	-	timeout	-	timeout	-	timeout	0.218s	sat
20-22.slack (converted)	19.696s	sat	-	timeout	0.749s	sat	1.137s	sat
20-24.slack (converted)	-	timeout	-	timeout	-	timeout	10.619s	sat
20-26.slack (converted)	-	timeout	-	timeout	-	timeout	22.858s	sat
20-28.slack (converted)	-	timeout	-	timeout	48.678s	sat	8.767s	sat
20-3.slack (converted)	1.067s	sat	-	timeout	0.325s	sat	0.014s	sat
20-30.slack (converted)	-	timeout	-	timeout	-	timeout	0.806s	sat
20-4.slack (converted)	0.065s	sat	-	timeout	0.183s	sat	0.012s	sat
20-5.slack (converted)	2.131s	sat	0.319s	sat	0.299s	sat	0.012s	sat
20-6.slack (converted)	-	timeout	0.676s	sat	0.883s	sat	0.027s	sat
20-7.slack (converted)	5.702s	sat	1.049s	sat	0.050s	sat	0.014s	sat
20-8.slack (converted)	2.440s	sat	0.314s	sat	0.056s	sat	0.013s	sat
20-9.slack (converted)	-	timeout	-	timeout	-	timeout	1.865s	sat
25-1.slack (converted)	-	timeout	-	timeout	0.044s	sat	0.012s	sat
25-10.slack (converted)	9.875s	sat	1.742s	sat	0.052s	sat	0.089s	sat
25-11.slack (converted)	-	timeout	-	timeout	8.056s	sat	0.029s	sat
25-12.slack (converted)	-	timeout	-	timeout	-	timeout	7.062s	sat
25-13.slack (converted)	20.823s	sat	4.288s	sat	0.468s	sat	7.038s	sat
25-14.slack (converted)	-	timeout	2.136s	sat	-	timeout	0.169s	sat
25-15.slack (converted)	-	timeout	-	timeout	-	timeout	0.104s	sat
25-16.slack (converted)	-	timeout	-	timeout	-	timeout	0.346s	sat
25-17.slack (converted)	-	timeout	-	timeout	-	timeout	0.017s	sat
25-18.slack (converted)	33.980s	sat	2.235s	sat	1.724s	sat	22.117s	sat
25-19.slack (converted)	-	timeout	-	timeout	8.198s	sat	-	timeout
25-2.slack (converted)	3.020s	sat	1.169s	sat	0.676s	sat	0.042s	sat
25-20.slack (converted)	-	timeout	-	timeout	41.614s	sat	7.117s	sat
25-21.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
25-22.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
25-23.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
25-24.slack (converted)	-	timeout	-	timeout	45.606s	sat	-	timeout
25-25.slack (converted)	-	timeout	-	timeout	3.669s	sat	1.289s	sat
25-26.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
25-27.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
25-28.slack (converted)	-	timeout	-	timeout	-	timeout	1.301s	sat
25-29.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
25-3.slack (converted)	7.445s	sat	0.840s	sat	0.525s	sat	0.014s	sat
25-30.slack (converted)	-	timeout	-	timeout	-	timeout	11.416s	sat
25-31.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
25-33.slack (converted)	-	timeout	-	timeout	-	timeout	10.543s	sat
25-35.slack (converted)	-	timeout	-	timeout	-	timeout	8.735s	sat
25-4.slack (converted)	12.377s	sat	0.700s	sat	0.046s	sat	0.013s	sat
25-5.slack (converted)	8.202s	sat	0.733s	sat	0.114s	sat	0.021s	sat
25-6.slack (converted)	23.598s	sat	-	timeout	0.057s	sat	7.796s	sat
25-7.slack (converted)	-	timeout	-	timeout	1.415s	sat	0.034s	sat
25-8.slack (converted)	11.762s	sat	1.749s	sat	2.060s	sat	0.013s	sat
25-9.slack (converted)	-	timeout	1.874s	sat	3.715s	sat	0.015s	sat
30-1.slack (converted)	3.497s	sat	-	timeout	0.052s	sat	0.013s	sat
30-10.slack (converted)	20.008s	sat	-	timeout	5.998s	sat	0.356s	sat
30-11.slack (converted)	-	timeout	-	timeout	4.215s	sat	-	timeout
30-12.slack (converted)	-	timeout	-	timeout	0.356s	sat	-	timeout
30-13.slack (converted)	-	timeout	-	timeout	16.458s	sat	7.258s	sat
30-14.slack (converted)	-	timeout	3.921s	sat	-	timeout	7.436s	sat
30-15.slack (converted)	-	timeout	-	timeout	38.680s	sat	7.231s	sat
30-16.slack (converted)	-	timeout	5.936s	sat	-	timeout	-	timeout
30-17.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
30-18.slack (converted)	-	timeout	-	timeout	-	timeout	1.639s	sat
30-19.slack (converted)	-	timeout	-	timeout	22.512s	sat	-	timeout
30-2.slack (converted)	-	timeout	-	timeout	0.139s	sat	0.031s	sat
30-20.slack (converted)	-	timeout	-	timeout	-	timeout	0.204s	sat
30-21.slack (converted)	-	timeout	-	timeout	6.586s	sat	-	timeout
30-22.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
30-23.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
30-24.slack (converted)	-	timeout	-	timeout	-	timeout	1.665s	sat
30-25.slack (converted)	-	timeout	-	timeout	-	timeout	7.663s	sat
30-26.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
30-27.slack (converted)	-	timeout	-	timeout	-	timeout	12.092s	sat
30-28.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
30-29.slack (converted)	-	timeout	-	timeout	-	timeout	0.016s	sat
30-3.slack (converted)	4.892s	sat	1.908s	sat	6.377s	sat	0.019s	sat
30-30.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
30-31.slack (converted)	-	timeout	-	timeout	24.692s	sat	-	timeout
30-33.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
30-34.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
30-35.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
30-4.slack (converted)	1.808s	sat	-	timeout	0.109s	sat	0.015s	sat
30-5.slack (converted)	1.771s	sat	1.301s	sat	0.047s	sat	0.013s	sat
30-6.slack (converted)	0.293s	sat	-	timeout	0.257s	sat	0.033s	sat
30-7.slack (converted)	-	timeout	-	timeout	0.790s	sat	0.025s	sat
30-8.slack (converted)	-	timeout	-	timeout	0.056s	sat	0.485s	sat
30-9.slack (converted)	-	timeout	-	timeout	0.485s	sat	0.175s	sat
35-1.slack (converted)	8.024s	sat	2.345s	sat	0.049s	sat	0.013s	sat
35-10.slack (converted)	-	timeout	24.449s	sat	4.366s	sat	0.331s	sat
35-11.slack (converted)	-	timeout	7.273s	sat	0.555s	sat	0.019s	sat
35-12.slack (converted)	-	timeout	-	timeout	53.553s	sat	0.073s	sat
35-13.slack (converted)	-	timeout	-	timeout	0.076s	sat	-	timeout
35-14.slack (converted)	-	timeout	-	timeout	25.724s	sat	8.329s	sat
35-15.slack (converted)	-	timeout	-	timeout	-	timeout	7.332s	sat
35-16.slack (converted)	-	timeout	-	timeout	18.688s	sat	-	timeout
35-17.slack (converted)	-	timeout	-	timeout	-	timeout	0.349s	sat
35-18.slack (converted)	-	timeout	12.753s	sat	-	timeout	8.930s	sat
35-19.slack (converted)	-	timeout	-	timeout	10.265s	sat	0.073s	sat
35-2.slack (converted)	19.645s	sat	3.736s	sat	1.747s	sat	0.016s	sat
35-20.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
35-21.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
35-22.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
35-23.slack (converted)	-	timeout	21.280s	sat	-	timeout	-	timeout
35-24.slack (converted)	-	timeout	-	timeout	-	timeout	8.453s	sat
35-25.slack (converted)	-	timeout	-	timeout	-	timeout	0.899s	sat
35-26.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
35-27.slack (converted)	-	timeout	-	timeout	-	timeout	10.648s	sat
35-28.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
35-29.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
35-3.slack (converted)	-	timeout	-	timeout	0.086s	sat	0.016s	sat
35-30.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
35-31.slack (converted)	-	timeout	-	timeout	-	timeout	11.029s	sat
35-32.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
35-33.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
35-34.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
35-35.slack (converted)	-	timeout	-	timeout	13.716s	sat	-	timeout
35-4.slack (converted)	1.103s	sat	-	timeout	0.052s	sat	0.014s	sat
35-5.slack (converted)	44.863s	sat	2.709s	sat	0.093s	sat	0.072s	sat
35-6.slack (converted)	-	timeout	2.549s	sat	3.891s	sat	0.022s	sat
35-7.slack (converted)	-	timeout	-	timeout	0.060s	sat	0.679s	sat
35-8.slack (converted)	11.442s	sat	5.186s	sat	11.835s	sat	0.028s	sat
35-9.slack (converted)	34.271s	sat	3.363s	sat	0.393s	sat	0.016s	sat
40-1.slack (converted)	32.437s	sat	3.922s	sat	0.120s	sat	7.276s	sat
40-10.slack (converted)	54.335s	sat	7.708s	sat	0.061s	sat	0.014s	sat
40-11.slack (converted)	-	timeout	-	timeout	21.048s	sat	-	timeout
40-12.slack (converted)	-	timeout	-	timeout	7.779s	sat	0.079s	sat
40-13.slack (converted)	-	timeout	-	timeout	41.877s	sat	0.606s	sat
40-14.slack (converted)	-	timeout	15.802s	sat	-	timeout	0.016s	sat
40-15.slack (converted)	-	timeout	-	timeout	-	timeout	0.354s	sat
40-16.slack (converted)	-	timeout	18.731s	sat	-	timeout	-	timeout
40-17.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
40-18.slack (converted)	-	timeout	-	timeout	37.154s	sat	-	timeout
40-19.slack (converted)	-	timeout	18.758s	sat	-	timeout	-	timeout
40-2.slack (converted)	-	timeout	-	timeout	2.099s	sat	0.015s	sat
40-20.slack (converted)	-	timeout	-	timeout	-	timeout	1.615s	sat
40-21.slack (converted)	-	timeout	-	timeout	-	timeout	7.717s	sat
40-22.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
40-23.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
40-24.slack (converted)	-	timeout	-	timeout	-	timeout	7.945s	sat
40-25.slack (converted)	-	timeout	-	timeout	17.763s	sat	-	timeout
40-26.slack (converted)	-	timeout	-	timeout	-	timeout	1.247s	sat
40-27.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
40-28.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
40-29.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
40-3.slack (converted)	48.786s	sat	8.882s	sat	0.103s	sat	0.014s	sat
40-30.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
40-31.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
40-32.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
40-33.slack (converted)	-	timeout	-	timeout	-	timeout	9.655s	sat
40-34.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
40-35.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
40-4.slack (converted)	0.948s	sat	3.532s	sat	0.057s	sat	0.015s	sat
40-5.slack (converted)	22.656s	sat	-	timeout	0.054s	sat	0.015s	sat
40-6.slack (converted)	-	timeout	4.662s	sat	0.066s	sat	0.015s	sat
40-7.slack (converted)	-	timeout	-	timeout	5.386s	sat	0.040s	sat
40-8.slack (converted)	-	timeout	-	timeout	15.993s	sat	1.319s	sat
40-9.slack (converted)	-	timeout	5.232s	sat	0.368s	sat	0.276s	sat
45-1.slack (converted)	-	timeout	6.814s	sat	0.058s	sat	0.014s	sat
45-10.slack (converted)	-	timeout	-	timeout	0.492s	sat	0.015s	sat
45-11.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-12.slack (converted)	-	timeout	8.191s	sat	0.072s	sat	0.016s	sat
45-13.slack (converted)	-	timeout	13.350s	sat	-	timeout	7.059s	sat
45-14.slack (converted)	-	timeout	-	timeout	38.343s	sat	1.377s	sat
45-15.slack (converted)	-	timeout	11.988s	sat	16.188s	sat	1.358s	sat
45-16.slack (converted)	-	timeout	-	timeout	32.468s	sat	0.065s	sat
45-17.slack (converted)	-	timeout	-	timeout	-	timeout	7.389s	sat
45-18.slack (converted)	-	timeout	-	timeout	43.605s	sat	-	timeout
45-19.slack (converted)	-	timeout	-	timeout	29.175s	sat	-	timeout
45-2.slack (converted)	41.383s	sat	5.451s	sat	0.113s	sat	0.015s	sat
45-20.slack (converted)	-	timeout	22.443s	sat	31.486s	sat	-	timeout
45-21.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-22.slack (converted)	-	timeout	-	timeout	-	timeout	10.930s	sat
45-23.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-24.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-25.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-26.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-27.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-28.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-29.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-3.slack (converted)	5.662s	sat	5.116s	sat	0.055s	sat	0.015s	sat
45-30.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-31.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-32.slack (converted)	-	timeout	-	timeout	-	timeout	0.964s	sat
45-33.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-34.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-35.slack (converted)	-	timeout	-	timeout	-	timeout	-	timeout
45-4.slack (converted)	18.851s	sat	6.968s	sat	0.057s	sat	0.014s	sat
45-5.slack (converted)	51.517s	sat	5.463s	sat	0.711s	sat	0.015s	sat
45-6.slack (converted)	-	timeout	13.839s	sat	0.298s	sat	0.017s	sat
45-7.slack (converted)	-	timeout	7.112s	sat	10.626s	sat	0.909s	sat
45-8.slack (converted)	-	timeout	-	timeout	0.068s	sat	0.016s	sat
45-9.slack (converted)	-	timeout	7.192s	sat	0.069s	sat	0.018s	sat