# .

* SAT 472
* UNSAT 270
* TIMEOUT 64
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-QF_LIA_hard-timeout10min-bb1
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=1"
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/arctic-matrix/constraint-526410.smt2  |    2.968s | 715.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-14.smt2 |    3.124s | 868.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-03.smt2 |    3.429s | 1290.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-01.smt2 |    3.531s | 2057.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-09.smt2 |    3.559s | 2042.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-10.smt2 |    3.560s | 1697.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-02.smt2 |    3.595s | 2062.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/2019-ezsmt/incrementalScheduling/214-incremental_scheduling-27000-0.smt2 |    3.705s | 270.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-09.smt2 |    3.801s | 1639.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-15.smt2 |    3.859s | 2041.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-12.smt2 |    4.154s | 1991.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-05.smt2 |    4.154s | 1989.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-05.smt2 |    4.172s | 1994.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-04.smt2 |    4.179s | 1976.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-02.smt2 |    4.193s | 2001.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-06.smt2 |    4.233s | 1976.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-14.smt2 |    4.241s | 1979.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-08.smt2 |    4.243s | 1983.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-15.smt2 |    4.287s | 1993.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-07.smt2 |    4.305s | 1977.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-14.smt2 |    4.359s | 820.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-12.smt2 |    4.375s | 1975.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-08.smt2 |    4.436s | 840.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-04.smt2 |    4.549s | 1981.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-08.smt2 |    4.583s | 818.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-11.smt2 |    4.624s | 1983.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-527358.smt2 |    4.693s | 855.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-11.smt2 |    4.757s | 1974.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-01.smt2 |    4.795s | 1977.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-00.smt2 |    4.852s | 1982.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-13.smt2 |    4.922s | 1975.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-15.smt2 |    4.934s | 1257.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-07.smt2 |    5.023s | 2010.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-11.smt2 |    5.040s | 1346.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-06.smt2 |    5.075s | 1979.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-12.smt2 |    5.082s | 1349.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-03.smt2 |    5.317s | 3860.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-10.smt2 |    5.469s | 2974.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-12.smt2 |    5.527s | 4044.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-10.smt2 |    5.754s | 4044.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-00.smt2 |    5.913s | 4201.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-01.smt2 |    6.059s | 4385.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-07.smt2 |    6.065s | 4260.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-02.smt2 |    6.175s | 4346.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-13.smt2 |    6.196s | 4348.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-03.smt2 |    6.231s | 4201.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-11.smt2 |    6.295s | 4332.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-14.smt2 |    6.360s | 4398.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-09.smt2 |    6.370s | 4185.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-15.smt2 |    6.461s | 4343.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-13.smt2 |    6.466s | 4187.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-00.smt2 |    6.593s | 4359.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-649834.smt2 |    6.638s | 1122.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-09.smt2 |    6.788s | 4143.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1007795.smt2 |    7.282s | 1284.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-916576.smt2  |    7.671s | 1262.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-392137.smt2  |    8.420s | 873.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-928134.smt2  |    9.634s | 1513.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-415996.smt2  |   10.187s | 994.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1015084.smt2 |   10.369s | 1523.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-689472.smt2  |   10.541s | 1485.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-916807.smt2 |   10.972s | 1721.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-794687.smt2 |   11.836s | 1651.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-705295.smt2 |   11.881s | 1621.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-47.smt2 |   11.967s | 577.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-47.smt2 |   13.467s | 248.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-901996.smt2 |   13.477s | 1874.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-906218.smt2  |   14.102s | 1728.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-917322.smt2 |   14.264s | 1822.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-47.smt2 |   14.428s | 248.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-758897.smt2 |   14.879s | 1732.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-49.smt2 |   14.899s | 612.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-901628.smt2  |   16.219s | 1737.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-46.smt2 |   16.236s | 599.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-46.smt2 |   16.918s | 623.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-413904.smt2 |   17.048s | 1244.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-48.smt2 |   17.130s | 250.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-864173.smt2  |   17.188s | 2150.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-50.smt2 |   17.316s | 736.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-49.smt2 |   18.840s | 671.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-48.smt2 |   19.020s | 583.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-618384.smt2  |   19.443s | 1620.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-33-50.smt2 |   19.704s | 791.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-17-50.smt2 |   19.720s | 679.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-481231.smt2  |   19.928s | 1385.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-48.smt2 |   19.986s | 692.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-48.smt2 |   19.987s | 693.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-30-50.smt2 |   20.152s | 857.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-5-50.smt2 |   20.372s | 820.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-9-50.smt2 |   20.382s | 797.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-49.smt2 |   20.514s | 620.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-30-48.smt2 |   20.775s | 677.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-48.smt2 |   20.885s | 689.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-45.smt2 |   21.028s | 599.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-16-50.smt2 |   21.289s | 915.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-23-50.smt2 |   22.087s | 848.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-48.smt2 |   22.093s | 613.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-50.smt2 |   22.122s | 699.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-21-50.smt2 |   22.207s | 901.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-31-50.smt2 |   22.337s | 824.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-50.smt2 |   22.477s | 826.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-13-48.smt2 |   22.494s | 675.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-14-50.smt2 |   22.607s | 871.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER10-13-fair.smt2        |   22.622s | 321.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-48.smt2 |   22.701s | 686.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-17-50.smt2 |   22.704s | 822.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-34-45.smt2 |   22.792s | 628.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-47.smt2 |   22.924s | 636.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-37-50.smt2 |   23.043s | 896.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-50.smt2 |   23.087s | 918.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-2-50.smt2 |   23.133s | 871.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1107622.smt2 |   23.290s | 2816.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-19-50.smt2 |   23.327s | 824.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-49.smt2 |   23.734s | 714.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-50.smt2 |   23.762s | 918.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1192684.smt2 |   23.984s | 2522.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-42-50.smt2 |   24.062s | 866.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-59-50.smt2 |   24.083s | 846.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-13-50.smt2 |   24.265s | 845.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-60-50.smt2 |   24.643s | 870.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-40-50.smt2 |   24.644s | 839.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-32-50.smt2 |   24.844s | 839.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-48.smt2 |   24.945s | 609.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1185949.smt2 |   25.014s | 2457.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-46-50.smt2 |   25.179s | 831.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-45-50.smt2 |   25.565s | 858.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-50.smt2 |   25.645s | 928.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-20-45.smt2 |   25.682s | 779.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-48-50.smt2 |   25.907s | 865.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-50.smt2 |   26.346s | 863.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-408585.smt2  |   26.408s | 1356.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-45.smt2 |   26.766s | 701.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-45.smt2 |   27.041s | 628.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-70-50.smt2 |   27.128s | 855.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-64-50.smt2 |   28.395s | 875.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-65-50.smt2 |   28.416s | 875.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-46.smt2 |   28.487s | 932.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-49.smt2 |   28.639s | 651.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-34-48.smt2 |   28.752s | 713.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-17-47.smt2 |   28.824s | 707.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-49.smt2 |   29.315s | 711.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1121941.smt2 |   29.377s | 2462.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-46.smt2 |   29.591s | 874.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-46.smt2 |   29.893s | 972.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-49.smt2 |   29.923s | 812.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-46.smt2 |   29.992s | 892.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-67-50.smt2 |   30.178s | 890.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-50.smt2 |   30.208s | 938.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-46.smt2 |   30.270s | 900.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-46.smt2 |   30.906s | 911.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-69-50.smt2 |   30.913s | 876.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-47.smt2 |   30.920s | 730.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-45.smt2 |   30.941s | 724.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-46.smt2 |   31.083s | 718.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-45.smt2 |   31.216s | 675.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-50.smt2 |   31.293s | 863.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-46.smt2 |   31.465s | 719.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-46.smt2 |   31.546s | 954.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-50.smt2 |   31.660s | 859.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-46.smt2 |   31.789s | 973.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-50.smt2 |   31.944s | 816.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-68-50.smt2 |   32.192s | 882.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-48.smt2 |   32.257s | 758.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-48.smt2 |   32.594s | 788.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-45.smt2 |   32.867s | 650.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-47.smt2 |   33.097s | 1103.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-46.smt2 |   33.125s | 1042.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-14-49.smt2 |   33.188s | 748.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-47.smt2 |   33.371s | 927.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-45.smt2 |   33.425s | 710.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-46.smt2 |   33.468s | 717.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-46.smt2 |   33.488s | 914.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-47.smt2 |   33.618s | 925.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-47.smt2 |   33.861s | 707.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-19-49.smt2 |   33.864s | 806.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-47.smt2 |   33.941s | 953.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-48.smt2 |   33.985s | 848.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-29-48.smt2 |   33.987s | 816.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-50.smt2 |   34.449s | 878.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-50.smt2 |   34.465s | 960.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-45.smt2 |   34.708s | 717.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-58-50.smt2 |   34.879s | 900.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-50.smt2 |   34.903s | 823.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-48.smt2 |   34.907s | 925.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-47.smt2 |   35.058s | 926.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-49.smt2 |   35.093s | 762.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-47.smt2 |   35.125s | 729.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-63-50.smt2 |   35.254s | 1006.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-47.smt2 |   35.446s | 927.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-46.smt2 |   35.565s | 946.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-47.smt2 |   35.614s | 922.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-47.smt2 |   35.644s | 1068.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-47.smt2 |   35.685s | 945.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-47.smt2 |   36.113s | 873.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-46.smt2 |   36.356s | 640.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-46.smt2 |   36.507s | 1079.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-47.smt2 |   36.617s | 959.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-47.smt2 |   36.820s | 751.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-50.smt2 |   36.932s | 883.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-29-50.smt2 |   37.047s | 819.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-45.smt2 |   37.088s | 696.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-48.smt2 |   37.113s | 683.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-47.smt2 |   37.115s | 972.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-45.smt2 |   37.326s | 795.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-49.smt2 |   37.452s | 873.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-33-50.smt2 |   37.471s | 826.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-47.smt2 |   37.481s | 1056.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-49.smt2 |   37.520s | 842.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-46.smt2 |   37.604s | 1071.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-50.smt2 |   37.648s | 954.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-906586.smt2 |   37.660s | 2942.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-45.smt2 |   37.722s | 754.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-45.smt2 |   37.763s | 749.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-45.smt2 |   38.234s | 734.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-49.smt2 |   38.395s | 817.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-47.smt2 |   38.592s | 722.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-46.smt2 |   38.940s | 761.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-46.smt2 |   39.363s | 1138.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-46.smt2 |   39.442s | 750.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-45.smt2 |   39.531s | 708.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-39-50.smt2 |   39.584s | 959.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-48.smt2 |   39.716s | 837.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-47.smt2 |   39.738s | 1282.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-46.smt2 |   39.838s | 1310.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-48.smt2 |   39.994s | 1125.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-50.smt2 |   40.303s | 772.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-48.smt2 |   40.335s | 1041.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-45.smt2 |   40.368s | 729.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-50.smt2 |   40.403s | 877.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-50.smt2 |   40.606s | 974.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-46.smt2 |   40.637s | 778.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-50.smt2 |   40.792s | 965.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-45.smt2 |   41.053s | 790.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-50.smt2 |   41.077s | 993.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-24-49.smt2 |   41.521s | 882.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-45.smt2 |   41.539s | 721.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-47.smt2 |   41.676s | 1306.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-49.smt2 |   42.059s | 1035.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-46.smt2 |   42.293s | 1372.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-47.smt2 |   42.303s | 847.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-48.smt2 |   42.343s | 1216.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-46.smt2 |   42.365s | 1347.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-14-50.smt2 |   42.621s | 811.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-48.smt2 |   42.626s | 1019.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-48.smt2 |   42.666s | 1322.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-48.smt2 |   42.691s | 1069.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-19-50.smt2 |   42.708s | 881.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-49.smt2 |   42.838s | 977.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-46.smt2 |   43.018s | 797.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-48.smt2 |   43.406s | 1094.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-49.smt2 |   43.454s | 1025.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-49.smt2 |   43.469s | 1019.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-47.smt2 |   43.479s | 1066.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-46.smt2 |   43.685s | 1321.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-46.smt2 |   43.700s | 758.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-46.smt2 |   43.776s | 874.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-48.smt2 |   43.956s | 1355.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-48.smt2 |   43.996s | 1158.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-46.smt2 |   44.345s | 1516.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-50.smt2 |   44.439s | 921.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-50.smt2 |   44.567s | 872.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-50.smt2 |   44.625s | 901.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-50.smt2 |   44.649s | 858.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-45.smt2 |   44.957s | 760.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-45.smt2 |   45.044s | 782.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-47.smt2 |   45.362s | 763.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-47.smt2 |   45.529s | 779.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-48.smt2 |   45.544s | 996.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-48.smt2 |   45.893s | 1031.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-48.smt2 |   46.042s | 1154.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-48.smt2 |   46.074s | 795.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-496324.smt2 |   46.295s | 1689.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-46.smt2 |   46.882s | 794.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-50.smt2 |   47.057s | 864.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-49.smt2 |   47.223s | 1163.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-48.smt2 |   47.426s | 849.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-49.smt2 |   47.490s | 1175.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-46.smt2 |   47.710s | 774.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-48.smt2 |   47.776s | 1255.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-47.smt2 |   47.879s | 834.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-45.smt2 |   47.932s | 757.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-49.smt2 |   48.165s | 1140.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-49.smt2 |   48.323s | 1143.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-48.smt2 |   48.353s | 1230.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-48.smt2 |   48.478s | 1164.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER11-14-fair.smt2        |   48.520s | 367.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-46.smt2 |   48.545s | 777.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-47.smt2 |   48.761s | 859.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-41-50.smt2 |   48.894s | 932.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-47.smt2 |   48.931s | 850.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-47.smt2 |   49.057s | 798.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-47.smt2 |   49.168s | 812.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-49.smt2 |   49.771s | 1063.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-49.smt2 |   49.839s | 1145.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-48.smt2 |   49.892s | 851.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-46.smt2 |   50.170s | 1143.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-48.smt2 |   50.207s | 1197.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-50.smt2 |   50.280s | 1151.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1145584.smt2 |   50.281s | 3644.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-49.smt2 |   50.782s | 1077.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-49.smt2 |   50.793s | 1342.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-50.smt2 |   50.799s | 1166.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-47.smt2 |   50.883s | 1255.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-50.smt2 |   51.328s | 1072.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-48.smt2 |   51.447s | 1399.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-50.smt2 |   51.595s | 1123.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-48.smt2 |   51.751s | 1569.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-50.smt2 |   51.793s | 891.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-50.smt2 |   51.883s | 770.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-47.smt2 |   51.917s | 777.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-47.smt2 |   51.932s | 780.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-49.smt2 |   51.952s | 1033.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-48.smt2 |   52.561s | 871.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-50.smt2 |   52.700s | 1129.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-46.smt2 |   52.914s | 1389.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-49.smt2 |   53.118s | 1471.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-49.smt2 |   53.222s | 1479.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-48.smt2 |   53.665s | 1289.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-50.smt2 |   53.850s | 899.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-46.smt2 |   53.999s | 1403.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-48.smt2 |   54.297s | 820.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-46.smt2 |   54.449s | 1428.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-48.smt2 |   54.497s | 1558.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-49.smt2 |   54.561s | 991.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-47.smt2 |   54.609s | 1383.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-48.smt2 |   54.631s | 823.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-50.smt2 |   54.642s | 1279.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-46.smt2 |   54.809s | 1039.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-48.smt2 |   55.024s | 1247.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-48.smt2 |   55.201s | 1562.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-50.smt2 |   55.235s | 1324.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-48.smt2 |   55.602s | 1282.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-48.smt2 |   55.843s | 961.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-50.smt2 |   56.146s | 1132.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-48.smt2 |   56.258s | 1386.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-48.smt2 |   56.439s | 799.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-47.smt2 |   56.968s | 822.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-47.smt2 |   57.081s | 858.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-47.smt2 |   57.195s | 838.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-46.smt2 |   57.579s | 984.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-47.smt2 |   57.629s | 811.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-47.smt2 |   57.920s | 816.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-48.smt2 |   58.019s | 832.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1148089.smt2 |   58.069s | 3325.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-48.smt2 |   58.415s | 1618.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-50.smt2 |   58.570s | 964.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-46.smt2 |   58.573s | 840.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-49.smt2 |   58.660s | 1225.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-49.smt2 |   59.353s | 866.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-50.smt2 |   59.538s | 1502.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-50.smt2 |   59.697s | 848.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-46.smt2 |   60.005s | 856.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-46.smt2 |   60.260s | 1093.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-47.smt2 |   60.463s | 989.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-48.smt2 |   60.615s | 1043.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-49.smt2 |   60.773s | 921.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-48.smt2 |   60.939s | 1402.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-46.smt2 |   61.049s | 1144.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-48.smt2 |   61.150s | 1422.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-46.smt2 |   61.161s | 1167.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-50.smt2 |   61.247s | 1149.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-46.smt2 |   61.331s | 881.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-50.smt2 |   61.387s | 1488.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-48.smt2 |   61.741s | 932.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-46.smt2 |   61.862s | 1031.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-47.smt2 |   62.063s | 825.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-49.smt2 |   62.215s | 847.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/2019-ezsmt/incrementalScheduling/258-incremental_scheduling-40698-0.smt2 |   62.339s | 286.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-50.smt2 |   62.401s | 1024.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-50.smt2 |   62.705s | 1342.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-46.smt2 |   62.717s | 761.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-49.smt2 |   63.035s | 1643.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-48.smt2 |   63.078s | 1453.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-49.smt2 |   63.156s | 885.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-48.smt2 |   63.449s | 807.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-48.smt2 |   63.573s | 1234.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-47.smt2 |   63.587s | 1175.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-48.smt2 |   63.726s | 1013.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-49.smt2 |   63.827s | 891.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-49.smt2 |   63.829s | 924.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-49.smt2 |   63.929s | 906.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-49.smt2 |   63.990s | 917.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-46.smt2 |   64.527s | 852.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-48.smt2 |   65.562s | 1201.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-48.smt2 |   66.164s | 1499.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-47.smt2 |   66.317s | 968.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-47.smt2 |   66.588s | 1002.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-50.smt2 |   66.794s | 1103.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-49.smt2 |   67.404s | 891.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER10-14-fair.smt2        |   67.431s | 357.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-48.smt2 |   67.940s | 1039.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-48.smt2 |   68.201s | 1023.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-49.smt2 |   68.242s | 899.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-50.smt2 |   68.743s | 877.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-46.smt2 |   68.916s | 1469.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-46.smt2 |   69.059s | 1035.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-48.smt2 |   69.270s | 1025.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-47.smt2 |   69.448s | 873.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-49.smt2 |   69.473s | 1327.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-48.smt2 |   69.677s | 836.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-49.smt2 |   70.283s | 890.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-47.smt2 |   70.284s | 1039.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-49.smt2 |   70.654s | 920.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-47.smt2 |   71.021s | 1383.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-49.smt2 |   71.073s | 1025.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-48.smt2 |   71.223s | 861.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-46.smt2 |   71.526s | 899.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-49.smt2 |   71.604s | 968.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-729964.smt2 |   72.167s | 2953.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-50.smt2 |   72.363s | 966.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-46.smt2 |   72.603s | 866.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-48.smt2 |   73.076s | 1580.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-48.smt2 |   73.241s | 1153.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-47.smt2 |   73.293s | 1661.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-46.smt2 |   73.545s | 860.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-48.smt2 |   73.877s | 1405.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-49.smt2 |   74.457s | 1053.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-50.smt2 |   75.130s | 922.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-47.smt2 |   75.473s | 889.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-46.smt2 |   75.593s | 842.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-48.smt2 |   75.623s | 1466.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-49.smt2 |   75.842s | 947.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-49.smt2 |   75.867s | 1623.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-50.smt2 |   76.274s | 1088.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-50.smt2 |   76.473s | 1059.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-48.smt2 |   76.562s | 1417.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-49.smt2 |   77.068s | 1643.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-49.smt2 |   77.308s | 1036.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-47.smt2 |   77.480s | 1201.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-50.smt2 |   77.573s | 1370.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-48.smt2 |   77.701s | 1086.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-48.smt2 |   77.914s | 1034.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-50.smt2 |   77.970s | 1547.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-614657.smt2 |   78.398s | 2351.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-47.smt2 |   78.698s | 1001.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-49.smt2 |   78.700s | 1104.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-50.smt2 |   78.908s | 1074.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-47.smt2 |   79.084s | 1500.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-49.smt2 |   79.294s | 1044.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-25-50.smt2 |   79.331s | 1103.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-50.smt2 |   80.030s | 1510.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-47.smt2 |   80.052s | 1235.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1096871.smt2 |   80.061s | 4259.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-50.smt2 |   80.381s | 1096.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-50.smt2 |   80.405s | 1137.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-48.smt2 |   80.653s | 866.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-49.smt2 |   81.095s | 938.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-518109.smt2  |   81.410s | 1653.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-48.smt2 |   81.697s | 1038.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-13-50.smt2 |   81.798s | 951.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-49.smt2 |   82.565s | 1053.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-47.smt2 |   82.811s | 1035.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-50.smt2 |   83.503s | 1089.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-47.smt2 |   85.838s | 1240.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-48.smt2 |   86.641s | 1906.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-50.smt2 |   86.881s | 1102.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-49.smt2 |   87.110s | 1030.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-46.smt2 |   87.722s | 897.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-46.smt2 |   87.981s | 1348.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-50.smt2 |   88.047s | 973.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-50.smt2 |   88.970s | 1104.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-48.smt2 |   88.971s | 1039.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-63-50.smt2 |   89.374s | 1088.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-50.smt2 |   89.547s | 1192.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-50.smt2 |   89.625s | 932.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-48.smt2 |   89.702s | 1589.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-46.smt2 |   89.818s | 1149.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-49.smt2 |   90.411s | 1081.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-46.smt2 |   90.963s | 1021.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-49.smt2 |   92.996s | 1245.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-50.smt2 |   93.261s | 1339.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-50.smt2 |   94.353s | 1504.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-49.smt2 |   94.359s | 1056.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-47.smt2 |   94.416s | 1037.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-50.smt2 |   95.286s | 1125.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-47.smt2 |   95.316s | 1415.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-48.smt2 |   95.666s | 1880.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-48.smt2 |   96.328s | 1087.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-46.smt2 |   96.530s | 974.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-50.smt2 |   96.609s | 1077.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-50.smt2 |   97.061s | 1337.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-50.smt2 |   97.130s | 982.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-47.smt2 |   97.552s | 1501.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-50.smt2 |   98.038s | 1157.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-45.smt2 |   98.411s | 1044.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-50.smt2 |   99.442s | 1101.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-46.smt2 |  102.179s | 1162.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-48.smt2 |  102.992s | 1274.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-48.smt2 |  103.661s | 1153.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-46.smt2 |  106.118s | 1124.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-49.smt2 |  106.172s | 1230.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-48.smt2 |  106.188s | 1044.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-48.smt2 |  106.386s | 1260.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-48.smt2 |  106.555s | 1237.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-46.smt2 |  106.634s | 1109.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-50.smt2 |  107.042s | 1024.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-47.smt2 |  107.382s | 1656.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-46.smt2 |  107.893s | 1153.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-50.smt2 |  109.377s | 1141.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-47.smt2 |  110.425s | 1199.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-49.smt2 |  111.026s | 1976.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-46.smt2 |  111.463s | 1246.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-48.smt2 |  112.246s | 1076.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-48.smt2 |  112.342s | 1295.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-47.smt2 |  112.806s | 1938.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-50.smt2 |  115.277s | 966.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-50.smt2 |  116.283s | 1273.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-50.smt2 |  116.582s | 1160.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-46.smt2 |  117.931s | 1806.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-50.smt2 |  118.035s | 2165.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-46.smt2 |  118.892s | 1152.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-48.smt2 |  119.023s | 1405.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-50.smt2 |  120.266s | 1060.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-50.smt2 |  122.047s | 1264.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-47.smt2 |  122.609s | 1047.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-46.smt2 |  122.787s | 1270.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-47.smt2 |  122.847s | 1851.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-47.smt2 |  123.032s | 1076.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-46.smt2 |  123.252s | 1936.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-47.smt2 |  125.290s | 1598.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-47.smt2 |  126.718s | 1272.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-50.smt2 |  129.227s | 1051.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-46.smt2 |  129.293s | 1199.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-47.smt2 |  130.525s | 1407.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-50.smt2 |  130.770s | 1781.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-49.smt2 |  131.809s | 1326.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-50.smt2 |  131.869s | 1203.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-49.smt2 |  132.081s | 1983.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-50.smt2 |  132.699s | 1310.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-48.smt2 |  133.313s | 1660.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-47.smt2 |  133.438s | 1534.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-47.smt2 |  134.655s | 2102.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-50.smt2 |  134.874s | 1340.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-48.smt2 |  135.978s | 1306.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-47.smt2 |  136.166s | 1894.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-46.smt2 |  136.332s | 2169.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-50.smt2 |  141.729s | 1372.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-47.smt2 |  141.961s | 1170.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-47.smt2 |  142.268s | 1976.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-48.smt2 |  143.144s | 1394.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-47.smt2 |  143.351s | 1364.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-551279.smt2  |  144.081s | 2357.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-46.smt2 |  144.091s | 1223.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-47.smt2 |  144.281s | 1219.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-50.smt2 |  144.953s | 1731.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-46.smt2 |  145.674s | 1152.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-391798.smt2  |  147.402s | 1470.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-46.smt2 |  148.013s | 1422.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1072007.smt2 |  148.490s | 5346.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-47.smt2 |  148.678s | 1864.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-50.smt2 |  150.473s | 1653.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-49.smt2 |  151.227s | 1076.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-47.smt2 |  154.793s | 1533.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-46.smt2 |  156.036s | 1288.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-47.smt2 |  156.155s | 1444.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-47.smt2 |  156.196s | 1515.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-47.smt2 |  156.696s | 1693.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-47.smt2 |  158.339s | 2025.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-495717.smt2 |  158.874s | 2033.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-49.smt2 |  160.353s | 1612.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-46.smt2 |  161.440s | 1630.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-48.smt2 |  162.146s | 1585.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-46.smt2 |  162.681s | 1435.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-46.smt2 |  162.767s | 1265.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-50.smt2 |  163.904s | 2092.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-48.smt2 |  165.488s | 1659.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-49.smt2 |  166.472s | 1297.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-47.smt2 |  167.414s | 1939.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-46.smt2 |  168.688s | 2069.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-50.smt2 |  170.420s | 2315.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-49.smt2 |  172.996s | 1705.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-47.smt2 |  174.201s | 1423.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-48.smt2 |  174.896s | 1328.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-48.smt2 |  174.905s | 1364.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-46.smt2 |  175.382s | 1510.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-48.smt2 |  176.742s | 1197.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-46.smt2 |  176.814s | 1233.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-48.smt2 |  177.038s | 1662.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-47.smt2 |  177.082s | 1349.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-50.smt2 |  178.486s | 1250.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-48.smt2 |  178.835s | 1483.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-47.smt2 |  180.098s | 1567.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-46.smt2 |  181.107s | 1102.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-47.smt2 |  181.267s | 1495.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-49.smt2 |  183.786s | 1504.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-46.smt2 |  184.070s | 1213.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-47.smt2 |  190.384s | 2257.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-479884.smt2 |  195.092s | 1853.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-46.smt2 |  196.133s | 1402.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-48.smt2 |  196.482s | 1630.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-47.smt2 |  199.293s | 1508.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-50.smt2 |  204.282s | 2168.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-49.smt2 |  204.779s | 1633.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-46.smt2 |  205.152s | 1159.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER11-15-fair.smt2        |  206.510s | 449.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-49.smt2 |  208.607s | 1417.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-46.smt2 |  209.731s | 1583.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-47.smt2 |  209.941s | 1106.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-46.smt2 |  210.058s | 1694.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-46.smt2 |  211.844s | 1285.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-46.smt2 |  212.313s | 1450.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-47.smt2 |  213.053s | 1271.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-48.smt2 |  213.468s | 1691.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-49.smt2 |  213.737s | 1676.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-46.smt2 |  214.004s | 1564.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-46.smt2 |  214.122s | 1781.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-49.smt2 |  215.897s | 2443.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-416752.smt2 |  216.558s | 1670.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-47.smt2 |  217.963s | 1558.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-46.smt2 |  219.135s | 1274.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-48.smt2 |  219.685s | 1879.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-49.smt2 |  219.756s | 2230.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-654327.smt2  |  221.138s | 3141.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-47.smt2 |  221.309s | 1704.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-49.smt2 |  222.738s | 1693.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-603294.smt2 |  226.734s | 2274.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-762853.smt2 |  226.830s | 3856.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-46.smt2 |  230.296s | 1405.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-47.smt2 |  231.269s | 1590.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-50.smt2 |  234.183s | 1616.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-50.smt2 |  235.843s | 2064.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-46.smt2 |  237.660s | 2073.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-46.smt2 |  238.859s | 1649.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-49.smt2 |  239.092s | 1287.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-49.smt2 |  241.341s | 1286.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-50.smt2 |  241.719s | 1631.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-48.smt2 |  242.395s | 1609.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-47.smt2 |  243.565s | 2491.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-47.smt2 |  243.682s | 1314.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-46.smt2 |  244.580s | 1405.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-47.smt2 |  245.197s | 1615.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-50.smt2 |  254.083s | 2462.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-47.smt2 |  258.419s | 1525.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-48.smt2 |  261.529s | 1624.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-47.smt2 |  262.032s | 2195.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-48.smt2 |  262.423s | 1912.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-49.smt2 |  263.941s | 3078.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-49.smt2 |  266.075s | 2353.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-48.smt2 |  266.714s | 1490.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-50.smt2 |  269.460s | 2340.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-49.smt2 |  274.583s | 1493.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-47.smt2 |  278.472s | 2796.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-46.smt2 |  278.851s | 1413.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-47.smt2 |  281.134s | 2804.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-658040.smt2 |  281.377s | 3114.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-49.smt2 |  281.504s | 1603.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-47.smt2 |  283.501s | 1469.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-47.smt2 |  286.118s | 2150.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-50.smt2 |  290.263s | 2097.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-48.smt2 |  290.699s | 1448.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-50.smt2 |  293.850s | 3008.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-50.smt2 |  294.168s | 2284.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-47.smt2 |  294.267s | 1892.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-46.smt2 |  297.136s | 1513.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-50.smt2 |  299.845s | 1774.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-46.smt2 |  300.114s | 1470.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-49.smt2 |  307.494s | 2039.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-687179.smt2 |  307.931s | 2544.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-47.smt2 |  308.313s | 1562.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-49.smt2 |  310.995s | 1626.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-48.smt2 |  314.902s | 1684.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-50.smt2 |  316.871s | 2320.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-47.smt2 |  319.984s | 1814.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-47.smt2 |  321.249s | 1655.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-50.smt2 |  323.002s | 2219.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-49.smt2 |  324.543s | 1690.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-49.smt2 |  325.898s | 1676.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-48.smt2 |  326.758s | 2242.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-50.smt2 |  328.421s | 1921.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-49.smt2 |  328.718s | 3186.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-48.smt2 |  332.478s | 1511.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-50.smt2 |  332.637s | 2288.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-50.smt2 |  333.696s | 1741.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-50.smt2 |  336.426s | 1758.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-50.smt2 |  339.987s | 1583.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-50.smt2 |  340.975s | 1802.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-49.smt2 |  342.362s | 2116.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-46.smt2 |  347.169s | 1688.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-47.smt2 |  349.854s | 1436.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-50.smt2 |  350.047s | 1617.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-49.smt2 |  352.467s | 3117.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-50.smt2 |  355.221s | 1469.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1000539.smt2 |  355.566s | 4784.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-46.smt2 |  357.692s | 1617.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-47.smt2 |  358.692s | 3101.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-49.smt2 |  361.340s | 3118.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-49.smt2 |  367.263s | 3169.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-49.smt2 |  367.980s | 1520.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-50.smt2 |  370.330s | 1939.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-49.smt2 |  371.880s | 1761.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-49.smt2 |  371.896s | 2234.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-48.smt2 |  372.119s | 1561.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-50.smt2 |  376.345s | 2378.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-478122.smt2  |  377.737s | 2166.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-50.smt2 |  379.894s | 2055.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-49.smt2 |  381.503s | 1625.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-49.smt2 |  383.980s | 1949.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-49.smt2 |  384.287s | 3058.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-50.smt2 |  391.893s | 1645.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-48.smt2 |  397.732s | 1971.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-47.smt2 |  398.225s | 1516.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-49.smt2 |  398.887s | 1758.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-49.smt2 |  403.607s | 2251.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-49.smt2 |  403.621s | 2279.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-48.smt2 |  406.730s | 2235.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-49.smt2 |  410.915s | 2091.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-50.smt2 |  413.981s | 3018.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-46.smt2 |  416.032s | 1942.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-48.smt2 |  419.635s | 2211.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-50.smt2 |  422.426s | 1677.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-50.smt2 |  423.118s | 2626.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-50.smt2 |  430.612s | 1175.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-48.smt2 |  440.217s | 1340.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-49.smt2 |  446.320s | 1628.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-50.smt2 |  456.909s | 2406.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-49.smt2 |  468.306s | 2373.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-49.smt2 |  468.720s | 3105.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-49.smt2 |  468.790s | 1871.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-50.smt2 |  478.642s | 2368.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-48.smt2 |  479.221s | 1940.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-928960.smt2  |  480.166s | 4556.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-49.smt2 |  483.373s | 1937.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-48.smt2 |  493.190s | 1918.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-47.smt2 |  495.372s | 3117.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-48.smt2 |  495.908s | 2379.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-49.smt2 |  497.752s | 1755.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-50.smt2 |  499.409s | 3281.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-50.smt2 |  503.278s | 2242.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-49.smt2 |  503.522s | 2340.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-49.smt2 |  506.912s | 2897.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-394532.smt2 |  513.606s | 1550.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-50.smt2 |  518.157s | 2161.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-49.smt2 |  527.382s | 3016.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-50.smt2 |  538.165s | 2131.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-49.smt2 |  546.484s | 1758.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-49.smt2 |  547.093s | 2191.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-50.smt2 |  556.738s | 2337.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-804609.smt2  |  571.368s | 4796.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-50.smt2 |  571.958s | 2193.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-49.smt2 |  575.767s | 3115.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-373262.smt2 |  584.995s | 1446.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-50.smt2 |  595.725s | 1173.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_18.txt.smt2               |  600.098s | 526.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/2019-ezsmt/incrementalScheduling/295-incremental_scheduling-40626-0.smt2 |  600.102s | 320.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_9.txt.smt2                |  600.119s | 510.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_15.txt.smt2               |  600.139s | 527.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-48.smt2 |  600.153s | 1441.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-50.smt2 |  600.169s | 1329.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-48.smt2 |  600.184s | 1481.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-46.smt2 |  600.192s | 1573.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-49.smt2 |  600.209s | 1930.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-50.smt2 |  600.218s | 1663.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-50.smt2 |  600.219s | 1526.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-50.smt2 |  600.224s | 1962.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-49.smt2 |  600.254s | 2252.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-50.smt2 |  600.263s | 2115.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-50.smt2 |  600.273s | 2184.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-49.smt2 |  600.279s | 2317.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-50.smt2 |  600.279s | 2181.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-49.smt2 |  600.285s | 2481.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-47.smt2 |  600.296s | 2261.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-506600.smt2  |  600.322s | 2188.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-49.smt2 |  600.327s | 1739.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-50.smt2 |  600.337s | 3399.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-49.smt2 |  600.338s | 3060.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-50.smt2 |  600.361s | 3065.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-487307.smt2  |  600.364s | 2343.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-49.smt2 |  600.367s | 2503.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-50.smt2 |  600.367s | 3047.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-49.smt2 |  600.373s | 3180.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-556171.smt2 |  600.374s | 2164.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-50.smt2 |  600.375s | 3253.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-533042.smt2  |  600.377s | 2568.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-569261.smt2  |  600.409s | 3264.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/20231117-c_inference/80_80_71_17_unsat.smt2 |  600.409s | 3272.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-50.smt2 |  600.414s | 3145.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-49.smt2 |  600.420s | 3017.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-645855.smt2 |  600.432s | 3002.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-740637.smt2 |  600.436s | 3772.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-579281.smt2 |  600.438s | 2600.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-696340.smt2 |  600.454s | 3625.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-737829.smt2 |  600.499s | 4208.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-715402.smt2 |  600.523s | 4143.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-655888.smt2  |  600.524s | 4014.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-687518.smt2  |  600.524s | 4068.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-765743.smt2  |  600.528s | 4343.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-989891.smt2 |  600.589s | 5055.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-873799.smt2  |  600.593s | 5199.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-735583.smt2 |  600.599s | 4327.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-863289.smt2  |  600.605s | 5318.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-797738.smt2 |  600.609s | 4477.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-983194.smt2 |  600.622s | 5822.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-968440.smt2  |  600.655s | 5690.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-861420.smt2 |  600.664s | 5205.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-902192.smt2  |  600.696s | 5087.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-985918.smt2  |  600.702s | 5888.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-777746.smt2  |  600.711s | 5211.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-644402.smt2  |  600.738s | 3773.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-987361.smt2  |  600.750s | 5073.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-993227.smt2  |  600.757s | 6166.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-943653.smt2  |  600.766s | 6174.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-904583.smt2  |  600.861s | 5889.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-851594.smt2 |  600.884s | 5240.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1060546.smt2 |  600.887s | 6871.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1065256.smt2 |  600.930s | 7030.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-985518.smt2  |  601.112s | 6476.0MiB| timeout | 0 |  |  |