# .

* SAT 390
* UNSAT 399
* TIMEOUT 11
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-2-QF_LIA_hard-timeout10min-bb2
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: c383004968f5bf66a9668a7ae254c83d45ac3afe
Z3 branch: fmcad26_artifact
Z3 options: "-T:1200 -v:0 smt.threads=2 tactic.default_tactic=smt smt.auto_config=false smt_parallel.num_global_bb_batch_threads=2"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_LIA.tar.zst?download=1
Z3 commit message: add ablate_backtracking experiment

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1550.smt2 |    0.493s | 149.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1567.smt2 |    0.553s | 151.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1533.smt2 |    0.563s | 148.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1607.smt2 |    0.566s | 153.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1575.smt2 |    0.571s | 151.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1565.smt2 |    0.691s | 151.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1591.smt2 |    0.700s | 152.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1617.smt2 |    0.756s | 154.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-14.smt2 |    1.516s | 449.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-03.smt2 |    1.749s | 634.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-526410.smt2  |    1.830s | 347.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-10.smt2 |    1.836s | 809.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-02.smt2 |    1.891s | 960.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-15.smt2 |    1.921s | 957.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-09.smt2 |    1.933s | 958.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-01.smt2 |    1.950s | 966.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-08.smt2 |    2.134s | 428.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-14.smt2 |    2.274s | 441.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-08.smt2 |    2.305s | 431.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-13.smt2 |    2.519s | 937.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-04.smt2 |    2.551s | 934.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-04.smt2 |    2.591s | 937.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-06.smt2 |    2.598s | 941.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-14.smt2 |    2.608s | 937.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-15.smt2 |    2.641s | 935.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-05.smt2 |    2.656s | 952.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-11.smt2 |    2.696s | 663.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-08.smt2 |    2.734s | 941.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-15.smt2 |    2.745s | 634.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-12.smt2 |    2.747s | 944.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-10.smt2 |    2.864s | 1379.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-11.smt2 |    2.920s | 946.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-03.smt2 |    2.987s | 1771.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-07.smt2 |    3.040s | 941.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-06.smt2 |    3.188s | 935.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-12.smt2 |    3.199s | 1855.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-07.smt2 |    3.210s | 1978.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-10.smt2 |    3.223s | 1856.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-05.smt2 |    3.224s | 620.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-06.smt2 |    3.239s | 621.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-01.smt2 |    3.254s | 624.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-00.smt2 |    3.262s | 935.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-12.smt2 |    3.263s | 623.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-00.smt2 |    3.299s | 620.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-11.smt2 |    3.314s | 620.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-00.smt2 |    3.317s | 1926.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-10.smt2 |    3.404s | 620.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-03.smt2 |    3.425s | 1925.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-09.smt2 |    3.437s | 1973.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-08.smt2 |    3.438s | 623.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-14.smt2 |    3.478s | 623.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-07.smt2 |    3.579s | 620.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-03.smt2 |    3.690s | 1120.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-13.smt2 |    3.764s | 1920.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-02.smt2 |    3.823s | 2022.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-13.smt2 |    3.840s | 2054.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r1000w0010/RC-08.smt2 |    3.855s | 743.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-06.smt2 |    3.856s | 2073.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-09.smt2 |    3.963s | 1918.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-05.smt2 |    4.000s | 1991.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-00.smt2 |    4.036s | 2039.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1007795.smt2 |    4.171s | 612.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-14.smt2 |    4.287s | 2055.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-413904.smt2 |    4.311s | 404.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-343499.smt2 |    4.571s | 369.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-04.smt2 |    4.764s | 2372.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-13.smt2 |    4.911s | 2938.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-00.smt2 |    4.927s | 2941.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-03.smt2 |    4.972s | 2727.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-06.smt2 |    5.059s | 2938.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-08.smt2 |    5.118s | 2937.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-10.smt2 |    5.142s | 2936.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-14.smt2 |    5.267s | 2937.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-15.smt2 |    5.286s | 2938.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-11.smt2 |    5.333s | 2938.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-02.smt2 |    5.345s | 2998.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-09.smt2 |    5.347s | 2940.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-01.smt2 |    5.493s | 2938.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-05.smt2 |    5.737s | 2938.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-13.smt2 |    5.780s | 2915.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-02.smt2 |    6.144s | 2916.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-09.smt2 |    6.206s | 2917.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-928134.smt2  |    6.317s | 731.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-12.smt2 |    7.160s | 5770.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-415996.smt2  |    7.427s | 499.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-01.smt2 |    7.578s | 2838.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1148089.smt2 |    7.646s | 826.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-04.smt2 |    7.807s | 3636.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-329386.smt2 |    7.930s | 379.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-392137.smt2  |    8.543s | 465.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-07.smt2 |    8.574s | 6080.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1205831.smt2 |    8.780s | 981.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-38.smt2 |    8.878s | 383.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-37.smt2 |    9.078s | 316.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-42.smt2 |    9.530s | 272.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-379665.smt2  |    9.788s | 472.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-39.smt2 |   10.086s | 381.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-40.smt2 |   10.474s | 401.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-50.smt2 |   11.401s | 416.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1015084.smt2 |   11.681s | 1052.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-917322.smt2 |   12.544s | 878.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-48.smt2 |   12.610s | 396.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-45.smt2 |   12.662s | 331.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-49.smt2 |   13.145s | 474.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-864173.smt2  |   13.227s | 1064.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-38.smt2 |   13.380s | 473.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-38.smt2 |   13.831s | 349.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-38.smt2 |   14.388s | 464.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-47.smt2 |   14.395s | 165.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-794687.smt2 |   14.506s | 916.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-38.smt2 |   14.543s | 391.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-47.smt2 |   14.842s | 165.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-19-50.smt2 |   14.853s | 466.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-16-49.smt2 |   14.998s | 570.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-200.smt2 |   15.377s | 638.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-199.smt2 |   15.528s | 596.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-39.smt2 |   15.719s | 360.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-916807.smt2 |   15.772s | 998.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-39.smt2 |   15.895s | 430.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-37-50.smt2 |   15.940s | 536.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-41.smt2 |   15.959s | 368.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-23-50.smt2 |   16.301s | 562.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-49.smt2 |   16.370s | 482.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-47.smt2 |   16.414s | 521.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-39.smt2 |   16.535s | 490.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-42.smt2 |   16.832s | 343.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-39.smt2 |   16.867s | 914.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-8-49.smt2 |   17.074s | 529.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-48.smt2 |   17.236s | 167.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-43.smt2 |   17.627s | 450.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-13-50.smt2 |   17.737s | 576.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-24-49.smt2 |   17.789s | 515.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-199.smt2 |   17.952s | 430.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1192684.smt2 |   18.010s | 1133.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-49.smt2 |   18.013s | 447.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-197.smt2 |   18.057s | 504.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-41.smt2 |   18.062s | 467.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-32-50.smt2 |   18.155s | 542.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-50.smt2 |   18.293s | 518.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-48.smt2 |   18.421s | 443.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-247831.smt2 |   18.445s | 341.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-48-50.smt2 |   18.481s | 497.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-60-50.smt2 |   18.497s | 467.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-49.smt2 |   18.776s | 446.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-49.smt2 |   18.945s | 521.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-50.smt2 |   19.116s | 572.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-57-49.smt2 |   19.315s | 490.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-49.smt2 |   19.488s | 460.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1275621.smt2 |   19.612s | 1493.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-42-50.smt2 |   19.778s | 470.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-48.smt2 |   19.783s | 490.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-527358.smt2 |   19.855s | 737.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-196.smt2 |   20.098s | 671.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-40.smt2 |   20.717s | 699.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1185949.smt2 |   20.736s | 1226.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-64-50.smt2 |   20.773s | 470.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-46.smt2 |   20.908s | 483.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-65-50.smt2 |   21.026s | 477.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-40.smt2 |   21.259s | 635.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-46.smt2 |   21.364s | 482.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-41.smt2 |   21.407s | 538.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-67-50.smt2 |   21.418s | 480.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-46.smt2 |   21.669s | 492.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-41.smt2 |   21.718s | 613.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-59-50.smt2 |   21.814s | 476.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-48.smt2 |   21.851s | 458.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-50.smt2 |   21.868s | 513.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-50.smt2 |   22.128s | 511.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-42.smt2 |   22.375s | 661.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-41.smt2 |   22.379s | 491.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-49.smt2 |   22.708s | 462.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-70-50.smt2 |   22.759s | 605.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-48.smt2 |   22.883s | 484.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-46.smt2 |   22.897s | 539.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-40-50.smt2 |   23.042s | 473.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-50.smt2 |   23.048s | 491.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1121941.smt2 |   23.159s | 1380.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-46.smt2 |   23.159s | 403.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1317511.smt2 |   23.215s | 1456.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-49.smt2 |   23.299s | 511.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-40.smt2 |   23.394s | 531.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-49.smt2 |   23.640s | 473.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-47.smt2 |   23.651s | 494.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-196.smt2 |   23.706s | 566.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-68-50.smt2 |   23.717s | 510.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-77-50.smt2 |   23.811s | 490.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-49.smt2 |   23.835s | 231.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-47.smt2 |   23.848s | 516.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-47.smt2 |   23.850s | 542.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-49.smt2 |   23.881s | 473.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-13-50.smt2 |   23.893s | 460.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-44.smt2 |   23.979s | 499.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-41.smt2 |   23.996s | 486.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-47.smt2 |   24.051s | 595.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-44.smt2 |   24.098s | 655.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-198.smt2 |   24.220s | 679.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-19-49.smt2 |   24.284s | 548.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-47.smt2 |   24.345s | 511.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-50.smt2 |   24.350s | 516.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-46.smt2 |   24.618s | 580.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-76-50.smt2 |   24.741s | 468.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-44.smt2 |   24.897s | 453.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-69-50.smt2 |   24.902s | 508.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-37-47.smt2 |   25.210s | 372.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-47.smt2 |   25.214s | 507.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-58-50.smt2 |   25.344s | 470.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-44.smt2 |   25.433s | 376.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-689472.smt2  |   25.485s | 1074.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-50.smt2 |   25.560s | 470.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-48.smt2 |   25.630s | 514.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-198.smt2 |   25.707s | 436.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-41.smt2 |   25.787s | 507.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-48.smt2 |   25.880s | 563.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-45.smt2 |   26.150s | 690.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-48.smt2 |   26.289s | 523.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-49.smt2 |   26.304s | 525.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-47.smt2 |   26.398s | 580.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-48.smt2 |   26.555s | 534.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-758897.smt2 |   26.556s | 1031.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-44.smt2 |   26.601s | 618.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-49.smt2 |   26.922s | 575.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-42.smt2 |   27.512s | 892.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-48.smt2 |   27.566s | 531.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-44.smt2 |   27.566s | 773.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-42.smt2 |   27.650s | 351.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-42.smt2 |   27.802s | 629.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-50.smt2 |   27.830s | 512.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-44.smt2 |   28.029s | 426.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-46.smt2 |   28.136s | 723.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-200.smt2 |   28.165s | 508.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-48.smt2 |   28.393s | 529.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-45.smt2 |   28.533s | 510.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-42.smt2 |   28.773s | 632.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-43.smt2 |   28.810s | 494.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-47.smt2 |   28.819s | 472.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-42.smt2 |   28.921s | 525.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-47.smt2 |   28.953s | 516.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-49.smt2 |   29.124s | 659.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-39-50.smt2 |   29.319s | 509.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1270163.smt2 |   29.447s | 1858.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-17-47.smt2 |   29.493s | 511.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-45.smt2 |   29.545s | 628.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-45.smt2 |   29.685s | 580.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1317230.smt2 |   29.719s | 1769.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-57-50.smt2 |   30.135s | 554.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-42.smt2 |   30.137s | 676.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-50.smt2 |   30.152s | 642.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-48.smt2 |   30.173s | 714.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-481231.smt2  |   30.185s | 748.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-42.smt2 |   30.267s | 746.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-42.smt2 |   30.341s | 648.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-48.smt2 |   30.387s | 570.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-46.smt2 |   30.416s | 1088.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-17-47.smt2 |   30.465s | 449.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-43.smt2 |   30.480s | 780.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-63-50.smt2 |   30.764s | 466.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-49.smt2 |   30.815s | 563.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-45.smt2 |   30.851s | 735.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-48.smt2 |   30.890s | 685.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-48.smt2 |   30.927s | 762.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-49.smt2 |   30.953s | 549.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-14-49.smt2 |   31.052s | 460.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-46.smt2 |   31.058s | 742.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-48.smt2 |   31.150s | 715.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-48.smt2 |   31.211s | 240.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-906586.smt2 |   31.225s | 1351.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-43.smt2 |   31.297s | 514.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-47.smt2 |   31.358s | 639.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-41.smt2 |   31.696s | 403.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-45.smt2 |   31.788s | 271.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-43.smt2 |   31.885s | 731.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-50.smt2 |   32.009s | 553.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-46.smt2 |   32.176s | 742.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-48.smt2 |   32.236s | 750.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-42.smt2 |   32.342s | 356.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-43.smt2 |   32.362s | 658.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-50.smt2 |   32.475s | 573.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-43.smt2 |   32.489s | 768.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER10-13-fair.smt2        |   32.586s | 167.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-46.smt2 |   32.601s | 935.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-44.smt2 |   32.657s | 636.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-42.smt2 |   32.715s | 1166.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-44.smt2 |   32.804s | 496.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-43.smt2 |   32.939s | 703.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-46.smt2 |   32.952s | 814.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-48.smt2 |   32.970s | 765.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-43.smt2 |   33.015s | 355.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-46.smt2 |   33.101s | 432.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-47.smt2 |   33.181s | 651.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-47.smt2 |   33.195s | 895.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-46.smt2 |   33.206s | 709.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-47.smt2 |   33.220s | 910.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-50.smt2 |   33.673s | 481.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-45.smt2 |   33.703s | 514.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-45.smt2 |   34.155s | 830.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-49.smt2 |   34.226s | 569.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-47.smt2 |   34.633s | 898.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-46.smt2 |   34.770s | 416.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-49.smt2 |   34.986s | 492.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-49.smt2 |   35.277s | 667.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-48.smt2 |   35.301s | 825.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-705295.smt2 |   35.420s | 1090.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-200.smt2 |   35.439s | 450.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-43.smt2 |   35.483s | 777.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-48.smt2 |   35.486s | 281.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-48.smt2 |   36.039s | 920.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-48.smt2 |   36.039s | 581.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-48.smt2 |   36.195s | 911.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-46.smt2 |   36.216s | 841.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-48.smt2 |   36.249s | 510.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-50.smt2 |   36.477s | 695.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-46.smt2 |   36.614s | 532.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-46.smt2 |   36.632s | 671.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-49.smt2 |   36.672s | 827.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-50.smt2 |   36.701s | 472.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-46.smt2 |   37.003s | 679.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-44.smt2 |   37.013s | 847.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-50.smt2 |   37.102s | 512.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-50.smt2 |   37.132s | 483.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-50.smt2 |   37.142s | 523.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-47.smt2 |   37.270s | 567.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-50.smt2 |   37.350s | 850.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-46.smt2 |   37.365s | 649.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-49.smt2 |   37.381s | 787.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-49.smt2 |   37.672s | 569.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-50.smt2 |   37.780s | 657.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-45.smt2 |   37.848s | 397.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-44.smt2 |   38.412s | 961.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-50.smt2 |   38.537s | 302.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-45.smt2 |   38.575s | 785.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-44.smt2 |   38.685s | 1001.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-49.smt2 |   39.260s | 658.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-46.smt2 |   39.279s | 505.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-47.smt2 |   39.360s | 977.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-47.smt2 |   39.423s | 723.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-49.smt2 |   39.460s | 584.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-48.smt2 |   39.526s | 448.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-43.smt2 |   39.763s | 409.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-47.smt2 |   39.860s | 416.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-47.smt2 |   39.936s | 778.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-48.smt2 |   40.538s | 495.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-45.smt2 |   40.574s | 893.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-49.smt2 |   40.731s | 870.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-48.smt2 |   40.789s | 758.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-48.smt2 |   40.872s | 707.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-49.smt2 |   41.460s | 717.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-50.smt2 |   41.769s | 764.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-197.smt2 |   41.796s | 530.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-47.smt2 |   42.124s | 674.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-50.smt2 |   42.426s | 833.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-47.smt2 |   42.490s | 783.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-199.smt2 |   42.629s | 444.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-46.smt2 |   42.778s | 454.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-45.smt2 |   43.147s | 468.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-901628.smt2  |   43.325s | 1501.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-45.smt2 |   43.436s | 1016.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-48.smt2 |   43.551s | 1032.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-50.smt2 |   43.609s | 973.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-49.smt2 |   43.620s | 1147.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-48.smt2 |   43.736s | 1157.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-50.smt2 |   43.839s | 737.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-44.smt2 |   43.879s | 533.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-47.smt2 |   43.935s | 715.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-48.smt2 |   44.188s | 939.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-46.smt2 |   44.385s | 1095.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-45.smt2 |   44.525s | 839.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-44.smt2 |   44.942s | 983.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-50.smt2 |   45.117s | 517.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-916576.smt2  |   45.185s | 1372.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-49.smt2 |   45.187s | 424.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-48.smt2 |   45.189s | 949.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-46.smt2 |   45.334s | 1202.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-48.smt2 |   45.569s | 733.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-46.smt2 |   45.797s | 1208.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-50.smt2 |   45.966s | 424.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-198.smt2 |   46.621s | 473.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-46.smt2 |   46.778s | 703.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-45.smt2 |   47.225s | 1013.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-43.smt2 |   47.237s | 1136.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-50.smt2 |   47.310s | 357.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-50.smt2 |   47.620s | 811.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-48.smt2 |   47.878s | 1045.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-48.smt2 |   48.358s | 823.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-47.smt2 |   48.400s | 603.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-47.smt2 |   48.465s | 805.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-49.smt2 |   48.501s | 592.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-48.smt2 |   48.670s | 865.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-48.smt2 |   48.750s | 828.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-48.smt2 |   48.844s | 1028.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-196.smt2 |   48.859s | 397.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-50.smt2 |   48.946s | 926.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-48.smt2 |   49.177s | 884.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-48.smt2 |   50.078s | 999.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-49.smt2 |   50.120s | 645.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-50.smt2 |   50.189s | 628.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-49.smt2 |   50.220s | 627.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-50.smt2 |   50.591s | 975.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-47.smt2 |   50.724s | 1125.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-48.smt2 |   50.936s | 1215.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-48.smt2 |   50.980s | 1049.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-41-50.smt2 |   51.047s | 759.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-49.smt2 |   51.049s | 341.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-46.smt2 |   51.173s | 1240.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-49.smt2 |   51.342s | 1100.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-49.smt2 |   51.723s | 606.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-47.smt2 |   52.111s | 598.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-48.smt2 |   52.243s | 941.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-46.smt2 |   52.309s | 791.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-48.smt2 |   52.425s | 849.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-48.smt2 |   52.442s | 1085.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-49.smt2 |   52.527s | 859.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-45.smt2 |   52.696s | 576.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-47.smt2 |   52.938s | 1055.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-49.smt2 |   53.086s | 780.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-46.smt2 |   53.266s | 818.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-49.smt2 |   53.505s | 1054.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-48.smt2 |   53.586s | 867.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-50.smt2 |   53.747s | 807.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-48.smt2 |   53.839s | 781.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-50.smt2 |   53.895s | 626.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-48.smt2 |   53.923s | 1053.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-46.smt2 |   54.037s | 1172.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-46.smt2 |   54.147s | 848.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-47.smt2 |   54.178s | 512.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-47.smt2 |   54.210s | 592.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-47.smt2 |   54.330s | 1067.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-47.smt2 |   54.580s | 862.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-46.smt2 |   54.683s | 697.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-48.smt2 |   54.902s | 1122.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-50.smt2 |   55.121s | 796.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-46.smt2 |   55.219s | 665.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1268455.smt2 |   55.276s | 1662.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-48.smt2 |   55.495s | 728.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-46.smt2 |   55.766s | 1583.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-49.smt2 |   55.895s | 1079.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-49.smt2 |   56.045s | 690.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-47.smt2 |   56.463s | 1310.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-49.smt2 |   56.704s | 667.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-46.smt2 |   56.981s | 736.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-46.smt2 |   57.210s | 1073.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-48.smt2 |   57.742s | 942.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-50.smt2 |   58.379s | 924.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-49.smt2 |   58.394s | 1102.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-50.smt2 |   58.583s | 719.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-50.smt2 |   58.726s | 1081.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-49.smt2 |   59.027s | 701.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-50.smt2 |   59.240s | 740.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-50.smt2 |   60.172s | 605.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-48.smt2 |   60.248s | 1214.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-48.smt2 |   60.286s | 1039.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-48.smt2 |   60.517s | 1080.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-49.smt2 |   60.620s | 1144.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-50.smt2 |   60.652s | 1161.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-49.smt2 |   60.823s | 571.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-47.smt2 |   61.322s | 1496.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-47.smt2 |   61.520s | 610.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-48.smt2 |   61.577s | 1246.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-408585.smt2  |   61.885s | 695.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-48.smt2 |   62.093s | 833.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-50.smt2 |   62.528s | 1046.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-48.smt2 |   62.728s | 691.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-50.smt2 |   62.831s | 1205.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-518109.smt2  |   63.419s | 787.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-49.smt2 |   64.257s | 1187.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-49.smt2 |   64.619s | 1129.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1360077.smt2 |   64.735s | 2237.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-495717.smt2 |   65.069s | 853.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-48.smt2 |   67.249s | 983.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-48.smt2 |   67.376s | 1079.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-49.smt2 |   67.481s | 1248.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-46.smt2 |   67.775s | 1631.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-21-40.smt2 |   67.838s | 722.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-50.smt2 |   68.575s | 1153.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-49.smt2 |   68.820s | 1417.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-50.smt2 |   69.743s | 589.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-48.smt2 |   70.067s | 1069.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-48.smt2 |   70.433s | 748.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-50.smt2 |   71.069s | 1086.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-31-42.smt2 |   71.952s | 854.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-48.smt2 |   72.158s | 1255.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-50.smt2 |   72.836s | 871.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-50.smt2 |   73.028s | 1034.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-48.smt2 |   73.275s | 1241.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-47.smt2 |   73.868s | 725.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-48.smt2 |   74.015s | 1023.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-49.smt2 |   74.095s | 1257.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-46.smt2 |   74.471s | 720.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-50.smt2 |   74.853s | 1413.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-48.smt2 |   74.998s | 960.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-46.smt2 |   75.152s | 1256.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-48.smt2 |   75.257s | 702.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-48.smt2 |   76.600s | 1213.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-50.smt2 |   76.999s | 733.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-47.smt2 |   77.137s | 619.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1361831.smt2 |   77.233s | 2048.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-49.smt2 |   77.812s | 626.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-49.smt2 |   77.832s | 1678.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-50.smt2 |   78.216s | 1882.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-48.smt2 |   79.610s | 1112.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-50.smt2 |   79.703s | 1577.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-48.smt2 |   80.446s | 998.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-47.smt2 |   80.637s | 883.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-283008.smt2 |   80.925s | 404.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-23-41.smt2 |   81.446s | 668.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-48.smt2 |   81.543s | 1158.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-46.smt2 |   81.887s | 705.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-48.smt2 |   81.978s | 905.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-50.smt2 |   82.181s | 1110.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-47.smt2 |   82.341s | 1573.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-46.smt2 |   82.572s | 1656.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-50.smt2 |   82.634s | 631.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-50.smt2 |   83.401s | 658.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-46.smt2 |   83.752s | 469.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-49.smt2 |   84.284s | 1664.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-50.smt2 |   84.343s | 872.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER10-14-fair.smt2        |   84.492s | 173.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-47.smt2 |   84.612s | 576.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-46.smt2 |   85.062s | 1461.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1072007.smt2 |   85.135s | 2003.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-49.smt2 |   85.252s | 820.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER11-14-fair.smt2        |   85.910s | 181.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-49.smt2 |   87.098s | 971.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-50.smt2 |   87.428s | 861.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-49.smt2 |   87.472s | 1187.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-49.smt2 |   87.985s | 1038.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-45.smt2 |   88.836s | 875.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-269353.smt2 |   89.371s | 389.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-46.smt2 |   89.960s | 1322.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-48.smt2 |   90.060s | 723.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-48.smt2 |   90.206s | 1077.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-50.smt2 |   90.621s | 1764.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-50.smt2 |   90.698s | 1781.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-46.smt2 |   91.660s | 620.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-46.smt2 |   92.748s | 582.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-48.smt2 |   92.835s | 664.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-50.smt2 |   93.094s | 1391.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-49.smt2 |   94.098s | 1961.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-50.smt2 |   95.796s | 870.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-46.smt2 |   97.484s | 1300.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-48.smt2 |   97.616s | 861.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-49.smt2 |   97.817s | 996.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-50.smt2 |   98.095s | 1242.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-50.smt2 |   99.004s | 546.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-47.smt2 |  100.227s | 1010.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-50.smt2 |  101.229s | 1565.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-49.smt2 |  101.634s | 1531.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-49.smt2 |  101.780s | 1037.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-47.smt2 |  102.549s | 727.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-50.smt2 |  103.096s | 1383.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-46.smt2 |  103.101s | 731.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-47.smt2 |  104.159s | 755.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-47.smt2 |  104.189s | 1024.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-47.smt2 |  104.866s | 583.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-50.smt2 |  105.222s | 1912.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-46.smt2 |  105.831s | 611.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-47.smt2 |  107.547s | 1534.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-48.smt2 |  107.584s | 1007.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-47.smt2 |  108.204s | 878.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-49.smt2 |  108.648s | 853.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-48.smt2 |  110.371s | 1549.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-47.smt2 |  112.027s | 731.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-46.smt2 |  112.146s | 1272.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-26-43.smt2 |  112.433s | 854.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-49.smt2 |  112.476s | 792.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-50.smt2 |  113.770s | 912.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-47.smt2 |  114.224s | 1503.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-46.smt2 |  114.647s | 618.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-44.smt2 |  115.712s | 1787.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-47.smt2 |  117.021s | 670.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-47.smt2 |  117.093s | 759.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-46.smt2 |  117.245s | 1148.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-47.smt2 |  118.093s | 1563.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1265513.smt2 |  119.422s | 2655.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-48.smt2 |  120.990s | 785.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-50.smt2 |  121.087s | 1231.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-50.smt2 |  121.339s | 961.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-50.smt2 |  121.761s | 892.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-47.smt2 |  123.882s | 1334.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-46.smt2 |  124.182s | 1143.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-50.smt2 |  124.381s | 863.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-48.smt2 |  126.348s | 698.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-47.smt2 |  126.665s | 1489.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-47.smt2 |  127.742s | 1248.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-478122.smt2  |  128.562s | 933.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-48.smt2 |  128.734s | 1770.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-46.smt2 |  129.405s | 967.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-48.smt2 |  129.724s | 1044.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-47.smt2 |  129.945s | 914.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-46.smt2 |  131.014s | 844.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-46.smt2 |  131.475s | 956.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-46.smt2 |  132.157s | 1228.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-50.smt2 |  134.398s | 903.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-46.smt2 |  135.325s | 1322.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-46.smt2 |  135.444s | 1337.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-46.smt2 |  138.447s | 1795.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-49.smt2 |  139.476s | 1117.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-48.smt2 |  141.823s | 750.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-46.smt2 |  144.162s | 874.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-47.smt2 |  146.059s | 954.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-47.smt2 |  147.068s | 1310.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-267105.smt2  |  147.571s | 445.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-46.smt2 |  147.654s | 727.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-46.smt2 |  147.705s | 883.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-46.smt2 |  150.085s | 799.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-47.smt2 |  152.073s | 1430.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-47.smt2 |  152.526s | 1284.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-63-50.smt2 |  153.470s | 1162.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-47.smt2 |  154.173s | 1142.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-50.smt2 |  155.651s | 881.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-48.smt2 |  157.167s | 972.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-50.smt2 |  158.909s | 631.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-47.smt2 |  160.209s | 958.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-47.smt2 |  161.006s | 866.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-48.smt2 |  163.089s | 827.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-618384.smt2  |  163.164s | 1425.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-48.smt2 |  163.672s | 683.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-46.smt2 |  167.060s | 1718.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-47.smt2 |  167.570s | 1488.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-47.smt2 |  169.113s | 575.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-47.smt2 |  171.416s | 785.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-46.smt2 |  171.978s | 823.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-47.smt2 |  174.606s | 1342.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1452366.smt2 |  175.796s | 3295.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-46.smt2 |  176.354s | 710.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1365816.smt2 |  177.817s | 3455.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-46.smt2 |  178.226s | 644.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-47.smt2 |  179.120s | 1331.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-50.smt2 |  179.127s | 1010.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-762853.smt2 |  179.525s | 1728.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-46.smt2 |  183.564s | 1359.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-49.smt2 |  184.860s | 2143.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-46.smt2 |  186.209s | 1081.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-48.smt2 |  187.039s | 1107.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-48.smt2 |  187.939s | 1035.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1138192.smt2 |  188.560s | 2599.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-49.smt2 |  189.958s | 975.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-46.smt2 |  190.296s | 881.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-49.smt2 |  192.441s | 1874.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-47.smt2 |  192.850s | 1473.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-48.smt2 |  195.394s | 1509.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-50.smt2 |  195.556s | 1242.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-47.smt2 |  195.756s | 2078.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-47.smt2 |  196.025s | 668.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-47.smt2 |  196.997s | 1215.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1262176.smt2 |  197.160s | 3238.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-47.smt2 |  197.252s | 793.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-49.smt2 |  199.021s | 726.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-46.smt2 |  199.188s | 801.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-49.smt2 |  199.499s | 1063.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-47.smt2 |  199.665s | 860.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-46.smt2 |  201.243s | 739.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-48.smt2 |  202.697s | 902.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-50.smt2 |  202.804s | 2007.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-47.smt2 |  204.137s | 1014.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-48.smt2 |  207.473s | 1320.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-48.smt2 |  207.918s | 1852.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-50.smt2 |  208.501s | 1299.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-50.smt2 |  212.289s | 1146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-49.smt2 |  214.505s | 862.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-50.smt2 |  214.981s | 1115.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-46.smt2 |  215.775s | 1307.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-47.smt2 |  216.764s | 911.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-48.smt2 |  217.851s | 842.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-48.smt2 |  218.527s | 1393.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-46.smt2 |  218.855s | 1538.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-49.smt2 |  223.270s | 1118.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-46.smt2 |  225.716s | 972.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-49.smt2 |  226.033s | 1513.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-49.smt2 |  226.305s | 1131.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-49.smt2 |  227.942s | 1166.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-50.smt2 |  227.960s | 1555.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-49.smt2 |  229.132s | 1277.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-48.smt2 |  229.586s | 1152.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-49.smt2 |  231.399s | 1062.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-46.smt2 |  231.419s | 809.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-46.smt2 |  232.051s | 983.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-49.smt2 |  232.595s | 915.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-49.smt2 |  232.935s | 630.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-47.smt2 |  233.014s | 1024.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-49.smt2 |  235.701s | 861.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-49.smt2 |  236.540s | 957.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-50.smt2 |  237.733s | 791.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-47.smt2 |  241.908s | 890.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-50.smt2 |  243.345s | 1146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-49.smt2 |  244.005s | 1479.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-47.smt2 |  245.250s | 850.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-928960.smt2  |  246.095s | 1810.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-47.smt2 |  246.116s | 1581.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-48.smt2 |  247.778s | 1137.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-46.smt2 |  249.779s | 2266.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-49.smt2 |  251.706s | 1006.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-49.smt2 |  254.119s | 949.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-46.smt2 |  255.034s | 675.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-49.smt2 |  256.770s | 1389.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-49.smt2 |  256.826s | 891.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-48.smt2 |  256.878s | 1813.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-49.smt2 |  262.339s | 1063.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-49.smt2 |  265.945s | 1066.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-48.smt2 |  268.207s | 1622.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-47.smt2 |  270.258s | 767.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-47.smt2 |  271.916s | 1253.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-50.smt2 |  277.699s | 1045.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-48.smt2 |  282.429s | 887.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-50.smt2 |  284.731s | 923.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-47.smt2 |  285.076s | 792.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-50.smt2 |  285.272s | 995.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-49.smt2 |  286.242s | 727.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-49.smt2 |  286.311s | 928.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-49.smt2 |  289.195s | 1092.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-46.smt2 |  298.070s | 653.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-49.smt2 |  298.602s | 2649.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-46.smt2 |  299.743s | 2233.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-50.smt2 |  299.753s | 873.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-49.smt2 |  300.359s | 1001.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-47.smt2 |  305.375s | 1797.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-50.smt2 |  309.276s | 961.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-49.smt2 |  310.677s | 1677.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-46.smt2 |  313.443s | 1333.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-50.smt2 |  319.554s | 1341.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-49.smt2 |  319.636s | 1674.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-285271.smt2 |  321.186s | 429.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-48.smt2 |  326.034s | 1112.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-50.smt2 |  326.344s | 2382.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-48.smt2 |  326.983s | 951.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-48.smt2 |  343.499s | 2365.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-48.smt2 |  345.800s | 1315.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-49.smt2 |  359.534s | 1065.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-49.smt2 |  360.635s | 1528.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-49.smt2 |  361.228s | 1133.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-49.smt2 |  366.991s | 1090.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-49.smt2 |  368.699s | 1117.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-48.smt2 |  370.744s | 1340.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-48.smt2 |  376.796s | 1766.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-50.smt2 |  378.278s | 859.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER11-15-fair.smt2        |  383.591s | 220.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-47.smt2 |  385.889s | 1582.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-50.smt2 |  389.107s | 1703.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-50.smt2 |  390.748s | 1130.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-50.smt2 |  393.679s | 1244.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-49.smt2 |  394.540s | 2011.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-50.smt2 |  395.273s | 1439.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-49.smt2 |  395.614s | 1179.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-49.smt2 |  406.567s | 1309.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-50.smt2 |  407.176s | 1578.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-50.smt2 |  414.490s | 1000.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-49.smt2 |  417.028s | 2043.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-50.smt2 |  417.299s | 2201.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-49.smt2 |  418.815s | 897.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-49.smt2 |  419.978s | 1639.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-50.smt2 |  422.955s | 2039.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-50.smt2 |  428.095s | 2541.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-50.smt2 |  431.036s | 1660.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-49.smt2 |  432.896s | 1774.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-50.smt2 |  439.514s | 1896.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-49.smt2 |  440.774s | 1108.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-50.smt2 |  444.256s | 1287.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-50.smt2 |  449.697s | 1997.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-368069.smt2 |  449.901s | 689.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-50.smt2 |  452.683s | 902.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-50.smt2 |  459.846s | 3335.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-47.smt2 |  460.165s | 1873.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-50.smt2 |  460.660s | 1241.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-49.smt2 |  472.537s | 2203.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-321761.smt2 |  501.956s | 540.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-50.smt2 |  502.490s | 1881.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-49.smt2 |  511.032s | 2503.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-49.smt2 |  512.106s | 1064.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-49.smt2 |  537.973s | 1844.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-50.smt2 |  551.557s | 1688.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-48.smt2 |  561.587s | 1276.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-50.smt2 |  563.140s | 2594.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-49.smt2 |  580.789s | 1486.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-50.smt2 |  633.602s | 2105.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-48.smt2 |  657.209s | 756.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-50.smt2 |  673.983s | 1432.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-50.smt2 |  719.290s | 1076.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-50.smt2 |  720.473s | 2553.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-49.smt2 |  737.477s | 2036.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-278378.smt2 |  748.926s | 425.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-50.smt2 |  778.589s | 1913.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-729964.smt2 |  790.030s | 1837.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-50.smt2 |  841.190s | 1075.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-46.smt2 |  891.889s | 1625.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-47.smt2 |  898.827s | 1386.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-49.smt2 |  946.526s | 1451.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-50.smt2 | 1014.118s | 1429.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-50.smt2 | 1026.672s | 1128.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-49.smt2 | 1083.804s | 1499.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-50.smt2 | 1093.073s | 1686.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_7.txt.smt2                | 1200.066s | 195.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_15.txt.smt2               | 1200.082s | 233.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-357303.smt2  | 1200.111s | 690.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-658040.smt2 | 1200.190s | 1584.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/20231117-c_inference/80_80_71_17_unsat.smt2 | 1200.234s | 1849.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-50.smt2 | 1200.291s | 1981.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-985518.smt2  | 1200.381s | 3164.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1060546.smt2 | 1200.396s | 3225.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1228327.smt2 | 1200.488s | 4535.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1400961.smt2 | 1200.582s | 5422.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1472027.smt2 | 1200.629s | 5757.0MiB| timeout | 0 |  |  |