# .

* SAT 282
* UNSAT 140
* TIMEOUT 378
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-QF_NIA_hard-timeout10min-bb2
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: f880fdccee614547c38c19beb7af5a027961646b
Z3 branch: core_min
Z3 options: "-T:600 -v:0 smt.threads=8 tactic.default_tactic=smt smt.auto_config=false smt_parallel.num_global_bb_batch_threads=2"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_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_0153.smt2   |    0.203s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0334.smt2   |    0.212s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0493.smt2   |    0.224s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0678.smt2   |    0.225s | 212.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0099.smt2   |    0.227s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0484.smt2   |    0.230s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0703.smt2   |    0.232s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0097.smt2   |    0.235s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0684.smt2   |    0.236s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0963.smt2   |    0.239s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0603.smt2   |    0.242s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0190.smt2   |    0.244s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0486.smt2   |    0.246s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-7fXGzy.smt2              |    0.246s | 225.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0369.smt2   |    0.248s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0816.smt2   |    0.252s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0883.smt2   |    0.264s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0244.smt2   |    0.267s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0315.smt2   |    0.275s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0330.smt2   |    0.279s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0944.smt2   |    0.281s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0722.smt2   |    0.281s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0825.smt2   |    0.284s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0656.smt2   |    0.288s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0540.smt2   |    0.303s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ex36.t2__p30283_safety_0.smt2 |    0.313s | 229.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0920.smt2   |    0.316s | 211.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ex36.t2_fixed__p23592_safety_0.smt2 |    0.320s | 232.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ex36.t2__p31955_safety_0.smt2 |    0.334s | 235.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__edn.t2__p20326_safety_0.smt2 |    0.358s | 231.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-lcm.jar-obl-10__p14126_edge_closing_0.smt2 |    0.372s | 246.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__RandomHard.jar-obl-10__p11831_safety_0.smt2 |    0.384s | 245.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__edn.t2__p20710_safety_0.smt2 |    0.406s | 234.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.414s | 231.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__edn.t2__p20632_safety_0.smt2 |    0.439s | 240.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p2225_safety_0.smt2 |    0.486s | 276.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ex36.t2__p31845_safety_0.smt2 |    0.492s | 236.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p32401_safety_0.smt2 |    0.508s | 276.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateRemove.jar-obl-11__p6932_safety_0.smt2 |    0.512s | 275.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_2vars_false-termination.c__p26899_terminationG_0.smt2 |    0.526s | 230.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreatePut.jar-obl-10__p6354_safety_0.smt2 |    0.542s | 282.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1398_edge_closing_0.smt2 |    0.551s | 271.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_true-termination.c__p20893_terminationG_0.smt2 |    0.553s | 284.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MainFind.jar-obl-10__p10621_edge_closing_0.smt2 |    0.564s | 259.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p1606_safety_0.smt2 |    0.573s | 301.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/SAT14/1813.smt2      |    0.577s | 287.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MainMove.jar-obl-11__p10745_edge_closing_0.smt2 |    0.596s | 262.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p322_safety_0.smt2 |    0.602s | 277.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p4392_safety_0.smt2 |    0.604s | 283.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/LCTES/digital-stopwatch.locals.smt2   |    0.605s | 270.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreatePut.jar-obl-10__p5497_safety_0.smt2 |    0.627s | 284.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91.t2__p2940_edge_closing_0.smt2 |    0.627s | 287.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MainFind.jar-obl-10__p10608_edge_closing_0.smt2 |    0.629s | 263.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-mirrorInterv.jar-obl-8__p14289_edge_closing_0.smt2 |    0.629s | 335.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31198_safety_0.smt2 |    0.632s | 279.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n-5.t2_fixed__p4589_terminationG_0.smt2 |    0.642s | 259.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT1335852993657230070.smt2 |    0.655s | 247.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7192_safety_0.smt2 |    0.699s | 332.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Samefringe.jar-obl-10__p11982_edge_closing_0.smt2 |    0.706s | 274.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p2436_safety_0.smt2 |    0.725s | 301.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__List.jar-obl-12__p10223_edge_closing_0.smt2 |    0.740s | 240.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-5-filtered.t2__p22882_terminationG_0.smt2 |    0.755s | 348.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p31928_safety_0.smt2 |    0.761s | 313.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31295_safety_0.smt2 |    0.784s | 314.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/LassoRanker/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-termination.c_Iteration1_Loop+nonterminationTemplate_0.smt2 |    0.785s | 235.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_3vars_false-termination.c__p27027_terminationG_0.smt2 |    0.790s | 254.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p1691_safety_0.smt2 |    0.798s | 311.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p5318_safety_0.smt2 |    0.808s | 319.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p1659_safety_0.smt2 |    0.850s | 312.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31063_safety_0.smt2 |    0.851s | 312.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT5753280746557461985.smt2 |    0.852s | 256.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Fig1_true-termination.c__p22155_terminationG_0.smt2 |    0.881s | 282.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MainGet.jar-obl-10__p10695_edge_closing_0.smt2 |    0.896s | 250.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT3457830339872275636.smt2 |    0.898s | 259.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-6k3pKM.smt2              |    0.959s | 271.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MainMove.jar-obl-11__p10752_edge_closing_0.smt2 |    0.971s | 274.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30026_safety_0.smt2 |    0.990s | 317.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__Prim_4.t2__p8016_terminationG_0.smt2 |    1.051s | 300.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Flatten.jar-obl-10__p29378_safety_0.smt2 |    1.066s | 336.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30127_safety_0.smt2 |    1.074s | 322.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31152_safety_0.smt2 |    1.120s | 321.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ppblock.t2__p7746_edge_closing_0.smt2 |    1.179s | 317.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p5104_safety_0.smt2 |    1.189s | 331.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-mirrorInterv.jar-obl-8__p14269_terminationG_0.smt2 |    1.194s | 265.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p4544_terminationG_0.smt2 |    1.202s | 407.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreatePut.jar-obl-10__p6217_safety_0.smt2 |    1.206s | 385.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1377_edge_closing_0.smt2 |    1.212s | 297.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT4259464554444412647.smt2 |    1.259s | 263.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p19848_safety_0.smt2 |    1.296s | 356.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__AProVE12-cyclic-Visit.jar-obl-9__p27687_edge_closing_0.smt2 |    1.301s | 280.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__BinTreeChanger.jar-obl-10__p27729_terminationG_0.smt2 |    1.325s | 301.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__opt-tree.c.t2__p6339_terminationG_0.smt2 |    1.349s | 441.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIteratorKeyLoop.jar-obl-12__p3697_safety_0.smt2 |    1.370s | 326.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-n1.t2_fixed__p23107_safety_0.smt2 |    1.418s | 314.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p5158_safety_0.smt2 |    1.433s | 330.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1-striped.t2__p12897_safety_0.smt2 |    1.434s | 348.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30539_safety_0.smt2 |    1.473s | 438.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__Prim_4.t2__p7976_terminationG_0.smt2 |    1.490s | 305.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__small15.t2__p23742_terminationG_0.smt2 |    1.495s | 292.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIteratorEntryLoop.jar-obl-12__p3178_safety_0.smt2 |    1.505s | 322.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__polyrank4.t2__p7482_terminationG_0.smt2 |    1.549s | 317.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__polyrank4.t2__p7477_terminationG_0.smt2 |    1.628s | 313.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31805_safety_0.smt2 |    1.641s | 450.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p19834_safety_0.smt2 |    1.648s | 359.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p2746_safety_0.smt2 |    1.657s | 445.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__AlternatingGrowReduceRec2.jar-obl-9__p27530_edge_closing_0.smt2 |    1.660s | 278.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__small15.t2__p23781_edge_closing_0.smt2 |    1.663s | 297.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__Prim_4.t2__p7936_terminationG_0.smt2 |    1.678s | 295.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT9064001295904670492.smt2 |    1.711s | 271.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p29915_safety_0.smt2 |    1.715s | 327.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__GulwaniJainKoskinen-PLDI2009-Fig1_true-termination.c__p23472_edge_closing_0.smt2 |    1.725s | 329.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__pgarch.t2__p7283_terminationG_0.smt2 |    1.763s | 556.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1287_edge_closing_0.smt2 |    1.763s | 256.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1-striped.t2_fixed__p9992_safety_0.smt2 |    1.778s | 352.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22607_safety_0.smt2 |    1.781s | 321.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.801s | 284.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p18338_safety_0.smt2 |    1.802s | 351.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__nakata.t2__p5305_terminationG_0.smt2 |    1.885s | 546.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__MirrorInterv.c__p24379_terminationG_0.smt2 |    1.911s | 287.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p32020_terminationG_0.smt2 |    1.946s | 455.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIsEmpty.jar-obl-10__p2113_safety_0.smt2 |    2.010s | 448.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__Prim_4.t2__p8035_terminationG_0.smt2 |    2.091s | 285.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31079_safety_0.smt2 |    2.175s | 460.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7322_safety_0.smt2 |    2.302s | 458.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p18948_safety_0.smt2 |    2.374s | 365.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/SAT14/585.smt2       |    2.443s | 503.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1485_edge_closing_0.smt2 |    2.465s | 328.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__NO_13.jar-obl-8__p11419_edge_closing_0.smt2 |    2.468s | 279.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p4624_safety_0.smt2 |    2.527s | 452.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31303_safety_0.smt2 |    2.582s | 456.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIteratorEntryLoop.jar-obl-12__p3008_safety_0.smt2 |    2.620s | 451.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p31947_safety_0.smt2 |    2.719s | 466.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1-striped.t2__p12943_safety_0.smt2 |    2.767s | 387.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAll.jar-obl-11__p9558_terminationG_0.smt2 |    2.771s | 634.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__svcomp_ex2.c__p25831_terminationG_0.smt2 |    2.784s | 366.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Matrix.jar-obl-16__p10815_safety_0.smt2 |    2.786s | 380.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ppblockterm.t2__p7916_edge_closing_0.smt2 |    2.827s | 323.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30313_safety_0.smt2 |    2.981s | 470.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT5521985939949569030.smt2 |    3.002s | 387.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27236_edge_closing_0.smt2 |    3.155s | 408.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-p9MQp4.smt2              |    3.155s | 312.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT1437438160177275586.smt2 |    3.161s | 339.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateRemove.jar-obl-11__p7017_terminationG_0.smt2 |    3.255s | 478.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22603_safety_0.smt2 |    3.456s | 558.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT1700028870436976635.smt2 |    3.505s | 264.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-live.t2_fixed__p16559_terminationG_0.smt2 |    3.588s | 795.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27239_edge_closing_0.smt2 |    3.608s | 888.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1460_edge_closing_0.smt2 |    3.631s | 344.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27166_terminationG_0.smt2 |    3.888s | 375.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1314_edge_closing_0.smt2 |    4.047s | 308.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__p-5.t2_fixed__p6782_edge_closing_0.smt2 |    4.115s | 408.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__st88.t2__p24217_terminationG_0.smt2 |    4.154s | 307.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-live.t2_fixed__p16564_terminationG_0.smt2 |    4.192s | 828.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__GulwaniJainKoskinen-PLDI2009-Fig1_true-termination.c__p23757_edge_closing_0.smt2 |    4.280s | 505.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1440_edge_closing_0.smt2 |    4.402s | 351.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT5642158517481563632.smt2 |    4.554s | 403.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1320_edge_closing_0.smt2 |    4.556s | 340.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__NO_03.c__p24634_terminationG_0.smt2 |    4.673s | 284.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p19377_safety_0.smt2 |    4.762s | 385.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT8619300169146917506.smt2 |    4.784s | 383.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Graph.jar-obl-17__p29774_edge_closing_0.smt2 |    4.810s | 342.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1378_edge_closing_0.smt2 |    4.820s | 348.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p31859_terminationG_0.smt2 |    4.865s | 593.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsValue.jar-obl-11__p32720_terminationG_0.smt2 |    5.154s | 522.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT463192377960637155.smt2 |    5.205s | 334.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-fib.jar-obl-8__p13930_edge_closing_0.smt2 |    5.333s | 394.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT7201733644041072759.smt2 |    5.352s | 353.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__janne_complex.t2__p2254_terminationG_0.smt2 |    5.664s | 391.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__matmul.t2_fixed__p2649_terminationG_0.smt2 |    5.667s | 396.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__janne_complex.t2__p2020_terminationG_0.smt2 |    5.755s | 362.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1354_edge_closing_0.smt2 |    5.759s | 377.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT180444191153863419.smt2 |    5.825s | 372.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT725924178667047452.smt2 |    5.876s | 370.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p8402_safety_0.smt2 |    6.016s | 962.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT9062228803117299674.smt2 |    6.139s | 491.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-termination.c__p21133_terminationG_0.smt2 |    6.209s | 388.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT5468773551032053543.smt2 |    6.248s | 591.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1413_edge_closing_0.smt2 |    6.323s | 405.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Test6.jar-obl-13__terminationS_24_0.smt2 |    6.592s | 922.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n-5.t2__p4703_edge_closing_0.smt2 |    6.678s | 458.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6225_edge_closing_0.smt2 |    6.815s | 577.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__narrowKonv_rec.jar-obl-8__p11136_edge_closing_0.smt2 |    6.825s | 256.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT6647586385534524663.smt2 |    7.105s | 400.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__DivTernary.jar-obl-10__p28667_terminationG_0.smt2 |    7.130s | 987.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p7969_safety_0.smt2 |    7.209s | 924.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1437_edge_closing_0.smt2 |    7.265s | 361.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.t2_fixed__terminationS_24_0.smt2 |    7.341s | 519.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.09_true-termination.c__p21247_terminationG_0.smt2 |    7.421s | 540.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__polyrank5.t2__p7556_terminationG_0.smt2 |    7.475s | 428.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__upAndDown_rec.jar-obl-8__p13161_edge_closing_0.smt2 |    7.724s | 416.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p8584_safety_0.smt2 |    7.838s | 1419.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__zlib-crc32-BYFOUR.c.t2__p26484_terminationG_0.smt2 |    7.915s | 400.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.t2_fixed__terminationS_55_0.smt2 |    8.017s | 443.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__UpAndDownIneq.c__p26235_terminationG_0.smt2 |    8.400s | 291.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__svdcmp.t2__term_unfeasibility_8_0.smt2 |    8.414s | 385.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2_fixed__p519_terminationG_0.smt2 |    8.489s | 993.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT2214668917450755150.smt2 |    8.641s | 396.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p8337_safety_0.smt2 |    8.683s | 1416.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p8073_terminationG_0.smt2 |    9.048s | 1305.0MiB| sat | 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 |    9.116s | 447.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2_fixed__terminationS_55_0.smt2 |    9.119s | 450.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.t2_fixed__terminationS_54_0.smt2 |    9.129s | 447.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p9027_safety_0.smt2 |    9.130s | 1524.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2_fixed__terminationS_25_0.smt2 |    9.219s | 532.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT6531155344723557531.smt2 |    9.513s | 421.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2_fixed__terminationS_27_0.smt2 |    9.584s | 540.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2__p24820_edge_closing_0.smt2 |    9.653s | 491.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__firewire.t2__terminationS_19_0.smt2 |    9.731s | 499.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAllAt.jar-obl-17__p8348_safety_0.smt2 |   10.067s | 1467.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12239_terminationG_0.smt2 |   10.148s | 425.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1406_edge_closing_0.smt2 |   10.193s | 458.0MiB| sat | 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 |   10.360s | 449.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__nakata.t2__terminationS_6_0.smt2 |   10.395s | 438.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 |   10.420s | 528.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__UpAndDown.c__p26202_terminationG_0.smt2 |   10.511s | 270.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT1813676864021281701.smt2 |   10.675s | 493.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27222_terminationG_0.smt2 |   10.956s | 471.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 |   11.071s | 536.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__janne_complex.t2__p2193_terminationG_0.smt2 |   11.072s | 397.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Count.jar-obl-10-2__p28115_terminationG_0.smt2 |   11.098s | 1105.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2__p679_terminationG_0.smt2 |   11.420s | 1884.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p17931_terminationG_0.smt2 |   11.682s | 455.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreate.jar-obl-10__p4709_terminationG_0.smt2 |   11.690s | 650.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT2276070888632403184.smt2 |   11.694s | 450.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__agafp.t2__p15626_terminationG_0.smt2 |   11.722s | 300.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p21995_terminationG_0.smt2 |   11.932s | 439.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIteratorEntryLoop.jar-obl-12__p3188_terminationG_0.smt2 |   12.758s | 663.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__ChooseLife.jar-obl-8__p27825_terminationG_0.smt2 |   12.768s | 356.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27186_terminationG_0.smt2 |   13.551s | 564.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-607QpU.smt2              |   13.846s | 391.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__sas2.t2__terminationS_1_0.smt2 |   13.985s | 294.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__polyrank4.t2__p7520_terminationG_0.smt2 |   14.289s | 636.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1393_edge_closing_0.smt2 |   14.453s | 430.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT3712394338782947208.smt2 |   14.497s | 330.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT6981420136966712689.smt2 |   14.499s | 353.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__terminationS_25_0.smt2 |   14.816s | 802.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.855s | 779.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.t2__terminationS_25_0.smt2 |   14.899s | 581.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__randomwalk.t2__p8416_terminationG_0.smt2 |   16.001s | 456.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__terminationS_24_0.smt2 |   16.915s | 838.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 |   16.918s | 471.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1309_edge_closing_0.smt2 |   16.958s | 414.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 |   17.592s | 641.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7210_terminationG_0.smt2 |   17.694s | 535.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT5210162955256537540.smt2 |   17.738s | 512.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__janne_complex.t2__p2263_terminationG_0.smt2 |   18.146s | 624.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__terminationS_26_0.smt2 |   18.379s | 844.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_28_0.smt2 |   18.407s | 2591.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1409_edge_closing_0.smt2 |   19.126s | 444.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__terminationS_19_0.smt2 |   19.127s | 871.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_5_0.smt2 |   19.147s | 2606.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__svdcmp.c.i.svdcmp.pl.t2.nor.t2.rlgfixed.t2__terminationS_27_0.smt2 |   19.234s | 644.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__NO_13.jar-obl-8__p11459_terminationG_0.smt2 |   20.038s | 271.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27151_terminationG_0.smt2 |   20.082s | 508.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31345_terminationG_0.smt2 |   20.094s | 704.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Test6.jar-obl-13__terminationS_13_0.smt2 |   20.365s | 1016.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22519_safety_0.smt2 |   20.450s | 676.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3358_terminationG_0.smt2 |   20.639s | 632.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__terminationS_49_0.smt2 |   20.646s | 641.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27136_terminationG_0.smt2 |   20.659s | 547.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__terminationS_21_0.smt2 |   20.810s | 865.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30338_terminationG_0.smt2 |   21.009s | 710.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_31_0.smt2 |   21.114s | 2625.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_24_0.smt2 |   21.599s | 2649.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_30_0.smt2 |   21.671s | 2644.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__LessLeavesRec.jar-obl-10__p10043_terminationG_0.smt2 |   22.238s | 661.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Count.jar-obl-10-2__p28120_terminationG_0.smt2 |   22.451s | 668.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateContainsKey.jar-obl-11__p31167_terminationG_0.smt2 |   22.493s | 699.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_15_0.smt2 |   22.519s | 2659.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2__p680_terminationG_0.smt2 |   22.796s | 2416.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_14_0.smt2 |   22.971s | 2661.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7211_terminationG_0.smt2 |   23.915s | 707.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__db3.t2__term_unfeasibility_0_0.smt2 |   24.261s | 891.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22479_terminationG_0.smt2 |   24.585s | 1170.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12232_terminationG_0.smt2 |   24.661s | 525.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_11_0.smt2 |   24.789s | 2675.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun7.t2__p1142_terminationG_0.smt2 |   25.463s | 492.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Power.jar-obl-10__p11798_terminationG_0.smt2 |   25.573s | 604.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22639_terminationG_0.smt2 |   25.786s | 694.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MirrorBinTreeRec.jar-obl-9__p10899_terminationG_0.smt2 |   26.037s | 675.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__terminationS_49_0.smt2 |   26.191s | 661.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__ex11.t2__p22126_terminationG_0.smt2 |   26.293s | 289.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__db2.t2__term_unfeasibility_0_0.smt2 |   26.613s | 913.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_16_0.smt2 |   26.887s | 2679.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1.t2__terminationQ_0_0.smt2 |   27.352s | 1055.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun6.t2__p1092_terminationG_0.smt2 |   28.858s | 551.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p22032_edge_closing_0.smt2 |   28.865s | 763.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__narrowing_rec.jar-obl-8__p11066_terminationG_0.smt2 |   28.985s | 274.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2__p24821_edge_closing_0.smt2 |   29.133s | 665.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT6828719750442006249.smt2 |   29.207s | 656.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_2_0.smt2 |   29.263s | 2698.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateContainsAll.jar-obl-11__terminationS_19_0.smt2 |   29.475s | 2701.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2__p17922_terminationG_0.smt2 |   29.522s | 911.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 |   29.601s | 672.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.t2_fixed__terminationS_53_0.smt2 |   29.706s | 577.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-3-new.t2__p22118_edge_closing_0.smt2 |   29.720s | 3406.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1.t2_fixed__p721_terminationG_0.smt2 |   32.099s | 1607.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2__terminationQ_0_0.smt2 |   32.269s | 1114.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-plait.jar-obl-8__p14482_terminationG_0.smt2 |   32.280s | 671.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0496.smt2   |   32.669s | 223.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-narrowing.jar-obl-8__p14385_terminationG_0.smt2 |   33.123s | 269.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__DivTernary.jar-obl-10__terminationQ_0_0.smt2 |   34.134s | 902.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__agafp.t2__p15636_terminationG_0.smt2 |   35.106s | 334.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2__p597_terminationG_0.smt2 |   36.049s | 2436.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__whileNestedOffset_rec.jar-obl-9__p14933_safety_0.smt2 |   36.282s | 298.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12142_terminationG_0.smt2 |   36.474s | 680.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Ton_Chanh_15__Hanoi_plus_false-termination.c__p27084_terminationG_0.smt2 |   36.909s | 1113.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted.t2_fixed__p16110_terminationG_0.smt2 |   38.916s | 1659.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__sas2.t2__p21311_terminationG_0.smt2 |   39.434s | 322.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30004_terminationG_0.smt2 |   41.418s | 749.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT3839584170547805483.smt2 |   41.421s | 547.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Matrix.jar-obl-16__p10775_terminationG_0.smt2 |   41.452s | 501.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2_fixed__p24590_edge_closing_0.smt2 |   41.572s | 545.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1.t2_fixed__p784_terminationG_0.smt2 |   41.693s | 1002.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__agafp.t2__terminationS_0_0.smt2 |   42.813s | 315.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_18_0.smt2 |   43.047s | 5337.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_19_0.smt2 |   43.513s | 5414.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_20_0.smt2 |   44.265s | 5230.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p22028_edge_closing_0.smt2 |   44.678s | 1049.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_12_0.smt2 |   45.957s | 5365.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_14_0.smt2 |   46.370s | 5401.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_17_0.smt2 |   46.513s | 5481.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-termination.c__p21396_terminationG_0.smt2 |   46.720s | 340.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3256_terminationG_0.smt2 |   47.344s | 599.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_15_0.smt2 |   47.617s | 5406.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreatePut.jar-obl-10__p6135_terminationG_0.smt2 |   47.662s | 780.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2_fixed__p577_terminationG_0.smt2 |   47.680s | 1075.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_11_0.smt2 |   47.842s | 5366.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2_fixed__p15180_terminationG_0.smt2 |   48.351s | 980.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12223_terminationG_0.smt2 |   48.702s | 561.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_13_0.smt2 |   48.765s | 5414.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_28_0.smt2 |   49.576s | 5481.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2__p24620_terminationG_0.smt2 |   51.273s | 813.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p21950_terminationG_0.smt2 |   53.408s | 884.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.fixed.t2__terminationS_50_0.smt2 |   54.512s | 909.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_10_0.smt2 |   55.319s | 5403.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_21_0.smt2 |   55.388s | 5603.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed.t2__terminationS_51_0.smt2 |   55.522s | 897.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_16_0.smt2 |   56.440s | 5490.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_23_0.smt2 |   56.822s | 5601.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__opt-tree.c.t2__p6340_terminationG_0.smt2 |   57.255s | 808.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_22_0.smt2 |   57.274s | 5599.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_29_0.smt2 |   58.323s | 5597.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_25_0.smt2 |   58.490s | 5626.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__GulwaniJainKoskinen-PLDI2009-Fig1_true-termination.c__p23748_edge_closing_0.smt2 |   58.525s | 794.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT3678576972294594665.smt2 |   59.765s | 836.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-termination.c__p21344_edge_closing_0.smt2 |   59.785s | 542.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_26_0.smt2 |   60.081s | 5630.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_24_0.smt2 |   60.879s | 5629.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__janne_complex.t2__p2041_terminationG_0.smt2 |   63.768s | 627.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2_fixed__p551_terminationG_0.smt2 |   64.637s | 1308.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MysteriousProgram.jar-obl-12__terminationQ_0_0.smt2 |   67.916s | 660.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun6.t2_fixed__p1055_terminationG_0.smt2 |   68.160s | 801.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_27_0.smt2 |   71.497s | 5629.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateAddAll.jar-obl-11__p9479_terminationG_0.smt2 |   73.283s | 1100.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__bs.t2_fixed__p17456_terminationG_0.smt2 |   75.759s | 747.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3169_terminationG_0.smt2 |   83.780s | 966.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1467_edge_closing_0.smt2 |   85.597s | 571.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__MysteriousProgram.jar-obl-12__p11031_terminationG_0.smt2 |   88.814s | 731.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__db3.t2__terminationQ_0_0.smt2 |   91.742s | 1682.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreatePut.jar-obl-10__p6496_terminationG_0.smt2 |   95.127s | 501.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIteratorEntryLoop.jar-obl-12__p3358_terminationG_0.smt2 |   98.669s | 529.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__sudoku.t2__p24867_terminationG_0.smt2 |  101.253s | 735.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__Et4.c__p22658_edge_closing_0.smt2 |  101.293s | 2080.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__efegp.t2__p21961_edge_closing_0.smt2 |  102.555s | 523.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateClear.jar-obl-11__p30824_terminationG_0.smt2 |  103.563s | 511.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1.t2_fixed__p705_terminationG_0.smt2 |  104.717s | 1680.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-live.t2__p16639_terminationG_0.smt2 |  110.223s | 1671.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-3wwoHp.smt2              |  111.369s | 818.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p22000_terminationG_0.smt2 |  120.502s | 1064.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3311_terminationG_0.smt2 |  122.018s | 960.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateSize.jar-obl-10__p7607_terminationG_0.smt2 |  124.321s | 514.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-live.t2_fixed__p16596_terminationG_0.smt2 |  124.375s | 1660.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__db2.t2__terminationQ_0_0.smt2 |  125.857s | 1727.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Matrix.jar-obl-16__p10849_edge_closing_0.smt2 |  126.221s | 757.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c__p21960_terminationG_0.smt2 |  133.549s | 1249.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22531_terminationG_0.smt2 |  147.073s | 2018.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_3_0.smt2 |  153.652s | 5877.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_0_0.smt2 |  154.390s | 5856.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_4_0.smt2 |  156.603s | 5809.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_1_0.smt2 |  159.898s | 5797.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted-fail.t2_fixed__p15830_terminationG_0.smt2 |  164.182s | 2120.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3221_terminationG_0.smt2 |  171.234s | 1088.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_2_0.smt2 |  178.393s | 5906.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_9_0.smt2 |  183.046s | 6009.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1-striped.t2_fixed__p9299_terminationG_0.smt2 |  193.022s | 1489.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3301_terminationG_0.smt2 |  210.146s | 1175.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__Pure3Phase_true-termination.c__p25560_terminationG_0.smt2 |  213.431s | 986.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3249_terminationG_0.smt2 |  236.822s | 1162.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__s1.t2_fixed__p15165_terminationG_0.smt2 |  240.278s | 1605.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_8_0.smt2 |  245.128s | 6098.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun1b.t2__p626_terminationG_0.smt2 |  277.081s | 3972.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n-5.t2__p4682_terminationG_0.smt2 |  290.094s | 3635.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__afagp-fail.t2__p15516_edge_closing_0.smt2 |  307.415s | 1382.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__hqr.t2__p1768_terminationG_0.smt2 |  316.373s | 1574.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted-fail.t2__p16000_terminationG_0.smt2 |  320.233s | 1918.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun9.t2__p1357_edge_closing_0.smt2 |  326.419s | 1007.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_7_0.smt2 |  326.903s | 6110.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_5_0.smt2 |  332.835s | 6095.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juLinkedListCreateRemoveAll.jar-obl-11__terminationS_6_0.smt2 |  334.754s | 6108.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12183_terminationG_0.smt2 |  341.514s | 1528.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22640_terminationG_0.smt2 |  354.684s | 1837.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__firewire.t2__p32301_edge_closing_0.smt2 |  359.382s | 1460.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__sas2.t2__p21302_terminationG_0.smt2 |  359.701s | 959.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted.t2_fixed__p16101_terminationG_0.smt2 |  376.911s | 2862.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT7924349461296395393.smt2 |  385.863s | 1157.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-live.t2_fixed__p16560_terminationG_0.smt2 |  386.790s | 2544.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__mc91test.t2__p3164_terminationG_0.smt2 |  409.313s | 1365.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__florian_sas2.t2__p32399_terminationG_0.smt2 |  431.475s | 1008.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__NO_24.c__p24816_terminationG_0.smt2 |  436.041s | 1336.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted.t2__p16269_terminationG_0.smt2 |  458.786s | 2294.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12128_terminationG_0.smt2 |  469.711s | 1436.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_4_0.smt2 |  479.811s | 6439.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__florian_sas2.t2__p32384_terminationG_0.smt2 |  481.809s | 4118.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver.bug.t2__p24573_terminationG_0.smt2 |  491.160s | 2075.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted-fail.t2_fixed__p15846_terminationG_0.smt2 |  520.118s | 3666.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_20_0.smt2 |  523.819s | 6787.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Graph.jar-obl-17__p29763_edge_closing_0.smt2 |  532.528s | 877.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_16_0.smt2 |  551.093s | 6833.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__sudoku.t2__p24862_terminationG_0.smt2 |  575.535s | 1330.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2__p24634_terminationG_0.smt2 |  576.193s | 1579.0MiB| sat | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_2_0.smt2 |  578.942s | 6586.0MiB| unsat | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0508.smt2   |  600.045s | 218.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0058.smt2   |  600.058s | 242.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInv8.smt2 |  600.061s | 270.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInvInitial.smt2 |  600.066s | 283.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0490.smt2   |  600.067s | 339.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0221.smt2   |  600.068s | 218.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0220.smt2   |  600.069s | 217.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0787.smt2   |  600.071s | 220.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0509.smt2   |  600.071s | 216.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0776.smt2   |  600.072s | 412.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0761.smt2   |  600.077s | 414.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0788.smt2   |  600.077s | 221.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0734.smt2   |  600.079s | 415.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0868.smt2   |  600.079s | 435.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0815.smt2   |  600.080s | 413.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0226.smt2   |  600.080s | 432.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0265.smt2   |  600.081s | 364.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0931.smt2   |  600.081s | 422.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0257.smt2   |  600.083s | 420.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0052.smt2   |  600.085s | 362.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0266.smt2   |  600.085s | 347.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0770.smt2   |  600.085s | 516.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0923.smt2   |  600.087s | 541.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0823.smt2   |  600.087s | 417.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0338.smt2   |  600.087s | 504.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0268.smt2   |  600.088s | 535.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0502.smt2   |  600.088s | 413.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0608.smt2   |  600.089s | 356.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0778.smt2   |  600.090s | 412.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInv16.smt2 |  600.090s | 464.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0247.smt2   |  600.091s | 569.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0904.smt2   |  600.091s | 517.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0906.smt2   |  600.091s | 549.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0859.smt2   |  600.092s | 413.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0274.smt2   |  600.092s | 491.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0483.smt2   |  600.092s | 586.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0768.smt2   |  600.093s | 554.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0364.smt2   |  600.094s | 446.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0070.smt2   |  600.094s | 513.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0498.smt2   |  600.094s | 336.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0824.smt2   |  600.095s | 411.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0814.smt2   |  600.095s | 415.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0499.smt2   |  600.096s | 364.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInv128.smt2 |  600.096s | 552.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0625.smt2   |  600.097s | 560.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0355.smt2   |  600.098s | 564.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0530.smt2   |  600.099s | 390.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0050.smt2   |  600.099s | 458.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0066.smt2   |  600.100s | 428.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0275.smt2   |  600.101s | 423.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0760.smt2   |  600.102s | 419.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0932.smt2   |  600.102s | 423.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0878.smt2   |  600.103s | 564.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0895.smt2   |  600.104s | 530.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0887.smt2   |  600.104s | 411.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0545.smt2   |  600.104s | 503.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0769.smt2   |  600.105s | 515.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__MirrorInterv.c__p24450_edge_closing_0.smt2 |  600.105s | 619.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0500.smt2   |  600.106s | 372.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0365.smt2   |  600.106s | 461.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0877.smt2   |  600.106s | 535.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0611.smt2   |  600.106s | 638.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0914.smt2   |  600.106s | 421.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0368.smt2   |  600.107s | 618.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0860.smt2   |  600.107s | 413.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0302.smt2   |  600.108s | 669.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0751.smt2   |  600.108s | 447.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0733.smt2   |  600.108s | 415.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInvStepSimplified.smt2 |  600.108s | 406.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0901.smt2   |  600.109s | 548.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0248.smt2   |  600.109s | 576.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0140.smt2   |  600.109s | 686.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0841.smt2   |  600.109s | 568.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0898.smt2   |  600.111s | 637.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0752.smt2   |  600.111s | 448.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0337.smt2   |  600.111s | 460.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0842.smt2   |  600.111s | 592.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0553.smt2   |  600.111s | 476.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0886.smt2   |  600.111s | 417.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0562.smt2   |  600.112s | 728.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0806.smt2   |  600.112s | 499.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0884.smt2   |  600.113s | 436.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0626.smt2   |  600.114s | 629.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0851.smt2   |  600.114s | 416.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0554.smt2   |  600.114s | 641.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0230.smt2   |  600.115s | 709.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0707.smt2   |  600.115s | 662.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__whileSingle_rec.jar-obl-8__p15018_terminationG_0.smt2 |  600.115s | 585.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0517.smt2   |  600.116s | 504.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0850.smt2   |  600.116s | 639.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0328.smt2   |  600.116s | 647.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0551.smt2   |  600.116s | 771.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0068.smt2   |  600.116s | 611.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0572.smt2   |  600.117s | 607.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInv64.smt2 |  600.117s | 534.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0518.smt2   |  600.118s | 602.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0366.smt2   |  600.118s | 500.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0031.smt2   |  600.118s | 737.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/mcm/26.smt2                           |  600.118s | 833.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0607.smt2   |  600.119s | 415.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0455.smt2   |  600.119s | 705.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0719.smt2   |  600.119s | 417.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__UpAndDown.c__p26203_terminationG_0.smt2 |  600.119s | 693.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInvFull.smt2 |  600.119s | 769.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0238.smt2   |  600.120s | 627.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0922.smt2   |  600.122s | 534.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0779.smt2   |  600.122s | 432.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0706.smt2   |  600.122s | 852.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0482.smt2   |  600.123s | 662.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0617.smt2   |  600.123s | 803.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0329.smt2   |  600.123s | 647.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0869.smt2   |  600.124s | 513.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0022.smt2   |  600.125s | 683.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0805.smt2   |  600.126s | 679.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0040.smt2   |  600.126s | 824.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInv32.smt2 |  600.126s | 577.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0367.smt2   |  600.127s | 601.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/MC_03.smt2      |  600.127s | 835.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0239.smt2   |  600.128s | 594.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0913.smt2   |  600.128s | 674.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0441.smt2   |  600.128s | 862.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0300.smt2   |  600.128s | 694.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0544.smt2   |  600.128s | 540.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0149.smt2   |  600.128s | 745.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0472.smt2   |  600.129s | 835.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0581.smt2   |  600.129s | 731.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0356.smt2   |  600.129s | 606.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0013.smt2   |  600.130s | 997.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0148.smt2   |  600.131s | 739.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0950.smt2   |  600.131s | 633.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/TA_03.smt2      |  600.131s | 553.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0229.smt2   |  600.132s | 600.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0041.smt2   |  600.132s | 739.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0563.smt2   |  600.132s | 750.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0347.smt2   |  600.133s | 759.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0427.smt2   |  600.133s | 817.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0236.smt2   |  600.133s | 600.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0131.smt2   |  600.133s | 956.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0014.smt2   |  600.134s | 808.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0940.smt2   |  600.134s | 750.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2_fixed__p24591_edge_closing_0.smt2 |  600.134s | 916.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0670.smt2   |  600.135s | 944.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0994.smt2   |  600.135s | 575.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0346.smt2   |  600.135s | 758.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__Swingers.c__p26085_terminationG_0.smt2 |  600.135s | 1386.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0139.smt2   |  600.136s | 764.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0959.smt2   |  600.136s | 657.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0411.smt2   |  600.136s | 913.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/AProVE/aproveSMT6545992645874542347.smt2 |  600.136s | 824.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0286.smt2   |  600.137s | 777.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0671.smt2   |  600.137s | 731.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0995.smt2   |  600.137s | 686.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__NO_13.jar-obl-8__p11440_edge_closing_0.smt2 |  600.137s | 1198.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0350.smt2   |  600.138s | 627.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0535.smt2   |  600.138s | 834.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0463.smt2   |  600.138s | 781.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0419.smt2   |  600.139s | 854.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0689.smt2   |  600.140s | 952.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0023.smt2   |  600.141s | 866.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0985.smt2   |  600.141s | 873.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-narrowing.jar-obl-8__p14386_terminationG_0.smt2 |  600.142s | 722.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0580.smt2   |  600.143s | 925.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0401.smt2   |  600.144s | 1031.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0527.smt2   |  600.144s | 831.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0409.smt2   |  600.144s | 975.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-termination.c__p21147_edge_closing_0.smt2 |  600.144s | 1877.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0049.smt2   |  600.145s | 688.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0986.smt2   |  600.145s | 664.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0643.smt2   |  600.145s | 889.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0310.smt2   |  600.145s | 741.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0833.smt2   |  600.145s | 707.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0418.smt2   |  600.146s | 1062.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__NO_13.c__p24750_terminationG_0.smt2 |  600.146s | 1314.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__narrowing_rec.jar-obl-8__p11067_terminationG_0.smt2 |  600.146s | 1087.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0292.smt2   |  600.147s | 932.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0383.smt2   |  600.148s | 794.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0958.smt2   |  600.148s | 823.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0391.smt2   |  600.148s | 1055.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0797.smt2   |  600.149s | 1093.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0138.smt2   |  600.149s | 780.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0976.smt2   |  600.149s | 1060.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0426.smt2   |  600.149s | 917.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0473.smt2   |  600.150s | 823.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0301.smt2   |  600.150s | 646.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0400.smt2   |  600.150s | 997.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0941.smt2   |  600.151s | 929.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0067.smt2   |  600.151s | 612.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0428.smt2   |  600.152s | 892.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0320.smt2   |  600.152s | 738.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__NonTerminationSimple7_false-termination.c__p25148_terminationG_0.smt2 |  600.152s | 1339.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInvStep.smt2 |  600.152s | 714.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0642.smt2   |  600.153s | 837.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0834.smt2   |  600.153s | 995.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0394.smt2   |  600.153s | 1083.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0679.smt2   |  600.153s | 741.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0740.smt2   |  600.153s | 821.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0644.smt2   |  600.154s | 882.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0481.smt2   |  600.154s | 730.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0949.smt2   |  600.155s | 721.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-termination.c__p21397_terminationG_0.smt2 |  600.155s | 841.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0293.smt2   |  600.156s | 782.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0571.smt2   |  600.156s | 991.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0716.smt2   |  600.156s | 741.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__UpAndDownIneq.c__p26236_terminationG_0.smt2 |  600.156s | 987.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0616.smt2   |  600.157s | 753.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0635.smt2   |  600.157s | 879.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0599.smt2   |  600.157s | 1072.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0436.smt2   |  600.157s | 1024.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0896.smt2   |  600.158s | 511.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0832.smt2   |  600.158s | 987.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0717.smt2   |  600.159s | 1165.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0112.smt2   |  600.159s | 1005.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0311.smt2   |  600.160s | 873.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0597.smt2   |  600.160s | 1021.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0582.smt2   |  600.161s | 852.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0454.smt2   |  600.161s | 830.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0100.smt2   |  600.161s | 832.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0967.smt2   |  600.162s | 820.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0598.smt2   |  600.162s | 1068.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0569.smt2   |  600.163s | 857.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0374.smt2   |  600.163s | 901.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__TaylorSeriesIte.jar-obl-13__p12477_terminationG_0.smt2 |  600.163s | 1086.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0592.smt2   |  600.164s | 877.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0319.smt2   |  600.164s | 764.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0284.smt2   |  600.164s | 1023.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0723.smt2   |  600.165s | 1108.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0680.smt2   |  600.165s | 860.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__sas2.t2__p21297_terminationG_0.smt2 |  600.165s | 1242.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0742.smt2   |  600.166s | 874.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-fib.jar-obl-8__p13881_terminationG_0.smt2 |  600.166s | 1264.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/mcm/99.smt2                           |  600.167s | 1409.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0464.smt2   |  600.169s | 860.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0392.smt2   |  600.169s | 946.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0590.smt2   |  600.170s | 1176.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0537.smt2   |  600.170s | 915.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6202_terminationG_0.smt2 |  600.170s | 1278.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0745.smt2   |  600.171s | 1247.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0373.smt2   |  600.171s | 972.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0382.smt2   |  600.171s | 913.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0113.smt2   |  600.172s | 1179.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0796.smt2   |  600.173s | 1202.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0697.smt2   |  600.174s | 1145.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0085.smt2   |  600.174s | 719.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/sqrtStepFinala.smt2 |  600.174s | 1138.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0410.smt2   |  600.175s | 972.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0202.smt2   |  600.175s | 1209.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0110.smt2   |  600.176s | 1330.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0122.smt2   |  600.177s | 1226.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0325.smt2   |  600.177s | 1140.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/LCTES/digital-stopwatch.locals.nosummaries.smt2 |  600.178s | 1356.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0536.smt2   |  600.180s | 1083.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0077.smt2   |  600.181s | 911.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0688.smt2   |  600.181s | 1048.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0445.smt2   |  600.182s | 1230.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0032.smt2   |  600.183s | 1228.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0715.smt2   |  600.184s | 846.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__select.t2__p21400_edge_closing_0.smt2 |  600.184s | 1137.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/sqrtStepFinal.smt2 |  600.184s | 982.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0698.smt2   |  600.185s | 1114.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0104.smt2   |  600.186s | 1009.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0283.smt2   |  600.186s | 1026.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20230328-sqrtmodinv-hoenicke/modInvVar1.smt2 |  600.186s | 1018.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__NO_13.jar-obl-8__p11405_terminationG_0.smt2 |  600.187s | 1250.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/TA_13.smt2      |  600.189s | 1340.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0121.smt2   |  600.189s | 985.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0451.smt2   |  600.190s | 1243.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0968.smt2   |  600.191s | 792.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0446.smt2   |  600.191s | 1077.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0076.smt2   |  600.191s | 1116.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0130.smt2   |  600.191s | 1195.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__tqli.t2_fixed__p25201_edge_closing_0.smt2 |  600.192s | 1276.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-unsat-05.smt2            |  600.192s | 1004.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0725.smt2   |  600.193s | 1384.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0136.smt2   |  600.193s | 1121.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.195s | 1407.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/MS_04.smt2      |  600.196s | 1141.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0983.smt2   |  600.196s | 1070.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__tqli.c.i.tqli.pl.t2.fixed.t2__p25046_edge_closing_0.smt2 |  600.196s | 1366.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0529.smt2   |  600.197s | 1045.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/MF_03.smt2      |  600.197s | 1465.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__MirrorIntervSim.c__p24484_terminationG_0.smt2 |  600.198s | 1330.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Swingers.jar-obl-8__p12435_terminationG_0.smt2 |  600.199s | 1650.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0589.smt2   |  600.200s | 1118.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0193.smt2   |  600.201s | 1622.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__nakata.t2__p5310_terminationG_0.smt2 |  600.201s | 1503.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-unsat-02.smt2            |  600.201s | 1258.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0977.smt2   |  600.203s | 1026.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.203s | 1457.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0653.smt2   |  600.205s | 1016.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0194.smt2   |  600.206s | 1456.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0662.smt2   |  600.209s | 1011.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0437.smt2   |  600.211s | 1212.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/TA_05.smt2      |  600.211s | 1150.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0163.smt2   |  600.213s | 1230.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0724.smt2   |  600.213s | 1404.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6193_terminationG_0.smt2 |  600.213s | 1596.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/SC_08.smt2      |  600.214s | 1495.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__florian_sas2.t2__p32380_terminationG_0.smt2 |  600.216s | 1470.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0389.smt2   |  600.218s | 1309.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6188_terminationG_0.smt2 |  600.218s | 1666.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0212.smt2   |  600.223s | 1288.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__4NestedWith3Variables_true-termination.c__p20212_terminationG_0.smt2 |  600.224s | 2349.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__Narrowing.c__p24540_terminationG_0.smt2 |  600.225s | 998.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fourn.t2__p32713_terminationG_0.smt2 |  600.225s | 1768.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0424.smt2   |  600.226s | 1404.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0103.smt2   |  600.226s | 1325.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0661.smt2   |  600.228s | 1220.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0175.smt2   |  600.231s | 1414.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__dumper.t2__p19134_terminationG_0.smt2 |  600.232s | 1423.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun7.t2__p1167_edge_closing_0.smt2 |  600.233s | 1686.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0176.smt2   |  600.236s | 1435.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12121_terminationG_0.smt2 |  600.236s | 1592.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6198_terminationG_0.smt2 |  600.238s | 1773.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__LessLeaves.jar-obl-10__p10014_edge_closing_0.smt2 |  600.238s | 1916.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.239s | 1830.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__tqli.c.i.tqli.pl.t2.nor.t2.rlgfixed.t2__p25078_terminationG_0.smt2 |  600.239s | 1861.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0211.smt2   |  600.243s | 1159.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6219_terminationG_0.smt2 |  600.244s | 1813.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n_firewire_instrumented-PP.t2__p6218_terminationG_0.smt2 |  600.245s | 1275.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__LessLeaves.jar-obl-10__p10002_edge_closing_0.smt2 |  600.245s | 1755.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12155_terminationG_0.smt2 |  600.247s | 1840.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-K5O3aH.smt2              |  600.247s | 1268.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0402.smt2   |  600.249s | 1543.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0743.smt2   |  600.249s | 994.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12256_terminationG_0.smt2 |  600.249s | 1513.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__nakata.t2__p5352_edge_closing_0.smt2 |  600.252s | 2086.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0203.smt2   |  600.254s | 1235.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fun6.t2_fixed__p1066_edge_closing_0.smt2 |  600.254s | 1398.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0578.smt2   |  600.257s | 1676.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__NO_24.jar-obl-8__p11510_terminationG_0.smt2 |  600.257s | 4045.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__SortCount.jar-obl-10__p12184_terminationG_0.smt2 |  600.259s | 2040.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0184.smt2   |  600.263s | 1641.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__fourn.t2__p32708_terminationG_0.smt2 |  600.269s | 1936.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__destroy_seg_leak.t2_fixed__p18858_edge_closing_0.smt2 |  600.274s | 1801.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-unsat-04.smt2            |  600.279s | 1448.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-unsat-03.smt2            |  600.279s | 1510.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__streamserver-succeed.t2__p24649_terminationG_0.smt2 |  600.287s | 2306.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0157.smt2   |  600.292s | 2279.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-4-filtered.t2__p22688_terminationG_0.smt2 |  600.295s | 1974.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreatePut.jar-obl-10__p6506_edge_closing_0.smt2 |  600.299s | 2490.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-l6cqQI.smt2              |  600.300s | 1587.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__juHashMapCreateIteratorEntryLoop.jar-obl-12__p3363_edge_closing_0.smt2 |  600.307s | 2392.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/STC_0158.smt2   |  600.314s | 2084.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.321s | 2577.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.342s | 2916.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__brp_withassume.t2__p17437_edge_closing_0.smt2 |  600.356s | 2312.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/MC_09.smt2      |  600.365s | 2507.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted-fail.t2__p16028_terminationG_0.smt2 |  600.371s | 2957.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Velroyen08-fib.jar-obl-8__p13896_terminationG_0.smt2 |  600.376s | 2196.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted.t2__p16279_terminationG_0.smt2 |  600.395s | 3011.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted-fail.t2__p15941_terminationG_0.smt2 |  600.399s | 3221.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_AProVE_2014__Test1.jar-obl-8__p12801_terminationG_0.smt2 |  600.416s | 6032.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/leipzig/term-MVylXc.smt2              |  600.430s | 2584.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__n-5.t2__p4677_terminationG_0.smt2 |  600.431s | 3728.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchildlive-succeed.t2__p16426_terminationG_0.smt2 |  600.460s | 4420.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted-fail.t2_fixed__p15799_terminationG_0.smt2 |  600.463s | 4137.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__tqli.t2__p25217_terminationG_0.smt2 |  600.473s | 2505.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__apchild-accepted.t2__p16298_terminationG_0.smt2 |  600.484s | 3199.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/MC_11.smt2      |  600.488s | 4153.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_17_0.smt2 |  600.604s | 6746.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_3_0.smt2 |  600.653s | 6723.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_8_0.smt2 |  600.653s | 6543.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_22_0.smt2 |  600.662s | 6835.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_7_0.smt2 |  600.664s | 6616.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-3.t2_fixed__p22135_terminationG_0.smt2 |  600.667s | 6358.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_32_0.smt2 |  600.669s | 6844.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_18_0.smt2 |  600.671s | 6898.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_13_0.smt2 |  600.684s | 6891.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_31_0.smt2 |  600.697s | 6867.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__slayer-3-new.t2_fixed__p21803_terminationG_0.smt2 |  600.700s | 5599.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_6_0.smt2 |  600.722s | 6596.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_28_0.smt2 |  600.727s | 6899.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_14_0.smt2 |  600.768s | 7073.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_24_0.smt2 |  600.771s | 7155.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_26_0.smt2 |  600.773s | 7178.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_15_0.smt2 |  600.779s | 7156.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20170427-VeryMax/ITS/From_T2__foo.t2__terminationS_19_0.smt2 |  600.798s | 7021.0MiB| timeout | 0 |  |  |
|non-incremental/QF_NIA/20220315-MathProblems/RTA_093.smt2    |  601.085s | 8230.0MiB| timeout | 0 |  |  |