# .

* SAT 94
* UNSAT 94
* TIMEOUT 67
* 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
Runner: lev-ripper
Z3 repo: ilanashapiro/z3
Z3 commit: e742d8ba0b05eaff1ccca5ff1116975780d26bb0
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: change some scoring strategies, add LIA and NIA param tuning

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|SMT-Temporal-Planning-Benchmarks/tempo-width-1.smt2          |    0.069s | 89.864MiB| sat | 0 |  |  |
|sal/fischer3-mutex-5.smt2                                    |    0.085s | 91.468MiB| unsat | 0 |  |  |
|check/bignum_rdl1.smt2                                       |    0.089s | 88.956MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-matrix1x1.pddl.smt2   |    0.090s | 89.72MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking02.smt2              |    0.091s | 90.796MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking01.smt2              |    0.092s | 90.648MiB| sat | 0 |  |  |
|sal/fischer3-mutex-2.smt2                                    |    0.094s | 90.268MiB| unsat | 0 |  |  |
|check/bignum_rdl2.smt2                                       |    0.106s | 88.98MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-6.smt2                                    |    0.106s | 91.928MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-3.smt2                                    |    0.107s | 90.648MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-2.smt2          |    0.109s | 92.084MiB| sat | 0 |  |  |
|sal/fischer9-mutex-2.smt2                                    |    0.109s | 91.672MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking06.smt2              |    0.110s | 92.844MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking03.smt2              |    0.113s | 91.16MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-03.smt2       |    0.119s | 92.18MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-2.smt2          |    0.120s | 92.748MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking05.smt2              |    0.121s | 92.44MiB| sat | 0 |  |  |
|sal/fischer6-mutex-1.smt2                                    |    0.122s | 89.88MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-4.smt2                                    |    0.122s | 92.96MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-3.smt2                                    |    0.125s | 91.672MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-3.smt2                                    |    0.126s | 93.176MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking04.smt2              |    0.127s | 91.856MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-05.smt2       |    0.129s | 93.392MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-06.smt2       |    0.131s | 93.212MiB| sat | 0 |  |  |
|sal/fischer6-mutex-5.smt2                                    |    0.131s | 93.44MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-5.smt2                                    |    0.132s | 96.284MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-04.smt2       |    0.133s | 91.936MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking07.smt2              |    0.133s | 93.408MiB| sat | 0 |  |  |
|sal/fischer6-mutex-2.smt2                                    |    0.135s | 90.876MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-7.smt2                                    |    0.137s | 92.952MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking08.smt2              |    0.138s | 94.072MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-07.smt2       |    0.146s | 94.876MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking09.smt2              |    0.148s | 95.008MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking10.smt2              |    0.149s | 95.636MiB| sat | 0 |  |  |
|sal/fischer9-mutex-1.smt2                                    |    0.150s | 90.136MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-6.smt2                                    |    0.151s | 94.616MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-08.smt2       |    0.152s | 94.868MiB| sat | 0 |  |  |
|sal/fischer9-mutex-4.smt2                                    |    0.154s | 94.24MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-10.smt2       |    0.155s | 95.66MiB| sat | 0 |  |  |
|sal/fischer3-mutex-9.smt2                                    |    0.155s | 94.48MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-1.smt2                                    |    0.158s | 89.88MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking12.smt2              |    0.162s | 96.264MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking11.smt2              |    0.162s | 95.864MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-09.smt2       |    0.164s | 95.976MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking14.smt2              |    0.183s | 97.184MiB| sat | 0 |  |  |
|sal/fischer3-mutex-4.smt2                                    |    0.183s | 91.02MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking13.smt2              |    0.188s | 96.664MiB| sat | 0 |  |  |
|sal/fischer3-mutex-8.smt2                                    |    0.189s | 92.968MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-10.smt2                                   |    0.191s | 94.98MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking15.smt2              |    0.193s | 97.704MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking16.smt2              |    0.196s | 98.74MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-3.smt2          |    0.204s | 97.952MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking18.smt2              |    0.205s | 99.288MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking19.smt2              |    0.213s | 99.912MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking17.smt2              |    0.215s | 99.392MiB| sat | 0 |  |  |
|scheduling/abz5_1000.smt2                                    |    0.223s | 99.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-7.smt2                                    |    0.225s | 96.116MiB| unsat | 0 |  |  |
|scheduling/orb05_700.smt2                                    |    0.227s | 100.0MiB| unsat | 0 |  |  |
|scheduling/orb10_800.smt2                                    |    0.227s | 100.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking20.smt2              |    0.227s | 98.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-11.smt2                                   |    0.227s | 95.724MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking22.smt2              |    0.230s | 99.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-8.smt2                                    |    0.234s | 97.652MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-12.smt2                                   |    0.235s | 95.86MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/cooking21.smt2              |    0.241s | 99.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-7.smt2                                    |    0.243s | 99.212MiB| unsat | 0 |  |  |
|scheduling/orb07_550.smt2                                    |    0.263s | 103.0MiB| sat | 0 |  |  |
|scheduling/orb09_800.smt2                                    |    0.269s | 100.0MiB| unsat | 0 |  |  |
|scheduling/orb09_1100.smt2                                   |    0.271s | 103.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-20.smt2       |    0.275s | 99.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-13.smt2                                   |    0.296s | 97.408MiB| unsat | 0 |  |  |
|scheduling/orb07_250.smt2                                    |    0.299s | 96.284MiB| unsat | 0 |  |  |
|scheduling/orb08_700.smt2                                    |    0.302s | 99.0MiB| unsat | 0 |  |  |
|scheduling/abz6_1100.smt2                                    |    0.314s | 102.0MiB| sat | 0 |  |  |
|scheduling/abz6_800.smt2                                     |    0.316s | 98.0MiB| unsat | 0 |  |  |
|scheduling/orb02_700.smt2                                    |    0.323s | 97.82MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-6.smt2                                    |    0.325s | 98.268MiB| unsat | 0 |  |  |
|scheduling/orb07_330.smt2                                    |    0.336s | 98.328MiB| unsat | 0 |  |  |
|scheduling/orb08_830.smt2                                    |    0.340s | 100.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-9.smt2                                    |    0.349s | 99.024MiB| unsat | 0 |  |  |
|scheduling/orb04_850.smt2                                    |    0.350s | 99.0MiB| unsat | 0 |  |  |
|scheduling/orb02_800.smt2                                    |    0.351s | 99.0MiB| unsat | 0 |  |  |
|scheduling/orb06_1200.smt2                                   |    0.362s | 102.0MiB| sat | 0 |  |  |
|scheduling/abz5_1400.smt2                                    |    0.370s | 101.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-8.smt2                                    |    0.374s | 99.0MiB| unsat | 0 |  |  |
|sal/fischer3-mutex-14.smt2                                   |    0.376s | 98.144MiB| unsat | 0 |  |  |
|scheduling/orb02_1000.smt2                                   |    0.384s | 101.0MiB| sat | 0 |  |  |
|scheduling/orb04_1200.smt2                                   |    0.390s | 104.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-16.smt2                                   |    0.396s | 99.664MiB| unsat | 0 |  |  |
|scheduling/orb03_850.smt2                                    |    0.413s | 101.0MiB| unsat | 0 |  |  |
|scheduling/abz6_1000.smt2                                    |    0.414s | 102.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-15.smt2                                   |    0.438s | 99.788MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-30.smt2       |    0.456s | 106.0MiB| sat | 0 |  |  |
|scheduling/orb10_1100.smt2                                   |    0.468s | 103.0MiB| sat | 0 |  |  |
|scheduling/orb09_1000.smt2                                   |    0.481s | 102.0MiB| sat | 0 |  |  |
|scheduling/orb05_800.smt2                                    |    0.508s | 102.0MiB| unsat | 0 |  |  |
|scheduling/abz6_900.smt2                                     |    0.537s | 101.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-3.smt2          |    0.551s | 101.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-17.smt2                                   |    0.552s | 98.0MiB| unsat | 0 |  |  |
|scheduling/orb06_900.smt2                                    |    0.597s | 101.0MiB| unsat | 0 |  |  |
|scheduling/orb03_1200.smt2                                   |    0.601s | 106.0MiB| sat | 0 |  |  |
|scheduling/orb05_1000.smt2                                   |    0.631s | 104.0MiB| sat | 0 |  |  |
|scheduling/orb04_950.smt2                                    |    0.633s | 103.0MiB| unsat | 0 |  |  |
|scheduling/orb08_1000.smt2                                   |    0.639s | 105.0MiB| sat | 0 |  |  |
|scheduling/abz5_1300.smt2                                    |    0.689s | 103.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-40.smt2       |    0.717s | 111.0MiB| sat | 0 |  |  |
|scheduling/orb01_900.smt2                                    |    0.728s | 102.0MiB| unsat | 0 |  |  |
|scheduling/orb04_1100.smt2                                   |    0.741s | 105.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-10.smt2                                   |    0.785s | 100.0MiB| unsat | 0 |  |  |
|skdmxa/skdmxa-3x3-5.smt2                                     |    0.811s | 134.0MiB| unsat | 0 |  |  |
|scheduling/orb03_1100.smt2                                   |    0.829s | 105.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-6.base.cvc.smt2                           |    0.833s | 178.0MiB| unsat | 0 |  |  |
|scheduling/orb07_430.smt2                                    |    0.842s | 104.0MiB| sat | 0 |  |  |
|scheduling/abz6_943.smt2                                     |    0.883s | 103.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-5.induction.cvc.smt2                      |    0.903s | 215.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-19.smt2                                   |    1.008s | 102.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-5.base.cvc.smt2                           |    1.073s | 155.0MiB| unsat | 0 |  |  |
|scheduling/orb10_900.smt2                                    |    1.090s | 103.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-7.base.cvc.smt2                           |    1.114s | 227.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-6.induction.cvc.smt2                      |    1.142s | 243.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-18.smt2                                   |    1.148s | 101.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-9.smt2                                    |    1.168s | 104.0MiB| unsat | 0 |  |  |
|scheduling/orb02_900.smt2                                    |    1.278s | 105.0MiB| sat | 0 |  |  |
|sal/fischer3-mutex-20.smt2                                   |    1.318s | 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.362s | 247.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-11.smt2                                   |    1.452s | 103.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-9.base.cvc.smt2                           |    1.572s | 266.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-7.induction.cvc.smt2                      |    1.627s | 338.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-12.smt2                                   |    1.712s | 105.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-10.smt2                                   |    1.809s | 108.0MiB| unsat | 0 |  |  |
|scheduling/yn1_750.smt2                                      |    1.824s | 244.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-8.induction.cvc.smt2                      |    1.875s | 352.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-60.smt2       |    1.909s | 123.0MiB| sat | 0 |  |  |
|scheduling/orb01_1200.smt2                                   |    1.986s | 108.0MiB| sat | 0 |  |  |
|scheduling/orb05_900.smt2                                    |    2.044s | 106.0MiB| sat | 0 |  |  |
|scheduling/abz7_500.smt2                                     |    2.252s | 189.0MiB| unsat | 0 |  |  |
|scheduling/orb09_900.smt2                                    |    2.309s | 106.0MiB| unsat | 0 |  |  |
|scheduling/orb06_1100.smt2                                   |    2.348s | 109.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-10.base.cvc.smt2                          |    2.402s | 290.0MiB| unsat | 0 |  |  |
|scheduling/orb02_888.smt2                                    |    2.692s | 107.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-13.smt2                                   |    2.792s | 108.0MiB| unsat | 0 |  |  |
|skdmxa/skdmxa-3x3-10.smt2                                    |    2.812s | 191.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-10.induction.cvc.smt2                     |    3.030s | 457.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-14.smt2                                   |    3.239s | 111.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-80.smt2       |    3.280s | 144.0MiB| sat | 0 |  |  |
|scheduling/abz5_1234.smt2                                    |    3.407s | 107.0MiB| sat | 0 |  |  |
|scheduling/abz5_1200.smt2                                    |    3.484s | 106.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-11.smt2                                   |    3.541s | 114.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-70.smt2       |    3.613s | 140.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-9.induction.cvc.smt2                      |    3.752s | 405.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-12.induction.cvc.smt2                     |    3.785s | 500.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-11.induction.cvc.smt2                     |    3.919s | 440.0MiB| sat | 0 |  |  |
|scheduling/orb10_1000.smt2                                   |    4.319s | 109.0MiB| sat | 0 |  |  |
|scheduling/orb10_944.smt2                                    |    4.528s | 108.0MiB| sat | 0 |  |  |
|scheduling/orb07_397.smt2                                    |    4.555s | 109.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-15.smt2                                   |    5.020s | 116.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tms-2-3-light-90.smt2       |    5.456s | 150.0MiB| sat | 0 |  |  |
|scheduling/yn3_750.smt2                                      |    5.611s | 267.0MiB| unsat | 0 |  |  |
|scheduling/yn2_750.smt2                                      |    5.727s | 256.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-11.base.cvc.smt2                          |    6.212s | 318.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-14.induction.cvc.smt2                     |    6.326s | 691.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-16.smt2                                   |    7.301s | 121.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-13.induction.cvc.smt2                     |    7.371s | 592.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-12.smt2                                   |    8.141s | 122.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-16.induction.cvc.smt2                     |    8.205s | 720.0MiB| sat | 0 |  |  |
|scheduling/orb05_887.smt2                                    |    8.685s | 111.0MiB| sat | 0 |  |  |
|scheduling/orb08_930.smt2                                    |    9.643s | 113.0MiB| sat | 0 |  |  |
|scheduling/orb09_934.smt2                                    |    9.880s | 112.0MiB| sat | 0 |  |  |
|scheduling/orb04_1005.smt2                                   |   10.224s | 113.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-13.smt2                                   |   10.241s | 130.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-17.smt2                                   |   10.252s | 128.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-19.induction.cvc.smt2                     |   11.120s | 796.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-18.induction.cvc.smt2                     |   12.215s | 808.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-17.induction.cvc.smt2                     |   12.511s | 861.0MiB| sat | 0 |  |  |
|skdmxa2/skdmxa-3x3-15.induction.cvc.smt2                     |   12.946s | 732.0MiB| sat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-5.smt2          |   13.411s | 141.0MiB| sat | 0 |  |  |
|scheduling/orb08_888.smt2                                    |   14.024s | 112.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-18.smt2                                   |   17.161s | 135.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-12.base.cvc.smt2                          |   20.697s | 364.0MiB| unsat | 0 |  |  |
|scheduling/orb03_950.smt2                                    |   21.376s | 114.0MiB| unsat | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-4.smt2          |   22.070s | 158.0MiB| sat | 0 |  |  |
|sal/fischer9-mutex-14.smt2                                   |   22.488s | 138.0MiB| unsat | 0 |  |  |
|skdmxa2/skdmxa-3x3-20.induction.cvc.smt2                     |   23.345s | 926.0MiB| sat | 0 |  |  |
|sal/fischer6-mutex-19.smt2                                   |   23.891s | 139.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-15.smt2                                   |   27.054s | 143.0MiB| unsat | 0 |  |  |
|sal/fischer6-mutex-20.smt2                                   |   27.151s | 141.0MiB| unsat | 0 |  |  |
|skdmxa/skdmxa-3x3-15.smt2                                    |   28.471s | 321.0MiB| unsat | 0 |  |  |
|sal/fischer9-mutex-18.smt2                                   |   30.025s | 152.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-6.smt2          |   30.026s | 189.0MiB| timeout | 0 |  |  |
|scheduling/orb01_1000.smt2                                   |   30.040s | 118.0MiB| timeout | 0 |  |  |
|scheduling/orb01_1100.smt2                                   |   30.041s | 119.0MiB| timeout | 0 |  |  |
|sal/fischer9-mutex-20.smt2                                   |   30.044s | 157.0MiB| timeout | 0 |  |  |
|scheduling/orb06_1000.smt2                                   |   30.047s | 118.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-5.smt2          |   30.048s | 260.0MiB| timeout | 0 |  |  |
|scheduling/yn3_828.smt2                                      |   30.049s | 307.0MiB| timeout | 0 |  |  |
|sal/fischer9-mutex-16.smt2                                   |   30.050s | 153.0MiB| timeout | 0 |  |  |
|sal/fischer9-mutex-19.smt2                                   |   30.052s | 157.0MiB| timeout | 0 |  |  |
|sal/fischer9-mutex-17.smt2                                   |   30.054s | 149.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-depth-7.smt2          |   30.055s | 278.0MiB| timeout | 0 |  |  |
|scheduling/abz7_600.smt2                                     |   30.057s | 251.0MiB| timeout | 0 |  |  |
|scheduling/orb03_1005.smt2                                   |   30.059s | 119.0MiB| timeout | 0 |  |  |
|scheduling/orb06_1010.smt2                                   |   30.063s | 119.0MiB| timeout | 0 |  |  |
|scheduling/abz7_670.smt2                                     |   30.067s | 265.0MiB| timeout | 0 |  |  |
|scheduling/yn3_950.smt2                                      |   30.070s | 332.0MiB| timeout | 0 |  |  |
|scheduling/abz7_700.smt2                                     |   30.070s | 272.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-matrix2x2.pddl.smt2   |   30.072s | 413.0MiB| timeout | 0 |  |  |
|scheduling/abz7_667.smt2                                     |   30.074s | 265.0MiB| timeout | 0 |  |  |
|scheduling/yn2_950.smt2                                      |   30.075s | 339.0MiB| timeout | 0 |  |  |
|scheduling/abz7_800.smt2                                     |   30.075s | 270.0MiB| timeout | 0 |  |  |
|scheduling/abz7_691.smt2                                     |   30.075s | 268.0MiB| timeout | 0 |  |  |
|scheduling/yn4_1000.smt2                                     |   30.076s | 311.0MiB| timeout | 0 |  |  |
|SMT-Temporal-Planning-Benchmarks/tempo-width-6.smt2          |   30.077s | 438.0MiB| timeout | 0 |  |  |
|scheduling/orb01_1059.smt2                                   |   30.078s | 118.0MiB| timeout | 0 |  |  |
|scheduling/yn4_969.smt2                                      |   30.080s | 325.0MiB| timeout | 0 |  |  |
|scheduling/yn4_850.smt2                                      |   30.083s | 296.0MiB| timeout | 0 |  |  |
|scheduling/yn2_862.smt2                                      |   30.085s | 310.0MiB| timeout | 0 |  |  |
|scheduling/yn1_827.smt2                                      |   30.087s | 296.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-16.base.cvc.smt2                          |   30.092s | 538.0MiB| timeout | 0 |  |  |
|skdmxa/skdmxa-3x3-20.smt2                                    |   30.094s | 405.0MiB| timeout | 0 |  |  |
|scheduling/yn4_950.smt2                                      |   30.094s | 306.0MiB| timeout | 0 |  |  |
|scheduling/yn4_919.smt2                                      |   30.095s | 306.0MiB| timeout | 0 |  |  |
|scheduling/yn1_850.smt2                                      |   30.096s | 299.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-14.base.cvc.smt2                          |   30.096s | 494.0MiB| timeout | 0 |  |  |
|scheduling/yn3_860.smt2                                      |   30.098s | 306.0MiB| timeout | 0 |  |  |
|scheduling/yn1_887.smt2                                      |   30.101s | 308.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-17.base.cvc.smt2                          |   30.101s | 600.0MiB| timeout | 0 |  |  |
|scheduling/yn2_890.smt2                                      |   30.102s | 313.0MiB| timeout | 0 |  |  |
|scheduling/yn3_894.smt2                                      |   30.104s | 306.0MiB| timeout | 0 |  |  |
|scheduling/yn2_910.smt2                                      |   30.106s | 314.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-19.base.cvc.smt2                          |   30.109s | 675.0MiB| timeout | 0 |  |  |
|scheduling/swv13_3150.smt2                                   |   30.113s | 719.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-13.base.cvc.smt2                          |   30.113s | 475.0MiB| timeout | 0 |  |  |
|scheduling/swv12_2900.smt2                                   |   30.118s | 665.0MiB| timeout | 0 |  |  |
|scheduling/swv11_2992.smt2                                   |   30.122s | 638.0MiB| timeout | 0 |  |  |
|scheduling/swv12_2990.smt2                                   |   30.124s | 668.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-20.base.cvc.smt2                          |   30.124s | 735.0MiB| timeout | 0 |  |  |
|scheduling/swv12_3050.smt2                                   |   30.126s | 734.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-15.base.cvc.smt2                          |   30.126s | 511.0MiB| timeout | 0 |  |  |
|scheduling/swv12_3004.smt2                                   |   30.127s | 685.0MiB| timeout | 0 |  |  |
|scheduling/swv14_2905.smt2                                   |   30.127s | 633.0MiB| timeout | 0 |  |  |
|scheduling/swv11_2983.smt2                                   |   30.130s | 657.0MiB| timeout | 0 |  |  |
|scheduling/swv14_2895.smt2                                   |   30.130s | 663.0MiB| timeout | 0 |  |  |
|scheduling/swv13_3104.smt2                                   |   30.131s | 705.0MiB| timeout | 0 |  |  |
|scheduling/swv13_3000.smt2                                   |   30.132s | 700.0MiB| timeout | 0 |  |  |
|scheduling/swv14_3000.smt2                                   |   30.132s | 666.0MiB| timeout | 0 |  |  |
|scheduling/swv12_2972.smt2                                   |   30.139s | 700.0MiB| timeout | 0 |  |  |
|scheduling/swv14_2800.smt2                                   |   30.141s | 634.0MiB| timeout | 0 |  |  |
|skdmxa2/skdmxa-3x3-18.base.cvc.smt2                          |   30.141s | 642.0MiB| timeout | 0 |  |  |
|scheduling/swv11_3050.smt2                                   |   30.147s | 613.0MiB| timeout | 0 |  |  |
|scheduling/swv11_2900.smt2                                   |   30.148s | 613.0MiB| timeout | 0 |  |  |
|scheduling/swv11_2988.smt2                                   |   30.150s | 629.0MiB| timeout | 0 |  |  |
|scheduling/yn1_950.smt2                                      |   30.151s | 317.0MiB| timeout | 0 |  |  |
|scheduling/swv13_3200.smt2                                   |   30.157s | 714.0MiB| timeout | 0 |  |  |
|scheduling/swv14_2885.smt2                                   |   30.178s | 644.0MiB| timeout | 0 |  |  |