# .

* SAT 470
* UNSAT 270
* 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-bb2
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=2"
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  |    3.340s | 783.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-14.smt2 |    3.367s | 822.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-10.smt2 |    3.608s | 1884.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-03.smt2 |    3.670s | 1418.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-09.smt2 |    3.739s | 1816.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-01.smt2 |    3.814s | 2287.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-15.smt2 |    3.897s | 2258.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-09.smt2 |    4.007s | 2258.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-02.smt2 |    4.089s | 2273.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-15.smt2 |    4.345s | 2201.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-04.smt2 |    4.421s | 2188.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-04.smt2 |    4.425s | 2210.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-06.smt2 |    4.431s | 2202.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-05.smt2 |    4.453s | 2201.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-05.smt2 |    4.454s | 2189.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-12.smt2 |    4.493s | 2201.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-01.smt2 |    4.536s | 2197.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-08.smt2 |    4.555s | 2214.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-11.smt2 |    4.576s | 2205.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-12.smt2 |    4.615s | 2195.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-14.smt2 |    4.661s | 2207.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-08.smt2 |    4.682s | 917.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-11.smt2 |    4.762s | 2191.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-08.smt2 |    4.827s | 902.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-527358.smt2 |    4.853s | 932.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-02.smt2 |    4.865s | 2214.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-07.smt2 |    4.964s | 2206.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-14.smt2 |    4.973s | 896.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-07.smt2 |    5.003s | 2209.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-13.smt2 |    5.037s | 2195.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-413904.smt2 |    5.125s | 948.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-12.smt2 |    5.233s | 1678.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-00.smt2 |    5.266s | 2197.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-15.smt2 |    5.272s | 1433.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-11.smt2 |    5.321s | 1305.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RC-06.smt2 |    5.324s | 2194.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/RwMutex-PT-r0010w0500/RF-03.smt2 |    5.518s | 4262.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-10.smt2 |    5.901s | 3292.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-07.smt2 |    6.125s | 4730.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-12.smt2 |    6.164s | 4480.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-10.smt2 |    6.188s | 4481.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-00.smt2 |    6.231s | 4655.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-09.smt2 |    6.434s | 4647.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-13.smt2 |    6.484s | 4639.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-02.smt2 |    6.511s | 4907.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-01.smt2 |    6.595s | 4804.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-00.smt2 |    6.625s | 4735.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-15.smt2 |    6.766s | 4911.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-14.smt2 |    6.835s | 4817.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RF-13.smt2 |    6.846s | 4718.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-11.smt2 |    7.051s | 4893.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-03.smt2 |    7.115s | 4655.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-649834.smt2 |    7.227s | 1256.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/20220307-SMPT/SharedMemory-PT-000050/RC-09.smt2 |    7.289s | 4636.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-906218.smt2  |    7.295s | 1364.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1015084.smt2 |    7.397s | 1581.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1007795.smt2 |    7.851s | 1399.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-392137.smt2  |    8.643s | 985.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-916576.smt2  |    8.943s | 1389.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1000539.smt2 |   10.120s | 1551.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-928134.smt2  |   10.384s | 1676.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-415996.smt2  |   10.587s | 1107.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-689472.smt2  |   10.757s | 1615.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-916807.smt2 |   11.556s | 1938.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-705295.smt2 |   12.360s | 1781.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-47.smt2 |   12.611s | 620.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1148089.smt2 |   12.970s | 1769.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-794687.smt2 |   13.387s | 1874.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-758897.smt2 |   13.441s | 1909.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-901996.smt2 |   14.458s | 2080.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-47.smt2 |   14.608s | 265.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-47.smt2 |   15.418s | 265.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-917322.smt2 |   15.611s | 2054.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-49.smt2 |   15.804s | 666.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-901628.smt2  |   15.968s | 1986.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-48.smt2 |   17.356s | 267.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER10-13-fair.smt2        |   17.920s | 341.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-8-50.smt2 |   18.134s | 897.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-20-45.smt2 |   18.191s | 771.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-618384.smt2  |   18.385s | 1791.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/2019-ezsmt/incrementalScheduling/214-incremental_scheduling-27000-0.smt2 |   18.790s | 301.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-46.smt2 |   19.763s | 704.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-5-50.smt2 |   20.007s | 843.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-17-50.smt2 |   20.041s | 785.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-481231.smt2  |   20.485s | 1539.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-30-48.smt2 |   20.554s | 770.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-864173.smt2  |   20.584s | 2443.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-46.smt2 |   20.673s | 745.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-17-50.smt2 |   20.910s | 972.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-19-49.smt2 |   20.935s | 780.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-33-50.smt2 |   21.105s | 933.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-19-50.smt2 |   21.421s | 904.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-2-50.smt2 |   21.450s | 922.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-14-50.smt2 |   21.478s | 907.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-21-50.smt2 |   21.714s | 981.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-31-50.smt2 |   21.733s | 874.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-9-50.smt2 |   21.814s | 865.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1107622.smt2 |   21.986s | 2863.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-23-50.smt2 |   22.010s | 948.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-45.smt2 |   22.127s | 868.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-38-50.smt2 |   22.440s | 1028.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-37-50.smt2 |   22.544s | 1016.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1192684.smt2 |   22.703s | 2803.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-34-45.smt2 |   22.718s | 696.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-16-50.smt2 |   22.822s | 998.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-48.smt2 |   23.032s | 703.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-50.smt2 |   23.032s | 814.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-32-50.smt2 |   23.222s | 998.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-47-50.smt2 |   23.397s | 1024.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-47.smt2 |   23.470s | 730.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-45.smt2 |   23.500s | 678.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-13-50.smt2 |   23.579s | 1007.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-46-50.smt2 |   23.583s | 899.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-45-50.smt2 |   23.588s | 897.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-47.smt2 |   23.590s | 709.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-69-50.smt2 |   23.606s | 917.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-30-50.smt2 |   23.665s | 1005.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-50.smt2 |   24.137s | 778.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-49.smt2 |   24.184s | 873.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-59-50.smt2 |   24.199s | 904.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-22-50.smt2 |   24.296s | 1081.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-49.smt2 |   24.326s | 799.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-49.smt2 |   24.418s | 788.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-42-50.smt2 |   24.532s | 1026.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-48-50.smt2 |   24.537s | 981.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-48.smt2 |   24.561s | 860.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-35-50.smt2 |   24.670s | 988.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1185949.smt2 |   25.631s | 2708.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-14-49.smt2 |   25.955s | 856.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-61-50.smt2 |   26.023s | 972.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-60-50.smt2 |   26.402s | 899.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-67-50.smt2 |   26.546s | 936.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-48.smt2 |   26.718s | 782.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-49-50.smt2 |   26.955s | 977.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-47.smt2 |   27.020s | 947.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-47.smt2 |   27.183s | 940.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-33-50.smt2 |   27.498s | 904.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-46.smt2 |   27.763s | 947.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-70-50.smt2 |   27.788s | 927.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-68-50.smt2 |   27.825s | 919.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-45.smt2 |   28.008s | 954.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1121941.smt2 |   28.980s | 2961.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-408585.smt2  |   29.332s | 1491.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-48.smt2 |   29.954s | 854.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-65-50.smt2 |   29.990s | 938.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-46.smt2 |   29.996s | 830.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-47.smt2 |   30.000s | 923.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-55-50.smt2 |   30.010s | 990.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-64-50.smt2 |   30.618s | 920.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-46.smt2 |   31.139s | 966.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-47.smt2 |   31.143s | 951.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-46.smt2 |   31.147s | 1065.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-19-50.smt2 |   31.469s | 1004.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-46.smt2 |   31.999s | 984.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-45.smt2 |   32.145s | 1008.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-49.smt2 |   32.288s | 1021.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-54-50.smt2 |   32.415s | 1179.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-28-48.smt2 |   32.466s | 968.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-45.smt2 |   32.471s | 949.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-47.smt2 |   32.544s | 1063.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-45.smt2 |   32.975s | 1126.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-46.smt2 |   33.101s | 1013.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-49.smt2 |   33.261s | 989.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-46.smt2 |   33.436s | 978.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-46.smt2 |   33.568s | 1137.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-47.smt2 |   33.739s | 1083.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-40-50.smt2 |   33.792s | 1026.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-58-50.smt2 |   33.919s | 959.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-50.smt2 |   34.131s | 917.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-29-48.smt2 |   34.305s | 1010.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-47.smt2 |   34.434s | 780.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-46.smt2 |   34.704s | 1019.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-47.smt2 |   34.887s | 1004.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-46.smt2 |   35.126s | 1123.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-63-50.smt2 |   35.133s | 932.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-48.smt2 |   35.301s | 1129.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-47.smt2 |   35.306s | 1023.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-46.smt2 |   35.673s | 1307.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-34-48.smt2 |   35.885s | 910.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-45.smt2 |   36.214s | 882.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-45.smt2 |   36.292s | 843.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-46.smt2 |   36.371s | 954.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-47.smt2 |   36.452s | 1071.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-47.smt2 |   36.560s | 994.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-32-50.smt2 |   36.825s | 972.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-45.smt2 |   36.906s | 1129.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-53-50.smt2 |   37.008s | 924.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-46.smt2 |   37.139s | 1043.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-46.smt2 |   37.165s | 1500.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-47.smt2 |   37.225s | 1015.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-47.smt2 |   37.524s | 1153.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-48.smt2 |   38.072s | 1054.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-47.smt2 |   38.076s | 1027.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-45.smt2 |   38.133s | 1739.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-47.smt2 |   38.148s | 1065.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-46.smt2 |   38.250s | 1590.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-906586.smt2 |   38.355s | 3318.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-50.smt2 |   38.554s | 782.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-52-50.smt2 |   38.944s | 965.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-47.smt2 |   39.352s | 1329.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-47.smt2 |   39.379s | 1257.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-48.smt2 |   39.460s | 1267.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-46.smt2 |   39.573s | 1017.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-49.smt2 |   39.881s | 1283.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-48.smt2 |   39.977s | 1104.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-48.smt2 |   39.983s | 996.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-14-50.smt2 |   40.477s | 982.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-46.smt2 |   40.733s | 1039.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-29-50.smt2 |   40.838s | 931.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-50-50.smt2 |   40.877s | 1037.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-39-50.smt2 |   40.912s | 1020.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-48.smt2 |   40.925s | 1211.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-48.smt2 |   40.946s | 1252.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-48.smt2 |   41.004s | 1200.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-45.smt2 |   41.064s | 1367.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-45.smt2 |   41.134s | 1224.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-45.smt2 |   41.415s | 1197.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-47.smt2 |   41.483s | 1083.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-48.smt2 |   41.619s | 1226.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-48.smt2 |   41.749s | 1199.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-47.smt2 |   41.828s | 1523.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-48.smt2 |   41.835s | 1209.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-51-50.smt2 |   41.869s | 1269.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-48.smt2 |   42.284s | 1421.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-48.smt2 |   42.499s | 1058.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-48.smt2 |   42.504s | 1370.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-45.smt2 |   42.639s | 1314.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-13-48.smt2 |   42.716s | 1089.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-47.smt2 |   42.819s | 1567.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-47.smt2 |   42.861s | 1107.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-45.smt2 |   42.923s | 1066.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-48.smt2 |   43.250s | 1223.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-36-49.smt2 |   43.280s | 1054.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-46.smt2 |   43.292s | 923.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-46.smt2 |   43.542s | 1548.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-46.smt2 |   43.913s | 1046.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-48.smt2 |   43.984s | 1452.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-48.smt2 |   44.183s | 972.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-49.smt2 |   44.217s | 1110.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-48.smt2 |   44.286s | 1472.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-48.smt2 |   44.565s | 1204.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-45.smt2 |   44.756s | 1115.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-47.smt2 |   44.933s | 921.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-45.smt2 |   45.437s | 1256.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-25-50.smt2 |   45.538s | 1058.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-24-49.smt2 |   45.542s | 1097.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-47.smt2 |   45.562s | 1434.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-47.smt2 |   45.722s | 1507.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-50.smt2 |   45.792s | 1132.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-38-50.smt2 |   45.840s | 1246.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-47.smt2 |   45.881s | 1538.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-496324.smt2 |   46.022s | 1874.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-46.smt2 |   46.048s | 1105.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-27-50.smt2 |   46.081s | 1081.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-46.smt2 |   46.162s | 1284.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-45.smt2 |   46.357s | 1494.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-46.smt2 |   46.521s | 1328.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-18-48.smt2 |   46.625s | 940.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-43-50.smt2 |   47.329s | 1003.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-49.smt2 |   47.383s | 1141.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-46.smt2 |   47.408s | 1127.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-50.smt2 |   47.527s | 1176.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-49.smt2 |   47.585s | 1152.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-47.smt2 |   47.608s | 1135.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-46.smt2 |   47.705s | 1547.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-49.smt2 |   47.713s | 1498.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-47.smt2 |   48.216s | 1374.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-45.smt2 |   48.314s | 1390.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-48.smt2 |   48.354s | 1557.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-49.smt2 |   48.416s | 1134.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-49.smt2 |   48.543s | 1279.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-46.smt2 |   48.552s | 1378.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1145584.smt2 |   48.560s | 4055.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-50.smt2 |   48.590s | 1275.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-44-50.smt2 |   48.651s | 1276.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-46.smt2 |   49.132s | 1371.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-50.smt2 |   49.261s | 955.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-47.smt2 |   49.359s | 1153.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-46.smt2 |   49.444s | 1734.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-48.smt2 |   49.858s | 1200.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-46.smt2 |   49.949s | 1738.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-47.smt2 |   50.090s | 1537.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-48.smt2 |   50.121s | 1703.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-50.smt2 |   50.213s | 1138.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/2019-ezsmt/incrementalScheduling/258-incremental_scheduling-40698-0.smt2 |   50.352s | 308.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-48.smt2 |   50.485s | 1135.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-46.smt2 |   50.611s | 1405.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-46.smt2 |   50.810s | 1144.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-50.smt2 |   51.071s | 1185.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-46.smt2 |   51.110s | 1367.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-12-50.smt2 |   51.255s | 1298.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-27-50.smt2 |   51.392s | 1224.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-40-49.smt2 |   51.502s | 1386.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-47.smt2 |   51.517s | 1447.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-49.smt2 |   51.677s | 1292.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-49.smt2 |   51.765s | 1122.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-47.smt2 |   51.848s | 1150.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-50.smt2 |   51.975s | 1557.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-46.smt2 |   52.236s | 1639.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-49.smt2 |   52.524s | 1494.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-48.smt2 |   52.556s | 932.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-45.smt2 |   52.659s | 1487.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-49.smt2 |   52.688s | 1571.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-6-50.smt2 |   52.715s | 1326.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-14-49.smt2 |   52.941s | 1308.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-41-50.smt2 |   53.103s | 1316.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-49.smt2 |   53.141s | 1446.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-47.smt2 |   53.177s | 1284.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-47.smt2 |   53.450s | 937.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-47.smt2 |   53.536s | 1204.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-47.smt2 |   53.568s | 1354.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-48.smt2 |   53.640s | 1463.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-46.smt2 |   53.946s | 1609.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-47.smt2 |   54.082s | 2015.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-13-50.smt2 |   54.099s | 992.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-48.smt2 |   54.256s | 1412.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-47.smt2 |   54.372s | 763.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-48.smt2 |   54.558s | 1656.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-47.smt2 |   54.570s | 1664.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-15-50.smt2 |   54.590s | 1246.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-48.smt2 |   54.731s | 1434.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-7-50.smt2 |   54.807s | 1414.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-48.smt2 |   55.040s | 1544.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-0-50.smt2 |   55.353s | 1237.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-47.smt2 |   55.449s | 1227.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-48.smt2 |   55.642s | 1861.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-48.smt2 |   55.694s | 1431.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-47.smt2 |   55.803s | 1361.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-49.smt2 |   56.223s | 1036.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-48.smt2 |   56.321s | 895.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-48.smt2 |   56.342s | 1389.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-46.smt2 |   56.357s | 1758.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-48.smt2 |   56.601s | 920.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-46.smt2 |   56.753s | 1845.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-46.smt2 |   56.947s | 1893.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-48.smt2 |   57.044s | 1370.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-46.smt2 |   57.140s | 1522.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-4-49.smt2 |   57.274s | 1262.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-48.smt2 |   57.384s | 1202.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-48.smt2 |   57.575s | 1847.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-49.smt2 |   57.831s | 1887.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-46.smt2 |   57.957s | 1479.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-48.smt2 |   57.997s | 1827.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-49.smt2 |   58.028s | 1275.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-48.smt2 |   58.305s | 1502.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-48.smt2 |   58.325s | 1702.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-49.smt2 |   58.793s | 1553.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-48.smt2 |   59.047s | 1598.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-48.smt2 |   59.196s | 1944.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-48.smt2 |   59.601s | 1723.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-48.smt2 |   59.758s | 1392.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-48.smt2 |   59.825s | 1595.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-49.smt2 |   60.076s | 1534.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-48.smt2 |   60.088s | 1900.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-47.smt2 |   60.547s | 1718.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-43-50.smt2 |   60.613s | 1483.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-48.smt2 |   60.648s | 1397.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-5-50.smt2 |   61.031s | 1248.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-49.smt2 |   61.328s | 1605.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-20-50.smt2 |   61.501s | 1717.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-48.smt2 |   61.923s | 1513.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-29-50.smt2 |   61.980s | 1107.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-47.smt2 |   62.376s | 1307.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-47.smt2 |   62.382s | 1937.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-49.smt2 |   62.413s | 1525.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-50.smt2 |   62.438s | 1768.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-48.smt2 |   62.523s | 1533.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-49.smt2 |   62.669s | 1694.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-49.smt2 |   62.669s | 1361.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-47.smt2 |   62.851s | 1592.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-48.smt2 |   63.036s | 1331.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-48.smt2 |   63.093s | 1305.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-26-50.smt2 |   63.124s | 1205.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-49.smt2 |   63.159s | 1670.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-49.smt2 |   63.272s | 1597.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-46.smt2 |   63.533s | 1679.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-46.smt2 |   63.605s | 2384.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-47.smt2 |   63.649s | 1891.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-48.smt2 |   63.810s | 1911.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-49.smt2 |   63.830s | 1800.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-48.smt2 |   63.875s | 1531.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-46.smt2 |   64.222s | 1434.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-17-47.smt2 |   64.286s | 1239.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-49.smt2 |   64.349s | 1500.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-21-50.smt2 |   65.210s | 1756.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-48.smt2 |   65.308s | 1479.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER10-14-fair.smt2        |   65.534s | 383.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-49.smt2 |   65.596s | 1735.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-46.smt2 |   66.380s | 1317.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-48.smt2 |   66.718s | 1628.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-46.smt2 |   66.899s | 1360.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-1-50.smt2 |   67.001s | 1555.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-46.smt2 |   67.090s | 2377.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-47.smt2 |   67.339s | 1586.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-762853.smt2 |   67.474s | 3378.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-46-49.smt2 |   67.846s | 1586.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-48.smt2 |   68.385s | 1122.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-47.smt2 |   68.513s | 1403.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-48.smt2 |   68.648s | 1909.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-49.smt2 |   68.689s | 1753.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-46.smt2 |   68.694s | 1065.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-48.smt2 |   68.840s | 1433.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-50.smt2 |   68.933s | 1705.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-47.smt2 |   69.657s | 1543.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-57-49.smt2 |   70.006s | 1663.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-50.smt2 |   70.190s | 1572.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-46.smt2 |   70.373s | 1499.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-48.smt2 |   70.381s | 1462.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-49.smt2 |   70.852s | 1641.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-49.smt2 |   72.243s | 1503.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-50.smt2 |   72.451s | 1921.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-18-50.smt2 |   72.592s | 1583.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-48.smt2 |   72.909s | 1381.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-49.smt2 |   73.215s | 1576.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-49.smt2 |   73.251s | 1216.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-46.smt2 |   73.516s | 2250.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-49.smt2 |   73.764s | 1595.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-49.smt2 |   74.574s | 1484.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-48.smt2 |   75.055s | 1153.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-49.smt2 |   75.096s | 1392.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-22-50.smt2 |   75.340s | 1401.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-47.smt2 |   75.556s | 2118.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-5-50.smt2 |   75.714s | 1171.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-4-50.smt2 |   75.989s | 1505.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-24-49.smt2 |   76.137s | 2474.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-47.smt2 |   76.339s | 1795.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-53-50.smt2 |   77.346s | 1918.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-1072007.smt2 |   77.653s | 4593.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-48.smt2 |   77.854s | 1690.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-49.smt2 |   78.037s | 1533.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-16-49.smt2 |   78.526s | 1111.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-8-49.smt2 |   78.872s | 1239.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-48.smt2 |   79.637s | 1715.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-49.smt2 |   79.945s | 2092.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-48.smt2 |   80.530s | 1257.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-27-49.smt2 |   80.552s | 1987.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-48.smt2 |   80.886s | 1612.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-39-46.smt2 |   80.892s | 1854.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-48.smt2 |   81.661s | 1654.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-46.smt2 |   81.846s | 1679.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-47.smt2 |   82.039s | 1082.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-46.smt2 |   84.400s | 1275.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER11-14-fair.smt2        |   84.439s | 420.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-49-49.smt2 |   84.794s | 2055.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-47.smt2 |   84.830s | 2091.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-47.smt2 |   85.659s | 2085.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-58-50.smt2 |   85.735s | 1709.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-50.smt2 |   86.512s | 1909.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-49.smt2 |   86.676s | 1666.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-49.smt2 |   86.704s | 2048.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1096871.smt2 |   86.747s | 4620.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-48.smt2 |   86.813s | 1584.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-5-50.smt2 |   87.592s | 1502.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-47.smt2 |   87.663s | 2389.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-63-50.smt2 |   88.301s | 2311.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-46.smt2 |   88.604s | 1418.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-49.smt2 |   88.667s | 2531.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-49.smt2 |   88.733s | 1618.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-48.smt2 |   88.750s | 1773.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-55-50.smt2 |   89.300s | 1686.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-46.smt2 |   89.792s | 2210.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-25-50.smt2 |   90.198s | 1198.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-48-50.smt2 |   90.251s | 2289.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-49.smt2 |   90.770s | 1618.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-56-50.smt2 |   90.855s | 1887.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-61-50.smt2 |   90.925s | 1240.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-50-50.smt2 |   91.528s | 2153.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-59-50.smt2 |   91.971s | 2359.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-52-50.smt2 |   92.374s | 1759.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-49.smt2 |   92.501s | 2339.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-54-50.smt2 |   92.910s | 2575.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-49.smt2 |   92.923s | 2458.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-49.smt2 |   93.344s | 1293.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-49.smt2 |   93.483s | 2359.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-47.smt2 |   93.661s | 1710.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-41-50.smt2 |   94.429s | 1811.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-26-50.smt2 |   95.240s | 2069.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-31-49.smt2 |   95.277s | 2445.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-47.smt2 |   95.385s | 1826.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-51-50.smt2 |   95.530s | 2187.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-45-50.smt2 |   96.056s | 1654.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-46.smt2 |   97.704s | 2003.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-614657.smt2 |   97.827s | 2683.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-46.smt2 |   98.041s | 1673.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-62-50.smt2 |   98.077s | 1854.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-49.smt2 |   98.447s | 1497.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-729964.smt2 |  100.158s | 3492.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-42-50.smt2 |  101.271s | 1816.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-44-50.smt2 |  101.649s | 2234.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-48.smt2 |  102.205s | 1729.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-46.smt2 |  104.656s | 2041.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-46.smt2 |  105.187s | 2292.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-36-50.smt2 |  106.649s | 2088.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-49.smt2 |  106.799s | 1671.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-48.smt2 |  107.291s | 1682.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-49.smt2 |  107.364s | 2252.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-48.smt2 |  109.915s | 1810.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-47.smt2 |  109.980s | 2750.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-46.smt2 |  111.447s | 2346.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-47.smt2 |  112.180s | 1859.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-48.smt2 |  113.569s | 1608.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-50.smt2 |  113.783s | 1640.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-60-50.smt2 |  114.137s | 1579.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-47.smt2 |  115.719s | 1298.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-47.smt2 |  116.208s | 1678.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-47.smt2 |  116.514s | 1278.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_group/prp-28-50.smt2 |  116.856s | 1151.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-46.smt2 |  117.686s | 1287.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-48.smt2 |  119.177s | 1477.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-47.smt2 |  122.072s | 2219.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-47.smt2 |  122.079s | 1484.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-46.smt2 |  122.086s | 1975.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-46.smt2 |  122.933s | 1082.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-48.smt2 |  123.091s | 2954.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-394532.smt2 |  123.106s | 1592.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-46.smt2 |  123.210s | 1603.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-47.smt2 |  124.322s | 1926.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-47.smt2 |  124.966s | 1701.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-46.smt2 |  125.780s | 1804.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-50.smt2 |  126.245s | 2543.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-47.smt2 |  127.100s | 1431.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-47-50.smt2 |  127.582s | 1976.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-48.smt2 |  127.636s | 1703.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-47.smt2 |  127.940s | 1816.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-48.smt2 |  128.433s | 2637.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-35-50.smt2 |  130.234s | 2742.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-50.smt2 |  131.237s | 1168.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-47.smt2 |  132.013s | 1339.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-48.smt2 |  134.098s | 1653.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-48.smt2 |  135.001s | 1587.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-46.smt2 |  135.558s | 1341.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-47.smt2 |  136.139s | 1647.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-46.smt2 |  137.867s | 1409.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-47.smt2 |  141.795s | 2561.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-46.smt2 |  144.017s | 1847.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-7-50.smt2 |  144.237s | 2131.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-49.smt2 |  144.980s | 2018.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-18-49.smt2 |  145.366s | 1608.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-48.smt2 |  145.661s | 1913.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-50.smt2 |  146.470s | 1637.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-47.smt2 |  148.329s | 1542.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-50.smt2 |  149.107s | 1670.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-46.smt2 |  149.866s | 1752.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-46.smt2 |  150.027s | 1729.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-943653.smt2  |  150.098s | 4785.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-48.smt2 |  150.684s | 1897.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-46.smt2 |  151.581s | 1478.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-45.smt2 |  152.857s | 3841.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-495717.smt2 |  153.201s | 2256.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-46.smt2 |  153.456s | 1458.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-0-50.smt2 |  153.702s | 2805.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-46.smt2 |  154.676s | 1891.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-47.smt2 |  156.663s | 1329.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-46.smt2 |  156.800s | 1697.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-47.smt2 |  158.221s | 1700.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-518109.smt2  |  158.769s | 1973.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-46.smt2 |  161.374s | 2167.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-46.smt2 |  162.040s | 3015.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-48.smt2 |  162.085s | 2563.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-47.smt2 |  162.361s | 2062.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-46.smt2 |  165.039s | 2905.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-47.smt2 |  165.506s | 2552.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-46.smt2 |  166.632s | 2564.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-50.smt2 |  167.249s | 1416.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-37-47.smt2 |  167.787s | 2623.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-551279.smt2  |  167.909s | 2641.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-48.smt2 |  168.352s | 1520.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-47.smt2 |  168.545s | 1724.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-48.smt2 |  168.825s | 2618.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-47.smt2 |  168.952s | 3184.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-47.smt2 |  171.511s | 1653.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-50.smt2 |  172.891s | 2603.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-49.smt2 |  174.195s | 1562.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-46.smt2 |  175.155s | 1360.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-48.smt2 |  180.085s | 1424.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-47.smt2 |  180.702s | 2435.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-47.smt2 |  181.536s | 1614.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-46.smt2 |  184.646s | 2515.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-49.smt2 |  184.920s | 1942.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-9-48.smt2 |  185.691s | 2539.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-46.smt2 |  186.440s | 3928.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-46.smt2 |  187.956s | 2067.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-49.smt2 |  190.381s | 2483.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-46.smt2 |  191.644s | 3780.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-46.smt2 |  191.669s | 2643.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-46.smt2 |  193.455s | 1650.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-48.smt2 |  193.788s | 1690.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-47.smt2 |  193.825s | 1679.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-47.smt2 |  195.106s | 2490.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-50.smt2 |  197.571s | 2297.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-49.smt2 |  197.769s | 2113.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-49.smt2 |  198.458s | 2701.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-49.smt2 |  199.083s | 3475.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-13-50.smt2 |  199.535s | 1800.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/checkpass_pwd/prp-35-46.smt2 |  201.956s | 2343.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-48.smt2 |  203.230s | 3461.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-48.smt2 |  204.073s | 2351.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-22-50.smt2 |  206.217s | 1491.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/mathsat/FISCHER11-15-fair.smt2        |  206.875s | 488.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-8-47.smt2 |  212.976s | 1987.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-48.smt2 |  215.398s | 1473.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-47.smt2 |  215.412s | 2363.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-46.smt2 |  217.352s | 2064.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-50.smt2 |  217.439s | 1773.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-47.smt2 |  220.688s | 2326.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-46.smt2 |  221.423s | 3730.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-23-50.smt2 |  223.688s | 2333.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-46.smt2 |  225.617s | 1771.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-1-49.smt2 |  225.810s | 2278.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-21-50.smt2 |  227.065s | 2447.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-416752.smt2 |  229.196s | 1856.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-50.smt2 |  231.890s | 2146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-47.smt2 |  232.580s | 3603.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-46.smt2 |  232.800s | 3724.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-46.smt2 |  233.350s | 2965.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-48.smt2 |  234.508s | 2097.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-50.smt2 |  234.869s | 1731.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-46.smt2 |  235.383s | 1944.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-49.smt2 |  236.076s | 1705.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-47.smt2 |  242.820s | 2321.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-47.smt2 |  244.443s | 3594.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-48.smt2 |  245.303s | 1585.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-47.smt2 |  245.774s | 2093.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-49.smt2 |  247.294s | 2908.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-46.smt2 |  248.612s | 1698.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-3-48.smt2 |  248.718s | 2292.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-50.smt2 |  248.848s | 2431.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-46.smt2 |  251.708s | 2344.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-47.smt2 |  252.019s | 1850.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-46.smt2 |  252.356s | 1693.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-47.smt2 |  256.730s | 3027.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-47.smt2 |  259.929s | 2020.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-46.smt2 |  260.853s | 1959.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-47.smt2 |  269.148s | 3672.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-47.smt2 |  273.432s | 1755.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-50.smt2 |  274.900s | 3700.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-47.smt2 |  277.582s | 2763.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-6-50.smt2 |  278.783s | 2433.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-479884.smt2 |  279.008s | 2094.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-24-50.smt2 |  279.232s | 2626.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-46.smt2 |  279.641s | 2287.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-49.smt2 |  280.396s | 2367.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-46.smt2 |  282.156s | 2021.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-49.smt2 |  284.536s | 1794.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-658040.smt2 |  284.686s | 3435.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-48.smt2 |  284.842s | 2581.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-48.smt2 |  288.410s | 4676.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-12-49.smt2 |  291.039s | 2255.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-13-49.smt2 |  291.182s | 2802.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-49.smt2 |  293.989s | 2246.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-48.smt2 |  301.106s | 2658.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-47.smt2 |  301.140s | 2735.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-46.smt2 |  301.341s | 2292.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-49.smt2 |  306.948s | 3924.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-7-50.smt2 |  308.275s | 2399.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-47.smt2 |  309.482s | 1732.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-46.smt2 |  310.964s | 2138.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-48-49.smt2 |  311.072s | 2222.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-14-47.smt2 |  311.102s | 2124.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-47.smt2 |  312.924s | 1814.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-48.smt2 |  315.303s | 2240.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-49.smt2 |  317.581s | 2773.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-49.smt2 |  318.904s | 1642.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-50.smt2 |  322.737s | 3520.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-51-50.smt2 |  325.524s | 2084.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-49.smt2 |  328.044s | 2620.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-49.smt2 |  339.575s | 2273.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-49.smt2 |  342.064s | 3193.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-20-50.smt2 |  343.309s | 2495.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-47.smt2 |  345.329s | 1974.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-8-49.smt2 |  347.069s | 2708.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-50.smt2 |  347.773s | 3850.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-48.smt2 |  348.637s | 2556.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-2-50.smt2 |  349.328s | 1850.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-43-50.smt2 |  353.354s | 2635.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-49.smt2 |  355.475s | 2443.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-49.smt2 |  355.476s | 1899.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-687179.smt2 |  356.607s | 2830.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-17-50.smt2 |  359.036s | 1948.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-47.smt2 |  360.423s | 2049.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-49.smt2 |  361.847s | 2533.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-645855.smt2 |  364.391s | 3253.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-17-50.smt2 |  364.955s | 2130.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-47.smt2 |  369.618s | 2820.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-48.smt2 |  372.155s | 2177.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-50.smt2 |  372.635s | 2326.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-478122.smt2  |  375.190s | 2386.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-50-49.smt2 |  376.176s | 4793.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-47-49.smt2 |  376.371s | 3652.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-48.smt2 |  382.791s | 2046.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-19-50.smt2 |  387.762s | 3459.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-48.smt2 |  391.109s | 2327.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-19-49.smt2 |  395.234s | 2830.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-49-50.smt2 |  396.487s | 4229.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-46.smt2 |  396.510s | 2379.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-5-46.smt2 |  397.653s | 2863.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-49.smt2 |  406.380s | 2489.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-49.smt2 |  415.032s | 3593.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-45-50.smt2 |  416.032s | 3411.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-16-50.smt2 |  417.885s | 2142.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-48.smt2 |  419.646s | 2688.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-48.smt2 |  423.979s | 1828.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-48.smt2 |  427.722s | 2453.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-32-50.smt2 |  431.984s | 3442.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-48.smt2 |  436.470s | 2489.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-49.smt2 |  436.593s | 3193.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-47.smt2 |  438.603s | 2590.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-22-49.smt2 |  445.379s | 2313.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-13-50.smt2 |  448.149s | 2946.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-46-50.smt2 |  452.952s | 2925.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-49.smt2 |  462.809s | 3194.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-16-49.smt2 |  465.688s | 2446.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-50.smt2 |  467.216s | 3019.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-38-50.smt2 |  468.319s | 4154.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-7-47.smt2 |  469.070s | 1936.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-25-50.smt2 |  470.909s | 3171.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-44-50.smt2 |  478.202s | 4238.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-48.smt2 |  480.263s | 4118.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-696340.smt2 |  482.636s | 3867.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-49.smt2 |  486.375s | 4757.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-50.smt2 |  488.781s | 3854.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-23-50.smt2 |  494.796s | 2765.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-49.smt2 |  495.782s | 2026.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-391798.smt2  |  498.320s | 1734.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-49.smt2 |  502.917s | 2244.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-47.smt2 |  514.595s | 3314.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-12-50.smt2 |  514.756s | 2494.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-48.smt2 |  518.749s | 2652.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-6-49.smt2 |  523.370s | 2447.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-15-50.smt2 |  526.782s | 2740.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-928960.smt2  |  529.973s | 4987.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-506600.smt2  |  536.506s | 2397.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-47.smt2 |  537.587s | 2437.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-2-50.smt2 |  541.361s | 3043.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-40-49.smt2 |  548.245s | 4317.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-11-50.smt2 |  553.438s | 4195.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-983194.smt2 |  557.950s | 6430.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-49.smt2 |  558.627s | 1887.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-804609.smt2  |  574.793s | 5330.0MiB| sat | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-50.smt2 |  589.260s | 4813.0MiB| unsat | 0 |  |  |
|non-incremental/QF_LIA/2019-ezsmt/incrementalScheduling/295-incremental_scheduling-40626-0.smt2 |  600.062s | 344.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_15.txt.smt2               |  600.102s | 547.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_18.txt.smt2               |  600.105s | 546.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/RWS/Example_9.txt.smt2                |  600.128s | 563.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-34-50.smt2 |  600.201s | 1509.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-4-50.smt2 |  600.216s | 2025.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-48.smt2 |  600.217s | 1899.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-49.smt2 |  600.233s | 1775.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-50.smt2 |  600.236s | 1794.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-49.smt2 |  600.243s | 1985.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-50.smt2 |  600.243s | 2079.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-11-49.smt2 |  600.248s | 2079.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-49.smt2 |  600.257s | 2261.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-10-50.smt2 |  600.273s | 2486.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-373262.smt2 |  600.281s | 1609.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-49.smt2 |  600.296s | 2398.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-3-50.smt2 |  600.316s | 2664.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-49.smt2 |  600.346s | 2983.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-556171.smt2 |  600.353s | 2409.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-603294.smt2 |  600.369s | 2646.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-42-50.smt2 |  600.371s | 3594.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-46.smt2 |  600.375s | 3455.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_directories/prp-10-50.smt2 |  600.387s | 3194.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-48.smt2 |  600.391s | 3384.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-9-50.smt2 |  600.393s | 2942.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-11-50.smt2 |  600.400s | 2846.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-487307.smt2  |  600.431s | 2588.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-579281.smt2 |  600.442s | 2904.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-39-49.smt2 |  600.445s | 4005.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-533042.smt2  |  600.452s | 2829.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-33-49.smt2 |  600.481s | 3892.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-49.smt2 |  600.483s | 4362.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-41-49.smt2 |  600.484s | 3705.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-569261.smt2  |  600.488s | 3642.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-29-50.smt2 |  600.515s | 4555.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/user_is_in_group/prp-10-47.smt2 |  600.528s | 3699.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-28-50.smt2 |  600.540s | 4384.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-50.smt2 |  600.549s | 5163.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-740637.smt2 |  600.551s | 4054.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-37-50.smt2 |  600.553s | 4278.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/nec-smt/large/getoption_user/prp-30-48.smt2 |  600.575s | 3677.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-655888.smt2  |  600.590s | 4435.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-654327.smt2  |  600.590s | 4072.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-644402.smt2  |  600.611s | 4157.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-715402.smt2 |  600.615s | 4577.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-737829.smt2 |  600.634s | 4752.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-735583.smt2 |  600.642s | 4800.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-687518.smt2  |  600.643s | 4511.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-797738.smt2 |  600.647s | 4963.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-851594.smt2 |  600.670s | 5647.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-765743.smt2  |  600.683s | 4879.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/20231117-c_inference/80_80_71_17_unsat.smt2 |  600.688s | 3577.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-989891.smt2 |  600.689s | 5577.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-777746.smt2  |  600.716s | 5777.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-863289.smt2  |  600.718s | 5881.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/tropical-matrix/constraint-861420.smt2 |  600.723s | 5805.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-902192.smt2  |  600.797s | 5631.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-873799.smt2  |  600.813s | 5710.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-968440.smt2  |  600.861s | 6365.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-985918.smt2  |  600.862s | 6483.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-987361.smt2  |  600.920s | 5659.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1065256.smt2 |  600.992s | 7810.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-993227.smt2  |  601.020s | 6799.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-1060546.smt2 |  601.079s | 7579.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-985518.smt2  |  601.090s | 7038.0MiB| timeout | 0 |  |  |
|non-incremental/QF_LIA/arctic-matrix/constraint-904583.smt2  |  601.153s | 6555.0MiB| timeout | 0 |  |  |