# . * SAT 94 * UNSAT 96 * TIMEOUT 65 * UNKNOWN 0 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/QF_RDL.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-QF_RDL.tar.zst-dow
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 4a90d3105054796562079406e125b9480ac3472b
Z3 branch: master
Z3 options: "-T:20 model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_RDL.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/QF_RDL/sal/fischer3-mutex-2.smt2 | 0.027s | 20.404MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-3.smt2 | 0.039s | 21.22MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-7.smt2 | 0.042s | 21.008MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-04.smt2 | 0.046s | 20.948MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-width-1.smt2 | 0.047s | 20.6MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-5.smt2 | 0.049s | 22.464MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb07_250.smt2 | 0.053s | 22.16MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-3.smt2 | 0.055s | 20.552MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/abz6_800.smt2 | 0.056s | 23.572MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-05.smt2 | 0.057s | 21.48MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking03.smt2 | 0.065s | 20.656MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/abz5_1000.smt2 | 0.070s | 23.384MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-03.smt2 | 0.070s | 21.152MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-width-2.smt2 | 0.071s | 21.068MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking16.smt2 | 0.086s | 23.032MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking10.smt2 | 0.087s | 22.192MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-2.smt2 | 0.092s | 20.884MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking18.smt2 | 0.093s | 23.216MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-matrix1x1.pddl.smt2 | 0.098s | 20.66MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-5.smt2 | 0.098s | 20.872MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-1.smt2 | 0.100s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-depth-3.smt2 | 0.104s | 23.3MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-4.smt2 | 0.104s | 20.684MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-4.smt2 | 0.107s | 21.756MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking21.smt2 | 0.109s | 23.712MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-3.smt2 | 0.109s | 21.12MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking05.smt2 | 0.111s | 21.128MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking17.smt2 | 0.113s | 23.268MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking04.smt2 | 0.114s | 21.292MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-4.smt2 | 0.114s | 21.224MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-1.smt2 | 0.117s | 20.376MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking01.smt2 | 0.119s | 20.364MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb07_330.smt2 | 0.124s | 22.884MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-2.smt2 | 0.124s | 20.628MiB| unsat | 0 | | | |non-incremental/QF_RDL/check/bignum_rdl1.smt2 | 0.125s | 19.852MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-5.smt2 | 0.125s | 21.7MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb05_700.smt2 | 0.126s | 23.5MiB| unsat | 0 | | | |non-incremental/QF_RDL/check/bignum_rdl2.smt2 | 0.127s | 19.852MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking02.smt2 | 0.127s | 20.636MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking07.smt2 | 0.135s | 21.388MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking06.smt2 | 0.136s | 21.128MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking08.smt2 | 0.137s | 21.644MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking09.smt2 | 0.142s | 21.684MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-08.smt2 | 0.142s | 22.004MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-07.smt2 | 0.147s | 21.768MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-9.smt2 | 0.150s | 21.74MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/abz5_1400.smt2 | 0.154s | 24.376MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-10.smt2 | 0.155s | 22.256MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking12.smt2 | 0.156s | 22.232MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-depth-2.smt2 | 0.156s | 21.0MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-1.smt2 | 0.156s | 20.056MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking11.smt2 | 0.160s | 22.236MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking14.smt2 | 0.161s | 22.676MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-11.smt2 | 0.161s | 22.484MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb02_700.smt2 | 0.166s | 22.628MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking19.smt2 | 0.168s | 23.304MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-10.smt2 | 0.168s | 22.024MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-6.smt2 | 0.169s | 20.868MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-06.smt2 | 0.172s | 21.548MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb08_700.smt2 | 0.173s | 23.604MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-7.smt2 | 0.177s | 22.18MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-6.smt2 | 0.179s | 22.868MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb10_800.smt2 | 0.180s | 23.736MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking20.smt2 | 0.180s | 23.496MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb07_550.smt2 | 0.186s | 24.876MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-8.smt2 | 0.186s | 21.252MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking13.smt2 | 0.187s | 22.476MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-6.smt2 | 0.198s | 21.98MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking15.smt2 | 0.201s | 22.756MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb02_800.smt2 | 0.202s | 23.704MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-09.smt2 | 0.209s | 22.424MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-8.smt2 | 0.214s | 22.748MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/abz6_1100.smt2 | 0.218s | 24.176MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb04_850.smt2 | 0.225s | 23.86MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking22.smt2 | 0.228s | 24.06MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-20.smt2 | 0.237s | 24.256MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb09_800.smt2 | 0.280s | 23.748MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa/skdmxa-3x3-5.smt2 | 0.286s | 34.712MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb06_900.smt2 | 0.324s | 24.136MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-9.smt2 | 0.328s | 23.42MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb09_1100.smt2 | 0.342s | 24.976MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-8.smt2 | 0.361s | 24.104MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-7.smt2 | 0.368s | 23.672MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/abz6_900.smt2 | 0.409s | 24.204MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb02_1000.smt2 | 0.419s | 24.492MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-13.smt2 | 0.424s | 22.688MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-12.smt2 | 0.429s | 22.428MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb05_1000.smt2 | 0.431s | 24.824MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-16.smt2 | 0.441s | 23.352MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb04_1200.smt2 | 0.451s | 25.156MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb03_850.smt2 | 0.466s | 24.212MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb04_950.smt2 | 0.484s | 24.72MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-30.smt2 | 0.519s | 26.692MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/abz6_1000.smt2 | 0.528s | 24.624MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-14.smt2 | 0.548s | 23.204MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-5.base.cvc.smt2 | 0.597s | 50.124MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb08_830.smt2 | 0.624s | 24.324MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/abz5_1300.smt2 | 0.625s | 25.008MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-40.smt2 | 0.630s | 28.252MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb05_800.smt2 | 0.632s | 24.2MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb01_900.smt2 | 0.668s | 24.612MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-15.smt2 | 0.675s | 23.456MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb02_900.smt2 | 0.684s | 25.216MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/abz6_943.smt2 | 0.760s | 24.48MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-width-3.smt2 | 0.809s | 24.512MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-6.base.cvc.smt2 | 0.823s | 56.06MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-17.smt2 | 0.826s | 24.036MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb03_1200.smt2 | 0.843s | 25.532MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-9.smt2 | 0.910s | 25.512MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-7.base.cvc.smt2 | 0.929s | 60.176MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-11.smt2 | 0.945s | 25.36MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-19.smt2 | 0.972s | 24.688MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-18.smt2 | 1.105s | 24.556MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-10.smt2 | 1.164s | 24.284MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb09_1000.smt2 | 1.229s | 25.744MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb10_1100.smt2 | 1.238s | 25.44MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb06_1200.smt2 | 1.256s | 26.12MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-9.base.cvc.smt2 | 1.265s | 87.664MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb07_430.smt2 | 1.286s | 25.6MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-12.smt2 | 1.309s | 25.076MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb04_1100.smt2 | 1.327s | 25.796MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-5.induction.cvc.smt2 | 1.333s | 66.848MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer3-mutex-20.smt2 | 1.337s | 25.184MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-6.induction.cvc.smt2 | 1.374s | 84.196MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-8.base.cvc.smt2 | 1.383s | 83.848MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb08_1000.smt2 | 1.436s | 26.248MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa/skdmxa-3x3-10.smt2 | 1.437s | 60.008MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb10_900.smt2 | 1.489s | 24.808MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-13.smt2 | 1.615s | 25.92MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/yn1_750.smt2 | 1.636s | 66.232MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-7.induction.cvc.smt2 | 1.647s | 87.92MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/yn3_750.smt2 | 1.678s | 65.484MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-depth-4.smt2 | 1.727s | 28.012MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb01_1200.smt2 | 1.753s | 26.144MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-9.induction.cvc.smt2 | 1.803s | 124.0MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/yn2_750.smt2 | 1.836s | 65.62MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-8.induction.cvc.smt2 | 2.276s | 107.0MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-10.smt2 | 2.606s | 27.884MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-10.induction.cvc.smt2 | 2.720s | 127.0MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb03_1100.smt2 | 2.850s | 26.364MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-11.smt2 | 2.920s | 27.472MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-60.smt2 | 2.944s | 48.696MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/abz7_500.smt2 | 2.972s | 49.548MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb09_934.smt2 | 3.062s | 26.268MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb09_900.smt2 | 3.089s | 25.864MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-11.induction.cvc.smt2 | 3.105s | 152.0MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb02_888.smt2 | 3.180s | 26.252MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/abz5_1200.smt2 | 3.216s | 25.708MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-12.induction.cvc.smt2 | 3.314s | 154.0MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-10.base.cvc.smt2 | 3.439s | 98.068MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-14.smt2 | 3.601s | 27.468MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-13.induction.cvc.smt2 | 3.742s | 184.0MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-16.smt2 | 3.815s | 27.428MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb10_1000.smt2 | 4.355s | 26.26MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-14.induction.cvc.smt2 | 4.612s | 184.0MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb06_1100.smt2 | 4.686s | 26.796MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb07_397.smt2 | 4.813s | 26.508MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-16.induction.cvc.smt2 | 4.882s | 239.0MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-80.smt2 | 4.962s | 44.848MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb05_900.smt2 | 5.513s | 26.904MiB| sat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-70.smt2 | 5.556s | 43.68MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-11.base.cvc.smt2 | 5.595s | 104.0MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb10_944.smt2 | 5.650s | 26.572MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-15.smt2 | 5.715s | 28.216MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-15.induction.cvc.smt2 | 5.790s | 223.0MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-12.smt2 | 5.840s | 29.028MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb04_1005.smt2 | 5.859s | 27.136MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-18.smt2 | 5.976s | 29.876MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb08_930.smt2 | 6.240s | 27.08MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-17.induction.cvc.smt2 | 6.294s | 250.0MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb03_950.smt2 | 6.474s | 26.764MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-17.smt2 | 6.753s | 29.388MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb01_1100.smt2 | 7.426s | 27.8MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb08_888.smt2 | 8.666s | 27.772MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-18.induction.cvc.smt2 | 8.935s | 275.0MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-19.smt2 | 9.113s | 30.524MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-13.base.cvc.smt2 | 9.121s | 117.0MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-14.smt2 | 9.591s | 30.992MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-90.smt2 | 9.998s | 47.62MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-19.induction.cvc.smt2 | 10.106s | 299.0MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/abz5_1234.smt2 | 10.827s | 28.1MiB| sat | 0 | | | |non-incremental/QF_RDL/scheduling/orb05_887.smt2 | 10.856s | 27.748MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-12.base.cvc.smt2 | 10.862s | 112.0MiB| unsat | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-13.smt2 | 12.816s | 32.38MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa/skdmxa-3x3-15.smt2 | 13.208s | 98.0MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-20.induction.cvc.smt2 | 13.807s | 371.0MiB| sat | 0 | | | |non-incremental/QF_RDL/sal/fischer6-mutex-20.smt2 | 15.760s | 32.036MiB| unsat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-14.base.cvc.smt2 | 16.253s | 125.0MiB| unsat | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-depth-5.smt2 | 19.349s | 46.672MiB| sat | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-15.base.cvc.smt2 | 19.442s | 140.0MiB| unsat | 0 | | | |non-incremental/QF_RDL/scheduling/orb06_1000.smt2 | 20.013s | 30.128MiB| timeout | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-15.smt2 | 20.030s | 34.524MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv14_2885.smt2 | 20.033s | 204.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv13_3104.smt2 | 20.033s | 206.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn2_910.smt2 | 20.034s | 88.78MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn3_828.smt2 | 20.039s | 81.42MiB| timeout | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-18.smt2 | 20.039s | 36.824MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn4_1000.smt2 | 20.044s | 93.264MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv12_2972.smt2 | 20.052s | 210.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv12_3050.smt2 | 20.056s | 225.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/orb01_1000.smt2 | 20.075s | 28.944MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/abz7_670.smt2 | 20.077s | 72.772MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/orb01_1059.smt2 | 20.079s | 29.584MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn1_850.smt2 | 20.082s | 82.68MiB| timeout | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-16.smt2 | 20.084s | 36.668MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn3_950.smt2 | 20.089s | 90.004MiB| timeout | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-20.smt2 | 20.089s | 36.932MiB| timeout | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-18.base.cvc.smt2 | 20.090s | 193.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/orb06_1010.smt2 | 20.091s | 29.66MiB| timeout | 0 | | | |non-incremental/QF_RDL/skdmxa/skdmxa-3x3-20.smt2 | 20.092s | 126.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn3_894.smt2 | 20.092s | 88.088MiB| timeout | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-17.base.cvc.smt2 | 20.094s | 192.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn4_850.smt2 | 20.095s | 78.372MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv12_2990.smt2 | 20.096s | 221.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/orb03_1005.smt2 | 20.097s | 29.324MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn1_887.smt2 | 20.097s | 85.788MiB| timeout | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-17.smt2 | 20.099s | 35.988MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn1_827.smt2 | 20.100s | 81.008MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv12_3004.smt2 | 20.101s | 206.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/abz7_667.smt2 | 20.103s | 71.916MiB| timeout | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-width-5.smt2 | 20.103s | 80.556MiB| timeout | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-width-6.smt2 | 20.103s | 143.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/sal/fischer9-mutex-19.smt2 | 20.104s | 35.968MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/abz7_800.smt2 | 20.107s | 76.264MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn4_919.smt2 | 20.109s | 87.268MiB| timeout | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-20.base.cvc.smt2 | 20.109s | 225.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn4_950.smt2 | 20.111s | 89.46MiB| timeout | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-width-4.smt2 | 20.114s | 46.772MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv11_2992.smt2 | 20.115s | 208.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/abz7_700.smt2 | 20.117s | 72.828MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn2_862.smt2 | 20.117s | 84.78MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/abz7_691.smt2 | 20.117s | 73.04MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn4_969.smt2 | 20.120s | 90.828MiB| timeout | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-depth-7.smt2 | 20.121s | 89.02MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv12_2900.smt2 | 20.122s | 210.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-depth-6.smt2 | 20.122s | 56.372MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv14_2800.smt2 | 20.123s | 206.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv14_2895.smt2 | 20.124s | 208.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-19.base.cvc.smt2 | 20.124s | 229.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv11_2988.smt2 | 20.130s | 226.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn2_950.smt2 | 20.131s | 92.736MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv11_3050.smt2 | 20.134s | 203.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv14_2905.smt2 | 20.135s | 212.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/SMT-Temporal-Planning-Benchmarks/tempo-matrix2x2.pddl.smt2 | 20.135s | 129.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv13_3200.smt2 | 20.139s | 216.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv13_3000.smt2 | 20.140s | 219.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn2_890.smt2 | 20.142s | 89.152MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/abz7_600.smt2 | 20.144s | 66.668MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn1_950.smt2 | 20.144s | 89.768MiB| timeout | 0 | | | |non-incremental/QF_RDL/skdmxa2/skdmxa-3x3-16.base.cvc.smt2 | 20.145s | 177.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/yn3_860.smt2 | 20.151s | 86.68MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv11_2900.smt2 | 20.155s | 211.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv13_3150.smt2 | 20.157s | 219.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv11_2983.smt2 | 20.162s | 200.0MiB| timeout | 0 | | | |non-incremental/QF_RDL/scheduling/swv14_3000.smt2 | 20.164s | 208.0MiB| timeout | 0 | | |