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 branch and bound incremental branch and bound CVC4 Z3
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 branch and bound incremental branch and bound CVC4 Z3
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