# .

* SAT 95
* UNSAT 92
* TIMEOUT 68
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: smt_qfrdl-threads-4-param_tuning-no_inprocessing-fullparams
Runner: lev-ripper
Z3 repo: ilanashapiro/z3
Z3 commit: 629b8b565df758effc676cf4d9e7c3319d9a989c
Z3 branch: param-tuning
Z3 options: "-T:30 smt.threads=4 tactic.default_tactic=smt smt.auto_config.false smt_parallel.inprocessing=false"
Z3 inputs: inputs/QF_RDL
Z3 commit message: restore params

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|sal/fischer3-mutex-2.smt2                                    |    0.080s | 90.392MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-2.smt2                                    |    0.090s | 91.68MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking01.smt2              |    0.094s | 90.648MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-1.smt2          |    0.094s | 89.628MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-matrix1x1.pddl.smt2   |    0.094s | 89.744MiB| sat | 0 |  |  |
|sal/fischer6-mutex-1.smt2                                    |    0.097s | 89.844MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-3.smt2                                    |    0.104s | 91.672MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking02.smt2              |    0.107s | 91.16MiB| sat | 0 |  |  |
|sal/fischer3-mutex-3.smt2                                    |    0.108s | 90.656MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-5.smt2                                    |    0.110s | 92.036MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-06.smt2       |    0.116s | 93.212MiB| sat | 0 |  |  |
|sal/fischer3-mutex-6.smt2                                    |    0.117s | 92.24MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking04.smt2              |    0.118s | 92.184MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking03.smt2              |    0.118s | 91.416MiB| sat | 0 |  |  |
|sal/fischer9-mutex-3.smt2                                    |    0.118s | 93.42MiB| unsat | 0 |  |  |
|check/bignum_rdl2.smt2                                       |    0.121s | 89.376MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-04.smt2       |    0.121s | 91.928MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-2.smt2          |    0.122s | 92.136MiB| sat | 0 |  |  |
|sal/fischer9-mutex-1.smt2                                    |    0.122s | 90.14MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking05.smt2              |    0.123s | 92.444MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-03.smt2       |    0.124s | 92.44MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-2.smt2          |    0.125s | 92.536MiB| sat | 0 |  |  |
|sal/fischer6-mutex-4.smt2                                    |    0.125s | 92.956MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-1.smt2                                    |    0.127s | 89.544MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-2.smt2                                    |    0.128s | 91.18MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-05.smt2       |    0.129s | 93.628MiB| sat | 0 |  |  |
|sal/fischer6-mutex-5.smt2                                    |    0.133s | 93.468MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking07.smt2              |    0.137s | 93.408MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking06.smt2              |    0.139s | 92.952MiB| sat | 0 |  |  |
|sal/fischer3-mutex-7.smt2                                    |    0.142s | 92.696MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking08.smt2              |    0.145s | 93.744MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-07.smt2       |    0.147s | 94.656MiB| sat | 0 |  |  |
|sal/fischer9-mutex-4.smt2                                    |    0.151s | 94.232MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking09.smt2              |    0.152s | 94.756MiB| sat | 0 |  |  |
|sal/fischer6-mutex-6.smt2                                    |    0.153s | 94.556MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking10.smt2              |    0.154s | 95.552MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking13.smt2              |    0.154s | 96.592MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-08.smt2       |    0.155s | 95.072MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-09.smt2       |    0.159s | 95.9MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-10.smt2       |    0.160s | 96.152MiB| sat | 0 |  |  |
|sal/fischer9-mutex-5.smt2                                    |    0.160s | 96.104MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-9.smt2                                    |    0.163s | 94.532MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking11.smt2              |    0.167s | 95.852MiB| sat | 0 |  |  |
|sal/fischer3-mutex-4.smt2                                    |    0.170s | 91.16MiB| unsat | 0 |  |  |
|check/bignum_rdl1.smt2                                       |    0.178s | 89.112MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking12.smt2              |    0.179s | 96.536MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking17.smt2              |    0.183s | 99.276MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking14.smt2              |    0.183s | 96.928MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking18.smt2              |    0.188s | 99.34MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking16.smt2              |    0.189s | 98.48MiB| sat | 0 |  |  |
|sal/fischer3-mutex-10.smt2                                   |    0.194s | 95.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking15.smt2              |    0.197s | 97.448MiB| sat | 0 |  |  |
|sal/fischer3-mutex-8.smt2                                    |    0.199s | 93.208MiB| unsat | 0 |  |  |
|scheduling/orb09_800.smt2                                    |    0.204s | 99.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking20.smt2              |    0.206s | 98.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-3.smt2          |    0.208s | 98.208MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking19.smt2              |    0.209s | 99.948MiB| sat | 0 |  |  |
|scheduling/orb07_250.smt2                                    |    0.210s | 96.544MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-7.smt2                                    |    0.212s | 95.864MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-8.smt2                                    |    0.217s | 97.604MiB| unsat | 0 |  |  |
|scheduling/abz6_800.smt2                                     |    0.218s | 98.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-11.smt2                                   |    0.218s | 95.472MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking22.smt2              |    0.229s | 99.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking21.smt2              |    0.234s | 98.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-7.smt2                                    |    0.240s | 99.244MiB| unsat | 0 |  |  |
|scheduling/abz5_1000.smt2                                    |    0.246s | 99.0MiB| unsat | 0 |  |  |
|scheduling/orb02_700.smt2                                    |    0.250s | 98.22MiB| unsat | 0 |  |  |
|scheduling/orb10_800.smt2                                    |    0.260s | 100.0MiB| unsat | 0 |  |  |
|scheduling/orb08_700.smt2                                    |    0.266s | 99.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-20.smt2       |    0.269s | 99.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-12.smt2                                   |    0.271s | 96.732MiB| unsat | 0 |  |  |
|scheduling/orb05_700.smt2                                    |    0.273s | 99.0MiB| unsat | 0 |  |  |
|scheduling/orb07_550.smt2                                    |    0.289s | 102.0MiB| sat | 0 |  |  |
|scheduling/abz6_1100.smt2                                    |    0.299s | 102.0MiB| sat | 0 |  |  |
|scheduling/orb04_850.smt2                                    |    0.303s | 99.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-13.smt2                                   |    0.307s | 97.664MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-9.smt2                                    |    0.327s | 99.452MiB| unsat | 0 |  |  |
|scheduling/orb04_1200.smt2                                   |    0.344s | 103.0MiB| sat | 0 |  |  |
|scheduling/orb02_1000.smt2                                   |    0.347s | 101.0MiB| sat | 0 |  |  |
|scheduling/orb07_330.smt2                                    |    0.361s | 98.328MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-14.smt2                                   |    0.367s | 97.924MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-8.smt2                                    |    0.372s | 99.0MiB| unsat | 0 |  |  |
|scheduling/orb10_1100.smt2                                   |    0.404s | 103.0MiB| sat | 0 |  |  |
|scheduling/orb08_830.smt2                                    |    0.407s | 101.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-16.smt2                                   |    0.407s | 97.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-6.smt2                                    |    0.407s | 98.348MiB| unsat | 0 |  |  |
|scheduling/abz5_1400.smt2                                    |    0.408s | 101.0MiB| sat | 0 |  |  |
|scheduling/orb09_1000.smt2                                   |    0.421s | 102.0MiB| sat | 0 |  |  |
|scheduling/abz6_1000.smt2                                    |    0.422s | 102.0MiB| sat | 0 |  |  |
|scheduling/orb02_800.smt2                                    |    0.425s | 100.0MiB| unsat | 0 |  |  |
|scheduling/orb05_800.smt2                                    |    0.431s | 101.0MiB| unsat | 0 |  |  |
|scheduling/orb09_1100.smt2                                   |    0.437s | 103.0MiB| sat | 0 |  |  |
|scheduling/orb06_1200.smt2                                   |    0.463s | 103.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-30.smt2       |    0.469s | 106.0MiB| sat | 0 |  |  |
|scheduling/abz6_900.smt2                                     |    0.470s | 101.0MiB| unsat | 0 |  |  |
|scheduling/orb03_850.smt2                                    |    0.490s | 101.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-15.smt2                                   |    0.513s | 97.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-3.smt2          |    0.586s | 101.0MiB| sat | 0 |  |  |
|scheduling/orb05_1000.smt2                                   |    0.590s | 104.0MiB| sat | 0 |  |  |
|scheduling/orb01_900.smt2                                    |    0.617s | 102.0MiB| unsat | 0 |  |  |
|scheduling/orb06_900.smt2                                    |    0.628s | 102.0MiB| unsat | 0 |  |  |
|scheduling/orb04_950.smt2                                    |    0.650s | 103.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-17.smt2                                   |    0.668s | 100.0MiB| unsat | 0 |  |  |
|scheduling/orb07_430.smt2                                    |    0.687s | 104.0MiB| sat | 0 |  |  |
|scheduling/orb03_1200.smt2                                   |    0.699s | 106.0MiB| sat | 0 |  |  |
|scheduling/abz5_1300.smt2                                    |    0.703s | 103.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-40.smt2       |    0.717s | 111.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-10.smt2                                   |    0.728s | 100.0MiB| unsat | 0 |  |  |
|scheduling/orb08_1000.smt2                                   |    0.743s | 105.0MiB| sat | 0 |  |  |
|skdmxa/skdmxa-3x3-5.smt2                                     |    0.750s | 133.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-6.base.cvc.smt2                           |    0.819s | 178.0MiB| unsat | 0 |  |  |
|scheduling/orb04_1100.smt2                                   |    0.828s | 105.0MiB| sat | 0 |  |  |
|scheduling/orb03_1100.smt2                                   |    0.839s | 106.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-18.smt2                                   |    0.868s | 100.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-19.smt2                                   |    0.870s | 101.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-5.induction.cvc.smt2                      |    0.892s | 214.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-5.base.cvc.smt2                           |    1.042s | 156.0MiB| unsat | 0 |  |  |
|scheduling/abz6_943.smt2                                     |    1.076s | 104.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-7.base.cvc.smt2                           |    1.117s | 227.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-6.induction.cvc.smt2                      |    1.137s | 242.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-9.smt2                                    |    1.203s | 104.0MiB| unsat | 0 |  |  |
|scheduling/orb10_1000.smt2                                   |    1.255s | 105.0MiB| sat | 0 |  |  |
|scheduling/orb10_900.smt2                                    |    1.290s | 103.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-4.smt2          |    1.366s | 109.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-8.base.cvc.smt2                           |    1.403s | 247.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-11.smt2                                   |    1.409s | 103.0MiB| unsat | 0 |  |  |
|scheduling/orb02_900.smt2                                    |    1.437s | 106.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-12.smt2                                   |    1.445s | 105.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-20.smt2                                   |    1.467s | 103.0MiB| unsat | 0 |  |  |
|scheduling/orb01_1200.smt2                                   |    1.602s | 108.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-7.induction.cvc.smt2                      |    1.655s | 336.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-9.base.cvc.smt2                           |    1.742s | 268.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-8.induction.cvc.smt2                      |    1.911s | 348.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-60.smt2       |    1.947s | 123.0MiB| sat | 0 |  |  |
|scheduling/yn1_750.smt2                                      |    1.965s | 242.0MiB| unsat | 0 |  |  |
|scheduling/orb09_900.smt2                                    |    2.329s | 106.0MiB| unsat | 0 |  |  |
|skdmxa/skdmxa-3x3-10.smt2                                    |    2.344s | 192.0MiB| unsat | 0 |  |  |
|scheduling/orb06_1100.smt2                                   |    2.355s | 108.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-10.base.cvc.smt2                          |    2.406s | 288.0MiB| unsat | 0 |  |  |
|scheduling/orb02_888.smt2                                    |    2.573s | 107.0MiB| sat | 0 |  |  |
|scheduling/abz7_500.smt2                                     |    2.583s | 190.0MiB| unsat | 0 |  |  |
|scheduling/orb08_930.smt2                                    |    2.713s | 107.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-10.smt2                                   |    2.785s | 110.0MiB| unsat | 0 |  |  |
|scheduling/abz5_1234.smt2                                    |    2.963s | 107.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-70.smt2       |    2.975s | 140.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-10.induction.cvc.smt2                     |    3.046s | 453.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-13.smt2                                   |    3.174s | 110.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-11.smt2                                   |    3.187s | 112.0MiB| unsat | 0 |  |  |
|scheduling/abz5_1200.smt2                                    |    3.340s | 106.0MiB| unsat | 0 |  |  |
|scheduling/orb05_900.smt2                                    |    3.367s | 108.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-80.smt2       |    3.450s | 144.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-9.induction.cvc.smt2                      |    3.989s | 403.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-12.induction.cvc.smt2                     |    4.039s | 512.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-11.induction.cvc.smt2                     |    4.142s | 446.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-15.smt2                                   |    4.527s | 116.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-14.smt2                                   |    5.378s | 115.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-12.smt2                                   |    5.895s | 119.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-11.base.cvc.smt2                          |    5.977s | 318.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-14.induction.cvc.smt2                     |    6.202s | 696.0MiB| sat | 0 |  |  |
|scheduling/orb07_397.smt2                                    |    6.292s | 110.0MiB| sat | 0 |  |  |
|scheduling/yn2_750.smt2                                      |    6.299s | 256.0MiB| unsat | 0 |  |  |
|scheduling/yn3_750.smt2                                      |    6.792s | 270.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-13.induction.cvc.smt2                     |    7.767s | 605.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-90.smt2       |    8.070s | 152.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-13.smt2                                   |    9.666s | 129.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-16.induction.cvc.smt2                     |    9.957s | 749.0MiB| sat | 0 |  |  |
|scheduling/orb10_944.smt2                                    |   10.129s | 111.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-16.smt2                                   |   11.350s | 124.0MiB| unsat | 0 |  |  |
|scheduling/orb08_888.smt2                                    |   11.956s | 112.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-17.induction.cvc.smt2                     |   12.005s | 856.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-17.smt2                                   |   12.559s | 129.0MiB| unsat | 0 |  |  |
|scheduling/orb05_887.smt2                                    |   12.595s | 113.0MiB| sat | 0 |  |  |
|scheduling/orb09_934.smt2                                    |   12.674s | 113.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-19.induction.cvc.smt2                     |   12.790s | 845.0MiB| sat | 0 |  |  |
|scheduling/orb04_1005.smt2                                   |   13.190s | 114.0MiB| sat | 0 |  |  |
|scheduling/orb03_950.smt2                                    |   13.846s | 112.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-5.smt2          |   13.895s | 141.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-15.induction.cvc.smt2                     |   14.122s | 738.0MiB| sat | 0 |  |  |
|scheduling/orb01_1100.smt2                                   |   16.964s | 115.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-18.smt2                                   |   17.136s | 132.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-18.induction.cvc.smt2                     |   17.366s | 975.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-20.induction.cvc.smt2                     |   18.055s | 893.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-12.base.cvc.smt2                          |   19.028s | 363.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-4.smt2          |   19.592s | 156.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-15.smt2                                   |   22.217s | 143.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-19.smt2                                   |   22.957s | 138.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-14.smt2                                   |   26.736s | 142.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-16.smt2                                   |   30.029s | 151.0MiB| timeout | 0 |  |  |
|sal/fischer6-mutex-20.smt2                                   |   30.032s | 142.0MiB| timeout | 0 |  |  |
|scheduling/orb06_1000.smt2                                   |   30.042s | 118.0MiB| timeout | 0 |  |  |
|sal/fischer9-mutex-19.smt2                                   |   30.042s | 157.0MiB| timeout | 0 |  |  |
|sal/fischer9-mutex-17.smt2                                   |   30.048s | 153.0MiB| timeout | 0 |  |  |
|sal/fischer9-mutex-20.smt2                                   |   30.050s | 156.0MiB| timeout | 0 |  |  |
|scheduling/yn4_1000.smt2                                     |   30.052s | 313.0MiB| timeout | 0 |  |  |
|sal/fischer9-mutex-18.smt2                                   |   30.052s | 156.0MiB| timeout | 0 |  |  |
|scheduling/orb01_1059.smt2                                   |   30.053s | 118.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-6.smt2          |   30.054s | 189.0MiB| timeout | 0 |  |  |
|scheduling/orb03_1005.smt2                                   |   30.055s | 120.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-7.smt2          |   30.055s | 279.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-5.smt2          |   30.057s | 261.0MiB| timeout | 0 |  |  |
|scheduling/orb01_1000.smt2                                   |   30.062s | 117.0MiB| timeout | 0 |  |  |
|scheduling/abz7_667.smt2                                     |   30.064s | 263.0MiB| timeout | 0 |  |  |
|scheduling/orb06_1010.smt2                                   |   30.066s | 118.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-6.smt2          |   30.068s | 439.0MiB| timeout | 0 |  |  |
|scheduling/abz7_700.smt2                                     |   30.070s | 270.0MiB| timeout | 0 |  |  |
|scheduling/abz7_600.smt2                                     |   30.070s | 256.0MiB| timeout | 0 |  |  |
|scheduling/yn4_969.smt2                                      |   30.071s | 320.0MiB| timeout | 0 |  |  |
|scheduling/yn3_828.smt2                                      |   30.071s | 307.0MiB| timeout | 0 |  |  |
|scheduling/yn3_950.smt2                                      |   30.072s | 329.0MiB| timeout | 0 |  |  |
|scheduling/yn4_919.smt2                                      |   30.072s | 303.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-matrix2x2.pddl.smt2   |   30.075s | 413.0MiB| timeout | 0 |  |  |
|scheduling/yn2_950.smt2                                      |   30.076s | 338.0MiB| timeout | 0 |  |  |
|scheduling/abz7_691.smt2                                     |   30.078s | 268.0MiB| timeout | 0 |  |  |
|scheduling/yn2_862.smt2                                      |   30.081s | 312.0MiB| timeout | 0 |  |  |
|scheduling/yn4_850.smt2                                      |   30.081s | 297.0MiB| timeout | 0 |  |  |
|scheduling/yn1_850.smt2                                      |   30.082s | 301.0MiB| timeout | 0 |  |  |
|scheduling/yn1_827.smt2                                      |   30.083s | 297.0MiB| timeout | 0 |  |  |
|scheduling/yn2_890.smt2                                      |   30.088s | 314.0MiB| timeout | 0 |  |  |
|scheduling/yn1_887.smt2                                      |   30.089s | 312.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-15.base.cvc.smt2                          |   30.089s | 509.0MiB| timeout | 0 |  |  |
|scheduling/yn3_894.smt2                                      |   30.092s | 312.0MiB| timeout | 0 |  |  |
|scheduling/yn3_860.smt2                                      |   30.094s | 305.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-19.base.cvc.smt2                          |   30.094s | 666.0MiB| timeout | 0 |  |  |
|skdmxa/skdmxa-3x3-15.smt2                                    |   30.095s | 323.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-14.base.cvc.smt2                          |   30.099s | 494.0MiB| timeout | 0 |  |  |
|skdmxa/skdmxa-3x3-20.smt2                                    |   30.100s | 403.0MiB| timeout | 0 |  |  |
|scheduling/abz7_670.smt2                                     |   30.104s | 265.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-17.base.cvc.smt2                          |   30.105s | 604.0MiB| timeout | 0 |  |  |
|scheduling/yn2_910.smt2                                      |   30.109s | 318.0MiB| timeout | 0 |  |  |
|scheduling/yn1_950.smt2                                      |   30.111s | 312.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-18.base.cvc.smt2                          |   30.112s | 644.0MiB| timeout | 0 |  |  |
|scheduling/swv12_2990.smt2                                   |   30.116s | 673.0MiB| timeout | 0 |  |  |
|scheduling/abz7_800.smt2                                     |   30.116s | 275.0MiB| timeout | 0 |  |  |
|scheduling/swv12_2900.smt2                                   |   30.116s | 684.0MiB| timeout | 0 |  |  |
|scheduling/swv14_2895.smt2                                   |   30.119s | 667.0MiB| timeout | 0 |  |  |
|scheduling/swv12_3004.smt2                                   |   30.121s | 696.0MiB| timeout | 0 |  |  |
|scheduling/yn4_950.smt2                                      |   30.123s | 307.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-13.base.cvc.smt2                          |   30.123s | 472.0MiB| timeout | 0 |  |  |
|scheduling/swv14_3000.smt2                                   |   30.124s | 661.0MiB| timeout | 0 |  |  |
|scheduling/swv12_3050.smt2                                   |   30.125s | 730.0MiB| timeout | 0 |  |  |
|scheduling/swv14_2905.smt2                                   |   30.126s | 670.0MiB| timeout | 0 |  |  |
|scheduling/swv11_2983.smt2                                   |   30.127s | 644.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-16.base.cvc.smt2                          |   30.128s | 538.0MiB| timeout | 0 |  |  |
|scheduling/swv14_2800.smt2                                   |   30.131s | 646.0MiB| timeout | 0 |  |  |
|scheduling/swv11_2992.smt2                                   |   30.133s | 626.0MiB| timeout | 0 |  |  |
|scheduling/swv11_2988.smt2                                   |   30.136s | 614.0MiB| timeout | 0 |  |  |
|scheduling/swv13_3104.smt2                                   |   30.138s | 696.0MiB| timeout | 0 |  |  |
|scheduling/swv14_2885.smt2                                   |   30.144s | 627.0MiB| timeout | 0 |  |  |
|scheduling/swv12_2972.smt2                                   |   30.157s | 683.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-20.base.cvc.smt2                          |   30.167s | 737.0MiB| timeout | 0 |  |  |
|scheduling/swv11_2900.smt2                                   |   30.202s | 633.0MiB| timeout | 0 |  |  |
|scheduling/swv13_3000.smt2                                   |   30.205s | 693.0MiB| timeout | 0 |  |  |
|scheduling/swv13_3150.smt2                                   |   30.226s | 718.0MiB| timeout | 0 |  |  |
|scheduling/swv13_3200.smt2                                   |   30.229s | 709.0MiB| timeout | 0 |  |  |
|scheduling/swv11_3050.smt2                                   |   30.233s | 649.0MiB| timeout | 0 |  |  |