# .

* SAT 287
* UNSAT 140
* TIMEOUT 373
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-QF_NIA_hard-timeout10min-bb0
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: f880fdccee614547c38c19beb7af5a027961646b
Z3 branch: core_min
Z3 options: "-T:600 -v:0 smt.threads=8 tactic.default_tactic=smt smt.auto_config=false smt_parallel.num_global_bb_batch_threads=0"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_NIA.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_NIA/20220315-MathProblems/STC_0486.smt2   |    0.183s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0244.smt2   |    0.189s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0369.smt2   |    0.189s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-7fXGzy.smt2              |    0.191s | 187.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0153.smt2   |    0.197s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0963.smt2   |    0.200s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0684.smt2   |    0.200s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0703.smt2   |    0.209s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0603.smt2   |    0.214s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0097.smt2   |    0.217s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0883.smt2   |    0.220s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0190.smt2   |    0.220s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0334.smt2   |    0.221s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0816.smt2   |    0.225s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0540.smt2   |    0.226s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0678.smt2   |    0.229s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0315.smt2   |    0.233s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0920.smt2   |    0.237s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0484.smt2   |    0.237s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0099.smt2   |    0.239s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0656.smt2   |    0.242s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0493.smt2   |    0.244s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0722.smt2   |    0.257s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0944.smt2   |    0.265s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0330.smt2   |    0.276s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ex36.t2__p30283_safety_0.smt2 |    0.280s | 189.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ex36.t2_fixed__p23592_safety_0.smt2 |    0.286s | 194.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__edn.t2__p20326_safety_0.smt2 |    0.295s | 192.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0825.smt2   |    0.307s | 176.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ex36.t2__p31955_safety_0.smt2 |    0.309s | 196.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__RandomHard.jar-obl-10__p11831_safety_0.smt2 |    0.319s | 203.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__edn.t2__p20632_safety_0.smt2 |    0.390s | 198.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__edn.t2__p20710_safety_0.smt2 |    0.390s | 193.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-lcm.jar-obl-10__p14126_edge_closing_0.smt2 |    0.394s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-termination.c__p21140_edge_closing_0.smt2 |    0.413s | 192.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-mirrorInterv.jar-obl-8__p14289_edge_closing_0.smt2 |    0.439s | 230.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ex36.t2__p31845_safety_0.smt2 |    0.459s | 195.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/SAT14/1813.smt2      |    0.463s | 238.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_true-termination.c__p20893_terminationG_0.smt2 |    0.470s | 234.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p1606_safety_0.smt2 |    0.477s | 244.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/LCTES/digital-stopwatch.locals.smt2   |    0.483s | 224.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreatePut.jar-obl-10__p6354_safety_0.smt2 |    0.497s | 234.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_2vars_false-termination.c__p26899_terminationG_0.smt2 |    0.507s | 192.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateRemove.jar-obl-11__p6932_safety_0.smt2 |    0.513s | 230.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MainMove.jar-obl-11__p10745_edge_closing_0.smt2 |    0.524s | 220.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p4392_safety_0.smt2 |    0.533s | 236.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreatePut.jar-obl-10__p5497_safety_0.smt2 |    0.553s | 235.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91.t2__p2940_edge_closing_0.smt2 |    0.578s | 238.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT1335852993657230070.smt2 |    0.579s | 205.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31198_safety_0.smt2 |    0.592s | 234.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n-5.t2_fixed__p4589_terminationG_0.smt2 |    0.599s | 217.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-5-filtered.t2__p22882_terminationG_0.smt2 |    0.600s | 284.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/LassoRanker/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-termination.c_Iteration1_Loop+nonterminationTemplate_0.smt2 |    0.607s | 195.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1398_edge_closing_0.smt2 |    0.630s | 228.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p2436_safety_0.smt2 |    0.679s | 250.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7192_safety_0.smt2 |    0.682s | 282.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p1691_safety_0.smt2 |    0.741s | 259.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p2225_safety_0.smt2 |    0.774s | 239.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT5753280746557461985.smt2 |    0.830s | 211.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Fig1_true-termination.c__p22155_terminationG_0.smt2 |    0.832s | 234.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__List.jar-obl-12__p10223_edge_closing_0.smt2 |    0.846s | 202.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-6k3pKM.smt2              |    0.895s | 230.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT3457830339872275636.smt2 |    0.922s | 215.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p19848_safety_0.smt2 |    0.947s | 289.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MainMove.jar-obl-11__p10752_edge_closing_0.smt2 |    0.960s | 231.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30026_safety_0.smt2 |    0.978s | 266.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p4544_terminationG_0.smt2 |    1.034s | 336.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30127_safety_0.smt2 |    1.052s | 266.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__Prim_4.t2__p8016_terminationG_0.smt2 |    1.052s | 248.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreatePut.jar-obl-10__p6217_safety_0.smt2 |    1.096s | 320.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31152_safety_0.smt2 |    1.105s | 269.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-n1.t2_fixed__p23107_safety_0.smt2 |    1.113s | 257.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p5104_safety_0.smt2 |    1.142s | 272.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-mirrorInterv.jar-obl-8__p14269_terminationG_0.smt2 |    1.146s | 220.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__opt-tree.c.t2__p6339_terminationG_0.smt2 |    1.158s | 368.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__Prim_4.t2__p7936_terminationG_0.smt2 |    1.159s | 235.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1377_edge_closing_0.smt2 |    1.176s | 243.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT4259464554444412647.smt2 |    1.199s | 215.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p1659_safety_0.smt2 |    1.210s | 263.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1-striped.t2__p12897_safety_0.smt2 |    1.223s | 284.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30539_safety_0.smt2 |    1.317s | 360.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__polyrank4.t2__p7482_terminationG_0.smt2 |    1.378s | 263.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27084_terminationG_0.smt2 |    1.406s | 614.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__Prim_4.t2__p7976_terminationG_0.smt2 |    1.441s | 247.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p19834_safety_0.smt2 |    1.445s | 293.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p2746_safety_0.smt2 |    1.454s | 363.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__polyrank4.t2__p7477_terminationG_0.smt2 |    1.498s | 258.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ppblock.t2__p7746_edge_closing_0.smt2 |    1.509s | 287.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31805_safety_0.smt2 |    1.526s | 368.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p18338_safety_0.smt2 |    1.602s | 290.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__AlternatingGrowReduceRec2.jar-obl-9__p27530_edge_closing_0.smt2 |    1.607s | 229.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/SAT14/585.smt2       |    1.625s | 404.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p32401_safety_0.smt2 |    1.641s | 244.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31295_safety_0.smt2 |    1.667s | 271.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_true-termination.c__p25430_terminationG_0.smt2 |    1.688s | 232.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22607_safety_0.smt2 |    1.704s | 263.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1287_edge_closing_0.smt2 |    1.756s | 213.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p5158_safety_0.smt2 |    1.760s | 274.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p29915_safety_0.smt2 |    1.787s | 271.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT9064001295904670492.smt2 |    1.817s | 227.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31063_safety_0.smt2 |    1.848s | 270.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__pgarch.t2__p7283_terminationG_0.smt2 |    1.887s | 490.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__MirrorInterv.c__p24379_terminationG_0.smt2 |    1.908s | 233.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7322_safety_0.smt2 |    1.953s | 369.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p2113_safety_0.smt2 |    1.967s | 368.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIteratorKeyLoop.jar-obl-12__p3697_safety_0.smt2 |    1.971s | 279.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__small15.t2__p23781_edge_closing_0.smt2 |    2.057s | 255.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p32020_terminationG_0.smt2 |    2.086s | 379.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31079_safety_0.smt2 |    2.091s | 376.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIteratorEntryLoop.jar-obl-12__p3178_safety_0.smt2 |    2.105s | 273.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAll.jar-obl-11__p9558_terminationG_0.smt2 |    2.170s | 510.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIteratorEntryLoop.jar-obl-12__p3008_safety_0.smt2 |    2.197s | 365.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__nakata.t2__p5305_terminationG_0.smt2 |    2.229s | 469.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p4624_safety_0.smt2 |    2.236s | 370.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p322_safety_0.smt2 |    2.253s | 249.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__Prim_4.t2__p8035_terminationG_0.smt2 |    2.397s | 236.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p18948_safety_0.smt2 |    2.460s | 300.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__zlib-crc32-BYFOUR.c.t2__p26484_terminationG_0.smt2 |    2.465s | 263.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT1700028870436976635.smt2 |    2.491s | 210.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31303_safety_0.smt2 |    2.683s | 381.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT1437438160177275586.smt2 |    2.776s | 278.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30313_safety_0.smt2 |    2.818s | 389.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ppblockterm.t2__p7916_edge_closing_0.smt2 |    2.863s | 266.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__svcomp_ex2.c__p25831_terminationG_0.smt2 |    2.898s | 303.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT5521985939949569030.smt2 |    3.001s | 331.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1-striped.t2__p12943_safety_0.smt2 |    3.010s | 301.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27236_edge_closing_0.smt2 |    3.042s | 349.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-p9MQp4.smt2              |    3.103s | 258.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateRemove.jar-obl-11__p7017_terminationG_0.smt2 |    3.231s | 389.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1320_edge_closing_0.smt2 |    3.398s | 260.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT6531155344723557531.smt2 |    3.405s | 300.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p5318_safety_0.smt2 |    3.409s | 310.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MainFind.jar-obl-10__p10608_edge_closing_0.smt2 |    3.414s | 294.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1460_edge_closing_0.smt2 |    3.474s | 278.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27166_terminationG_0.smt2 |    3.502s | 320.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22603_safety_0.smt2 |    3.562s | 355.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Flatten.jar-obl-10__p29378_safety_0.smt2 |    3.638s | 343.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-live.t2_fixed__p16559_terminationG_0.smt2 |    3.691s | 688.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT5642158517481563632.smt2 |    3.733s | 390.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p31947_safety_0.smt2 |    3.739s | 401.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-live.t2_fixed__p16564_terminationG_0.smt2 |    3.920s | 676.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-plait.jar-obl-8__p14482_terminationG_0.smt2 |    3.996s | 328.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__st88.t2__p24217_terminationG_0.smt2 |    4.031s | 259.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__small15.t2__p23742_terminationG_0.smt2 |    4.137s | 317.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p19377_safety_0.smt2 |    4.234s | 311.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1440_edge_closing_0.smt2 |    4.404s | 297.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__GulwaniJainKoskinen-PLDI2009-Fig1_true-termination.c__p23757_edge_closing_0.smt2 |    4.421s | 429.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__NO_03.c__p24634_terminationG_0.smt2 |    4.499s | 229.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__p-5.t2_fixed__p6782_edge_closing_0.smt2 |    4.529s | 337.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT463192377960637155.smt2 |    4.693s | 289.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT8619300169146917506.smt2 |    4.734s | 328.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1-striped.t2_fixed__p9992_safety_0.smt2 |    4.903s | 310.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p32720_terminationG_0.smt2 |    4.906s | 429.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT7201733644041072759.smt2 |    5.003s | 301.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p31859_terminationG_0.smt2 |    5.018s | 490.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__NO_13.jar-obl-8__p11419_edge_closing_0.smt2 |    5.089s | 263.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p31928_safety_0.smt2 |    5.179s | 297.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-fib.jar-obl-8__p13930_edge_closing_0.smt2 |    5.427s | 366.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__janne_complex.t2__p2254_terminationG_0.smt2 |    5.479s | 327.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-termination.c__p21344_edge_closing_0.smt2 |    5.480s | 255.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__janne_complex.t2__p2193_terminationG_0.smt2 |    5.619s | 285.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__janne_complex.t2__p2020_terminationG_0.smt2 |    5.726s | 298.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1378_edge_closing_0.smt2 |    5.739s | 295.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__janne_complex.t2__p2263_terminationG_0.smt2 |    5.769s | 343.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p8402_safety_0.smt2 |    5.783s | 789.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT725924178667047452.smt2 |    5.788s | 277.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Test6.jar-obl-13__terminationS_24_0.smt2 |    6.011s | 752.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n-5.t2__p4703_edge_closing_0.smt2 |    6.257s | 373.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Matrix.jar-obl-16__p10815_safety_0.smt2 |    6.349s | 339.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p7969_safety_0.smt2 |    6.533s | 755.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT2214668917450755150.smt2 |    6.572s | 311.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Graph.jar-obl-17__p29774_edge_closing_0.smt2 |    6.587s | 289.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1413_edge_closing_0.smt2 |    6.595s | 5340.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__matmul.t2_fixed__p2649_terminationG_0.smt2 |    6.626s | 272.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT5468773551032053543.smt2 |    6.692s | 544.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p8584_safety_0.smt2 |    6.832s | 1156.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__narrowKonv_rec.jar-obl-8__p11136_edge_closing_0.smt2 |    6.919s | 212.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6225_edge_closing_0.smt2 |    6.925s | 468.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2_fixed__p519_terminationG_0.smt2 |    7.050s | 798.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_3vars_false-termination.c__p27027_terminationG_0.smt2 |    7.230s | 540.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.09_true-termination.c__p21247_terminationG_0.smt2 |    7.293s | 418.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT6647586385534524663.smt2 |    7.526s | 360.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2_fixed__terminationS_55_0.smt2 |    7.647s | 364.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__polyrank5.t2__p7556_terminationG_0.smt2 |    7.649s | 335.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__svdcmp.t2__term_unfeasibility_8_0.smt2 |    7.906s | 309.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1314_edge_closing_0.smt2 |    8.121s | 264.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.t2_fixed__terminationS_24_0.smt2 |    8.154s | 424.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p8337_safety_0.smt2 |    8.172s | 1150.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p9027_safety_0.smt2 |    8.194s | 1248.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.t2_fixed__terminationS_54_0.smt2 |    8.371s | 363.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7210_terminationG_0.smt2 |    8.414s | 406.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p8073_terminationG_0.smt2 |    8.433s | 1071.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT180444191153863419.smt2 |    8.479s | 325.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2_fixed__terminationS_62_0.smt2 |    8.730s | 361.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2_fixed__terminationS_25_0.smt2 |    8.857s | 432.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12239_terminationG_0.smt2 |    8.881s | 347.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2__p24820_edge_closing_0.smt2 |    9.012s | 399.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p8348_safety_0.smt2 |    9.061s | 1196.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22519_safety_0.smt2 |    9.137s | 492.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2_fixed__terminationS_26_0.smt2 |    9.219s | 432.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2_fixed__terminationS_26_0.smt2 |    9.272s | 426.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27239_edge_closing_0.smt2 |    9.333s | 790.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Count.jar-obl-10-2__p28115_terminationG_0.smt2 |    9.543s | 891.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2__p679_terminationG_0.smt2 |    9.788s | 1527.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__firewire.t2__terminationS_19_0.smt2 |    9.859s | 407.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__ChooseLife.jar-obl-8__p27825_terminationG_0.smt2 |    9.899s | 235.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2_fixed__terminationS_54_0.smt2 |    9.967s | 368.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__UpAndDown.c__p26202_terminationG_0.smt2 |   10.354s | 223.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__nakata.t2__terminationS_6_0.smt2 |   10.520s | 363.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT6981420136966712689.smt2 |   10.809s | 284.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.t2_fixed__terminationS_55_0.smt2 |   10.823s | 366.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__agafp.t2__p15626_terminationG_0.smt2 |   10.849s | 247.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1357_edge_closing_0.smt2 |   10.849s | 369.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__UpAndDownIneq.c__p26235_terminationG_0.smt2 |   11.652s | 244.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT2276070888632403184.smt2 |   11.884s | 345.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Power.jar-obl-10__p11798_terminationG_0.smt2 |   11.895s | 458.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p4709_terminationG_0.smt2 |   12.249s | 536.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__sas2.t2__terminationS_1_0.smt2 |   12.581s | 241.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT9062228803117299674.smt2 |   12.956s | 403.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1437_edge_closing_0.smt2 |   13.625s | 310.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-607QpU.smt2              |   13.630s | 316.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.t2__terminationS_25_0.smt2 |   13.787s | 463.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__terminationS_27_0.smt2 |   14.637s | 641.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30004_terminationG_0.smt2 |   14.995s | 547.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31167_terminationG_0.smt2 |   15.700s | 542.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT3712394338782947208.smt2 |   15.793s | 266.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1354_edge_closing_0.smt2 |   16.126s | 326.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2_fixed__terminationS_27_0.smt2 |   16.174s | 455.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_5_0.smt2 |   16.334s | 2123.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT5210162955256537540.smt2 |   16.476s | 508.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__terminationS_24_0.smt2 |   16.596s | 688.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_28_0.smt2 |   16.703s | 2113.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__terminationS_25_0.smt2 |   16.757s | 651.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun6.t2__p1092_terminationG_0.smt2 |   17.096s | 432.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1309_edge_closing_0.smt2 |   17.179s | 340.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__DivTernary.jar-obl-10__p28667_terminationG_0.smt2 |   17.411s | 888.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Test6.jar-obl-13__terminationS_13_0.smt2 |   17.739s | 824.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_31_0.smt2 |   18.300s | 2146.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Matrix.jar-obl-16__p10775_terminationG_0.smt2 |   18.482s | 361.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_24_0.smt2 |   19.035s | 2161.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__NO_13.jar-obl-8__p11459_terminationG_0.smt2 |   19.132s | 224.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__polyrank4.t2__p7520_terminationG_0.smt2 |   19.719s | 584.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__terminationS_26_0.smt2 |   19.728s | 689.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3358_terminationG_0.smt2 |   19.746s | 517.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7211_terminationG_0.smt2 |   20.210s | 559.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_30_0.smt2 |   20.659s | 2149.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2_fixed__terminationS_57_0.smt2 |   21.092s | 389.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p17931_terminationG_0.smt2 |   21.290s | 382.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__agafp.t2__p15636_terminationG_0.smt2 |   21.304s | 271.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_14_0.smt2 |   21.400s | 2172.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__db3.t2__term_unfeasibility_0_0.smt2 |   21.462s | 734.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun7.t2__p1142_terminationG_0.smt2 |   21.849s | 470.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT1813676864021281701.smt2 |   21.882s | 429.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__svdcmp.c.i.svdcmp.pl.t2.nor.t2.rlgfixed.t2__terminationS_7_0.smt2 |   21.920s | 534.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_15_0.smt2 |   22.013s | 2174.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-termination.c__p21147_edge_closing_0.smt2 |   22.091s | 443.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2__p680_terminationG_0.smt2 |   22.152s | 1935.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22479_terminationG_0.smt2 |   22.392s | 929.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__svdcmp.c.i.svdcmp.pl.t2.nor.t2.rlgfixed.t2__terminationS_27_0.smt2 |   22.669s | 532.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_16_0.smt2 |   22.865s | 2176.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_11_0.smt2 |   22.905s | 2179.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__whileNestedOffset_rec.jar-obl-9__p14933_safety_0.smt2 |   23.059s | 249.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1409_edge_closing_0.smt2 |   23.232s | 368.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_2_0.smt2 |   23.333s | 2169.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT3839584170547805483.smt2 |   23.671s | 416.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT6828719750442006249.smt2 |   24.530s | 515.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n-5.t2__p4682_terminationG_0.smt2 |   25.053s | 597.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2__terminationQ_0_0.smt2 |   25.118s | 882.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__LessLeavesRec.jar-obl-10__p10043_terminationG_0.smt2 |   25.164s | 550.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__db2.t2__term_unfeasibility_0_0.smt2 |   25.406s | 743.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1.t2__terminationQ_0_0.smt2 |   25.579s | 881.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__DivTernary.jar-obl-10__terminationQ_0_0.smt2 |   25.804s | 719.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_19_0.smt2 |   25.835s | 2203.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__GulwaniJainKoskinen-PLDI2009-Fig1_true-termination.c__p23748_edge_closing_0.smt2 |   25.934s | 395.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__svdcmp.c.i.svdcmp.pl.t2.nor.t2.rlgfixed.t2__terminationS_28_0.smt2 |   26.163s | 538.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31345_terminationG_0.smt2 |   26.644s | 596.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1406_edge_closing_0.smt2 |   26.788s | 400.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Count.jar-obl-10-2__p28120_terminationG_0.smt2 |   26.918s | 546.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-3-new.t2__p22118_edge_closing_0.smt2 |   27.352s | 2782.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__terminationS_49_0.smt2 |   27.419s | 534.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__terminationS_49_0.smt2 |   27.472s | 525.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__terminationS_21_0.smt2 |   27.739s | 717.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__florian_sas2.t2__p32399_terminationG_0.smt2 |   27.939s | 407.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIteratorEntryLoop.jar-obl-12__p3188_terminationG_0.smt2 |   28.581s | 585.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ex11.t2__p22126_terminationG_0.smt2 |   28.826s | 240.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1485_edge_closing_0.smt2 |   28.961s | 349.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MirrorBinTreeRec.jar-obl-9__p10899_terminationG_0.smt2 |   29.122s | 529.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.t2_fixed__terminationS_53_0.smt2 |   29.560s | 478.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-narrowing.jar-obl-8__p14385_terminationG_0.smt2 |   29.752s | 234.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1393_edge_closing_0.smt2 |   30.695s | 360.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__terminationS_19_0.smt2 |   30.740s | 724.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1.t2_fixed__p784_terminationG_0.smt2 |   32.126s | 789.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1.t2_fixed__p721_terminationG_0.smt2 |   32.143s | 1243.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__narrowing_rec.jar-obl-8__p11066_terminationG_0.smt2 |   32.188s | 226.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__janne_complex.t2__p2041_terminationG_0.smt2 |   33.021s | 495.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27186_terminationG_0.smt2 |   33.097s | 433.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3169_terminationG_0.smt2 |   33.729s | 659.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0496.smt2   |   33.763s | 188.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2_fixed__p577_terminationG_0.smt2 |   33.868s | 811.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n-5.t2__p4677_terminationG_0.smt2 |   33.919s | 1276.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12183_terminationG_0.smt2 |   35.528s | 801.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1.t2_fixed__p705_terminationG_0.smt2 |   36.149s | 1168.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__sas2.t2__p21311_terminationG_0.smt2 |   36.451s | 287.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_20_0.smt2 |   37.130s | 4263.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted.t2_fixed__p16110_terminationG_0.smt2 |   37.403s | 1335.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_28_0.smt2 |   38.663s | 4455.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-termination.c__p21396_terminationG_0.smt2 |   38.938s | 270.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12142_terminationG_0.smt2 |   38.972s | 545.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__florian_sas2.t2__p32384_terminationG_0.smt2 |   39.202s | 411.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__opt-tree.c.t2__p6340_terminationG_0.smt2 |   39.698s | 1241.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_18_0.smt2 |   39.854s | 4362.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__afagp-fail.t2__p15516_edge_closing_0.smt2 |   40.047s | 523.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_11_0.smt2 |   40.400s | 4341.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_17_0.smt2 |   40.515s | 4457.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2__p597_terminationG_0.smt2 |   40.623s | 1930.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2_fixed__p24590_edge_closing_0.smt2 |   40.845s | 444.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_14_0.smt2 |   41.715s | 4381.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_15_0.smt2 |   41.792s | 4381.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreatePut.jar-obl-10__p6135_terminationG_0.smt2 |   43.095s | 645.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_12_0.smt2 |   43.253s | 4362.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p21950_terminationG_0.smt2 |   43.339s | 894.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_21_0.smt2 |   44.730s | 4544.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_13_0.smt2 |   44.767s | 4386.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_10_0.smt2 |   44.870s | 4371.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27151_terminationG_0.smt2 |   47.096s | 509.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MysteriousProgram.jar-obl-12__terminationQ_0_0.smt2 |   47.387s | 520.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_23_0.smt2 |   47.547s | 4572.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_19_0.smt2 |   47.843s | 4439.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__terminationS_50_0.smt2 |   48.193s | 732.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2__p24620_terminationG_0.smt2 |   49.624s | 654.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p22032_edge_closing_0.smt2 |   51.353s | 748.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_16_0.smt2 |   51.796s | 4431.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_22_0.smt2 |   51.863s | 4576.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MainGet.jar-obl-10__p10695_edge_closing_0.smt2 |   53.517s | 484.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_29_0.smt2 |   53.887s | 4574.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Graph.jar-obl-17__p29763_edge_closing_0.smt2 |   54.733s | 437.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__terminationS_51_0.smt2 |   54.880s | 664.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1467_edge_closing_0.smt2 |   55.136s | 430.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_24_0.smt2 |   55.596s | 4615.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_25_0.smt2 |   55.876s | 4612.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__randomwalk.t2__p8416_terminationG_0.smt2 |   56.920s | 377.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_26_0.smt2 |   58.861s | 4622.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT3678576972294594665.smt2 |   59.658s | 726.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__bs.t2_fixed__p17456_terminationG_0.smt2 |   61.196s | 476.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30338_terminationG_0.smt2 |   61.891s | 680.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MainFind.jar-obl-10__p10621_edge_closing_0.smt2 |   62.158s | 2017.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Samefringe.jar-obl-10__p11982_edge_closing_0.smt2 |   62.630s | 1016.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3256_terminationG_0.smt2 |   63.506s | 503.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p21995_terminationG_0.smt2 |   63.586s | 796.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_27_0.smt2 |   67.117s | 4600.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2_fixed__p551_terminationG_0.smt2 |   68.300s | 1065.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-K5O3aH.smt2              |   69.161s | 559.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2__p24821_edge_closing_0.smt2 |   69.493s | 591.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22639_terminationG_0.smt2 |   74.415s | 665.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAll.jar-obl-11__p9479_terminationG_0.smt2 |   74.624s | 912.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7607_terminationG_0.smt2 |   86.138s | 413.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__Et4.c__p22658_edge_closing_0.smt2 |   86.712s | 921.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27222_terminationG_0.smt2 |   87.074s | 819.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__db3.t2__terminationQ_0_0.smt2 |   87.136s | 1361.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1-striped.t2_fixed__p9299_terminationG_0.smt2 |   89.103s | 1016.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p21960_terminationG_0.smt2 |   94.358s | 706.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22531_terminationG_0.smt2 |   97.541s | 1484.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__sudoku.t2__p24867_terminationG_0.smt2 |  102.114s | 595.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30824_terminationG_0.smt2 |  103.286s | 429.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__db2.t2__terminationQ_0_0.smt2 |  103.915s | 1369.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2_fixed__p15180_terminationG_0.smt2 |  108.596s | 927.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-live.t2__p16639_terminationG_0.smt2 |  109.877s | 1322.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIteratorEntryLoop.jar-obl-12__p3358_terminationG_0.smt2 |  112.474s | 442.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3221_terminationG_0.smt2 |  121.489s | 808.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__BinTreeChanger.jar-obl-10__p27729_terminationG_0.smt2 |  123.709s | 594.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreatePut.jar-obl-10__p6496_terminationG_0.smt2 |  126.531s | 437.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MysteriousProgram.jar-obl-12__p11031_terminationG_0.smt2 |  129.628s | 634.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun6.t2_fixed__p1055_terminationG_0.smt2 |  134.342s | 777.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3311_terminationG_0.smt2 |  148.346s | 839.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted-fail.t2_fixed__p15830_terminationG_0.smt2 |  151.309s | 1719.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3301_terminationG_0.smt2 |  156.000s | 855.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_3_0.smt2 |  166.555s | 4770.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p17922_terminationG_0.smt2 |  170.173s | 946.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2__p24634_terminationG_0.smt2 |  170.916s | 805.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__sudoku.t2__p24862_terminationG_0.smt2 |  175.744s | 706.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__sas2.t2__p21302_terminationG_0.smt2 |  182.188s | 595.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_9_0.smt2 |  183.784s | 4823.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__efegp.t2__p21961_edge_closing_0.smt2 |  186.572s | 565.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_4_0.smt2 |  189.545s | 4685.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3164_terminationG_0.smt2 |  190.140s | 930.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_2_0.smt2 |  199.435s | 4798.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__upAndDown_rec.jar-obl-8__p13161_edge_closing_0.smt2 |  199.721s | 1160.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_1_0.smt2 |  207.289s | 4822.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__firewire.t2__p32301_edge_closing_0.smt2 |  208.045s | 1091.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27136_terminationG_0.smt2 |  217.015s | 1259.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__GulwaniJainKoskinen-PLDI2009-Fig1_true-termination.c__p23472_edge_closing_0.smt2 |  222.827s | 1186.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_6_0.smt2 |  225.662s | 4754.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_5_0.smt2 |  229.755s | 4884.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_0_0.smt2 |  237.793s | 4806.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.t2__p1768_terminationG_0.smt2 |  248.390s | 1217.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Matrix.jar-obl-16__p10849_edge_closing_0.smt2 |  249.855s | 771.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2_fixed__p15165_terminationG_0.smt2 |  253.568s | 1300.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_7_0.smt2 |  264.577s | 4858.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__TaylorSeriesIte.jar-obl-13__p12477_terminationG_0.smt2 |  273.618s | 609.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2__p626_terminationG_0.smt2 |  277.733s | 3248.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver.bug.t2__p24573_terminationG_0.smt2 |  306.592s | 1473.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted.t2_fixed__p16101_terminationG_0.smt2 |  326.396s | 2295.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22688_terminationG_0.smt2 |  330.998s | 1639.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12121_terminationG_0.smt2 |  332.338s | 899.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__NO_24.c__p24816_terminationG_0.smt2 |  348.551s | 996.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_8_0.smt2 |  359.060s | 5001.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3249_terminationG_0.smt2 |  359.776s | 1106.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-live.t2_fixed__p16560_terminationG_0.smt2 |  367.012s | 2068.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted-fail.t2__p16000_terminationG_0.smt2 |  382.485s | 1587.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/LCTES/digital-stopwatch.locals.nosummaries.smt2 |  387.781s | 776.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-live.t2_fixed__p16596_terminationG_0.smt2 |  408.037s | 2076.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__tqli.c.i.tqli.pl.t2.nor.t2.rlgfixed.t2__p25078_terminationG_0.smt2 |  418.906s | 1320.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__tqli.c.i.tqli.pl.t2.fixed.t2__p25046_edge_closing_0.smt2 |  427.827s | 926.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted.t2__p16269_terminationG_0.smt2 |  431.865s | 1882.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22640_terminationG_0.smt2 |  447.641s | 1450.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_4_0.smt2 |  450.633s | 5132.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__select.t2__p21400_edge_closing_0.smt2 |  462.550s | 886.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12223_terminationG_0.smt2 |  466.908s | 916.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Test1.jar-obl-8__p12801_terminationG_0.smt2 |  511.291s | 2483.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_20_0.smt2 |  521.788s | 5579.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12232_terminationG_0.smt2 |  527.721s | 1036.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__florian_sas2.t2__p32380_terminationG_0.smt2 |  549.842s | 1275.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-3wwoHp.smt2              |  557.460s | 1241.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p22000_terminationG_0.smt2 |  562.199s | 1349.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p22028_edge_closing_0.smt2 |  594.096s | 1147.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_16_0.smt2 |  596.307s | 5602.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_8_0.smt2 |  597.629s | 5343.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0788.smt2   |  600.050s | 186.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0787.smt2   |  600.055s | 184.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0058.smt2   |  600.056s | 207.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0509.smt2   |  600.057s | 181.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0608.smt2   |  600.062s | 318.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0776.smt2   |  600.063s | 324.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0220.smt2   |  600.065s | 182.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0265.smt2   |  600.066s | 325.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0887.smt2   |  600.067s | 376.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0221.smt2   |  600.068s | 183.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0508.smt2   |  600.068s | 181.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInvInitial.smt2 |  600.069s | 244.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0859.smt2   |  600.071s | 377.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0607.smt2   |  600.073s | 379.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0851.smt2   |  600.073s | 383.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0562.smt2   |  600.074s | 329.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0868.smt2   |  600.074s | 405.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0719.smt2   |  600.074s | 381.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0914.smt2   |  600.075s | 384.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0733.smt2   |  600.075s | 379.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0266.smt2   |  600.076s | 310.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0768.smt2   |  600.076s | 516.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0236.smt2   |  600.077s | 437.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInv8.smt2 |  600.077s | 227.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0824.smt2   |  600.078s | 375.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0941.smt2   |  600.078s | 525.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInvStepSimplified.smt2 |  600.078s | 321.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0553.smt2   |  600.079s | 315.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0545.smt2   |  600.079s | 327.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0490.smt2   |  600.080s | 301.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0832.smt2   |  600.081s | 527.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0551.smt2   |  600.081s | 350.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0499.smt2   |  600.082s | 328.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0769.smt2   |  600.082s | 480.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0906.smt2   |  600.082s | 510.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0823.smt2   |  600.083s | 378.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0931.smt2   |  600.083s | 381.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0498.smt2   |  600.083s | 300.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__agafp.t2__terminationS_0_0.smt2 |  600.083s | 317.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInv16.smt2 |  600.083s | 376.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0366.smt2   |  600.084s | 461.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0950.smt2   |  600.084s | 460.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0554.smt2   |  600.084s | 328.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0625.smt2   |  600.085s | 517.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0706.smt2   |  600.085s | 545.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0734.smt2   |  600.086s | 346.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0500.smt2   |  600.086s | 377.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0778.smt2   |  600.086s | 377.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0986.smt2   |  600.086s | 358.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0502.smt2   |  600.086s | 377.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0760.smt2   |  600.087s | 386.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0239.smt2   |  600.087s | 435.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0518.smt2   |  600.087s | 313.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0365.smt2   |  600.087s | 419.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0268.smt2   |  600.087s | 494.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0877.smt2   |  600.088s | 502.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0841.smt2   |  600.088s | 532.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0932.smt2   |  600.088s | 382.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0563.smt2   |  600.088s | 512.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0842.smt2   |  600.089s | 558.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0815.smt2   |  600.089s | 379.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0671.smt2   |  600.089s | 558.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0679.smt2   |  600.089s | 580.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0373.smt2   |  600.090s | 513.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0238.smt2   |  600.090s | 385.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0814.smt2   |  600.090s | 335.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0770.smt2   |  600.091s | 483.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0740.smt2   |  600.091s | 578.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0898.smt2   |  600.092s | 602.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0022.smt2   |  600.092s | 513.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0922.smt2   |  600.092s | 495.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0274.smt2   |  600.092s | 430.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0066.smt2   |  600.092s | 391.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0977.smt2   |  600.093s | 593.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0761.smt2   |  600.093s | 378.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0337.smt2   |  600.094s | 424.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0052.smt2   |  600.094s | 326.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0806.smt2   |  600.094s | 463.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0569.smt2   |  600.094s | 430.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0382.smt2   |  600.094s | 610.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0884.smt2   |  600.094s | 403.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0896.smt2   |  600.095s | 483.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0247.smt2   |  600.095s | 529.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0643.smt2   |  600.095s | 578.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__NO_13.jar-obl-8__p11440_edge_closing_0.smt2 |  600.095s | 855.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInv32.smt2 |  600.095s | 494.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInvFull.smt2 |  600.095s | 572.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0368.smt2   |  600.096s | 583.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0940.smt2   |  600.096s | 434.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0320.smt2   |  600.096s | 691.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0356.smt2   |  600.097s | 566.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0530.smt2   |  600.097s | 354.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0329.smt2   |  600.097s | 604.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-termination.c__p21397_terminationG_0.smt2 |  600.097s | 639.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0517.smt2   |  600.098s | 327.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0572.smt2   |  600.098s | 420.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0995.smt2   |  600.098s | 367.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__NO_13.c__p24750_terminationG_0.smt2 |  600.098s | 1111.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0302.smt2   |  600.099s | 630.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0392.smt2   |  600.099s | 728.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0070.smt2   |  600.099s | 461.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0707.smt2   |  600.099s | 513.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0257.smt2   |  600.100s | 381.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0544.smt2   |  600.100s | 352.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0886.smt2   |  600.100s | 377.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0688.smt2   |  600.101s | 638.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__MirrorIntervSim.c__p24484_terminationG_0.smt2 |  600.101s | 522.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0653.smt2   |  600.102s | 679.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0834.smt2   |  600.102s | 571.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0597.smt2   |  600.102s | 710.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0149.smt2   |  600.102s | 706.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInv128.smt2 |  600.102s | 579.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0275.smt2   |  600.103s | 383.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0869.smt2   |  600.103s | 478.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0959.smt2   |  600.103s | 508.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0364.smt2   |  600.103s | 402.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0958.smt2   |  600.103s | 515.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/TA_03.smt2      |  600.103s | 454.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0537.smt2   |  600.103s | 532.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0248.smt2   |  600.104s | 516.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0670.smt2   |  600.104s | 597.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0968.smt2   |  600.104s | 669.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0860.smt2   |  600.104s | 343.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0300.smt2   |  600.104s | 624.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0226.smt2   |  600.104s | 399.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__MirrorInterv.c__p24450_edge_closing_0.smt2 |  600.104s | 492.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0616.smt2   |  600.105s | 602.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0985.smt2   |  600.105s | 545.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0779.smt2   |  600.105s | 401.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0068.smt2   |  600.105s | 564.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-unsat-05.smt2            |  600.105s | 784.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0482.smt2   |  600.106s | 615.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0751.smt2   |  600.106s | 405.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0050.smt2   |  600.106s | 427.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0571.smt2   |  600.107s | 545.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0535.smt2   |  600.107s | 599.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0483.smt2   |  600.107s | 551.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0904.smt2   |  600.107s | 481.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0013.smt2   |  600.107s | 707.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0716.smt2   |  600.107s | 566.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0536.smt2   |  600.107s | 637.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0023.smt2   |  600.108s | 553.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0923.smt2   |  600.108s | 458.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0850.smt2   |  600.108s | 604.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0698.smt2   |  600.108s | 757.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0644.smt2   |  600.109s | 565.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0077.smt2   |  600.109s | 611.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0752.smt2   |  600.110s | 409.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0411.smt2   |  600.110s | 874.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0913.smt2   |  600.110s | 642.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0976.smt2   |  600.110s | 655.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0715.smt2   |  600.110s | 548.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0230.smt2   |  600.110s | 434.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/sqrtStepFinal.smt2 |  600.110s | 786.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0626.smt2   |  600.111s | 583.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0229.smt2   |  600.111s | 436.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0642.smt2   |  600.111s | 624.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0350.smt2   |  600.112s | 596.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0419.smt2   |  600.112s | 775.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0949.smt2   |  600.113s | 489.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInv64.smt2 |  600.113s | 425.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0833.smt2   |  600.114s | 510.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0599.smt2   |  600.115s | 830.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0581.smt2   |  600.115s | 689.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0895.smt2   |  600.115s | 454.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0463.smt2   |  600.115s | 735.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__Narrowing.c__p24540_terminationG_0.smt2 |  600.115s | 704.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__narrowing_rec.jar-obl-8__p11067_terminationG_0.smt2 |  600.115s | 773.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0805.smt2   |  600.116s | 491.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0967.smt2   |  600.116s | 512.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0994.smt2   |  600.116s | 413.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0338.smt2   |  600.116s | 459.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0347.smt2   |  600.117s | 721.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0301.smt2   |  600.117s | 623.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT6545992645874542347.smt2 |  600.117s | 845.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0455.smt2   |  600.118s | 671.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0617.smt2   |  600.118s | 636.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0374.smt2   |  600.118s | 576.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0367.smt2   |  600.118s | 499.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0328.smt2   |  600.118s | 647.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0355.smt2   |  600.119s | 529.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0112.smt2   |  600.119s | 793.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-narrowing.jar-obl-8__p14386_terminationG_0.smt2 |  600.119s | 720.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0878.smt2   |  600.120s | 529.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0797.smt2   |  600.120s | 665.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__UpAndDown.c__p26203_terminationG_0.smt2 |  600.120s | 608.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0742.smt2   |  600.121s | 515.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0481.smt2   |  600.121s | 700.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__NonTerminationSimple7_false-termination.c__p25148_terminationG_0.smt2 |  600.121s | 941.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0049.smt2   |  600.122s | 645.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0745.smt2   |  600.122s | 679.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0410.smt2   |  600.122s | 933.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0680.smt2   |  600.122s | 553.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__Pure3Phase_true-termination.c__p25560_terminationG_0.smt2 |  600.122s | 1233.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0796.smt2   |  600.123s | 768.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0212.smt2   |  600.123s | 863.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__whileSingle_rec.jar-obl-8__p15018_terminationG_0.smt2 |  600.123s | 766.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-unsat-02.smt2            |  600.123s | 980.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0901.smt2   |  600.124s | 512.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0635.smt2   |  600.124s | 722.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0286.smt2   |  600.125s | 733.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0527.smt2   |  600.125s | 598.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0131.smt2   |  600.125s | 919.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0689.smt2   |  600.126s | 695.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0383.smt2   |  600.126s | 552.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0148.smt2   |  600.126s | 699.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0203.smt2   |  600.126s | 952.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0441.smt2   |  600.126s | 811.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0472.smt2   |  600.127s | 791.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0409.smt2   |  600.127s | 931.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT7924349461296395393.smt2 |  600.127s | 768.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0139.smt2   |  600.128s | 717.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2_fixed__p24591_edge_closing_0.smt2 |  600.128s | 769.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0592.smt2   |  600.129s | 826.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0292.smt2   |  600.129s | 802.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0454.smt2   |  600.129s | 764.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__Swingers.c__p26085_terminationG_0.smt2 |  600.129s | 942.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-termination.c__p21133_terminationG_0.smt2 |  600.129s | 1068.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0582.smt2   |  600.130s | 819.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0401.smt2   |  600.130s | 773.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0122.smt2   |  600.131s | 776.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0067.smt2   |  600.131s | 571.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__UpAndDownIneq.c__p26236_terminationG_0.smt2 |  600.131s | 901.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0427.smt2   |  600.132s | 782.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0662.smt2   |  600.132s | 778.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0529.smt2   |  600.132s | 617.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0725.smt2   |  600.133s | 951.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0311.smt2   |  600.133s | 805.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0040.smt2   |  600.133s | 788.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0446.smt2   |  600.133s | 979.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInvVar1.smt2 |  600.133s | 699.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0580.smt2   |  600.134s | 848.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0697.smt2   |  600.134s | 904.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0611.smt2   |  600.134s | 602.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0031.smt2   |  600.134s | 701.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__AProVE12-cyclic-Visit.jar-obl-9__p27687_edge_closing_0.smt2 |  600.135s | 979.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0473.smt2   |  600.136s | 794.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0983.smt2   |  600.138s | 618.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/mcm/99.smt2                           |  600.138s | 1201.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0743.smt2   |  600.139s | 569.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/TA_13.smt2      |  600.139s | 1061.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0426.smt2   |  600.139s | 879.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0418.smt2   |  600.139s | 1007.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__NO_13.jar-obl-8__p11405_terminationG_0.smt2 |  600.139s | 867.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0041.smt2   |  600.140s | 704.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInvStep.smt2 |  600.140s | 663.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0104.smt2   |  600.141s | 816.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0436.smt2   |  600.141s | 989.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0283.smt2   |  600.141s | 980.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0014.smt2   |  600.142s | 659.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0140.smt2   |  600.142s | 648.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0202.smt2   |  600.143s | 991.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0389.smt2   |  600.143s | 1000.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0085.smt2   |  600.143s | 692.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0136.smt2   |  600.144s | 1083.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0394.smt2   |  600.144s | 832.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0724.smt2   |  600.144s | 954.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0211.smt2   |  600.145s | 837.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0310.smt2   |  600.145s | 677.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0717.smt2   |  600.145s | 721.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0589.smt2   |  600.146s | 949.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0346.smt2   |  600.146s | 724.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0110.smt2   |  600.147s | 973.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/MC_03.smt2      |  600.147s | 708.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6218_terminationG_0.smt2 |  600.147s | 1060.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/mcm/26.smt2                           |  600.149s | 1132.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0661.smt2   |  600.151s | 795.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0076.smt2   |  600.151s | 705.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/sqrtStepFinala.smt2 |  600.151s | 969.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0293.smt2   |  600.153s | 742.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0723.smt2   |  600.154s | 859.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0445.smt2   |  600.154s | 1176.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0464.smt2   |  600.155s | 820.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0402.smt2   |  600.156s | 966.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0194.smt2   |  600.156s | 1105.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0400.smt2   |  600.156s | 755.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0138.smt2   |  600.157s | 787.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/TA_05.smt2      |  600.158s | 853.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0176.smt2   |  600.158s | 1161.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0121.smt2   |  600.159s | 793.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0100.smt2   |  600.159s | 799.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0598.smt2   |  600.160s | 835.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0163.smt2   |  600.160s | 1221.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-unsat-04.smt2            |  600.160s | 1153.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0424.smt2   |  600.163s | 1366.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0130.smt2   |  600.163s | 1118.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/MF_03.smt2      |  600.164s | 1235.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0113.smt2   |  600.165s | 849.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0325.smt2   |  600.165s | 1101.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0319.smt2   |  600.166s | 753.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0428.smt2   |  600.166s | 863.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__4NestedWith3Variables_true-termination.c__p20212_terminationG_0.smt2 |  600.166s | 1499.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__dumper.t2__p19134_terminationG_0.smt2 |  600.167s | 1162.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0391.smt2   |  600.169s | 804.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__sas2.t2__p21297_terminationG_0.smt2 |  600.171s | 1052.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6198_terminationG_0.smt2 |  600.172s | 1335.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6202_terminationG_0.smt2 |  600.172s | 1100.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Swingers.jar-obl-8__p12435_terminationG_0.smt2 |  600.172s | 1228.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__tqli.t2_fixed__p25201_edge_closing_0.smt2 |  600.173s | 1035.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/MS_04.smt2      |  600.174s | 827.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0103.smt2   |  600.174s | 989.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0451.smt2   |  600.175s | 1274.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun6.t2_fixed__p1066_edge_closing_0.smt2 |  600.176s | 1166.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fourn.c.i.fourn.pl.t2.nor.t2.rlgfixed.t2__p32699_edge_closing_0.smt2 |  600.176s | 1127.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0578.smt2   |  600.177s | 1224.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0590.smt2   |  600.177s | 962.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0175.smt2   |  600.182s | 1103.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__LessLeaves.jar-obl-10__p10002_edge_closing_0.smt2 |  600.182s | 1427.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/SC_08.smt2      |  600.183s | 1292.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0032.smt2   |  600.183s | 991.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6188_terminationG_0.smt2 |  600.184s | 1316.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__NO_24.jar-obl-8__p11510_terminationG_0.smt2 |  600.187s | 2042.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6193_terminationG_0.smt2 |  600.188s | 1192.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fourn.c.i.fourn.pl.t2.fixed.t2__p32602_terminationG_0.smt2 |  600.191s | 1161.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0284.smt2   |  600.193s | 981.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-fib.jar-obl-8__p13896_terminationG_0.smt2 |  600.193s | 1604.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fourn.t2__p32713_terminationG_0.smt2 |  600.198s | 1409.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0437.smt2   |  600.201s | 1179.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__p1650_edge_closing_0.smt2 |  600.207s | 1476.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12256_terminationG_0.smt2 |  600.211s | 1238.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-unsat-03.smt2            |  600.211s | 1224.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0157.smt2   |  600.212s | 1747.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0193.smt2   |  600.216s | 1378.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIteratorEntryLoop.jar-obl-12__p3363_edge_closing_0.smt2 |  600.218s | 1919.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0184.smt2   |  600.221s | 1361.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-MVylXc.smt2              |  600.221s | 1975.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12128_terminationG_0.smt2 |  600.224s | 1258.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0158.smt2   |  600.227s | 1640.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-fib.jar-obl-8__p13881_terminationG_0.smt2 |  600.230s | 1282.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6219_terminationG_0.smt2 |  600.235s | 1292.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-l6cqQI.smt2              |  600.236s | 1789.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2__p24649_terminationG_0.smt2 |  600.237s | 1790.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__LessLeaves.jar-obl-10__p10014_edge_closing_0.smt2 |  600.242s | 1517.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__brp_withassume.t2__p17437_edge_closing_0.smt2 |  600.246s | 1897.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun7.t2__p1167_edge_closing_0.smt2 |  600.256s | 1368.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fourn.t2__p32708_terminationG_0.smt2 |  600.261s | 1538.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12184_terminationG_0.smt2 |  600.265s | 1592.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__tqli.t2__p25217_terminationG_0.smt2 |  600.271s | 2007.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__nakata.t2__p5310_terminationG_0.smt2 |  600.275s | 1298.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/MC_09.smt2      |  600.286s | 2109.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreatePut.jar-obl-10__p6506_edge_closing_0.smt2 |  600.291s | 1977.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted-fail.t2__p16028_terminationG_0.smt2 |  600.301s | 2438.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12155_terminationG_0.smt2 |  600.308s | 1811.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted-fail.t2_fixed__p15846_terminationG_0.smt2 |  600.326s | 3054.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2_fixed__p1608_terminationG_0.smt2 |  600.330s | 2421.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted.t2__p16279_terminationG_0.smt2 |  600.331s | 2462.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__tqli.c.i.tqli.pl.t2.fixed.t2__p25001_terminationG_0.smt2 |  600.341s | 2042.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted.t2__p16298_terminationG_0.smt2 |  600.356s | 2592.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__nakata.t2__p5352_edge_closing_0.smt2 |  600.394s | 1675.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/MC_11.smt2      |  600.406s | 3447.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__destroy_seg_leak.t2_fixed__p18858_edge_closing_0.smt2 |  600.407s | 1510.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchildlive-succeed.t2__p16426_terminationG_0.smt2 |  600.442s | 3606.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted-fail.t2_fixed__p15799_terminationG_0.smt2 |  600.464s | 3395.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted-fail.t2__p15941_terminationG_0.smt2 |  600.472s | 2614.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_7_0.smt2 |  600.510s | 5395.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_28_0.smt2 |  600.515s | 5536.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-3-new.t2_fixed__p21803_terminationG_0.smt2 |  600.538s | 4686.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_13_0.smt2 |  600.542s | 5633.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_26_0.smt2 |  600.552s | 5651.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_6_0.smt2 |  600.553s | 5422.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_32_0.smt2 |  600.556s | 5453.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_14_0.smt2 |  600.556s | 5774.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_18_0.smt2 |  600.563s | 5725.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_15_0.smt2 |  600.564s | 5625.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_31_0.smt2 |  600.565s | 5644.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-3.t2_fixed__p22135_terminationG_0.smt2 |  600.583s | 5377.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_17_0.smt2 |  600.587s | 5602.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_2_0.smt2 |  600.591s | 5367.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_22_0.smt2 |  600.591s | 5751.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_3_0.smt2 |  600.603s | 5467.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_19_0.smt2 |  600.639s | 5753.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_24_0.smt2 |  600.663s | 5726.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/RTA_093.smt2    |  600.703s | 6776.0MiB| timeout | 0 |  |  |