# .

* SAT 473
* UNSAT 267
* TIMEOUT 66
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-QF_LIA_hard-timeout10min-bb0
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: f880fdccee614547c38c19beb7af5a027961646b
Z3 branch: core_min
Z3 options: "-T:600 -v:0 smt.threads=8 tactic.default_tactic=smt smt.auto_config=false smt_parallel.num_global_bb_batch_threads=0"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_LIA.tar.zst?download=1
Z3 commit message: Merge branch 'master' of github.com:Z3Prover/z3 into core_min

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-14.smt2 |    2.468s | 793.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-03.smt2 |    2.717s | 1159.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-10.smt2 |    2.833s | 1517.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-526410.smt2  |    2.844s | 629.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-09.smt2 |    2.914s | 1468.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-09.smt2 |    3.048s | 1817.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-01.smt2 |    3.139s | 1837.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-02.smt2 |    3.149s | 1828.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-15.smt2 |    3.282s | 1817.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-12.smt2 |    3.639s | 1768.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-14.smt2 |    3.652s | 1766.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-05.smt2 |    3.672s | 1772.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-05.smt2 |    3.679s | 1771.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-15.smt2 |    3.696s | 1767.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-11.smt2 |    3.736s | 1775.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-04.smt2 |    3.745s | 1772.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-01.smt2 |    3.754s | 1774.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-07.smt2 |    3.770s | 1767.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-527358.smt2 |    3.774s | 762.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-06.smt2 |    3.788s | 1765.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-08.smt2 |    3.789s | 758.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-13.smt2 |    3.795s | 1762.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/2019-ezsmt/incrementalScheduling/214-incremental_scheduling-27000-0.smt2 |    3.811s | 245.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-08.smt2 |    3.816s | 1763.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-04.smt2 |    3.823s | 1764.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-02.smt2 |    3.851s | 1766.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-14.smt2 |    3.861s | 746.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-08.smt2 |    3.872s | 731.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-12.smt2 |    4.105s | 1764.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-11.smt2 |    4.247s | 1761.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-11.smt2 |    4.263s | 1126.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-07.smt2 |    4.279s | 1759.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-12.smt2 |    4.305s | 1425.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-03.smt2 |    4.421s | 3445.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-15.smt2 |    4.443s | 1162.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-06.smt2 |    4.531s | 1768.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-10.smt2 |    4.629s | 2647.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-00.smt2 |    4.789s | 1760.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-01.smt2 |    5.274s | 3852.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-07.smt2 |    5.278s | 3783.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-12.smt2 |    5.281s | 3598.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-10.smt2 |    5.286s | 3598.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-00.smt2 |    5.338s | 3738.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-03.smt2 |    5.427s | 3738.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-09.smt2 |    5.462s | 3724.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-09.smt2 |    5.579s | 3840.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-00.smt2 |    5.602s | 3937.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-649834.smt2 |    5.606s | 1004.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-13.smt2 |    5.660s | 3724.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-15.smt2 |    5.687s | 3888.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-13.smt2 |    5.706s | 3883.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1007795.smt2 |    5.850s | 1136.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-02.smt2 |    5.850s | 3867.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-14.smt2 |    6.035s | 3932.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-11.smt2 |    6.274s | 3849.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-916576.smt2  |    6.648s | 1094.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-392137.smt2  |    8.391s | 798.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-928134.smt2  |    8.429s | 1369.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1015084.smt2 |    9.032s | 1373.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-689472.smt2  |    9.504s | 1311.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-916807.smt2 |    9.899s | 1513.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-415996.smt2  |   10.272s | 875.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-794687.smt2 |   10.618s | 1465.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-47.smt2 |   10.805s | 511.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-705295.smt2 |   11.451s | 1427.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-901996.smt2 |   12.852s | 1653.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-758897.smt2 |   12.943s | 1510.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-906218.smt2  |   13.197s | 1515.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-49.smt2 |   13.556s | 558.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-917322.smt2 |   14.313s | 1716.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-47.smt2 |   14.803s | 231.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-46.smt2 |   15.013s | 512.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-47.smt2 |   15.549s | 231.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-48.smt2 |   15.557s | 431.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-20-45.smt2 |   15.691s | 508.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-50.smt2 |   15.835s | 674.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-48.smt2 |   16.061s | 518.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-413904.smt2 |   16.229s | 1105.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-901628.smt2  |   16.761s | 1592.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-49.smt2 |   17.159s | 469.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-618384.smt2  |   17.373s | 1420.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-48.smt2 |   17.454s | 233.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-48.smt2 |   18.103s | 443.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-49.smt2 |   18.695s | 463.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-2-50.smt2 |   18.732s | 720.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-5-50.smt2 |   18.761s | 714.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-45.smt2 |   18.814s | 457.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-47.smt2 |   19.055s | 456.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-13-50.smt2 |   19.428s | 730.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-21-50.smt2 |   19.470s | 729.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-19-50.smt2 |   19.559s | 721.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-17-50.smt2 |   19.621s | 548.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-9-50.smt2 |   19.738s | 740.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-14-50.smt2 |   19.774s | 726.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-33-50.smt2 |   19.785s | 743.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-37-50.smt2 |   19.975s | 814.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-34-45.smt2 |   20.109s | 446.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-30-50.smt2 |   20.400s | 747.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-16-50.smt2 |   20.414s | 747.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1107622.smt2 |   20.418s | 2271.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-23-50.smt2 |   20.652s | 740.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1192684.smt2 |   21.522s | 2284.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-32-50.smt2 |   21.561s | 746.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-481231.smt2  |   21.634s | 1241.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-50.smt2 |   21.700s | 752.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-31-50.smt2 |   21.841s | 744.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-34-48.smt2 |   21.970s | 547.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1185949.smt2 |   22.139s | 2156.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-49.smt2 |   22.399s | 540.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-48-50.smt2 |   22.440s | 764.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-50.smt2 |   22.440s | 826.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-42-50.smt2 |   22.521s | 753.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-46-50.smt2 |   22.749s | 762.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-50.smt2 |   22.919s | 823.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-47.smt2 |   23.340s | 463.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-19-49.smt2 |   23.363s | 550.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-30-48.smt2 |   23.486s | 539.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-47.smt2 |   23.576s | 538.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-45-50.smt2 |   23.756s | 768.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-17-50.smt2 |   23.851s | 756.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-59-50.smt2 |   24.007s | 767.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-60-50.smt2 |   24.115s | 763.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-864173.smt2  |   24.343s | 2191.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-50.smt2 |   24.343s | 763.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-50.smt2 |   24.565s | 563.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-46.smt2 |   24.778s | 795.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-46.smt2 |   24.866s | 466.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-50.smt2 |   24.866s | 837.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-47.smt2 |   24.879s | 712.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-49.smt2 |   25.146s | 564.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-49.smt2 |   25.262s | 558.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-33-50.smt2 |   25.398s | 580.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-48.smt2 |   25.679s | 485.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-49.smt2 |   25.704s | 554.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-64-50.smt2 |   25.784s | 776.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-45.smt2 |   26.093s | 458.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-46.smt2 |   26.470s | 787.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-50.smt2 |   26.509s | 847.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-70-50.smt2 |   26.667s | 768.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-49.smt2 |   26.827s | 574.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-46.smt2 |   26.924s | 779.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-19-50.smt2 |   27.438s | 566.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-46.smt2 |   27.900s | 699.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-69-50.smt2 |   28.003s | 785.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-46.smt2 |   28.208s | 812.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER10-13-fair.smt2        |   28.367s | 298.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-46.smt2 |   28.472s | 806.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-46.smt2 |   28.541s | 810.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1121941.smt2 |   28.795s | 2448.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-67-50.smt2 |   28.860s | 784.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-45.smt2 |   28.970s | 484.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-29-48.smt2 |   28.978s | 566.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-68-50.smt2 |   29.045s | 779.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-65-50.smt2 |   29.158s | 781.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-50.smt2 |   29.369s | 558.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-46.smt2 |   29.418s | 829.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-49.smt2 |   30.035s | 758.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-50.smt2 |   30.191s | 576.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-47.smt2 |   30.314s | 822.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-47.smt2 |   30.353s | 824.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-47.smt2 |   30.366s | 806.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-45.smt2 |   30.606s | 474.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-46.smt2 |   30.766s | 818.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-47.smt2 |   31.020s | 813.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-45.smt2 |   31.398s | 474.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-46.smt2 |   31.545s | 862.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-45.smt2 |   31.553s | 458.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-48.smt2 |   31.589s | 869.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-47.smt2 |   31.627s | 984.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-47.smt2 |   32.221s | 844.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-47.smt2 |   32.387s | 852.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-50.smt2 |   32.595s | 771.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-50.smt2 |   32.682s | 787.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-63-50.smt2 |   32.905s | 772.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-47.smt2 |   33.018s | 849.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-48.smt2 |   33.432s | 857.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-46.smt2 |   33.446s | 1028.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-58-50.smt2 |   33.448s | 785.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-47.smt2 |   33.598s | 845.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-47.smt2 |   33.782s | 724.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-48.smt2 |   34.146s | 830.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-39-50.smt2 |   34.180s | 855.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-47.smt2 |   34.318s | 849.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-46.smt2 |   34.340s | 828.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-48.smt2 |   34.473s | 582.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-48.smt2 |   34.652s | 746.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-46.smt2 |   34.719s | 1027.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-48.smt2 |   34.792s | 741.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-45.smt2 |   34.874s | 487.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-48.smt2 |   35.128s | 746.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-48.smt2 |   35.207s | 867.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-40-50.smt2 |   35.332s | 779.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-45.smt2 |   35.334s | 491.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-48.smt2 |   35.517s | 867.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-48.smt2 |   35.556s | 495.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-50.smt2 |   35.687s | 788.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-50.smt2 |   35.814s | 862.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-17-47.smt2 |   35.839s | 546.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-46.smt2 |   35.886s | 502.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-46.smt2 |   35.915s | 713.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-45.smt2 |   35.983s | 488.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-50.smt2 |   36.013s | 600.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-47.smt2 |   36.233s | 1005.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-48.smt2 |   36.240s | 867.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-48.smt2 |   36.424s | 592.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-48.smt2 |   36.464s | 469.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-49.smt2 |   36.522s | 950.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-50.smt2 |   36.572s | 786.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-50.smt2 |   36.952s | 608.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-29-50.smt2 |   37.211s | 610.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-906586.smt2 |   37.345s | 2605.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-49.smt2 |   37.358s | 935.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-47.smt2 |   37.470s | 517.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-48.smt2 |   37.670s | 896.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-47.smt2 |   37.820s | 474.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-48.smt2 |   37.854s | 1045.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-48.smt2 |   37.947s | 878.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-49.smt2 |   38.472s | 754.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-49.smt2 |   38.486s | 588.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-46.smt2 |   38.536s | 477.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-45.smt2 |   38.611s | 499.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-49.smt2 |   38.618s | 601.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-48.smt2 |   38.731s | 1071.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-24-49.smt2 |   38.751s | 598.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-45.smt2 |   39.090s | 503.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-13-48.smt2 |   39.249s | 557.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-50.smt2 |   39.373s | 517.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-47.smt2 |   39.471s | 618.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-48.smt2 |   39.482s | 536.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-45.smt2 |   39.578s | 501.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-46.smt2 |   39.609s | 1031.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-47.smt2 |   39.610s | 520.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-45.smt2 |   39.734s | 498.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-46.smt2 |   39.756s | 871.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-48.smt2 |   39.845s | 608.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-47.smt2 |   39.859s | 1030.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-48.smt2 |   39.867s | 941.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-45.smt2 |   40.089s | 494.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-45.smt2 |   40.124s | 512.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-45.smt2 |   40.388s | 495.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-45.smt2 |   40.684s | 507.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-49.smt2 |   40.848s | 1084.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-47.smt2 |   40.895s | 865.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-14-49.smt2 |   40.899s | 587.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-46.smt2 |   40.983s | 715.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-48.smt2 |   41.001s | 734.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-47.smt2 |   41.017s | 528.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-46.smt2 |   41.064s | 479.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-48.smt2 |   41.077s | 578.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-49.smt2 |   41.601s | 923.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-45.smt2 |   41.691s | 492.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-48.smt2 |   41.875s | 535.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-48.smt2 |   42.020s | 899.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-49.smt2 |   42.128s | 956.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-50.smt2 |   42.139s | 868.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-46.smt2 |   42.566s | 515.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-50.smt2 |   42.677s | 601.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-47.smt2 |   42.707s | 575.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-47.smt2 |   43.353s | 617.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-49.smt2 |   43.687s | 930.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-50.smt2 |   43.741s | 791.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-46.smt2 |   43.928s | 532.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-46.smt2 |   43.991s | 719.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-46.smt2 |   44.159s | 530.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-50.smt2 |   44.194s | 874.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-45.smt2 |   44.299s | 521.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-50.smt2 |   44.335s | 654.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-46.smt2 |   44.336s | 522.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-50.smt2 |   44.502s | 937.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-46.smt2 |   44.510s | 863.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-47.smt2 |   44.651s | 894.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-50.smt2 |   44.735s | 981.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-45.smt2 |   44.856s | 530.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-46.smt2 |   45.113s | 538.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-49.smt2 |   45.321s | 957.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-49.smt2 |   45.333s | 939.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-46.smt2 |   45.409s | 570.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-49.smt2 |   45.415s | 960.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-46.smt2 |   45.634s | 513.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-49.smt2 |   45.993s | 1136.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-50.smt2 |   46.071s | 612.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-48.smt2 |   46.156s | 546.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-25-50.smt2 |   46.160s | 629.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-48.smt2 |   46.239s | 899.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-47.smt2 |   46.362s | 527.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-50.smt2 |   46.678s | 989.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-49.smt2 |   46.717s | 967.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-48.smt2 |   46.767s | 917.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-46.smt2 |   47.061s | 714.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-50.smt2 |   47.094s | 969.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-48.smt2 |   47.208s | 1093.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-50.smt2 |   47.417s | 961.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-47.smt2 |   47.488s | 573.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-48.smt2 |   47.533s | 975.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-47.smt2 |   47.572s | 887.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-50.smt2 |   47.636s | 1004.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-14-50.smt2 |   47.755s | 599.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-46.smt2 |   48.011s | 525.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-47.smt2 |   48.136s | 533.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-49.smt2 |   48.286s | 629.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-50.smt2 |   48.305s | 1017.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-13-50.smt2 |   48.485s | 618.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-47.smt2 |   48.756s | 539.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-48.smt2 |   48.761s | 647.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-48.smt2 |   48.942s | 600.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-496324.smt2 |   48.984s | 1515.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-50.smt2 |   49.109s | 1030.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-50.smt2 |   49.202s | 987.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-47.smt2 |   49.318s | 533.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-46.smt2 |   49.656s | 550.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-47.smt2 |   49.734s | 518.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-48.smt2 |   49.775s | 899.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-48.smt2 |   49.922s | 1110.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-50.smt2 |   50.381s | 630.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-48.smt2 |   50.829s | 571.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-48.smt2 |   50.839s | 761.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-47.smt2 |   50.975s | 550.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-49.smt2 |   50.995s | 775.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-48.smt2 |   51.383s | 561.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1145584.smt2 |   51.725s | 3256.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-46.smt2 |   51.953s | 541.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-48.smt2 |   52.042s | 932.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-47.smt2 |   52.317s | 905.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-47.smt2 |   52.793s | 546.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-48.smt2 |   52.917s | 954.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-49.smt2 |   52.965s | 526.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-49.smt2 |   53.077s | 569.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-48.smt2 |   53.410s | 1124.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-48.smt2 |   53.498s | 910.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-41-50.smt2 |   53.564s | 876.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-46.smt2 |   53.618s | 876.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-48.smt2 |   53.695s | 567.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-50.smt2 |   53.997s | 634.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-50.smt2 |   54.418s | 654.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-46.smt2 |   54.461s | 531.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-49.smt2 |   54.488s | 1172.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-48.smt2 |   54.536s | 602.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-48.smt2 |   54.664s | 1107.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-46.smt2 |   54.864s | 739.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-46.smt2 |   55.010s | 737.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-47.smt2 |   55.539s | 567.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-47.smt2 |   55.613s | 533.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-48.smt2 |   55.650s | 1099.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-46.smt2 |   55.759s | 582.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-46.smt2 |   55.966s | 736.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-46.smt2 |   56.242s | 510.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-50.smt2 |   56.399s | 1177.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-47.smt2 |   56.837s | 903.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-48.smt2 |   56.927s | 566.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-47.smt2 |   57.342s | 553.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-50.smt2 |   57.474s | 1178.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-46.smt2 |   57.508s | 551.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-50.smt2 |   57.737s | 1052.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-49.smt2 |   57.771s | 599.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-50.smt2 |   57.773s | 552.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-47.smt2 |   57.860s | 572.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-46.smt2 |   57.931s | 550.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-46.smt2 |   58.301s | 579.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-47.smt2 |   58.584s | 745.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-46.smt2 |   58.882s | 557.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-46.smt2 |   59.165s | 883.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-49.smt2 |   59.183s | 583.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-48.smt2 |   59.211s | 566.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-48.smt2 |   59.253s | 604.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-46.smt2 |   59.277s | 560.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-48.smt2 |   59.712s | 607.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-49.smt2 |   59.988s | 584.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1148089.smt2 |   60.089s | 3019.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-46.smt2 |   60.090s | 878.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-48.smt2 |   60.151s | 579.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-48.smt2 |   60.236s | 577.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-49.smt2 |   60.391s | 569.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-46.smt2 |   60.600s | 569.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-50.smt2 |   60.618s | 591.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-47.smt2 |   60.951s | 549.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-48.smt2 |   61.025s | 1093.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-48.smt2 |   62.002s | 571.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-49.smt2 |   62.510s | 986.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-50.smt2 |   63.058s | 625.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-50.smt2 |   63.062s | 1164.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-48.smt2 |   63.226s | 585.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-49.smt2 |   63.782s | 621.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-46.smt2 |   64.056s | 586.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-48.smt2 |   64.351s | 579.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-46.smt2 |   64.513s | 888.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-49.smt2 |   64.656s | 660.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-50.smt2 |   64.802s | 619.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-49.smt2 |   64.921s | 581.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-50.smt2 |   65.285s | 813.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER11-14-fair.smt2        |   65.517s | 347.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-47.smt2 |   65.773s | 747.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-46.smt2 |   65.778s | 586.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-48.smt2 |   65.941s | 956.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-47.smt2 |   66.105s | 553.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-49.smt2 |   66.272s | 615.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-49.smt2 |   66.302s | 1155.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-48.smt2 |   66.504s | 620.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-48.smt2 |   66.839s | 586.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-49.smt2 |   66.955s | 699.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-49.smt2 |   67.173s | 688.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-50.smt2 |   67.214s | 613.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-47.smt2 |   67.420s | 569.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-48.smt2 |   67.486s | 953.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-50.smt2 |   67.503s | 551.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-50.smt2 |   67.660s | 1210.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-49.smt2 |   68.222s | 621.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-48.smt2 |   68.469s | 967.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-49.smt2 |   68.799s | 578.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-50.smt2 |   68.904s | 832.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-48.smt2 |   69.169s | 587.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-49.smt2 |   69.254s | 621.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-50.smt2 |   69.588s | 602.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-50.smt2 |   69.997s | 817.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-47.smt2 |   70.533s | 749.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-49.smt2 |   70.605s | 633.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-47.smt2 |   70.628s | 1045.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-47.smt2 |   70.678s | 572.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-48.smt2 |   70.684s | 975.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-48.smt2 |   70.862s | 958.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-48.smt2 |   70.965s | 965.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-47.smt2 |   71.059s | 514.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-46.smt2 |   71.166s | 547.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-47.smt2 |   71.952s | 582.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-50.smt2 |   72.107s | 641.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-48.smt2 |   72.358s | 598.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-48.smt2 |   72.891s | 956.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-49.smt2 |   72.891s | 594.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER10-14-fair.smt2        |   72.892s | 335.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-47.smt2 |   73.294s | 540.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-49.smt2 |   73.659s | 617.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-46.smt2 |   73.844s | 567.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-46.smt2 |   74.020s | 561.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/2019-ezsmt/incrementalScheduling/258-incremental_scheduling-40698-0.smt2 |   74.261s | 258.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-48.smt2 |   74.304s | 785.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-49.smt2 |   74.545s | 616.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-48.smt2 |   74.807s | 766.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-46.smt2 |   74.929s | 932.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-46.smt2 |   75.553s | 703.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-50.smt2 |   75.941s | 678.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-50.smt2 |   76.064s | 638.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-50.smt2 |   76.080s | 816.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-49.smt2 |   76.565s | 629.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-49.smt2 |   76.991s | 999.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-47.smt2 |   77.085s | 604.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-48.smt2 |   77.359s | 944.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-49.smt2 |   77.715s | 650.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-46.smt2 |   77.894s | 600.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-49.smt2 |   78.540s | 616.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-48.smt2 |   79.047s | 590.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-50.smt2 |   79.503s | 688.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-50.smt2 |   80.070s | 628.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-614657.smt2 |   80.517s | 2074.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-47.smt2 |   80.891s | 595.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-47.smt2 |   80.950s | 930.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-50.smt2 |   81.107s | 647.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-49.smt2 |   81.249s | 554.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-50.smt2 |   81.528s | 793.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-48.smt2 |   81.975s | 636.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-49.smt2 |   82.290s | 653.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-49.smt2 |   82.344s | 614.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-48.smt2 |   82.878s | 620.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-48.smt2 |   82.952s | 983.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-47.smt2 |   83.360s | 610.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-46.smt2 |   83.582s | 536.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-50.smt2 |   83.705s | 666.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1096871.smt2 |   84.016s | 3828.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-63-50.smt2 |   84.121s | 632.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-408585.smt2  |   84.294s | 1343.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-48.smt2 |   84.985s | 779.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-48.smt2 |   85.234s | 571.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-49.smt2 |   85.463s | 814.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-50.smt2 |   85.895s | 1046.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-47.smt2 |   86.117s | 763.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-48.smt2 |   86.500s | 938.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-50.smt2 |   86.597s | 697.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-47.smt2 |   87.315s | 918.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-48.smt2 |   87.419s | 588.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-49.smt2 |   87.439s | 624.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-47.smt2 |   87.471s | 761.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-49.smt2 |   88.352s | 648.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-50.smt2 |   88.469s | 832.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-47.smt2 |   89.711s | 936.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-50.smt2 |   90.132s | 574.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-50.smt2 |   91.135s | 1042.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-49.smt2 |   91.236s | 819.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-46.smt2 |   92.282s | 517.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-50.smt2 |   92.528s | 681.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-50.smt2 |   93.623s | 713.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-46.smt2 |   93.908s | 614.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-46.smt2 |   93.998s | 906.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-50.smt2 |   94.778s | 675.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-47.smt2 |   95.148s | 614.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-49.smt2 |   95.922s | 1014.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-48.smt2 |   96.590s | 962.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-50.smt2 |   96.816s | 850.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-47.smt2 |   97.719s | 733.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-47.smt2 |   98.323s | 765.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-50.smt2 |   98.692s | 638.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-50.smt2 |   99.770s | 691.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-49.smt2 |   99.962s | 1015.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-50.smt2 |  101.120s | 822.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-50.smt2 |  101.285s | 716.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-50.smt2 |  101.637s | 686.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-50.smt2 |  104.418s | 658.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-46.smt2 |  104.962s | 607.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-50.smt2 |  105.688s | 827.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-47.smt2 |  106.867s | 776.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-50.smt2 |  107.243s | 1059.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-46.smt2 |  107.629s | 1103.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-46.smt2 |  108.870s | 917.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-45.smt2 |  109.479s | 572.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-46.smt2 |  110.042s | 918.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-46.smt2 |  110.411s | 947.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-48.smt2 |  111.672s | 972.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-49.smt2 |  112.979s | 1024.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-50.smt2 |  113.587s | 680.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-47.smt2 |  113.796s | 952.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-47.smt2 |  115.800s | 951.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-48.smt2 |  115.932s | 795.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-46.smt2 |  116.096s | 917.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-46.smt2 |  116.884s | 967.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-48.smt2 |  116.964s | 802.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-46.smt2 |  120.106s | 922.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-50.smt2 |  120.636s | 680.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-47.smt2 |  123.167s | 952.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-46.smt2 |  123.441s | 931.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-46.smt2 |  124.281s | 677.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-46.smt2 |  125.146s | 924.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-47.smt2 |  125.495s | 960.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-47.smt2 |  126.956s | 688.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-46.smt2 |  128.214s | 744.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-47.smt2 |  129.071s | 949.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-49.smt2 |  130.814s | 673.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-48.smt2 |  131.091s | 648.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-47.smt2 |  133.073s | 1092.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-49.smt2 |  137.090s | 692.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-46.smt2 |  137.960s | 774.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-50.smt2 |  139.146s | 858.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-729964.smt2 |  139.799s | 2933.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-47.smt2 |  141.347s | 960.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-518109.smt2  |  141.711s | 1592.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-50.smt2 |  143.187s | 746.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-46.smt2 |  143.190s | 682.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-48.smt2 |  144.415s | 805.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-47.smt2 |  144.986s | 808.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-47.smt2 |  145.315s | 605.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-46.smt2 |  146.557s | 783.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-569261.smt2  |  146.801s | 2229.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-46.smt2 |  148.639s | 929.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-50.smt2 |  149.214s | 1130.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-394532.smt2 |  149.276s | 1296.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-49.smt2 |  149.519s | 960.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-46.smt2 |  150.186s | 931.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-49.smt2 |  152.740s | 838.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-47.smt2 |  152.929s | 954.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-943653.smt2  |  153.193s | 3837.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1072007.smt2 |  153.788s | 4613.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-49.smt2 |  153.862s | 868.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-48.smt2 |  154.931s | 992.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-495717.smt2 |  155.290s | 1809.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-47.smt2 |  156.195s | 1114.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-48.smt2 |  156.437s | 818.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-48.smt2 |  156.679s | 678.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-50.smt2 |  157.849s | 704.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-46.smt2 |  158.509s | 1133.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-46.smt2 |  158.596s | 780.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-46.smt2 |  159.811s | 633.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-46.smt2 |  161.366s | 946.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-48.smt2 |  162.390s | 1013.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-47.smt2 |  163.055s | 962.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-50.smt2 |  168.605s | 882.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-46.smt2 |  170.041s | 966.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-46.smt2 |  170.359s | 963.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-49.smt2 |  173.836s | 713.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-49.smt2 |  173.931s | 1253.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-49.smt2 |  175.015s | 718.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-49.smt2 |  175.259s | 848.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-47.smt2 |  177.470s | 724.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-47.smt2 |  178.954s | 973.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-50.smt2 |  179.741s | 1099.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-46.smt2 |  180.289s | 983.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-46.smt2 |  181.152s | 633.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-50.smt2 |  181.204s | 1118.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-46.smt2 |  184.337s | 970.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-50.smt2 |  184.840s | 875.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-47.smt2 |  187.401s | 973.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-46.smt2 |  187.759s | 569.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-50.smt2 |  190.524s | 742.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-47.smt2 |  192.218s | 810.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-47.smt2 |  192.748s | 1137.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-47.smt2 |  193.340s | 690.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-49.smt2 |  193.797s | 705.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-47.smt2 |  196.376s | 576.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-48.smt2 |  199.172s | 752.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-50.smt2 |  200.536s | 763.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-50.smt2 |  201.733s | 1028.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-50.smt2 |  201.755s | 739.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-47.smt2 |  205.364s | 1007.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-46.smt2 |  207.842s | 1136.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-47.smt2 |  208.445s | 994.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-48.smt2 |  210.258s | 842.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-49.smt2 |  211.373s | 1069.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-48.smt2 |  212.023s | 1007.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-48.smt2 |  212.040s | 782.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-47.smt2 |  212.295s | 1009.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-46.smt2 |  214.701s | 961.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-49.smt2 |  216.828s | 699.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-48.smt2 |  221.953s | 728.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-50.smt2 |  224.892s | 750.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-47.smt2 |  225.179s | 1000.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-50.smt2 |  225.468s | 918.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-46.smt2 |  232.857s | 998.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-654327.smt2  |  235.934s | 2800.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-48.smt2 |  238.464s | 1028.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-49.smt2 |  239.100s | 881.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-49.smt2 |  242.107s | 1035.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-49.smt2 |  242.929s | 809.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-50.smt2 |  244.587s | 1065.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-47.smt2 |  245.655s | 992.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-47.smt2 |  249.245s | 1003.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-47.smt2 |  249.249s | 835.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-48.smt2 |  249.570s | 710.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-47.smt2 |  253.231s | 1162.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-46.smt2 |  254.100s | 982.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-50.smt2 |  254.980s | 1134.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-50.smt2 |  255.228s | 1167.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-49.smt2 |  258.677s | 1085.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-49.smt2 |  259.070s | 875.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-50.smt2 |  261.360s | 920.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-47.smt2 |  261.609s | 683.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-47.smt2 |  263.569s | 828.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-49.smt2 |  263.951s | 1090.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-46.smt2 |  265.664s | 833.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-49.smt2 |  266.850s | 813.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-47.smt2 |  269.506s | 1027.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-47.smt2 |  269.757s | 667.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-47.smt2 |  270.984s | 722.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-48.smt2 |  271.011s | 1034.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-48.smt2 |  272.770s | 693.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-50.smt2 |  274.631s | 918.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-48.smt2 |  275.840s | 698.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-48.smt2 |  277.075s | 1024.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-48.smt2 |  277.843s | 713.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-50.smt2 |  282.144s | 930.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-49.smt2 |  282.576s | 1097.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-46.smt2 |  283.786s | 977.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-46.smt2 |  284.061s | 1157.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-658040.smt2 |  292.919s | 2757.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-49.smt2 |  293.868s | 1120.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-50.smt2 |  294.482s | 1316.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-47.smt2 |  294.578s | 1046.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-49.smt2 |  298.093s | 1092.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-46.smt2 |  300.892s | 1018.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-50.smt2 |  300.902s | 950.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-49.smt2 |  303.024s | 755.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-47.smt2 |  304.307s | 1047.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-46.smt2 |  309.174s | 843.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-48.smt2 |  310.386s | 1048.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-50.smt2 |  312.518s | 1175.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-479884.smt2 |  317.607s | 1708.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-687179.smt2 |  317.723s | 2224.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-46.smt2 |  320.683s | 1026.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-49.smt2 |  324.038s | 915.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-49.smt2 |  325.073s | 911.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-48.smt2 |  325.156s | 1038.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-551279.smt2  |  327.670s | 2212.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-49.smt2 |  330.684s | 820.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-47.smt2 |  331.277s | 1005.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-49.smt2 |  331.922s | 1157.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-50.smt2 |  332.555s | 1184.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER11-15-fair.smt2        |  335.443s | 444.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-47.smt2 |  336.510s | 1037.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-50.smt2 |  336.963s | 787.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-49.smt2 |  337.844s | 768.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-49.smt2 |  339.308s | 1152.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-50.smt2 |  347.069s | 1147.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-50.smt2 |  347.382s | 1194.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-47.smt2 |  348.056s | 698.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-46.smt2 |  348.528s | 1002.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-50.smt2 |  350.689s | 1160.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-48.smt2 |  352.646s | 1210.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-47.smt2 |  354.251s | 901.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-47.smt2 |  356.439s | 722.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-50.smt2 |  358.027s | 1249.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-49.smt2 |  358.601s | 1148.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-48.smt2 |  359.741s | 1059.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-49.smt2 |  362.740s | 1118.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1000539.smt2 |  368.466s | 4317.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-47.smt2 |  368.870s | 1035.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-416752.smt2 |  369.546s | 1511.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-46.smt2 |  369.937s | 991.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-48.smt2 |  374.242s | 1000.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-645855.smt2 |  375.655s | 2614.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-48.smt2 |  384.280s | 726.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-478122.smt2  |  388.492s | 1929.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-49.smt2 |  389.965s | 1129.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-49.smt2 |  391.211s | 766.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-49.smt2 |  394.884s | 1177.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-49.smt2 |  399.661s | 1137.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-50.smt2 |  403.510s | 953.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-49.smt2 |  405.583s | 1134.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-50.smt2 |  405.693s | 966.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-47.smt2 |  409.097s | 1070.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-50.smt2 |  409.718s | 1199.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-47.smt2 |  410.397s | 970.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-48.smt2 |  414.097s | 980.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-48.smt2 |  418.320s | 1058.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-50.smt2 |  419.292s | 788.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-696340.smt2 |  420.563s | 3037.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-46.smt2 |  432.889s | 704.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-50.smt2 |  433.857s | 1211.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-48.smt2 |  434.245s | 750.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-48.smt2 |  435.733s | 1082.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-50.smt2 |  436.674s | 1181.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-49.smt2 |  450.975s | 775.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-50.smt2 |  459.190s | 1176.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-50.smt2 |  466.800s | 1223.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-47.smt2 |  475.806s | 1064.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-49.smt2 |  480.035s | 1186.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-49.smt2 |  486.830s | 1198.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-49.smt2 |  493.860s | 1151.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-49.smt2 |  496.856s | 1353.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-50.smt2 |  500.049s | 1285.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-391798.smt2  |  502.648s | 1369.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-49.smt2 |  503.497s | 1160.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-50.smt2 |  504.008s | 890.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-49.smt2 |  506.382s | 1376.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-49.smt2 |  510.177s | 1159.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-49.smt2 |  511.719s | 1203.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-47.smt2 |  513.035s | 1210.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-49.smt2 |  521.217s | 934.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-50.smt2 |  531.186s | 1303.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-603294.smt2 |  537.477s | 2139.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-49.smt2 |  537.477s | 1350.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-49.smt2 |  543.838s | 1113.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-49.smt2 |  560.730s | 1234.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-49.smt2 |  567.369s | 1168.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-50.smt2 |  581.618s | 1193.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-762853.smt2 |  599.202s | 3798.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-983194.smt2 |  599.907s | 5167.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_18.txt.smt2               |  600.080s | 447.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/2019-ezsmt/incrementalScheduling/295-incremental_scheduling-40626-0.smt2 |  600.097s | 291.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_9.txt.smt2                |  600.104s | 471.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_15.txt.smt2               |  600.111s | 467.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-47.smt2 |  600.116s | 801.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-48.smt2 |  600.129s | 766.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-50.smt2 |  600.136s | 824.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-50.smt2 |  600.149s | 1211.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-49.smt2 |  600.155s | 1172.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-50.smt2 |  600.156s | 1236.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-50.smt2 |  600.156s | 1286.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-48.smt2 |  600.158s | 1109.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-50.smt2 |  600.158s | 1202.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-50.smt2 |  600.161s | 996.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-50.smt2 |  600.165s | 1184.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-50.smt2 |  600.165s | 1271.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-48.smt2 |  600.167s | 1140.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-49.smt2 |  600.168s | 1190.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-50.smt2 |  600.177s | 1225.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-49.smt2 |  600.178s | 1171.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-49.smt2 |  600.179s | 1189.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-49.smt2 |  600.180s | 1158.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-50.smt2 |  600.182s | 1214.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-50.smt2 |  600.182s | 1402.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-50.smt2 |  600.182s | 1195.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-50.smt2 |  600.185s | 1408.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-50.smt2 |  600.186s | 1257.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-50.smt2 |  600.188s | 1342.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-49.smt2 |  600.194s | 1307.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-49.smt2 |  600.229s | 1168.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-373262.smt2 |  600.240s | 1291.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-50.smt2 |  600.248s | 1223.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-50.smt2 |  600.260s | 1293.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-50.smt2 |  600.282s | 1199.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-556171.smt2 |  600.304s | 1924.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-579281.smt2 |  600.339s | 2294.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-533042.smt2  |  600.390s | 2263.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-487307.smt2  |  600.399s | 2088.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/20231117-c_inference/80_80_71_17_unsat.smt2 |  600.408s | 2791.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-506600.smt2  |  600.437s | 1938.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-644402.smt2  |  600.475s | 3331.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-687518.smt2  |  600.481s | 3586.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-737829.smt2 |  600.528s | 3718.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-765743.smt2  |  600.530s | 3861.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-655888.smt2  |  600.557s | 3520.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-735583.smt2 |  600.562s | 3822.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-928960.smt2  |  600.566s | 4223.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-740637.smt2 |  600.573s | 3335.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-804609.smt2  |  600.592s | 4329.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-985918.smt2  |  600.626s | 5243.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-863289.smt2  |  600.653s | 4654.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-968440.smt2  |  600.661s | 5049.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-989891.smt2 |  600.661s | 4460.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-851594.smt2 |  600.668s | 4560.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-861420.smt2 |  600.681s | 4633.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-777746.smt2  |  600.689s | 4599.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-715402.smt2 |  600.701s | 3632.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-797738.smt2 |  600.722s | 4000.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-993227.smt2  |  600.725s | 5465.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-902192.smt2  |  600.730s | 4553.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-873799.smt2  |  600.788s | 4583.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-904583.smt2  |  600.807s | 5231.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-985518.smt2  |  600.812s | 5839.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1065256.smt2 |  600.851s | 6309.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1060546.smt2 |  600.855s | 5902.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-987361.smt2  |  600.940s | 4531.0MiB| timeout | 0 |  |  |