# .

* SAT 94
* UNSAT 93
* 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-newscoring
Runner: lev-ripper
Z3 repo: ilanashapiro/z3
Z3 commit: c9b7c405bd0ab6885db6886544c4e88180ae6d34
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: new RDL scoring

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|sal/fischer3-mutex-5.smt2                                    |    0.088s | 91.66MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-matrix1x1.pddl.smt2   |    0.094s | 89.624MiB| sat | 0 |  |  |
|sal/fischer3-mutex-2.smt2                                    |    0.094s | 90.36MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-1.smt2          |    0.096s | 89.624MiB| sat | 0 |  |  |
|sal/fischer6-mutex-4.smt2                                    |    0.098s | 92.976MiB| unsat | 0 |  |  |
|check/bignum_rdl2.smt2                                       |    0.102s | 89.112MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-2.smt2                                    |    0.103s | 91.196MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking02.smt2              |    0.104s | 90.904MiB| sat | 0 |  |  |
|check/bignum_rdl1.smt2                                       |    0.106s | 89.384MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking01.smt2              |    0.106s | 90.4MiB| sat | 0 |  |  |
|sal/fischer3-mutex-3.smt2                                    |    0.108s | 90.904MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-6.smt2                                    |    0.110s | 92.156MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-3.smt2                                    |    0.113s | 93.172MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-03.smt2       |    0.114s | 91.932MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking04.smt2              |    0.115s | 91.928MiB| sat | 0 |  |  |
|sal/fischer6-mutex-1.smt2                                    |    0.117s | 89.624MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-2.smt2          |    0.118s | 91.84MiB| sat | 0 |  |  |
|sal/fischer6-mutex-2.smt2                                    |    0.118s | 90.972MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking03.smt2              |    0.121s | 91.488MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-04.smt2       |    0.122s | 91.928MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking05.smt2              |    0.123s | 92.444MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-2.smt2          |    0.125s | 92.496MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking06.smt2              |    0.127s | 92.7MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-07.smt2       |    0.128s | 94.868MiB| sat | 0 |  |  |
|sal/fischer6-mutex-5.smt2                                    |    0.129s | 93.248MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-5.smt2                                    |    0.131s | 96.148MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-1.smt2                                    |    0.132s | 90.648MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-05.smt2       |    0.133s | 93.176MiB| sat | 0 |  |  |
|sal/fischer6-mutex-3.smt2                                    |    0.133s | 91.68MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-06.smt2       |    0.135s | 93.208MiB| sat | 0 |  |  |
|sal/fischer3-mutex-9.smt2                                    |    0.136s | 94.492MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking07.smt2              |    0.138s | 93.404MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking08.smt2              |    0.139s | 93.996MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking09.smt2              |    0.144s | 94.756MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-08.smt2       |    0.147s | 94.664MiB| sat | 0 |  |  |
|sal/fischer3-mutex-7.smt2                                    |    0.147s | 92.696MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking10.smt2              |    0.153s | 95.636MiB| sat | 0 |  |  |
|sal/fischer6-mutex-6.smt2                                    |    0.154s | 95.168MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking13.smt2              |    0.155s | 96.328MiB| sat | 0 |  |  |
|sal/fischer9-mutex-4.smt2                                    |    0.160s | 94.232MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-10.smt2       |    0.161s | 95.892MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking11.smt2              |    0.162s | 95.856MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-09.smt2       |    0.164s | 96.156MiB| sat | 0 |  |  |
|sal/fischer3-mutex-8.smt2                                    |    0.168s | 93.196MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking12.smt2              |    0.172s | 96.272MiB| sat | 0 |  |  |
|sal/fischer3-mutex-10.smt2                                   |    0.182s | 95.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking14.smt2              |    0.186s | 97.448MiB| sat | 0 |  |  |
|sal/fischer3-mutex-1.smt2                                    |    0.189s | 90.14MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking15.smt2              |    0.191s | 98.34MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking16.smt2              |    0.196s | 98.468MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking18.smt2              |    0.203s | 99.236MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-3.smt2          |    0.205s | 97.944MiB| sat | 0 |  |  |
|sal/fischer6-mutex-7.smt2                                    |    0.205s | 96.132MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking20.smt2              |    0.206s | 98.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking17.smt2              |    0.207s | 99.156MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking19.smt2              |    0.212s | 97.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-7.smt2                                    |    0.216s | 99.156MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-11.smt2                                   |    0.223s | 95.396MiB| unsat | 0 |  |  |
|scheduling/orb07_330.smt2                                    |    0.229s | 98.84MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking22.smt2              |    0.233s | 99.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-8.smt2                                    |    0.234s | 97.664MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking21.smt2              |    0.236s | 98.0MiB| sat | 0 |  |  |
|scheduling/orb09_800.smt2                                    |    0.242s | 100.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-12.smt2                                   |    0.243s | 96.432MiB| unsat | 0 |  |  |
|scheduling/abz5_1000.smt2                                    |    0.246s | 98.0MiB| unsat | 0 |  |  |
|scheduling/abz6_800.smt2                                     |    0.247s | 98.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-4.smt2                                    |    0.248s | 91.416MiB| unsat | 0 |  |  |
|scheduling/orb10_800.smt2                                    |    0.265s | 100.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-20.smt2       |    0.267s | 99.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-13.smt2                                   |    0.283s | 97.572MiB| unsat | 0 |  |  |
|scheduling/orb07_250.smt2                                    |    0.294s | 96.408MiB| unsat | 0 |  |  |
|scheduling/orb02_800.smt2                                    |    0.299s | 100.0MiB| unsat | 0 |  |  |
|scheduling/orb04_850.smt2                                    |    0.301s | 99.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-9.smt2                                    |    0.301s | 99.244MiB| unsat | 0 |  |  |
|scheduling/orb05_700.smt2                                    |    0.306s | 100.0MiB| unsat | 0 |  |  |
|scheduling/orb09_1100.smt2                                   |    0.306s | 103.0MiB| sat | 0 |  |  |
|scheduling/orb02_700.smt2                                    |    0.313s | 97.312MiB| unsat | 0 |  |  |
|scheduling/orb08_700.smt2                                    |    0.316s | 99.0MiB| unsat | 0 |  |  |
|scheduling/orb07_550.smt2                                    |    0.317s | 103.0MiB| sat | 0 |  |  |
|scheduling/orb08_830.smt2                                    |    0.329s | 100.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-6.smt2                                    |    0.333s | 98.268MiB| unsat | 0 |  |  |
|scheduling/orb06_1200.smt2                                   |    0.360s | 102.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-8.smt2                                    |    0.363s | 99.0MiB| unsat | 0 |  |  |
|scheduling/abz6_1100.smt2                                    |    0.368s | 102.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-14.smt2                                   |    0.376s | 98.424MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-16.smt2                                   |    0.390s | 99.928MiB| unsat | 0 |  |  |
|scheduling/orb02_1000.smt2                                   |    0.422s | 101.0MiB| sat | 0 |  |  |
|scheduling/abz5_1400.smt2                                    |    0.423s | 101.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-15.smt2                                   |    0.424s | 99.944MiB| unsat | 0 |  |  |
|scheduling/orb04_1200.smt2                                   |    0.425s | 103.0MiB| sat | 0 |  |  |
|scheduling/orb10_1100.smt2                                   |    0.426s | 103.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-30.smt2       |    0.464s | 106.0MiB| sat | 0 |  |  |
|scheduling/orb09_1000.smt2                                   |    0.467s | 102.0MiB| sat | 0 |  |  |
|scheduling/abz6_900.smt2                                     |    0.473s | 101.0MiB| unsat | 0 |  |  |
|scheduling/orb03_850.smt2                                    |    0.476s | 101.0MiB| unsat | 0 |  |  |
|scheduling/abz6_1000.smt2                                    |    0.483s | 102.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-3.smt2          |    0.509s | 101.0MiB| sat | 0 |  |  |
|scheduling/orb05_800.smt2                                    |    0.526s | 102.0MiB| unsat | 0 |  |  |
|scheduling/orb06_900.smt2                                    |    0.540s | 102.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-17.smt2                                   |    0.574s | 98.0MiB| unsat | 0 |  |  |
|scheduling/orb03_1200.smt2                                   |    0.612s | 105.0MiB| sat | 0 |  |  |
|scheduling/orb08_1000.smt2                                   |    0.643s | 105.0MiB| sat | 0 |  |  |
|scheduling/orb05_1000.smt2                                   |    0.650s | 105.0MiB| sat | 0 |  |  |
|scheduling/orb04_1100.smt2                                   |    0.665s | 105.0MiB| sat | 0 |  |  |
|scheduling/orb01_900.smt2                                    |    0.684s | 102.0MiB| unsat | 0 |  |  |
|scheduling/orb04_950.smt2                                    |    0.689s | 103.0MiB| unsat | 0 |  |  |
|scheduling/abz5_1300.smt2                                    |    0.693s | 103.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-40.smt2       |    0.717s | 112.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-18.smt2                                   |    0.796s | 100.0MiB| unsat | 0 |  |  |
|skdmxa/skdmxa-3x3-5.smt2                                     |    0.802s | 133.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-6.base.cvc.smt2                           |    0.817s | 179.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-10.smt2                                   |    0.823s | 100.0MiB| unsat | 0 |  |  |
|scheduling/orb07_430.smt2                                    |    0.856s | 104.0MiB| sat | 0 |  |  |
|scheduling/abz6_943.smt2                                     |    0.865s | 102.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-5.induction.cvc.smt2                      |    0.888s | 214.0MiB| sat | 0 |  |  |
|scheduling/orb02_900.smt2                                    |    0.968s | 105.0MiB| sat | 0 |  |  |
|scheduling/orb10_900.smt2                                    |    0.990s | 103.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-19.smt2                                   |    1.082s | 102.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-5.base.cvc.smt2                           |    1.106s | 156.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-6.induction.cvc.smt2                      |    1.119s | 242.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-9.smt2                                    |    1.144s | 104.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-7.base.cvc.smt2                           |    1.150s | 227.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-11.smt2                                   |    1.208s | 102.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-12.smt2                                   |    1.243s | 104.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-20.smt2                                   |    1.285s | 103.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-4.smt2          |    1.348s | 109.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-8.base.cvc.smt2                           |    1.375s | 247.0MiB| unsat | 0 |  |  |
|scheduling/orb01_1200.smt2                                   |    1.598s | 108.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-9.base.cvc.smt2                           |    1.667s | 268.0MiB| unsat | 0 |  |  |
|scheduling/orb05_900.smt2                                    |    1.676s | 105.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-7.induction.cvc.smt2                      |    1.707s | 338.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-8.induction.cvc.smt2                      |    1.889s | 345.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-60.smt2       |    1.905s | 123.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-13.smt2                                   |    1.999s | 107.0MiB| unsat | 0 |  |  |
|scheduling/orb06_1100.smt2                                   |    2.041s | 108.0MiB| sat | 0 |  |  |
|scheduling/orb09_900.smt2                                    |    2.078s | 107.0MiB| unsat | 0 |  |  |
|skdmxa/skdmxa-3x3-10.smt2                                    |    2.273s | 192.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-10.smt2                                   |    2.317s | 109.0MiB| unsat | 0 |  |  |
|scheduling/orb10_1000.smt2                                   |    2.442s | 107.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-10.base.cvc.smt2                          |    2.446s | 289.0MiB| unsat | 0 |  |  |
|scheduling/orb03_1100.smt2                                   |    2.838s | 109.0MiB| sat | 0 |  |  |
|scheduling/yn1_750.smt2                                      |    2.875s | 250.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-10.induction.cvc.smt2                     |    2.905s | 448.0MiB| sat | 0 |  |  |
|scheduling/abz7_500.smt2                                     |    2.953s | 190.0MiB| unsat | 0 |  |  |
|scheduling/orb02_888.smt2                                    |    2.992s | 108.0MiB| sat | 0 |  |  |
|scheduling/abz5_1200.smt2                                    |    3.322s | 106.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-14.smt2                                   |    3.359s | 112.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-11.smt2                                   |    3.483s | 113.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-70.smt2       |    3.542s | 140.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-80.smt2       |    3.835s | 145.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-9.induction.cvc.smt2                      |    3.895s | 404.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-11.induction.cvc.smt2                     |    3.944s | 448.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-12.induction.cvc.smt2                     |    3.987s | 503.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-12.smt2                                   |    5.293s | 119.0MiB| unsat | 0 |  |  |
|scheduling/orb10_944.smt2                                    |    5.544s | 109.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-15.smt2                                   |    5.884s | 118.0MiB| unsat | 0 |  |  |
|scheduling/orb07_397.smt2                                    |    6.012s | 110.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-11.base.cvc.smt2                          |    6.115s | 316.0MiB| unsat | 0 |  |  |
|scheduling/orb09_934.smt2                                    |    6.167s | 110.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-14.induction.cvc.smt2                     |    6.691s | 697.0MiB| sat | 0 |  |  |
|scheduling/yn2_750.smt2                                      |    6.810s | 254.0MiB| unsat | 0 |  |  |
|scheduling/abz5_1234.smt2                                    |    7.073s | 110.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-16.smt2                                   |    7.509s | 123.0MiB| unsat | 0 |  |  |
|scheduling/yn3_750.smt2                                      |    7.624s | 270.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-16.induction.cvc.smt2                     |    8.367s | 718.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-13.induction.cvc.smt2                     |    8.432s | 638.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-90.smt2       |    8.496s | 152.0MiB| sat | 0 |  |  |
|scheduling/orb04_1005.smt2                                   |    9.060s | 112.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-17.induction.cvc.smt2                     |   10.206s | 782.0MiB| sat | 0 |  |  |
|scheduling/orb08_888.smt2                                    |   11.645s | 112.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-19.induction.cvc.smt2                     |   11.816s | 849.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-15.induction.cvc.smt2                     |   11.891s | 742.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-17.smt2                                   |   12.256s | 128.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-18.induction.cvc.smt2                     |   12.258s | 790.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-13.smt2                                   |   12.452s | 130.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-5.smt2          |   12.734s | 140.0MiB| sat | 0 |  |  |
|scheduling/orb05_887.smt2                                    |   12.754s | 112.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-18.smt2                                   |   13.707s | 129.0MiB| unsat | 0 |  |  |
|scheduling/orb03_950.smt2                                    |   15.279s | 114.0MiB| unsat | 0 |  |  |
|scheduling/orb08_930.smt2                                    |   17.281s | 115.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-20.induction.cvc.smt2                     |   18.233s | 848.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-14.smt2                                   |   18.440s | 138.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-12.base.cvc.smt2                          |   18.959s | 364.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-19.smt2                                   |   20.947s | 138.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-4.smt2          |   21.294s | 158.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-15.smt2                                   |   25.104s | 148.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-13.base.cvc.smt2                          |   28.952s | 477.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-17.smt2                                   |   30.025s | 153.0MiB| timeout | 0 |  |  |
|scheduling/orb01_1000.smt2                                   |   30.028s | 118.0MiB| timeout | 0 |  |  |
|sal/fischer9-mutex-18.smt2                                   |   30.034s | 155.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-5.smt2          |   30.035s | 260.0MiB| timeout | 0 |  |  |
|scheduling/orb06_1000.smt2                                   |   30.037s | 118.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-6.smt2          |   30.040s | 190.0MiB| timeout | 0 |  |  |
|sal/fischer6-mutex-20.smt2                                   |   30.040s | 140.0MiB| timeout | 0 |  |  |
|sal/fischer9-mutex-16.smt2                                   |   30.041s | 156.0MiB| timeout | 0 |  |  |
|sal/fischer9-mutex-20.smt2                                   |   30.043s | 158.0MiB| timeout | 0 |  |  |
|scheduling/orb01_1100.smt2                                   |   30.044s | 119.0MiB| timeout | 0 |  |  |
|scheduling/orb03_1005.smt2                                   |   30.057s | 120.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-7.smt2          |   30.057s | 278.0MiB| timeout | 0 |  |  |
|sal/fischer9-mutex-19.smt2                                   |   30.059s | 158.0MiB| timeout | 0 |  |  |
|scheduling/abz7_600.smt2                                     |   30.062s | 252.0MiB| timeout | 0 |  |  |
|scheduling/orb01_1059.smt2                                   |   30.065s | 120.0MiB| timeout | 0 |  |  |
|scheduling/abz7_700.smt2                                     |   30.067s | 269.0MiB| timeout | 0 |  |  |
|scheduling/yn2_950.smt2                                      |   30.070s | 335.0MiB| timeout | 0 |  |  |
|scheduling/abz7_691.smt2                                     |   30.070s | 270.0MiB| timeout | 0 |  |  |
|scheduling/yn1_827.smt2                                      |   30.071s | 301.0MiB| timeout | 0 |  |  |
|scheduling/orb06_1010.smt2                                   |   30.071s | 119.0MiB| timeout | 0 |  |  |
|scheduling/yn3_828.smt2                                      |   30.071s | 308.0MiB| timeout | 0 |  |  |
|scheduling/yn1_887.smt2                                      |   30.071s | 311.0MiB| timeout | 0 |  |  |
|scheduling/abz7_670.smt2                                     |   30.075s | 268.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-6.smt2          |   30.076s | 439.0MiB| timeout | 0 |  |  |
|scheduling/abz7_667.smt2                                     |   30.077s | 263.0MiB| timeout | 0 |  |  |
|scheduling/yn1_850.smt2                                      |   30.077s | 300.0MiB| timeout | 0 |  |  |
|scheduling/abz7_800.smt2                                     |   30.077s | 275.0MiB| timeout | 0 |  |  |
|scheduling/yn3_860.smt2                                      |   30.077s | 310.0MiB| timeout | 0 |  |  |
|scheduling/yn3_950.smt2                                      |   30.079s | 326.0MiB| timeout | 0 |  |  |
|scheduling/yn4_1000.smt2                                     |   30.080s | 313.0MiB| timeout | 0 |  |  |
|skdmxa/skdmxa-3x3-15.smt2                                    |   30.081s | 324.0MiB| timeout | 0 |  |  |
|scheduling/yn4_919.smt2                                      |   30.081s | 307.0MiB| timeout | 0 |  |  |
|scheduling/yn4_969.smt2                                      |   30.082s | 321.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-15.base.cvc.smt2                          |   30.083s | 515.0MiB| timeout | 0 |  |  |
|scheduling/yn2_862.smt2                                      |   30.084s | 311.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-matrix2x2.pddl.smt2   |   30.084s | 413.0MiB| timeout | 0 |  |  |
|scheduling/yn2_890.smt2                                      |   30.085s | 317.0MiB| timeout | 0 |  |  |
|scheduling/yn4_850.smt2                                      |   30.085s | 296.0MiB| timeout | 0 |  |  |
|scheduling/yn1_950.smt2                                      |   30.085s | 318.0MiB| timeout | 0 |  |  |
|scheduling/yn4_950.smt2                                      |   30.091s | 308.0MiB| timeout | 0 |  |  |
|scheduling/yn3_894.smt2                                      |   30.094s | 310.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-14.base.cvc.smt2                          |   30.097s | 495.0MiB| timeout | 0 |  |  |
|skdmxa/skdmxa-3x3-20.smt2                                    |   30.098s | 402.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-19.base.cvc.smt2                          |   30.104s | 667.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-18.base.cvc.smt2                          |   30.106s | 642.0MiB| timeout | 0 |  |  |
|scheduling/swv11_2983.smt2                                   |   30.112s | 641.0MiB| timeout | 0 |  |  |
|scheduling/swv11_2900.smt2                                   |   30.118s | 628.0MiB| timeout | 0 |  |  |
|scheduling/swv12_2990.smt2                                   |   30.119s | 678.0MiB| timeout | 0 |  |  |
|scheduling/swv11_2988.smt2                                   |   30.119s | 610.0MiB| timeout | 0 |  |  |
|scheduling/swv14_2895.smt2                                   |   30.121s | 644.0MiB| timeout | 0 |  |  |
|scheduling/swv13_3104.smt2                                   |   30.122s | 682.0MiB| timeout | 0 |  |  |
|scheduling/swv12_3050.smt2                                   |   30.123s | 740.0MiB| timeout | 0 |  |  |
|scheduling/swv13_3000.smt2                                   |   30.127s | 669.0MiB| timeout | 0 |  |  |
|scheduling/swv11_2992.smt2                                   |   30.131s | 618.0MiB| timeout | 0 |  |  |
|scheduling/swv14_3000.smt2                                   |   30.135s | 686.0MiB| timeout | 0 |  |  |
|scheduling/swv14_2885.smt2                                   |   30.136s | 643.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-17.base.cvc.smt2                          |   30.138s | 604.0MiB| timeout | 0 |  |  |
|scheduling/yn2_910.smt2                                      |   30.139s | 314.0MiB| timeout | 0 |  |  |
|scheduling/swv14_2800.smt2                                   |   30.139s | 651.0MiB| timeout | 0 |  |  |
|scheduling/swv12_2900.smt2                                   |   30.140s | 663.0MiB| timeout | 0 |  |  |
|scheduling/swv12_2972.smt2                                   |   30.142s | 674.0MiB| timeout | 0 |  |  |
|scheduling/swv13_3200.smt2                                   |   30.147s | 684.0MiB| timeout | 0 |  |  |
|scheduling/swv14_2905.smt2                                   |   30.147s | 625.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-16.base.cvc.smt2                          |   30.147s | 544.0MiB| timeout | 0 |  |  |
|scheduling/swv12_3004.smt2                                   |   30.148s | 707.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-20.base.cvc.smt2                          |   30.176s | 733.0MiB| timeout | 0 |  |  |
|scheduling/swv13_3150.smt2                                   |   30.211s | 728.0MiB| timeout | 0 |  |  |
|scheduling/swv11_3050.smt2                                   |   30.220s | 649.0MiB| timeout | 0 |  |  |