# .

* SAT 378
* UNSAT 375
* TIMEOUT 47
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-1-QF_LIA_hard-timeout10min-bb2
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: c383004968f5bf66a9668a7ae254c83d45ac3afe
Z3 branch: fmcad26_artifact
Z3 options: "-T:600 -v:0 smt.threads=1 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.336s | 31.152MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1575.smt2 |    0.352s | 31.56MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1567.smt2 |    0.424s | 31.424MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1591.smt2 |    0.467s | 31.672MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1533.smt2 |    0.468s | 30.62MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-14.smt2 |    0.475s | 94.04MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1565.smt2 |    0.475s | 31.288MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1617.smt2 |    0.491s | 32.192MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-12.smt2 |    0.545s | 104.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-03.smt2 |    0.578s | 138.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/convert/convert-jpg2gif-query-1607.smt2 |    0.618s | 32.132MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-10.smt2 |    0.672s | 184.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-08.smt2 |    0.718s | 92.144MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-14.smt2 |    0.724s | 90.74MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-08.smt2 |    0.729s | 90.736MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-09.smt2 |    0.733s | 220.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-01.smt2 |    0.734s | 223.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-15.smt2 |    0.736s | 219.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-02.smt2 |    0.755s | 222.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-01.smt2 |    1.087s | 121.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-12.smt2 |    1.088s | 122.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-08.smt2 |    1.096s | 121.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-06.smt2 |    1.098s | 121.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-11.smt2 |    1.104s | 122.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-07.smt2 |    1.114s | 122.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-14.smt2 |    1.125s | 122.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-11.smt2 |    1.137s | 155.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-10.smt2 |    1.143s | 122.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-10.smt2 |    1.152s | 323.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-15.smt2 |    1.193s | 146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-05.smt2 |    1.228s | 122.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-00.smt2 |    1.282s | 122.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-03.smt2 |    1.345s | 408.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-10.smt2 |    1.371s | 441.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-13.smt2 |    1.371s | 216.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-06.smt2 |    1.375s | 217.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-14.smt2 |    1.381s | 217.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-08.smt2 |    1.412s | 224.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-04.smt2 |    1.415s | 217.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-15.smt2 |    1.415s | 217.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-12.smt2 |    1.418s | 442.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-04.smt2 |    1.421s | 217.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-07.smt2 |    1.427s | 474.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-05.smt2 |    1.432s | 224.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-526410.smt2  |    1.457s | 97.916MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-03.smt2 |    1.473s | 245.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r1000w0010/RC-08.smt2 |    1.478s | 152.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-00.smt2 |    1.527s | 459.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-03.smt2 |    1.592s | 459.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-09.smt2 |    1.762s | 479.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-11.smt2 |    1.814s | 217.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-07.smt2 |    1.870s | 222.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-13.smt2 |    1.920s | 458.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-04.smt2 |    1.930s | 557.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-09.smt2 |    1.934s | 457.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-14.smt2 |    1.960s | 495.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-13.smt2 |    1.969s | 495.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-02.smt2 |    1.969s | 495.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-00.smt2 |    1.983s | 495.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-00.smt2 |    1.991s | 217.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-06.smt2 |    1.998s | 217.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-05.smt2 |    2.019s | 497.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-06.smt2 |    2.042s | 507.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-03.smt2 |    2.269s | 646.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-02.smt2 |    2.273s | 718.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-13.smt2 |    2.293s | 699.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-00.smt2 |    2.302s | 699.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-14.smt2 |    2.307s | 699.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-01.smt2 |    2.320s | 699.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-11.smt2 |    2.320s | 698.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-08.smt2 |    2.410s | 699.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-06.smt2 |    2.447s | 699.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-10.smt2 |    2.454s | 699.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-15.smt2 |    2.467s | 699.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-05.smt2 |    2.479s | 699.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1015084.smt2 |    2.534s | 159.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-09.smt2 |    2.537s | 700.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-09.smt2 |    3.137s | 694.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-02.smt2 |    3.182s | 693.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RC-13.smt2 |    3.256s | 694.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-04.smt2 |    3.280s | 746.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-12.smt2 |    4.047s | 1408.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w1000/RF-07.smt2 |    4.296s | 1486.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-901628.smt2  |    5.182s | 230.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-01.smt2 |    5.560s | 708.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-38.smt2 |    6.579s | 44.848MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1270163.smt2 |    6.837s | 259.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-379665.smt2  |    7.377s | 111.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-39.smt2 |    8.166s | 46.88MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-38.smt2 |    8.256s | 45.852MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-41.smt2 |    9.084s | 50.68MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-37.smt2 |    9.132s | 47.116MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-39.smt2 |    9.463s | 46.588MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-758897.smt2 |    9.565s | 214.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-8-49.smt2 |    9.629s | 140.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-38.smt2 |    9.754s | 46.624MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-38.smt2 |    9.980s | 45.596MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-917322.smt2 |   10.105s | 231.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-415996.smt2  |   10.615s | 123.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-38.smt2 |   10.645s | 45.984MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-17-47.smt2 |   10.970s | 56.372MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-24-49.smt2 |   11.141s | 109.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-32-50.smt2 |   11.464s | 146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-49.smt2 |   11.582s | 140.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-19-50.smt2 |   11.714s | 146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-200.smt2 |   11.889s | 78.828MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-392137.smt2  |   12.329s | 126.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-906586.smt2 |   12.512s | 234.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-39.smt2 |   12.527s | 48.688MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-50.smt2 |   12.811s | 113.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-16-49.smt2 |   13.018s | 141.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-46.smt2 |   13.029s | 60.456MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-50.smt2 |   13.035s | 147.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-60-50.smt2 |   13.125s | 144.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-43.smt2 |   13.183s | 54.032MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-42.smt2 |   13.341s | 50.176MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-48.smt2 |   13.416s | 59.072MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-49.smt2 |   13.452s | 141.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-49.smt2 |   13.516s | 140.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-329386.smt2 |   13.620s | 103.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-23-50.smt2 |   13.787s | 147.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-19-49.smt2 |   13.821s | 68.556MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-57-49.smt2 |   13.969s | 139.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-343499.smt2 |   14.018s | 109.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-47.smt2 |   14.026s | 89.516MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-48-50.smt2 |   14.063s | 145.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-47.smt2 |   14.167s | 89.256MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-49.smt2 |   14.204s | 80.26MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-48.smt2 |   14.259s | 70.828MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-42-50.smt2 |   14.491s | 146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-39.smt2 |   14.746s | 50.8MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-37-50.smt2 |   14.900s | 146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-49.smt2 |   14.989s | 140.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-59-50.smt2 |   15.139s | 144.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-64-50.smt2 |   15.262s | 145.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-40.smt2 |   15.377s | 51.96MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-48.smt2 |   15.415s | 62.776MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-39.smt2 |   15.429s | 50.996MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-46.smt2 |   15.441s | 122.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-48.smt2 |   15.509s | 102.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-46.smt2 |   15.524s | 123.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-49.smt2 |   15.608s | 139.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-413904.smt2 |   15.622s | 147.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-50.smt2 |   16.090s | 147.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-49.smt2 |   16.355s | 139.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-13-50.smt2 |   16.463s | 148.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-48.smt2 |   16.482s | 89.776MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-49.smt2 |   16.713s | 138.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-47.smt2 |   16.755s | 119.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-41.smt2 |   16.841s | 54.272MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-68-50.smt2 |   16.846s | 145.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-76-50.smt2 |   16.880s | 145.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER10-13-fair.smt2        |   16.917s | 38.004MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-46.smt2 |   17.049s | 123.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-42.smt2 |   17.217s | 55.292MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-41.smt2 |   17.236s | 53.98MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-13-50.smt2 |   17.567s | 70.96MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-65-50.smt2 |   17.633s | 146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-48.smt2 |   17.673s | 69.728MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-46.smt2 |   17.677s | 58.168MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-40.smt2 |   17.685s | 51.708MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-49.smt2 |   17.724s | 139.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-70-50.smt2 |   17.781s | 146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-50.smt2 |   17.816s | 148.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-49.smt2 |   17.824s | 139.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-45.smt2 |   17.865s | 60.728MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-47.smt2 |   17.892s | 121.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-67-50.smt2 |   17.892s | 146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1192684.smt2 |   17.992s | 352.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-42.smt2 |   18.102s | 56.136MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-199.smt2 |   18.269s | 103.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-48.smt2 |   18.280s | 70.956MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-49.smt2 |   18.354s | 140.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-50.smt2 |   18.485s | 146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-42.smt2 |   18.507s | 57.848MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-50.smt2 |   18.540s | 146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-77-50.smt2 |   18.552s | 146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-49.smt2 |   18.645s | 140.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-48.smt2 |   18.717s | 101.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-40.smt2 |   18.786s | 53.988MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-41.smt2 |   18.846s | 55.296MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-44.smt2 |   18.967s | 57.136MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-50.smt2 |   19.022s | 146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-199.smt2 |   19.080s | 88.048MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-47.smt2 |   19.247s | 60.212MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-47.smt2 |   19.351s | 61.556MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-916807.smt2 |   19.549s | 297.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-48.smt2 |   19.576s | 130.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-45.smt2 |   19.595s | 60.976MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-50.smt2 |   19.603s | 72.492MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-196.smt2 |   19.635s | 156.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-69-50.smt2 |   19.660s | 146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-44.smt2 |   19.740s | 55.536MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-47.smt2 |   19.791s | 122.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-41.smt2 |   19.804s | 54.516MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-40.smt2 |   20.145s | 52.992MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-47.smt2 |   20.247s | 98.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-197.smt2 |   20.253s | 128.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-42.smt2 |   20.296s | 59.144MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-37-47.smt2 |   20.336s | 46.816MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-48.smt2 |   20.398s | 130.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-46.smt2 |   20.573s | 62.012MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-45.smt2 |   20.597s | 58.924MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-527358.smt2 |   20.606s | 206.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-47.smt2 |   20.650s | 122.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-41.smt2 |   20.650s | 58.112MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-41.smt2 |   20.807s | 54.652MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-46.smt2 |   20.908s | 123.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-48.smt2 |   21.026s | 104.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-42.smt2 |   21.110s | 58.112MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-58-50.smt2 |   21.128s | 147.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-57-50.smt2 |   21.137s | 145.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-46.smt2 |   21.183s | 125.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-46.smt2 |   21.210s | 125.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-50.smt2 |   21.317s | 146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-49.smt2 |   21.331s | 74.84MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-3-198.smt2 |   21.494s | 116.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-40-50.smt2 |   21.513s | 147.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-48.smt2 |   21.688s | 133.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-44.smt2 |   21.747s | 58.688MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-50.smt2 |   21.777s | 74.544MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-44.smt2 |   21.866s | 60.892MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-49.smt2 |   21.894s | 77.984MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-46.smt2 |   21.909s | 127.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-49.smt2 |   21.980s | 140.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-45.smt2 |   22.057s | 63.544MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-48.smt2 |   22.424s | 132.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-47.smt2 |   22.485s | 122.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-50.smt2 |   22.657s | 146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-46.smt2 |   22.709s | 65.08MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-46.smt2 |   22.914s | 63.536MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-63-50.smt2 |   22.955s | 145.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-42.smt2 |   23.164s | 56.836MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-42.smt2 |   23.307s | 57.348MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-48.smt2 |   23.417s | 104.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-50.smt2 |   23.419s | 78.3MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-48.smt2 |   23.480s | 130.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-48.smt2 |   23.574s | 108.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-46.smt2 |   23.613s | 63.064MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-48.smt2 |   23.848s | 64.96MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-48.smt2 |   23.956s | 133.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-47.smt2 |   24.010s | 81.72MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-689472.smt2  |   24.022s | 293.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-42.smt2 |   24.079s | 60.16MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-42.smt2 |   24.164s | 60.252MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-47.smt2 |   24.269s | 124.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-49.smt2 |   24.365s | 142.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-42.smt2 |   24.413s | 60.368MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-44.smt2 |   24.445s | 62.664MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-44.smt2 |   24.447s | 60.728MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-47.smt2 |   24.486s | 124.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-45.smt2 |   24.493s | 63.28MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-47.smt2 |   24.831s | 76.348MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-50.smt2 |   24.836s | 51.988MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-43.smt2 |   25.099s | 58.56MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-44.smt2 |   25.105s | 62.26MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-49.smt2 |   25.208s | 145.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-44.smt2 |   25.315s | 61.104MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-47.smt2 |   25.379s | 105.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-44.smt2 |   25.439s | 58.744MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-48.smt2 |   25.453s | 133.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-44.smt2 |   25.469s | 62.52MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-48.smt2 |   25.485s | 134.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-46.smt2 |   25.509s | 66.332MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-50.smt2 |   25.607s | 146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-45.smt2 |   25.907s | 63.908MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-45.smt2 |   26.053s | 62.52MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-39-50.smt2 |   26.113s | 147.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-46.smt2 |   26.281s | 126.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-47.smt2 |   26.301s | 120.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-44.smt2 |   26.374s | 61.688MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-42.smt2 |   26.378s | 58.568MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-47.smt2 |   26.440s | 124.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-50.smt2 |   26.475s | 147.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-48.smt2 |   26.682s | 104.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-50.smt2 |   26.697s | 88.148MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-45.smt2 |   26.699s | 63.312MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-17-47.smt2 |   26.763s | 97.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-45.smt2 |   26.866s | 62.628MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-47.smt2 |   27.070s | 79.16MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-45.smt2 |   27.418s | 59.956MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-47.smt2 |   27.513s | 79.64MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-200.smt2 |   27.557s | 99.056MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-49.smt2 |   27.614s | 145.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-43.smt2 |   27.718s | 61.024MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-43.smt2 |   27.831s | 64.064MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-44.smt2 |   28.024s | 63.54MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-45.smt2 |   28.303s | 63.796MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-50.smt2 |   28.318s | 146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-46.smt2 |   28.428s | 62.772MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-49.smt2 |   28.660s | 110.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-49.smt2 |   28.845s | 142.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-48.smt2 |   28.873s | 135.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-47.smt2 |   28.915s | 120.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-48.smt2 |   29.128s | 77.992MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-50.smt2 |   29.134s | 80.484MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-196.smt2 |   29.160s | 177.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-46.smt2 |   29.177s | 125.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-46.smt2 |   29.260s | 125.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-47.smt2 |   29.286s | 120.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-50.smt2 |   29.298s | 147.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-48.smt2 |   29.334s | 78.68MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-47.smt2 |   29.345s | 121.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1185949.smt2 |   29.425s | 341.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-48.smt2 |   29.486s | 49.68MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-47.smt2 |   29.676s | 120.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-50.smt2 |   29.700s | 146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-46.smt2 |   30.098s | 64.048MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-50.smt2 |   30.419s | 52.24MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-43.smt2 |   30.420s | 62.784MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-49.smt2 |   30.839s | 146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-46.smt2 |   30.894s | 65.844MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-50.smt2 |   30.905s | 146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-47.smt2 |   30.912s | 121.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-44.smt2 |   30.912s | 65.084MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-49.smt2 |   31.036s | 146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-48.smt2 |   31.264s | 132.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-2-198.smt2 |   31.611s | 110.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-49.smt2 |   31.632s | 142.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-43.smt2 |   31.829s | 66.14MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-50.smt2 |   31.965s | 147.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-48.smt2 |   32.058s | 135.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-49.smt2 |   32.060s | 65.016MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-49.smt2 |   32.121s | 148.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-42.smt2 |   32.154s | 60.928MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-45.smt2 |   32.245s | 64.312MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-48.smt2 |   32.603s | 129.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-50.smt2 |   32.797s | 148.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-46.smt2 |   32.809s | 66.104MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-47.smt2 |   32.827s | 121.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-46.smt2 |   32.865s | 66.956MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-50.smt2 |   32.931s | 147.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-43.smt2 |   33.015s | 64.572MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-49.smt2 |   33.164s | 147.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-48.smt2 |   33.278s | 130.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-49.smt2 |   33.298s | 146.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-49.smt2 |   33.736s | 73.516MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-47.smt2 |   33.739s | 122.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-48.smt2 |   33.804s | 129.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-45.smt2 |   34.038s | 63.012MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-43.smt2 |   34.276s | 64.764MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-198.smt2 |   34.331s | 133.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-45.smt2 |   34.346s | 66.36MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-47.smt2 |   34.805s | 123.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-44.smt2 |   34.852s | 64.56MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-45.smt2 |   34.985s | 65.92MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-47.smt2 |   34.995s | 124.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-48.smt2 |   35.075s | 130.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-48.smt2 |   35.148s | 79.52MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-48.smt2 |   35.532s | 82.544MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-48.smt2 |   35.554s | 107.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-43.smt2 |   35.900s | 64.596MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-43.smt2 |   35.906s | 66.36MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-46.smt2 |   35.925s | 66.82MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-48.smt2 |   36.013s | 78.356MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-48.smt2 |   36.342s | 132.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-45.smt2 |   36.416s | 63.796MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-47.smt2 |   36.668s | 122.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-49.smt2 |   36.698s | 82.328MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-48.smt2 |   36.815s | 132.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-48.smt2 |   36.826s | 130.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-199.smt2 |   36.924s | 114.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-46.smt2 |   37.024s | 127.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-196.smt2 |   37.029s | 187.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-50.smt2 |   37.435s | 149.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-48.smt2 |   37.542s | 132.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-43.smt2 |   37.609s | 66.364MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-48.smt2 |   37.872s | 81.912MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-48.smt2 |   38.092s | 133.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-48.smt2 |   38.108s | 50.048MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-48.smt2 |   38.227s | 77.224MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-43.smt2 |   38.337s | 64.74MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-50.smt2 |   39.100s | 149.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-47.smt2 |   39.144s | 125.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-45.smt2 |   39.656s | 68.116MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-47.smt2 |   40.188s | 128.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-48.smt2 |   40.193s | 137.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-47.smt2 |   40.456s | 128.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-0-49.smt2 |   40.663s | 52.256MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-48.smt2 |   40.855s | 81.764MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-46.smt2 |   40.977s | 85.036MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-47.smt2 |   41.037s | 81.056MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-50.smt2 |   41.079s | 85.672MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-46.smt2 |   41.236s | 127.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-50.smt2 |   41.593s | 84.904MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-47.smt2 |   41.704s | 124.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-41.smt2 |   41.743s | 59.86MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-49.smt2 |   41.767s | 72.208MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-48.smt2 |   42.257s | 135.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-197.smt2 |   42.292s | 125.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-50.smt2 |   42.311s | 84.32MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-48.smt2 |   42.349s | 133.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-46.smt2 |   42.631s | 67.128MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-267105.smt2  |   42.787s | 98.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-49.smt2 |   42.904s | 86.7MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-47.smt2 |   43.133s | 123.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-50.smt2 |   43.406s | 150.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-46.smt2 |   43.476s | 83.76MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-41-50.smt2 |   43.577s | 149.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-47.smt2 |   43.653s | 124.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-48.smt2 |   43.703s | 72.28MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-48.smt2 |   44.032s | 78.448MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-50.smt2 |   44.155s | 149.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/int_from_list/prp-1-49.smt2 |   44.272s | 51.728MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-50.smt2 |   44.405s | 79.636MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-48.smt2 |   44.586s | 133.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-46.smt2 |   45.053s | 82.488MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-50.smt2 |   45.318s | 152.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-49.smt2 |   45.899s | 89.512MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-47.smt2 |   45.928s | 125.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-49.smt2 |   46.086s | 114.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-23-41.smt2 |   46.244s | 58.86MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-49.smt2 |   46.293s | 83.3MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-47.smt2 |   46.301s | 125.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-864173.smt2  |   46.398s | 404.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-49.smt2 |   46.454s | 144.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-47.smt2 |   46.575s | 82.34MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-48.smt2 |   46.783s | 135.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-46.smt2 |   46.790s | 104.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-47.smt2 |   47.533s | 82.04MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-49.smt2 |   48.372s | 84.576MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-50.smt2 |   48.411s | 85.92MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-48.smt2 |   48.881s | 135.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-48.smt2 |   48.926s | 138.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-48.smt2 |   49.213s | 135.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-47.smt2 |   49.330s | 126.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-49.smt2 |   49.886s | 81.324MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-49.smt2 |   50.034s | 87.196MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-49.smt2 |   50.172s | 151.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-50.smt2 |   50.299s | 149.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-50.smt2 |   50.500s | 85.328MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-14-49.smt2 |   50.783s | 72.712MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-50.smt2 |   50.819s | 88.392MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption/prp-0-200.smt2 |   51.127s | 118.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1148089.smt2 |   51.268s | 519.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-47.smt2 |   51.993s | 72.944MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-50.smt2 |   53.040s | 90.708MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-46.smt2 |   53.051s | 73.392MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-46.smt2 |   53.461s | 84.132MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-48.smt2 |   53.924s | 86.38MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-49.smt2 |   53.973s | 92.32MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-50.smt2 |   54.202s | 96.088MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-50.smt2 |   54.449s | 152.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-48.smt2 |   54.663s | 86.184MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-48.smt2 |   54.952s | 88.336MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-50.smt2 |   54.978s | 89.92MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-49.smt2 |   55.118s | 93.836MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-50.smt2 |   55.290s | 150.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-49.smt2 |   55.385s | 83.044MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-47.smt2 |   55.797s | 78.668MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-50.smt2 |   55.886s | 152.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-47.smt2 |   55.963s | 76.084MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-47.smt2 |   56.226s | 126.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-47.smt2 |   56.329s | 85.156MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-50.smt2 |   56.449s | 93.856MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-48.smt2 |   56.473s | 83.78MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-48.smt2 |   56.773s | 137.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-50.smt2 |   56.796s | 73.152MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-46.smt2 |   57.167s | 80.812MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-47.smt2 |   57.319s | 88.88MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER10-14-fair.smt2        |   57.508s | 41.964MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-48.smt2 |   57.543s | 137.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-49.smt2 |   57.631s | 147.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-46.smt2 |   58.025s | 72.972MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-49.smt2 |   58.211s | 87.252MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-47.smt2 |   58.537s | 88.14MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-49.smt2 |   58.830s | 86.112MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-50.smt2 |   59.304s | 89.512MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-49.smt2 |   59.381s | 89.248MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-50.smt2 |   59.683s | 90.712MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-21-40.smt2 |   60.004s | 60.416MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-50.smt2 |   60.939s | 89.58MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-47.smt2 |   60.974s | 83.624MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-50.smt2 |   61.124s | 93.276MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-50.smt2 |   61.268s | 91.9MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-48.smt2 |   61.499s | 87.924MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-50.smt2 |   61.915s | 120.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-46.smt2 |   61.985s | 85.428MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-48.smt2 |   62.367s | 86.264MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-49.smt2 |   62.846s | 93.668MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-49.smt2 |   63.562s | 143.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-47.smt2 |   63.614s | 77.772MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-50.smt2 |   64.283s | 151.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-47.smt2 |   64.347s | 88.488MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-48.smt2 |   64.732s | 139.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-48.smt2 |   64.798s | 138.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-48.smt2 |   65.492s | 89.192MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-49.smt2 |   65.725s | 147.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-50.smt2 |   67.737s | 90.208MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-31-42.smt2 |   67.812s | 63.744MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-46.smt2 |   67.895s | 128.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-48.smt2 |   67.964s | 93.812MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-916576.smt2  |   68.044s | 454.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-47.smt2 |   68.748s | 108.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-928134.smt2  |   68.995s | 449.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-46.smt2 |   69.262s | 106.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-49.smt2 |   69.392s | 95.076MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-46.smt2 |   70.094s | 127.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-50.smt2 |   70.870s | 102.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-50.smt2 |   70.929s | 91.684MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-63-50.smt2 |   72.095s | 92.06MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-46.smt2 |   72.435s | 126.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1317230.smt2 |   72.603s | 563.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-50.smt2 |   73.104s | 97.708MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1007795.smt2 |   74.035s | 512.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-47.smt2 |   74.065s | 76.72MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-48.smt2 |   74.259s | 139.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-44.smt2 |   74.834s | 70.956MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-47.smt2 |   76.127s | 79.532MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER11-14-fair.smt2        |   76.708s | 45.356MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-50.smt2 |   76.767s | 152.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-26-43.smt2 |   76.876s | 68.924MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-46.smt2 |   76.993s | 74.664MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-50.smt2 |   77.733s | 152.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-46.smt2 |   78.199s | 73.912MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-408585.smt2  |   80.166s | 193.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-49.smt2 |   80.302s | 92.64MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-47.smt2 |   80.419s | 124.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-49.smt2 |   80.851s | 144.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-50.smt2 |   81.264s | 89.904MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1121941.smt2 |   82.747s | 577.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-46.smt2 |   82.847s | 74.448MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-47.smt2 |   82.990s | 126.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-45.smt2 |   83.350s | 77.624MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-47.smt2 |   84.034s | 95.916MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-48.smt2 |   84.435s | 91.24MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-50.smt2 |   86.688s | 97.144MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-46.smt2 |   87.546s | 128.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-47.smt2 |   88.781s | 113.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-46.smt2 |   89.175s | 77.484MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-47.smt2 |   89.776s | 125.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-46.smt2 |   90.246s | 74.868MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-48.smt2 |   91.318s | 81.076MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-50.smt2 |   92.100s | 153.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-48.smt2 |   92.430s | 81.068MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-48.smt2 |   93.251s | 119.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-49.smt2 |   94.053s | 97.956MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-48.smt2 |   94.269s | 142.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-46.smt2 |   95.625s | 75.528MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-50.smt2 |   97.627s | 87.104MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-48.smt2 |   98.368s | 118.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-46.smt2 |   98.440s | 109.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-49.smt2 |   99.297s | 151.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-47.smt2 |  100.892s | 81.584MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-47.smt2 |  101.676s | 98.916MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-50.smt2 |  101.751s | 113.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-46.smt2 |  101.756s | 110.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-47.smt2 |  102.708s | 127.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-46.smt2 |  102.764s | 76.464MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-48.smt2 |  102.766s | 139.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1268455.smt2 |  102.937s | 605.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-50.smt2 |  103.057s | 151.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1275621.smt2 |  103.977s | 709.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-47.smt2 |  104.181s | 116.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-49.smt2 |  104.906s | 84.876MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-47.smt2 |  106.052s | 79.532MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-48.smt2 |  106.975s | 121.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-46.smt2 |  107.155s | 132.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-47.smt2 |  107.177s | 127.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-46.smt2 |  107.871s | 127.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-48.smt2 |  109.771s | 81.78MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1265513.smt2 |  110.485s | 678.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-46.smt2 |  111.457s | 75.732MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-46.smt2 |  113.009s | 76.916MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-46.smt2 |  113.295s | 76.812MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-47.smt2 |  113.939s | 113.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-49.smt2 |  114.696s | 125.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-47.smt2 |  115.112s | 79.044MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-46.smt2 |  115.209s | 131.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-46.smt2 |  115.400s | 130.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-47.smt2 |  116.858s | 79.276MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-48.smt2 |  117.584s | 83.628MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-50.smt2 |  119.007s | 101.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-48.smt2 |  119.365s | 82.916MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-50.smt2 |  122.389s | 88.484MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-49.smt2 |  123.027s | 86.84MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-49.smt2 |  123.169s | 153.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-481231.smt2  |  124.273s | 250.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-47.smt2 |  124.305s | 135.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-48.smt2 |  125.173s | 84.908MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-48.smt2 |  125.187s | 119.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-50.smt2 |  125.379s | 90.992MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-49.smt2 |  127.407s | 87.4MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-46.smt2 |  127.614s | 79.9MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-48.smt2 |  129.091s | 83.884MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-49.smt2 |  129.327s | 86.572MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-48.smt2 |  129.479s | 82.348MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-46.smt2 |  129.483s | 132.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-48.smt2 |  129.719s | 84.5MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-48.smt2 |  129.951s | 140.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-48.smt2 |  130.234s | 139.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-46.smt2 |  131.390s | 131.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-48.smt2 |  131.549s | 138.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-47.smt2 |  131.987s | 80.844MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-47.smt2 |  133.543s | 80.012MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-49.smt2 |  133.935s | 87.544MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1365816.smt2 |  134.601s | 829.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-46.smt2 |  135.143s | 77.7MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-49.smt2 |  136.530s | 115.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-47.smt2 |  138.138s | 82.352MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-47.smt2 |  138.202s | 81.24MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-50.smt2 |  138.310s | 153.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-47.smt2 |  139.241s | 130.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-48.smt2 |  143.962s | 86.264MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-48.smt2 |  144.781s | 85.02MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-49.smt2 |  145.619s | 87.72MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-49.smt2 |  145.844s | 86.44MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-49.smt2 |  146.212s | 87.988MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-47.smt2 |  146.582s | 85.308MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-48.smt2 |  149.207s | 85.692MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1205831.smt2 |  151.036s | 723.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-47.smt2 |  151.137s | 127.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-48.smt2 |  153.999s | 85.416MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1317511.smt2 |  154.050s | 821.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-47.smt2 |  154.678s | 128.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-48.smt2 |  156.222s | 85.132MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-49.smt2 |  156.336s | 126.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-47.smt2 |  157.814s | 82.076MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-46.smt2 |  158.184s | 127.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-49.smt2 |  160.498s | 129.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-50.smt2 |  161.536s | 89.264MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-46.smt2 |  163.335s | 133.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-47.smt2 |  163.588s | 81.328MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-48.smt2 |  164.377s | 85.16MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-46.smt2 |  164.702s | 131.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-48.smt2 |  166.009s | 86.94MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-705295.smt2 |  167.149s | 353.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-46.smt2 |  168.708s | 133.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-46.smt2 |  168.913s | 134.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-46.smt2 |  169.375s | 128.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-50.smt2 |  170.071s | 91.864MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-46.smt2 |  171.207s | 134.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-49.smt2 |  171.759s | 89.408MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-48.smt2 |  172.928s | 85.348MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-49.smt2 |  173.933s | 126.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-47.smt2 |  174.984s | 131.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-50.smt2 |  177.022s | 92.076MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-49.smt2 |  177.185s | 89.26MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-50.smt2 |  178.815s | 93.268MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-49.smt2 |  179.263s | 89.648MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-46.smt2 |  180.044s | 134.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-49.smt2 |  182.209s | 89.828MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-50.smt2 |  182.920s | 129.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-46.smt2 |  183.542s | 133.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-50.smt2 |  183.694s | 92.552MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-46.smt2 |  185.786s | 133.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-49.smt2 |  186.391s | 90.344MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-46.smt2 |  186.997s | 137.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-48.smt2 |  187.976s | 141.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-50.smt2 |  189.250s | 133.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-50.smt2 |  190.344s | 90.284MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-48.smt2 |  192.494s | 142.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-48.smt2 |  193.930s | 85.54MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-46.smt2 |  194.288s | 134.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-49.smt2 |  194.952s | 155.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-46.smt2 |  195.298s | 131.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-47.smt2 |  195.902s | 130.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-49.smt2 |  196.044s | 91.724MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1452366.smt2 |  196.132s | 1024.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-50.smt2 |  196.421s | 92.584MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-49.smt2 |  201.341s | 89.628MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-48.smt2 |  202.254s | 85.82MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-46.smt2 |  202.771s | 81.524MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-47.smt2 |  202.775s | 82.864MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-49.smt2 |  203.168s | 90.544MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-46.smt2 |  204.311s | 137.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-46.smt2 |  207.604s | 138.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-47.smt2 |  209.792s | 82.824MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-50.smt2 |  210.482s | 93.58MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-48.smt2 |  210.580s | 145.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-49.smt2 |  212.913s | 156.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-47.smt2 |  214.142s | 135.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-50.smt2 |  214.220s | 93.596MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-50.smt2 |  225.336s | 135.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-48.smt2 |  231.351s | 143.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-47.smt2 |  231.356s | 135.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-49.smt2 |  233.370s | 92.96MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-50.smt2 |  235.657s | 95.008MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-46.smt2 |  242.502s | 138.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-50.smt2 |  242.865s | 136.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-50.smt2 |  243.105s | 95.144MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER11-15-fair.smt2        |  244.010s | 59.64MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-48.smt2 |  244.368s | 143.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-47.smt2 |  250.778s | 132.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-46.smt2 |  251.754s | 84.272MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-46.smt2 |  252.040s | 139.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-48.smt2 |  252.648s | 143.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-50.smt2 |  252.710s | 161.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-46.smt2 |  257.209s | 136.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-794687.smt2 |  259.229s | 505.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-50.smt2 |  260.892s | 157.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-50.smt2 |  270.256s | 160.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-46.smt2 |  274.049s | 138.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-48.smt2 |  278.668s | 146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-50.smt2 |  280.094s | 158.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-50.smt2 |  283.506s | 158.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-50.smt2 |  285.762s | 95.664MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-46.smt2 |  287.002s | 142.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-50.smt2 |  289.232s | 99.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-729964.smt2 |  290.152s | 427.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-48.smt2 |  290.894s | 143.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-50.smt2 |  294.867s | 161.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-269353.smt2 |  295.283s | 97.12MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-50.smt2 |  305.595s | 94.344MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-50.smt2 |  308.512s | 161.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-49.smt2 |  313.602s | 160.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-46.smt2 |  322.834s | 138.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-928960.smt2  |  323.531s | 523.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-49.smt2 |  326.692s | 153.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-50.smt2 |  327.680s | 166.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-49.smt2 |  330.262s | 159.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-618384.smt2  |  350.235s | 349.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-49.smt2 |  364.367s | 159.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-50.smt2 |  364.400s | 165.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-49.smt2 |  367.907s | 153.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-46.smt2 |  368.000s | 145.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-50.smt2 |  369.263s | 165.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-50.smt2 |  374.241s | 162.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-49.smt2 |  376.599s | 96.044MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-47.smt2 |  380.644s | 138.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-49.smt2 |  385.896s | 160.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-49.smt2 |  386.291s | 159.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-49.smt2 |  397.726s | 160.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-47.smt2 |  398.518s | 139.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-49.smt2 |  403.836s | 163.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-50.smt2 |  409.312s | 169.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-49.smt2 |  409.675s | 163.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-50.smt2 |  413.377s | 162.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-50.smt2 |  414.426s | 167.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-49.smt2 |  419.973s | 163.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-50.smt2 |  424.516s | 166.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-49.smt2 |  426.773s | 163.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-49.smt2 |  448.815s | 162.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-48.smt2 |  450.737s | 147.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-283008.smt2 |  454.244s | 101.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1072007.smt2 |  466.431s | 768.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-49.smt2 |  472.753s | 168.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-49.smt2 |  487.047s | 164.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-49.smt2 |  496.756s | 165.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-48.smt2 |  498.574s | 148.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-49.smt2 |  503.639s | 169.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-50.smt2 |  503.688s | 174.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-49.smt2 |  504.935s | 165.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-50.smt2 |  523.221s | 166.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1361831.smt2 |  530.653s | 849.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-50.smt2 |  532.139s | 173.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-50.smt2 |  540.804s | 173.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-658040.smt2 |  542.405s | 367.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-48.smt2 |  542.839s | 152.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-50.smt2 |  548.077s | 165.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-49.smt2 |  580.217s | 172.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-48.smt2 |  590.401s | 153.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-49.smt2 |  597.474s | 168.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-368069.smt2 |  600.023s | 160.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-49.smt2 |  600.023s | 175.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-50.smt2 |  600.024s | 170.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-49.smt2 |  600.024s | 173.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_15.txt.smt2               |  600.030s | 60.844MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-247831.smt2 |  600.033s | 89.924MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-285271.smt2 |  600.033s | 101.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-278378.smt2 |  600.033s | 99.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-49.smt2 |  600.035s | 169.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-321761.smt2 |  600.037s | 135.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_7.txt.smt2                |  600.040s | 54.784MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-495717.smt2 |  600.040s | 239.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-47.smt2 |  600.040s | 97.284MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-50.smt2 |  600.041s | 101.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-49.smt2 |  600.042s | 169.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-50.smt2 |  600.044s | 175.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-50.smt2 |  600.045s | 167.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-49.smt2 |  600.045s | 165.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-49.smt2 |  600.045s | 170.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-50.smt2 |  600.045s | 168.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-50.smt2 |  600.045s | 175.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-50.smt2 |  600.045s | 172.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-49.smt2 |  600.046s | 169.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-50.smt2 |  600.046s | 167.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-50.smt2 |  600.047s | 178.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-50.smt2 |  600.047s | 171.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-49.smt2 |  600.047s | 167.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-50.smt2 |  600.047s | 173.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-50.smt2 |  600.047s | 169.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-49.smt2 |  600.047s | 171.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-49.smt2 |  600.048s | 174.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-49.smt2 |  600.048s | 168.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-357303.smt2  |  600.051s | 159.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-478122.smt2  |  600.052s | 235.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-49.smt2 |  600.054s | 166.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-518109.smt2  |  600.055s | 217.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-50.smt2 |  600.055s | 170.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-762853.smt2 |  600.060s | 480.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/20231117-c_inference/80_80_71_17_unsat.smt2 |  600.069s | 338.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1138192.smt2 |  600.082s | 815.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1262176.smt2 |  600.096s | 979.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-985518.smt2  |  600.105s | 733.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1060546.smt2 |  600.107s | 778.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1360077.smt2 |  600.110s | 943.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1228327.smt2 |  600.137s | 1059.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1400961.smt2 |  600.155s | 1275.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1472027.smt2 |  600.160s | 1324.0MiB| timeout | 0 |  |  |