# .

* SAT 5
* UNSAT 1019
* TIMEOUT 454
* UNKNOWN 2

* ERRORS 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/AUFNIRA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-AUFNIRA.tar.zst-do
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 4a90d3105054796562079406e125b9480ac3472b
Z3 branch: master
Z3 options: "-T:20 model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/AUFNIRA.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0102.fof.smt2 |    0.027s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0241.fof.smt2 |    0.027s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0385.fof.smt2 |    0.027s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0019.fof.smt2 |    0.028s | 19.792MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0263.fof.smt2 |    0.028s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0029.fof.smt2 |    0.028s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0543.fof.smt2 |    0.028s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0360.fof.smt2 |    0.029s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0273.fof.smt2 |    0.029s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0006.fof.smt2 |    0.029s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0293.fof.smt2 |    0.029s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1206.fof.smt2 |    0.029s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0096.fof.smt2 |    0.030s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0135.fof.smt2 |    0.030s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0092.fof.smt2 |    0.030s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0280.fof.smt2 |    0.030s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0319.fof.smt2 |    0.030s | 19.58MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0272.fof.smt2 |    0.030s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0963.fof.smt2 |    0.030s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0031.fof.smt2 |    0.030s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1047.fof.smt2 |    0.030s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0106.fof.smt2 |    0.031s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0181.fof.smt2 |    0.031s | 19.552MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0282.fof.smt2 |    0.031s | 19.564MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0187.fof.smt2 |    0.031s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0211.fof.smt2 |    0.031s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0058.fof.smt2 |    0.031s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0224.fof.smt2 |    0.031s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0196.fof.smt2 |    0.031s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0054.fof.smt2 |    0.031s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0370.fof.smt2 |    0.031s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0489.fof.smt2 |    0.031s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0032.fof.smt2 |    0.031s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0115.fof.smt2 |    0.032s | 19.564MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0120.fof.smt2 |    0.032s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0118.fof.smt2 |    0.032s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0306.fof.smt2 |    0.032s | 19.576MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0237.fof.smt2 |    0.032s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0356.fof.smt2 |    0.032s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0045.fof.smt2 |    0.032s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0098.fof.smt2 |    0.032s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0033.fof.smt2 |    0.032s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0008.fof.smt2 |    0.032s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1049.fof.smt2 |    0.032s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1303.fof.smt2 |    0.032s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1000.fof.smt2 |    0.032s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0544.fof.smt2 |    0.032s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0545.fof.smt2 |    0.032s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0429.fof.smt2 |    0.032s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0725.fof.smt2 |    0.032s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1302.fof.smt2 |    0.032s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0365.fof.smt2 |    0.033s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0199.fof.smt2 |    0.033s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0107.fof.smt2 |    0.033s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0386.fof.smt2 |    0.033s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0377.fof.smt2 |    0.033s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0141.fof.smt2 |    0.033s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0079.fof.smt2 |    0.033s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0347.fof.smt2 |    0.033s | 19.564MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0384.fof.smt2 |    0.033s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0316.fof.smt2 |    0.033s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0123.fof.smt2 |    0.033s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0889.fof.smt2 |    0.033s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0311.fof.smt2 |    0.033s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0266.fof.smt2 |    0.033s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0010.fof.smt2 |    0.033s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0237.fof.smt2 |    0.033s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0681.fof.smt2 |    0.033s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0032.fof.smt2 |    0.033s | 19.54MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0803.fof.smt2 |    0.033s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0667.fof.smt2 |    0.033s | 19.58MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1298.fof.smt2 |    0.033s | 19.792MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0542.fof.smt2 |    0.033s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/quaternion_ds1_symm_0005.fof.smt2 |    0.033s | 19.516MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0009.fof.smt2 |    0.034s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0367.fof.smt2 |    0.034s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0212.fof.smt2 |    0.034s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0323.fof.smt2 |    0.034s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0337.fof.smt2 |    0.034s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0215.fof.smt2 |    0.034s | 19.56MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0351.fof.smt2 |    0.034s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0296.fof.smt2 |    0.034s | 19.576MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0129.fof.smt2 |    0.034s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0210.fof.smt2 |    0.034s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0043.fof.smt2 |    0.034s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/thruster_symm_0162.fof.smt2 |    0.034s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0004.fof.smt2 |    0.034s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0436.fof.smt2 |    0.034s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0810.fof.smt2 |    0.034s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0290.fof.smt2 |    0.034s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1313.fof.smt2 |    0.034s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0739.fof.smt2 |    0.034s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1050.fof.smt2 |    0.034s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0122.fof.smt2 |    0.034s | 19.728MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0262.fof.smt2 |    0.034s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlib5966a0.smt2                |    0.035s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0292.fof.smt2 |    0.035s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0052.fof.smt2 |    0.035s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0170.fof.smt2 |    0.035s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0297.fof.smt2 |    0.035s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0122.fof.smt2 |    0.035s | 19.56MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0018.fof.smt2 |    0.035s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0291.fof.smt2 |    0.035s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0046.fof.smt2 |    0.035s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0340.fof.smt2 |    0.035s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0101.fof.smt2 |    0.035s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0264.fof.smt2 |    0.035s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0219.fof.smt2 |    0.035s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0318.fof.smt2 |    0.035s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0004.fof.smt2 |    0.035s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0217.fof.smt2 |    0.035s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0151.fof.smt2 |    0.035s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1257.fof.smt2 |    0.035s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0096.fof.smt2 |    0.035s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0801.fof.smt2 |    0.035s | 20.0MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0804.fof.smt2 |    0.035s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/thruster_symm_1697.fof.smt2 |    0.035s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0528.fof.smt2 |    0.035s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0811.fof.smt2 |    0.035s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1041.fof.smt2 |    0.035s | 19.572MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0520.fof.smt2 |    0.035s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0015.fof.smt2 |    0.035s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0079.fof.smt2 |    0.035s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0644.fof.smt2 |    0.035s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1155.fof.smt2 |    0.035s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0556.fof.smt2 |    0.035s | 19.544MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0274.fof.smt2 |    0.035s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0014.fof.smt2 |    0.035s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0553.fof.smt2 |    0.035s | 20.096MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0020.fof.smt2 |    0.035s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/thruster_symm_0013.fof.smt2 |    0.035s | 19.564MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/thruster_symm_0016.fof.smt2 |    0.035s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0238.fof.smt2 |    0.036s | 20.02MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0346.fof.smt2 |    0.036s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0140.fof.smt2 |    0.036s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0354.fof.smt2 |    0.036s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0172.fof.smt2 |    0.036s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0067.fof.smt2 |    0.036s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0383.fof.smt2 |    0.036s | 19.584MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0299.fof.smt2 |    0.036s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0061.fof.smt2 |    0.036s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0036.fof.smt2 |    0.036s | 19.78MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0025.fof.smt2 |    0.036s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0382.fof.smt2 |    0.036s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0381.fof.smt2 |    0.036s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0038.fof.smt2 |    0.036s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0786.fof.smt2 |    0.036s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1007.fof.smt2 |    0.036s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0077.fof.smt2 |    0.036s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1243.fof.smt2 |    0.036s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0036.fof.smt2 |    0.036s | 19.552MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1046.fof.smt2 |    0.036s | 19.78MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0184.fof.smt2 |    0.036s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0019.fof.smt2 |    0.036s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1347.fof.smt2 |    0.036s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0614.fof.smt2 |    0.036s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0348.fof.smt2 |    0.036s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0263.fof.smt2 |    0.036s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1068.fof.smt2 |    0.036s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0130.fof.smt2 |    0.036s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0540.fof.smt2 |    0.036s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0042.fof.smt2 |    0.036s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0133.fof.smt2 |    0.037s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0358.fof.smt2 |    0.037s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0286.fof.smt2 |    0.037s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0028.fof.smt2 |    0.037s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0093.fof.smt2 |    0.037s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0198.fof.smt2 |    0.037s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0249.fof.smt2 |    0.037s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0048.fof.smt2 |    0.037s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0013.fof.smt2 |    0.037s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0059.fof.smt2 |    0.037s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0177.fof.smt2 |    0.037s | 19.576MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0317.fof.smt2 |    0.037s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0005.fof.smt2 |    0.037s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1044.fof.smt2 |    0.037s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0748.fof.smt2 |    0.037s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0809.fof.smt2 |    0.037s | 19.792MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0674.fof.smt2 |    0.037s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0021.fof.smt2 |    0.037s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0047.fof.smt2 |    0.037s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0005.fof.smt2 |    0.037s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0280.fof.smt2 |    0.037s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0004.fof.smt2 |    0.037s | 19.552MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1222.fof.smt2 |    0.037s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0843.fof.smt2 |    0.037s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0850.fof.smt2 |    0.037s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0522.fof.smt2 |    0.037s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1014.fof.smt2 |    0.037s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0525.fof.smt2 |    0.037s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0547.fof.smt2 |    0.037s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0517.fof.smt2 |    0.037s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1176.fof.smt2 |    0.037s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0163.fof.smt2 |    0.038s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0146.fof.smt2 |    0.038s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0169.fof.smt2 |    0.038s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0260.fof.smt2 |    0.038s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0344.fof.smt2 |    0.038s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0205.fof.smt2 |    0.038s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0322.fof.smt2 |    0.038s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0032.fof.smt2 |    0.038s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0056.fof.smt2 |    0.038s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0031.fof.smt2 |    0.038s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0010.fof.smt2 |    0.038s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0070.fof.smt2 |    0.038s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0285.fof.smt2 |    0.038s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0797.fof.smt2 |    0.038s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0214.fof.smt2 |    0.038s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0954.fof.smt2 |    0.038s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0503.fof.smt2 |    0.038s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0688.fof.smt2 |    0.038s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1146.fof.smt2 |    0.038s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0110.fof.smt2 |    0.038s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0584.fof.smt2 |    0.038s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0537.fof.smt2 |    0.038s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1330.fof.smt2 |    0.038s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1070.fof.smt2 |    0.038s | 19.792MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0031.fof.smt2 |    0.038s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/thruster_symm_0017.fof.smt2 |    0.038s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlibce35b2.smt2                |    0.039s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0176.fof.smt2 |    0.039s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0225.fof.smt2 |    0.039s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0226.fof.smt2 |    0.039s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0099.fof.smt2 |    0.039s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0341.fof.smt2 |    0.039s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0329.fof.smt2 |    0.039s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0111.fof.smt2 |    0.039s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0220.fof.smt2 |    0.039s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0002.fof.smt2 |    0.039s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0207.fof.smt2 |    0.039s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0189.fof.smt2 |    0.039s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/cl5_nebula_norm_0023.fof.smt2 |    0.039s | 20.896MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0783.fof.smt2 |    0.039s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0805.fof.smt2 |    0.039s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0012.fof.smt2 |    0.039s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0009.fof.smt2 |    0.039s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0782.fof.smt2 |    0.039s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1066.fof.smt2 |    0.039s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1118.fof.smt2 |    0.039s | 19.904MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0078.fof.smt2 |    0.039s | 19.712MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0268.fof.smt2 |    0.039s | 19.728MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0408.fof.smt2 |    0.039s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlibf37c88.smt2                |    0.040s | 19.836MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0182.fof.smt2 |    0.040s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0073.fof.smt2 |    0.040s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0333.fof.smt2 |    0.040s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0180.fof.smt2 |    0.040s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0016.fof.smt2 |    0.040s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0034.fof.smt2 |    0.040s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0095.fof.smt2 |    0.040s | 19.728MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0078.fof.smt2 |    0.040s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_arithmetics/cl5_nebula_norm_0006.fof.smt2 |    0.040s | 20.972MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0998.fof.smt2 |    0.040s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0332.fof.smt2 |    0.040s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0267.fof.smt2 |    0.040s | 19.528MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0829.fof.smt2 |    0.040s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0991.fof.smt2 |    0.040s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0066.fof.smt2 |    0.040s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0028.fof.smt2 |    0.040s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0082.fof.smt2 |    0.040s | 19.816MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0530.fof.smt2 |    0.040s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0177.fof.smt2 |    0.040s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.629057.smt2               |    0.041s | 20.152MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlibfe2816.smt2                |    0.041s | 19.964MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0330.fof.smt2 |    0.041s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0332.fof.smt2 |    0.041s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0285.fof.smt2 |    0.041s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0047.fof.smt2 |    0.041s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0145.fof.smt2 |    0.041s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/thruster_symm_0187.fof.smt2 |    0.041s | 21.192MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0082.fof.smt2 |    0.041s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0150.fof.smt2 |    0.041s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0192.fof.smt2 |    0.041s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0083.fof.smt2 |    0.041s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1071.fof.smt2 |    0.041s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0258.fof.smt2 |    0.041s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0570.fof.smt2 |    0.041s | 19.816MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0278.fof.smt2 |    0.041s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1324.fof.smt2 |    0.041s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0105.fof.smt2 |    0.041s | 20.88MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0334.fof.smt2 |    0.041s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1327.fof.smt2 |    0.041s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0362.fof.smt2 |    0.041s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0193.fof.smt2 |    0.041s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0200.fof.smt2 |    0.041s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0798.fof.smt2 |    0.041s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0452.fof.smt2 |    0.041s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0016.fof.smt2 |    0.041s | 21.044MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0315.fof.smt2 |    0.042s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0390.fof.smt2 |    0.042s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0321.fof.smt2 |    0.042s | 19.552MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0326.fof.smt2 |    0.042s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0012.fof.smt2 |    0.042s | 19.584MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0190.fof.smt2 |    0.042s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0311.fof.smt2 |    0.042s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0258.fof.smt2 |    0.042s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0183.fof.smt2 |    0.042s | 19.916MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0324.fof.smt2 |    0.042s | 19.572MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0081.fof.smt2 |    0.042s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0375.fof.smt2 |    0.042s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/thruster_symm_0158.fof.smt2 |    0.042s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0051.fof.smt2 |    0.042s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0257.fof.smt2 |    0.042s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0271.fof.smt2 |    0.042s | 19.54MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0232.fof.smt2 |    0.042s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0142.fof.smt2 |    0.042s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0387.fof.smt2 |    0.042s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0071.fof.smt2 |    0.042s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0651.fof.smt2 |    0.042s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0030.fof.smt2 |    0.042s | 20.824MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/thruster_symm_1735.fof.smt2 |    0.042s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0473.fof.smt2 |    0.042s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0282.fof.smt2 |    0.042s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0260.fof.smt2 |    0.042s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0550.fof.smt2 |    0.042s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0065.fof.smt2 |    0.042s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/thruster_symm_1620.fof.smt2 |    0.042s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/thruster_symm_1552.fof.smt2 |    0.042s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1236.fof.smt2 |    0.042s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0017.fof.smt2 |    0.042s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0799.fof.smt2 |    0.042s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0010.fof.smt2 |    0.042s | 21.008MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0301.fof.smt2 |    0.043s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0309.fof.smt2 |    0.043s | 19.976MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0352.fof.smt2 |    0.043s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0335.fof.smt2 |    0.043s | 19.712MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0094.fof.smt2 |    0.043s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0105.fof.smt2 |    0.043s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0144.fof.smt2 |    0.043s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0312.fof.smt2 |    0.043s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0039.fof.smt2 |    0.043s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0221.fof.smt2 |    0.043s | 19.552MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0295.fof.smt2 |    0.043s | 19.728MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0165.fof.smt2 |    0.043s | 19.584MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0288.fof.smt2 |    0.043s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0012.fof.smt2 |    0.043s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0790.fof.smt2 |    0.043s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0034.fof.smt2 |    0.043s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0134.fof.smt2 |    0.043s | 20.868MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0016.fof.smt2 |    0.043s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0780.fof.smt2 |    0.043s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0023.fof.smt2 |    0.043s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0126.fof.smt2 |    0.043s | 21.016MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0006.fof.smt2 |    0.043s | 19.712MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0129.fof.smt2 |    0.043s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0108.fof.smt2 |    0.043s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0802.fof.smt2 |    0.043s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_forall/cl5_nebula_norm_0029.fof.smt2 |    0.043s | 20.956MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0216.fof.smt2 |    0.044s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0245.fof.smt2 |    0.044s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0075.fof.smt2 |    0.044s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0125.fof.smt2 |    0.044s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0186.fof.smt2 |    0.044s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0278.fof.smt2 |    0.044s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0152.fof.smt2 |    0.044s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0044.fof.smt2 |    0.044s | 19.728MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0388.fof.smt2 |    0.044s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0234.fof.smt2 |    0.044s | 19.792MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0022.fof.smt2 |    0.044s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0269.fof.smt2 |    0.044s | 19.584MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0227.fof.smt2 |    0.044s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0041.fof.smt2 |    0.044s | 19.78MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0027.fof.smt2 |    0.044s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0097.fof.smt2 |    0.044s | 19.792MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0353.fof.smt2 |    0.044s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1148.fof.smt2 |    0.044s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0704.fof.smt2 |    0.044s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0018.fof.smt2 |    0.044s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0887.fof.smt2 |    0.044s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0533.fof.smt2 |    0.044s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0036.fof.smt2 |    0.044s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1315.fof.smt2 |    0.044s | 19.728MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0007.fof.smt2 |    0.044s | 21.028MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0808.fof.smt2 |    0.044s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0814.fof.smt2 |    0.044s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0014.fof.smt2 |    0.044s | 20.876MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0040.fof.smt2 |    0.044s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0131.fof.smt2 |    0.044s | 20.868MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0371.fof.smt2 |    0.044s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0924.fof.smt2 |    0.044s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0053.fof.smt2 |    0.045s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0104.fof.smt2 |    0.045s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0228.fof.smt2 |    0.045s | 19.78MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0366.fof.smt2 |    0.045s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0223.fof.smt2 |    0.045s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0233.fof.smt2 |    0.045s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0320.fof.smt2 |    0.045s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0231.fof.smt2 |    0.045s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0343.fof.smt2 |    0.045s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0313.fof.smt2 |    0.045s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0247.fof.smt2 |    0.045s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0011.fof.smt2 |    0.045s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0230.fof.smt2 |    0.045s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1038.fof.smt2 |    0.045s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0369.fof.smt2 |    0.045s | 20.0MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0548.fof.smt2 |    0.045s | 19.864MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0546.fof.smt2 |    0.045s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0852.fof.smt2 |    0.045s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1111.fof.smt2 |    0.045s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0103.fof.smt2 |    0.045s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0284.fof.smt2 |    0.045s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1368.fof.smt2 |    0.045s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0593.fof.smt2 |    0.045s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0836.fof.smt2 |    0.045s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1266.fof.smt2 |    0.045s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1332.fof.smt2 |    0.045s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1125.fof.smt2 |    0.045s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0480.fof.smt2 |    0.045s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0033.fof.smt2 |    0.045s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/quaternion_ds1_symm_0001.fof.smt2 |    0.045s | 20.976MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0037.fof.smt2 |    0.045s | 20.924MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0024.fof.smt2 |    0.046s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0074.fof.smt2 |    0.046s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/cl5_nebula_norm_0013.fof.smt2 |    0.046s | 20.96MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0201.fof.smt2 |    0.046s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0143.fof.smt2 |    0.046s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0300.fof.smt2 |    0.046s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0274.fof.smt2 |    0.046s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0254.fof.smt2 |    0.046s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0345.fof.smt2 |    0.046s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0298.fof.smt2 |    0.046s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0076.fof.smt2 |    0.046s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1074.fof.smt2 |    0.046s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0519.fof.smt2 |    0.046s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0296.fof.smt2 |    0.046s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1340.fof.smt2 |    0.046s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/thruster_symm_1765.fof.smt2 |    0.046s | 21.324MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0269.fof.smt2 |    0.046s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0539.fof.smt2 |    0.046s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0073.fof.smt2 |    0.046s | 20.976MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1069.fof.smt2 |    0.046s | 19.972MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1490.fof.smt2 |    0.046s | 21.616MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0807.fof.smt2 |    0.046s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0812.fof.smt2 |    0.046s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0977.fof.smt2 |    0.046s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0044.fof.smt2 |    0.046s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0005.fof.smt2 |    0.046s | 20.992MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0361.fof.smt2 |    0.047s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0214.fof.smt2 |    0.047s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/cl5_nebula_norm_0004.fof.smt2 |    0.047s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0030.fof.smt2 |    0.047s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0267.fof.smt2 |    0.047s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/cl5_nebula_norm_0010.fof.smt2 |    0.047s | 19.584MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0293.fof.smt2 |    0.047s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0287.fof.smt2 |    0.047s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0077.fof.smt2 |    0.047s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0362.fof.smt2 |    0.047s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0185.fof.smt2 |    0.047s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0109.fof.smt2 |    0.047s | 19.56MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0188.fof.smt2 |    0.047s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0303.fof.smt2 |    0.047s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1322.fof.smt2 |    0.047s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1043.fof.smt2 |    0.047s | 19.82MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0170.fof.smt2 |    0.047s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0466.fof.smt2 |    0.047s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1073.fof.smt2 |    0.047s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1062.fof.smt2 |    0.047s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1139.fof.smt2 |    0.047s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0445.fof.smt2 |    0.047s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0536.fof.smt2 |    0.047s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1307.fof.smt2 |    0.047s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/cl5_nebula_norm_0003.fof.smt2 |    0.047s | 20.88MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0085.fof.smt2 |    0.048s | 19.564MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0204.fof.smt2 |    0.048s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0265.fof.smt2 |    0.048s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0124.fof.smt2 |    0.048s | 19.78MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0090.fof.smt2 |    0.048s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0236.fof.smt2 |    0.048s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0389.fof.smt2 |    0.048s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0117.fof.smt2 |    0.048s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0305.fof.smt2 |    0.048s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0203.fof.smt2 |    0.048s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0128.fof.smt2 |    0.048s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0155.fof.smt2 |    0.048s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0202.fof.smt2 |    0.048s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0246.fof.smt2 |    0.048s | 19.712MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0003.fof.smt2 |    0.048s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0049.fof.smt2 |    0.048s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0374.fof.smt2 |    0.048s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0213.fof.smt2 |    0.048s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0379.fof.smt2 |    0.048s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0064.fof.smt2 |    0.048s | 19.576MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0665.fof.smt2 |    0.048s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0294.fof.smt2 |    0.048s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0399.fof.smt2 |    0.048s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1317.fof.smt2 |    0.048s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0149.fof.smt2 |    0.048s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0099.fof.smt2 |    0.048s | 20.972MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0070.fof.smt2 |    0.048s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0531.fof.smt2 |    0.048s | 19.58MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0010.fof.smt2 |    0.048s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0046.fof.smt2 |    0.048s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1259.fof.smt2 |    0.048s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1311.fof.smt2 |    0.048s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0020.fof.smt2 |    0.048s | 21.176MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0275.fof.smt2 |    0.049s | 19.552MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0166.fof.smt2 |    0.049s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0359.fof.smt2 |    0.049s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0149.fof.smt2 |    0.049s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0290.fof.smt2 |    0.049s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0121.fof.smt2 |    0.049s | 19.564MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0364.fof.smt2 |    0.049s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0250.fof.smt2 |    0.049s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0157.fof.smt2 |    0.049s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0268.fof.smt2 |    0.049s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0071.fof.smt2 |    0.049s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0001.fof.smt2 |    0.049s | 19.584MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0075.fof.smt2 |    0.049s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0591.fof.smt2 |    0.049s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0910.fof.smt2 |    0.049s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0538.fof.smt2 |    0.049s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0112.fof.smt2 |    0.049s | 21.0MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0815.fof.smt2 |    0.049s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0984.fof.smt2 |    0.049s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1314.fof.smt2 |    0.049s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1319.fof.smt2 |    0.049s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0600.fof.smt2 |    0.049s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1304.fof.smt2 |    0.049s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0156.fof.smt2 |    0.050s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0314.fof.smt2 |    0.050s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0279.fof.smt2 |    0.050s | 19.78MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/cl5_nebula_norm_0006.fof.smt2 |    0.050s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0363.fof.smt2 |    0.050s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0795.fof.smt2 |    0.050s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0961.fof.smt2 |    0.050s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/thruster_symm_1614.fof.smt2 |    0.050s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0119.fof.smt2 |    0.050s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0630.fof.smt2 |    0.050s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/thruster_symm_1475.fof.smt2 |    0.050s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0072.fof.smt2 |    0.050s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1305.fof.smt2 |    0.050s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1162.fof.smt2 |    0.050s | 19.58MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0793.fof.smt2 |    0.050s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.637378.smt2               |    0.051s | 20.368MiB| sat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/cl5_nebula_norm_0005.fof.smt2 |    0.051s | 20.96MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0035.fof.smt2 |    0.051s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0153.fof.smt2 |    0.051s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0307.fof.smt2 |    0.051s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0066.fof.smt2 |    0.051s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0175.fof.smt2 |    0.051s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0262.fof.smt2 |    0.051s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/thruster_symm_0164.fof.smt2 |    0.051s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0018.fof.smt2 |    0.051s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1057.fof.smt2 |    0.051s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1308.fof.smt2 |    0.051s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0034.fof.smt2 |    0.051s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0261.fof.smt2 |    0.051s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0011.fof.smt2 |    0.051s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1064.fof.smt2 |    0.051s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0459.fof.smt2 |    0.051s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0003.fof.smt2 |    0.051s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0017.fof.smt2 |    0.051s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0806.fof.smt2 |    0.051s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0796.fof.smt2 |    0.051s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0295.fof.smt2 |    0.051s | 19.96MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0239.fof.smt2 |    0.052s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0040.fof.smt2 |    0.052s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0108.fof.smt2 |    0.052s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0162.fof.smt2 |    0.052s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0385.fof.smt2 |    0.052s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0137.fof.smt2 |    0.052s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0261.fof.smt2 |    0.052s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0339.fof.smt2 |    0.052s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0334.fof.smt2 |    0.052s | 19.564MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0304.fof.smt2 |    0.052s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0380.fof.smt2 |    0.052s | 19.528MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0050.fof.smt2 |    0.052s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0200.fof.smt2 |    0.052s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0110.fof.smt2 |    0.052s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1199.fof.smt2 |    0.052s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0526.fof.smt2 |    0.052s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1301.fof.smt2 |    0.052s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0186.fof.smt2 |    0.052s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1045.fof.smt2 |    0.052s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0223.fof.smt2 |    0.052s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0273.fof.smt2 |    0.052s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0527.fof.smt2 |    0.052s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0541.fof.smt2 |    0.052s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0822.fof.smt2 |    0.052s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0277.fof.smt2 |    0.052s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0002.fof.smt2 |    0.052s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0534.fof.smt2 |    0.052s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0076.fof.smt2 |    0.052s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0112.fof.smt2 |    0.053s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0242.fof.smt2 |    0.053s | 19.58MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0069.fof.smt2 |    0.053s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0086.fof.smt2 |    0.053s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0184.fof.smt2 |    0.053s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0310.fof.smt2 |    0.053s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0277.fof.smt2 |    0.053s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0302.fof.smt2 |    0.053s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0371.fof.smt2 |    0.053s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1328.fof.smt2 |    0.053s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0051.fof.smt2 |    0.053s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0066.fof.smt2 |    0.053s | 21.156MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0297.fof.smt2 |    0.053s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0033.fof.smt2 |    0.053s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0052.fof.smt2 |    0.053s | 20.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0111.fof.smt2 |    0.053s | 21.116MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0549.fof.smt2 |    0.053s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0038.fof.smt2 |    0.053s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0195.fof.smt2 |    0.054s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0235.fof.smt2 |    0.054s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0369.fof.smt2 |    0.054s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0063.fof.smt2 |    0.054s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0327.fof.smt2 |    0.054s | 19.58MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0368.fof.smt2 |    0.054s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0020.fof.smt2 |    0.054s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0357.fof.smt2 |    0.054s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0133.fof.smt2 |    0.054s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0535.fof.smt2 |    0.054s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0903.fof.smt2 |    0.054s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1053.fof.smt2 |    0.054s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0107.fof.smt2 |    0.054s | 19.98MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0121.fof.smt2 |    0.054s | 19.576MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0271.fof.smt2 |    0.054s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1300.fof.smt2 |    0.054s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0637.fof.smt2 |    0.054s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0813.fof.smt2 |    0.054s | 19.936MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0103.fof.smt2 |    0.054s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/cl5_nebula_norm_0009.fof.smt2 |    0.055s | 21.144MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0328.fof.smt2 |    0.055s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0130.fof.smt2 |    0.055s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0037.fof.smt2 |    0.055s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0103.fof.smt2 |    0.055s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0015.fof.smt2 |    0.055s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0055.fof.smt2 |    0.055s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0159.fof.smt2 |    0.055s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0193.fof.smt2 |    0.055s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0126.fof.smt2 |    0.055s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0244.fof.smt2 |    0.055s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0147.fof.smt2 |    0.055s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0100.fof.smt2 |    0.055s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0134.fof.smt2 |    0.055s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1040.fof.smt2 |    0.055s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1213.fof.smt2 |    0.055s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0006.fof.smt2 |    0.055s | 19.728MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1333.fof.smt2 |    0.055s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0037.fof.smt2 |    0.055s | 19.576MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0482.fof.smt2 |    0.055s | 19.904MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1331.fof.smt2 |    0.055s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/thruster_symm_0014.fof.smt2 |    0.055s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0350.fof.smt2 |    0.056s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0131.fof.smt2 |    0.056s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0139.fof.smt2 |    0.056s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0132.fof.smt2 |    0.056s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0050.fof.smt2 |    0.056s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0776.fof.smt2 |    0.056s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1326.fof.smt2 |    0.056s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1063.fof.smt2 |    0.056s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0355.fof.smt2 |    0.056s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0041.fof.smt2 |    0.056s | 19.564MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1296.fof.smt2 |    0.056s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0800.fof.smt2 |    0.056s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0933.fof.smt2 |    0.056s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0552.fof.smt2 |    0.056s | 19.836MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0026.fof.smt2 |    0.056s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1037.fof.smt2 |    0.056s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1052.fof.smt2 |    0.056s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0392.fof.smt2 |    0.056s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.622683.smt2                   |    0.057s | 26.384MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlibdba7a4.smt2                |    0.057s | 21.896MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0252.fof.smt2 |    0.057s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0283.fof.smt2 |    0.057s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0042.fof.smt2 |    0.057s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0089.fof.smt2 |    0.057s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/cl5_nebula_norm_0007.fof.smt2 |    0.057s | 21.128MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0057.fof.smt2 |    0.057s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0229.fof.smt2 |    0.057s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0088.fof.smt2 |    0.057s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/cl5_nebula_norm_0004.fof.smt2 |    0.057s | 20.988MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0156.fof.smt2 |    0.057s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0270.fof.smt2 |    0.057s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0049.fof.smt2 |    0.057s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0037.fof.smt2 |    0.057s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0880.fof.smt2 |    0.057s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0019.fof.smt2 |    0.057s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0784.fof.smt2 |    0.057s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1054.fof.smt2 |    0.057s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0873.fof.smt2 |    0.057s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0264.fof.smt2 |    0.057s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0794.fof.smt2 |    0.057s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0621.fof.smt2 |    0.057s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0415.fof.smt2 |    0.057s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0778.fof.smt2 |    0.057s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0762.fof.smt2 |    0.057s | 19.948MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlib7a3a8e.smt2                |    0.058s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0001.fof.smt2 |    0.058s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0087.fof.smt2 |    0.058s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0248.fof.smt2 |    0.058s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0062.fof.smt2 |    0.058s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/thruster_symm_0151.fof.smt2 |    0.058s | 19.52MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0112.fof.smt2 |    0.058s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1287.fof.smt2 |    0.058s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1310.fof.smt2 |    0.058s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0287.fof.smt2 |    0.058s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0102.fof.smt2 |    0.058s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0947.fof.smt2 |    0.058s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0896.fof.smt2 |    0.058s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0045.fof.smt2 |    0.058s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0279.fof.smt2 |    0.058s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0695.fof.smt2 |    0.058s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0104.fof.smt2 |    0.058s | 21.044MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0521.fof.smt2 |    0.058s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0256.fof.smt2 |    0.059s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0373.fof.smt2 |    0.059s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0338.fof.smt2 |    0.059s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0206.fof.smt2 |    0.059s | 19.548MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0023.fof.smt2 |    0.059s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0243.fof.smt2 |    0.059s | 19.58MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0024.fof.smt2 |    0.059s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1061.fof.smt2 |    0.059s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0275.fof.smt2 |    0.059s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0013.fof.smt2 |    0.059s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1132.fof.smt2 |    0.059s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0101.fof.smt2 |    0.059s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0563.fof.smt2 |    0.059s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0658.fof.smt2 |    0.059s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0286.fof.smt2 |    0.059s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0940.fof.smt2 |    0.059s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1312.fof.smt2 |    0.059s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0554.fof.smt2 |    0.059s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0007.fof.smt2 |    0.059s | 19.712MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0029.fof.smt2 |    0.059s | 19.816MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0787.fof.smt2 |    0.059s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0270.fof.smt2 |    0.060s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0171.fof.smt2 |    0.060s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0178.fof.smt2 |    0.060s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0376.fof.smt2 |    0.060s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1229.fof.smt2 |    0.060s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0378.fof.smt2 |    0.060s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0917.fof.smt2 |    0.060s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0022.fof.smt2 |    0.060s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0529.fof.smt2 |    0.060s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0496.fof.smt2 |    0.060s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1280.fof.smt2 |    0.060s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0532.fof.smt2 |    0.060s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1297.fof.smt2 |    0.060s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0207.fof.smt2 |    0.060s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0174.fof.smt2 |    0.061s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0372.fof.smt2 |    0.061s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0348.fof.smt2 |    0.061s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0167.fof.smt2 |    0.061s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/thruster_symm_0155.fof.smt2 |    0.061s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1109.fof.smt2 |    0.061s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0022.fof.smt2 |    0.061s | 20.764MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0788.fof.smt2 |    0.061s | 19.712MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0607.fof.smt2 |    0.061s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0230.fof.smt2 |    0.061s | 19.54MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0866.fof.smt2 |    0.061s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0209.fof.smt2 |    0.062s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0325.fof.smt2 |    0.062s | 19.864MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0378.fof.smt2 |    0.062s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0160.fof.smt2 |    0.062s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1081.fof.smt2 |    0.062s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0163.fof.smt2 |    0.062s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1220.fof.smt2 |    0.062s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0074.fof.smt2 |    0.062s | 20.916MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1065.fof.smt2 |    0.062s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0318.fof.smt2 |    0.062s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.629149.smt2               |    0.063s | 19.912MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlibfc99e2.smt2                |    0.063s | 21.972MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0060.fof.smt2 |    0.063s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0119.fof.smt2 |    0.063s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0065.fof.smt2 |    0.063s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0197.fof.smt2 |    0.063s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0091.fof.smt2 |    0.063s | 19.78MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0026.fof.smt2 |    0.063s | 19.78MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0114.fof.smt2 |    0.063s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0289.fof.smt2 |    0.063s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0292.fof.smt2 |    0.063s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0030.fof.smt2 |    0.063s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1309.fof.smt2 |    0.063s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1185.fof.smt2 |    0.063s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1299.fof.smt2 |    0.063s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1095.fof.smt2 |    0.063s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1039.fof.smt2 |    0.063s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0069.fof.smt2 |    0.063s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1294.fof.smt2 |    0.063s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0304.fof.smt2 |    0.063s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0341.fof.smt2 |    0.063s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0281.fof.smt2 |    0.063s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0100.fof.smt2 |    0.063s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0406.fof.smt2 |    0.063s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlibd85203.smt2                |    0.064s | 22.08MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0068.fof.smt2 |    0.064s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0331.fof.smt2 |    0.064s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0005.fof.smt2 |    0.064s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1482.fof.smt2 |    0.064s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1058.fof.smt2 |    0.064s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0126.fof.smt2 |    0.064s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0244.fof.smt2 |    0.064s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/thruster_symm_1537.fof.smt2 |    0.064s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0027.fof.smt2 |    0.064s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlibb47bdc.smt2                |    0.065s | 22.088MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0084.fof.smt2 |    0.065s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0194.fof.smt2 |    0.065s | 19.544MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0294.fof.smt2 |    0.065s | 20.028MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0113.fof.smt2 |    0.065s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/cl5_nebula_norm_0014.fof.smt2 |    0.065s | 21.036MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0349.fof.smt2 |    0.065s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0265.fof.smt2 |    0.065s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/thruster_symm_1628.fof.smt2 |    0.065s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1088.fof.smt2 |    0.065s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1354.fof.smt2 |    0.065s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/thruster_symm_1689.fof.smt2 |    0.065s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/cl5_nebula_norm_0004.fof.smt2 |    0.065s | 20.844MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlib8e6000.smt2                |    0.066s | 20.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/cl5_nebula_norm_0008.fof.smt2 |    0.066s | 19.956MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0158.fof.smt2 |    0.066s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0218.fof.smt2 |    0.066s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1169.fof.smt2 |    0.066s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1320.fof.smt2 |    0.066s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1192.fof.smt2 |    0.066s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0859.fof.smt2 |    0.066s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1056.fof.smt2 |    0.066s | 19.728MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0043.fof.smt2 |    0.066s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0272.fof.smt2 |    0.066s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0741.fof.smt2 |    0.066s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0253.fof.smt2 |    0.067s | 19.816MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0138.fof.smt2 |    0.067s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0355.fof.smt2 |    0.067s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1072.fof.smt2 |    0.067s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0276.fof.smt2 |    0.067s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0140.fof.smt2 |    0.067s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0755.fof.smt2 |    0.067s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1323.fof.smt2 |    0.067s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0702.fof.smt2 |    0.067s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1048.fof.smt2 |    0.067s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0045.fof.smt2 |    0.067s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0289.fof.smt2 |    0.067s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlibf3ad77.smt2                |    0.068s | 21.976MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlib14c92b.smt2                |    0.068s | 21.916MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0072.fof.smt2 |    0.068s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1329.fof.smt2 |    0.068s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0123.fof.smt2 |    0.068s | 20.82MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1060.fof.smt2 |    0.068s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0038.fof.smt2 |    0.068s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0025.fof.smt2 |    0.068s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0147.fof.smt2 |    0.068s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0013.fof.smt2 |    0.068s | 19.936MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0789.fof.smt2 |    0.068s | 19.78MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/quaternion_ds1_symm_0017.fof.smt2 |    0.068s | 21.532MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/thruster_symm_0010.fof.smt2 |    0.068s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0039.fof.smt2 |    0.068s | 20.92MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.951967.smt2                   |    0.069s | 21.468MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/why/smtlibdff996.smt2                |    0.069s | 21.76MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0173.fof.smt2 |    0.069s | 19.584MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0127.fof.smt2 |    0.069s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0281.fof.smt2 |    0.069s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0255.fof.smt2 |    0.069s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_arithmetics/quaternion_ds1_symm_0001.fof.smt2 |    0.069s | 21.144MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0106.fof.smt2 |    0.069s | 20.996MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1306.fof.smt2 |    0.069s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1102.fof.smt2 |    0.069s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0577.fof.smt2 |    0.069s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/thruster_symm_0031.fof.smt2 |    0.069s | 21.296MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0259.fof.smt2 |    0.070s | 19.56MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0240.fof.smt2 |    0.070s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0136.fof.smt2 |    0.070s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0251.fof.smt2 |    0.070s | 19.58MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0222.fof.smt2 |    0.070s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0148.fof.smt2 |    0.070s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0161.fof.smt2 |    0.070s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0785.fof.smt2 |    0.070s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0926.fof.smt2 |    0.070s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0068.fof.smt2 |    0.070s | 19.544MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0110.fof.smt2 |    0.070s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.629241.smt2               |    0.071s | 20.328MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0116.fof.smt2 |    0.071s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0523.fof.smt2 |    0.071s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0422.fof.smt2 |    0.071s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0443.fof.smt2 |    0.071s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0792.fof.smt2 |    0.071s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0011.fof.smt2 |    0.071s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/thruster_symm_0153.fof.smt2 |    0.072s | 19.548MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0168.fof.smt2 |    0.072s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0325.fof.smt2 |    0.072s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1325.fof.smt2 |    0.072s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1318.fof.smt2 |    0.072s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0628.fof.smt2 |    0.072s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/cl5_nebula_norm_0006.fof.smt2 |    0.072s | 21.06MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0021.fof.smt2 |    0.073s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0718.fof.smt2 |    0.073s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/cl5_nebula_norm_0003.fof.smt2 |    0.074s | 20.948MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/thruster_symm_0160.fof.smt2 |    0.074s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0021.fof.smt2 |    0.074s | 21.068MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0510.fof.smt2 |    0.074s | 19.864MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0035.fof.smt2 |    0.074s | 19.5MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1028.fof.smt2 |    0.074s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/aviation/clash_alloc_why.smt2        |    0.075s | 20.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1183.fof.smt2 |    0.075s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0779.fof.smt2 |    0.075s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1361.fof.smt2 |    0.075s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0109.fof.smt2 |    0.076s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_arithmetics/cl5_nebula_norm_0003.fof.smt2 |    0.077s | 20.944MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0081.fof.smt2 |    0.077s | 20.82MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0555.fof.smt2 |    0.077s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0059.fof.smt2 |    0.077s | 19.712MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.641708.smt2                   |    0.078s | 19.908MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.637372.smt2               |    0.078s | 20.496MiB| sat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0063.fof.smt2 |    0.078s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1067.fof.smt2 |    0.078s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0284.fof.smt2 |    0.079s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0308.fof.smt2 |    0.079s | 19.792MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0035.fof.smt2 |    0.079s | 19.816MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0020.fof.smt2 |    0.079s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.626115.smt2               |    0.080s | 20.604MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0191.fof.smt2 |    0.080s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0014.fof.smt2 |    0.080s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/thruster_symm_1704.fof.smt2 |    0.081s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0291.fof.smt2 |    0.081s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/thruster_symm_1658.fof.smt2 |    0.081s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0014.fof.smt2 |    0.081s | 20.348MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0089.fof.smt2 |    0.083s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0073.fof.smt2 |    0.084s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1059.fof.smt2 |    0.085s | 19.792MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1321.fof.smt2 |    0.085s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0208.fof.smt2 |    0.086s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0154.fof.smt2 |    0.086s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.951208.smt2                   |    0.087s | 23.008MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0276.fof.smt2 |    0.087s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0283.fof.smt2 |    0.087s | 19.952MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0015.fof.smt2 |    0.087s | 20.96MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0342.fof.smt2 |    0.088s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0336.fof.smt2 |    0.088s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0524.fof.smt2 |    0.088s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1316.fof.smt2 |    0.088s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0080.fof.smt2 |    0.089s | 21.072MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1042.fof.smt2 |    0.089s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1051.fof.smt2 |    0.090s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0781.fof.smt2 |    0.090s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1035.fof.smt2 |    0.090s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0031.fof.smt2 |    0.090s | 21.128MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/aviation/conflict_why.smt2           |    0.091s | 23.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_arithmetics/cl5_nebula_norm_0013.fof.smt2 |    0.091s | 21.38MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0009.fof.smt2 |    0.091s | 19.728MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/aviation/minusminus_why.smt2         |    0.092s | 23.692MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.637239.smt2               |    0.092s | 20.84MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0179.fof.smt2 |    0.092s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0970.fof.smt2 |    0.092s | 19.78MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0251.fof.smt2 |    0.092s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0164.fof.smt2 |    0.093s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0052.fof.smt2 |    0.093s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0221.fof.smt2 |    0.093s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0288.fof.smt2 |    0.094s | 19.804MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/thruster_symm_0161.fof.smt2 |    0.094s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1021.fof.smt2 |    0.094s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/aviation/bts6364_why.smt2            |    0.095s | 23.84MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0551.fof.smt2 |    0.095s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0769.fof.smt2 |    0.096s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1273.fof.smt2 |    0.096s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/quaternion_ds1_symm_0001.fof.smt2 |    0.097s | 21.132MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0080.fof.smt2 |    0.099s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0791.fof.smt2 |    0.099s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0007.fof.smt2 |    0.101s | 19.56MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.629331.smt2               |    0.102s | 20.612MiB| sat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0032.fof.smt2 |    0.102s | 21.396MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0064.fof.smt2 |    0.104s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0017.fof.smt2 |    0.104s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0008.fof.smt2 |    0.105s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.629402.smt2               |    0.106s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.634265.smt2                   |    0.106s | 21.128MiB| sat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/thruster_symm_0189.fof.smt2 |    0.106s | 21.132MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify/quaternion_ds1_symm_0266.fof.smt2 |    0.107s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1250.fof.smt2 |    0.107s | 19.984MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0011.fof.smt2 |    0.107s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/thruster_symm_0015.fof.smt2 |    0.108s | 20.044MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0711.fof.smt2 |    0.111s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/aviation/consts_why.smt2             |    0.114s | 23.876MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.627369.smt2               |    0.115s | 28.968MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_1055.fof.smt2 |    0.115s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/quaternion_ds1_symm_0732.fof.smt2 |    0.115s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.629335.smt2               |    0.119s | 20.012MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0013.fof.smt2 |    0.119s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/quaternion_ds1_symm_0418.fof.smt2 |    0.123s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/aviation/bts6453_why.smt2            |    0.124s | 23.94MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.677614.smt2                   |    0.124s | 22.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.638953.smt2               |    0.125s | 20.348MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/quaternion_ds1_symm_0423.fof.smt2 |    0.125s | 21.648MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/cl5_nebula_norm_0024.fof.smt2 |    0.125s | 21.22MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/cl5_nebula_norm_0005.fof.smt2 |    0.125s | 22.048MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.625933.smt2                   |    0.126s | 20.376MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/cl5_nebula_norm_0003.fof.smt2 |    0.126s | 20.86MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.951712.smt2                   |    0.134s | 22.22MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.634248.smt2                   |    0.134s | 20.62MiB| sat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.623344.smt2               |    0.141s | 28.308MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/cl5_nebula_norm_0018.fof.smt2 |    0.141s | 21.132MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.640322.smt2               |    0.142s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.628546.smt2                   |    0.145s | 26.776MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.950199.smt2                   |    0.150s | 26.372MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.630048.smt2                   |    0.150s | 20.12MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_arithmetics/cl5_nebula_norm_0012.fof.smt2 |    0.150s | 22.164MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_arithmetics/cl5_nebula_norm_0005.fof.smt2 |    0.151s | 21.94MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_structure_prop/cl5_nebula_norm_0017.fof.smt2 |    0.151s | 22.08MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.950232.smt2               |    0.152s | 27.272MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.624862.smt2               |    0.152s | 20.584MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.549864.smt2                   |    0.155s | 21.896MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/aviation/bts0063_why.smt2            |    0.158s | 26.008MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.627094.smt2                   |    0.160s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.631366.smt2                   |    0.180s | 20.856MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.620440.smt2               |    0.184s | 29.784MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.549916.smt2               |    0.185s | 23.912MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.701134.smt2                   |    0.195s | 24.208MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/aviation/bts0071_why.smt2            |    0.203s | 25.812MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.709094.smt2                   |    0.209s | 40.528MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.624507.smt2                   |    0.218s | 26.764MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.630683.smt2               |    0.231s | 20.72MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/thruster_symm_0001.fof.smt2 |    0.250s | 24.7MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.620661.smt2                   |    0.264s | 30.492MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.676882.smt2                   |    0.276s | 24.2MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.637082.smt2               |    0.277s | 29.932MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.701866.smt2                   |    0.284s | 22.872MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.637413.smt2               |    0.293s | 20.636MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.710024.smt2               |    0.371s | 33.424MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/quaternion_ds1_symm_0011.fof.smt2 |    0.402s | 31.464MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.622079.smt2               |    0.576s | 32.48MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.688983.smt2               |    1.155s | 92.148MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.689469.smt2                   |    1.209s | 105.0MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.700096.smt2               |    1.644s | 24.756MiB| unknown | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.674037.smt2               |    1.825s | 24.792MiB| unknown | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.622405.smt2                   |    2.716s | 523.0MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.638004.smt2                   |    4.115s | 549.0MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.640149.smt2                   |    7.283s | 1114.0MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.639724.smt2                   |   14.990s | 2421.0MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.637557.smt2                   |   17.441s | 2290.0MiB| unsat | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/cl5_nebula_norm_0016.fof.smt2 |   20.016s | 38.064MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0128.fof.smt2 |   20.020s | 64.308MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0039.fof.smt2 |   20.037s | 62.66MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0075.fof.smt2 |   20.048s | 38.808MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0067.fof.smt2 |   20.051s | 26.56MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0008.fof.smt2 |   20.056s | 60.112MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0016.fof.smt2 |   20.073s | 43.988MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0021.fof.smt2 |   20.074s | 30.14MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.699515.smt2                   |   20.077s | 82.544MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/cl5_nebula_norm_0010.fof.smt2 |   20.077s | 46.268MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0120.fof.smt2 |   20.083s | 46.844MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/cl5_nebula_norm_0011.fof.smt2 |   20.087s | 34.248MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/cl5_nebula_norm_0015.fof.smt2 |   20.089s | 26.568MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array_only/cl5_nebula_norm_0048.fof.smt2 |   20.096s | 34.224MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/cl5_nebula_norm_0027.fof.smt2 |   20.109s | 69.172MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0019.fof.smt2 |   20.122s | 34.704MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0036.fof.smt2 |   20.123s | 34.196MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/cl5_nebula_norm_0007.fof.smt2 |   20.130s | 51.72MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0012.fof.smt2 |   20.131s | 46.02MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/cl5_nebula_norm_0025.fof.smt2 |   20.143s | 43.652MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0006.fof.smt2 |   20.151s | 35.352MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/fol_simplify_array/cl5_nebula_norm_0008.fof.smt2 |   20.152s | 48.38MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0038.fof.smt2 |   20.154s | 31.836MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.561423.smt2                   |   20.179s | 457.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.691631.smt2                   |   20.179s | 740.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.613729.smt2                   |   20.181s | 1017.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.711486.smt2               |   20.190s | 1341.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.946559.smt2                   |   20.213s | 754.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.656050.smt2               |   20.227s | 1293.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.714299.smt2                   |   20.230s | 379.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.561727.smt2               |   20.230s | 592.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.675263.smt2                   |   20.238s | 28.768MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.954082.smt2                   |   20.253s | 860.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.560298.smt2                   |   20.279s | 1263.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0004.fof.smt2 |   20.280s | 156.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.610121.smt2                   |   20.290s | 194.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.921143.smt2               |   20.293s | 320.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.942623.smt2                   |   20.306s | 234.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.609085.smt2                   |   20.326s | 1450.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.908174.smt2               |   20.343s | 327.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.682948.smt2                   |   20.351s | 1733.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.681188.smt2               |   20.357s | 1269.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.766657.smt2                   |   20.358s | 2048.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.869313.smt2                   |   20.364s | 2117.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.825916.smt2                   |   20.367s | 643.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.672054.smt2               |   20.371s | 1930.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.560602.smt2               |   20.381s | 1130.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.672518.smt2                   |   20.391s | 141.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.809799.smt2               |   20.393s | 2106.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.654657.smt2                   |   20.395s | 1400.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/nasa/vc_normalize_subst/cl5_nebula_norm_0015.fof.smt2 |   20.398s | 486.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.692863.smt2                   |   20.406s | 186.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.648629.smt2                   |   20.428s | 117.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.823996.smt2                   |   20.429s | 1316.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.661260.smt2               |   20.442s | 2725.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.822925.smt2               |   20.458s | 1557.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.821891.smt2               |   20.459s | 2144.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.784716.smt2                   |   20.460s | 2826.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.849348.smt2               |   20.470s | 1670.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.944272.smt2               |   20.478s | 1330.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.829846.smt2                   |   20.480s | 2112.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.848054.smt2                   |   20.481s | 1527.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.856156.smt2                   |   20.492s | 483.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.645472.smt2               |   20.498s | 1762.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.674628.smt2                   |   20.503s | 1262.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.647039.smt2                   |   20.505s | 2496.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.868686.smt2                   |   20.513s | 1540.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.954058.smt2               |   20.523s | 1166.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.940561.smt2               |   20.525s | 2410.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.616911.smt2               |   20.526s | 368.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.634210.smt2                   |   20.533s | 277.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.805649.smt2                   |   20.533s | 1545.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.684910.smt2                   |   20.551s | 1138.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.938815.smt2                   |   20.554s | 309.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.764451.smt2               |   20.558s | 2047.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.638194.smt2                   |   20.568s | 2545.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.635015.smt2               |   20.598s | 2744.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.619057.smt2                   |   20.609s | 386.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.947491.smt2                   |   20.612s | 1954.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.607667.smt2               |   20.624s | 355.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.835930.smt2                   |   20.649s | 2077.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.784327.smt2                   |   20.662s | 2292.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.754420.smt2                   |   20.663s | 2081.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.649332.smt2                   |   20.666s | 399.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.837770.smt2                   |   20.668s | 2053.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.916820.smt2               |   20.676s | 322.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.912497.smt2               |   20.682s | 323.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.673963.smt2               |   20.687s | 4081.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.859684.smt2                   |   20.688s | 470.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.860677.smt2                   |   20.693s | 2092.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.788836.smt2               |   20.694s | 2566.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.810979.smt2               |   20.713s | 2242.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.790700.smt2                   |   20.717s | 2068.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.929857.smt2                   |   20.719s | 2351.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.818913.smt2               |   20.725s | 2643.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.794968.smt2                   |   20.726s | 2096.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.792845.smt2                   |   20.734s | 1900.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.612263.smt2               |   20.759s | 688.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.614416.smt2                   |   20.772s | 388.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.659996.smt2                   |   20.772s | 465.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.682088.smt2                   |   20.774s | 381.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/array_double_why.smt2       |   20.780s | 550.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.912508.smt2                   |   20.834s | 1402.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.638801.smt2               |   20.850s | 2881.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.621785.smt2               |   20.851s | 2897.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.667685.smt2                   |   20.854s | 3134.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.667943.smt2                   |   20.889s | 573.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.666124.smt2                   |   20.896s | 1078.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.700083.smt2               |   20.946s | 5317.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.707123.smt2               |   20.957s | 604.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.797178.smt2               |   20.957s | 1482.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.635554.smt2                   |   20.978s | 1163.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.618374.smt2                   |   20.985s | 812.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.835099.smt2               |   20.989s | 1359.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.782459.smt2                   |   21.092s | 856.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.853506.smt2               |   21.208s | 1224.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.659235.smt2                   |   21.221s | 1923.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.706995.smt2                   |   21.224s | 1387.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.633492.smt2                   |   21.266s | 1311.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.696723.smt2                   |   21.269s | 743.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.632775.smt2               |   21.271s | 827.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.647696.smt2               |   21.284s | 1336.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.942602.smt2               |   21.284s | 820.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.702239.smt2                   |   21.290s | 1255.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.797113.smt2                   |   21.308s | 764.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.686904.smt2                   |   21.350s | 1138.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.675941.smt2               |   21.378s | 829.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.933657.smt2                   |   21.392s | 1022.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.811946.smt2                   |   21.401s | 1409.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/false2_why.smt2             |   21.402s | 1335.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.694291.smt2                   |   21.412s | 1655.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.755420.smt2                   |   21.429s | 983.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.609741.smt2                   |   21.459s | 1220.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.784698.smt2               |   21.461s | 1184.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.619415.smt2                   |   21.469s | 1663.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.955132.smt2               |   21.473s | 1358.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.813971.smt2               |   21.479s | 1320.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.852276.smt2                   |   21.490s | 1472.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.659604.smt2               |   21.522s | 1498.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.669565.smt2                   |   21.559s | 1517.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.607838.smt2                   |   21.560s | 1515.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.861632.smt2                   |   21.564s | 1059.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.800411.smt2                   |   21.570s | 2053.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.864863.smt2               |   21.580s | 1125.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.916894.smt2                   |   21.594s | 1574.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.714183.smt2               |   21.638s | 1069.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.958319.smt2               |   21.656s | 1064.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.849188.smt2                   |   21.668s | 1492.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.749181.smt2                   |   21.671s | 1484.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.880728.smt2               |   21.688s | 1192.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.692368.smt2                   |   21.706s | 2568.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.868836.smt2               |   21.720s | 1103.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.869659.smt2                   |   21.724s | 1553.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.837455.smt2               |   21.733s | 1202.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.830659.smt2               |   21.772s | 2066.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.881698.smt2                   |   21.773s | 1334.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.801381.smt2                   |   21.781s | 1521.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.857393.smt2               |   21.785s | 1204.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.857918.smt2                   |   21.793s | 1272.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/extern_why.smt2             |   21.794s | 1758.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.682065.smt2               |   21.802s | 1181.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.677987.smt2                   |   21.818s | 1110.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.833494.smt2               |   21.822s | 2086.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.955145.smt2                   |   21.826s | 1138.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.833776.smt2                   |   21.836s | 1647.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.698880.smt2                   |   21.849s | 1265.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.711517.smt2                   |   21.854s | 1033.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.763578.smt2                   |   21.861s | 1183.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.767580.smt2               |   21.866s | 2056.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.778229.smt2                   |   21.867s | 1134.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.838140.smt2                   |   21.877s | 1283.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.750595.smt2               |   21.895s | 1233.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.829528.smt2                   |   21.895s | 1711.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.850480.smt2               |   21.907s | 1246.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.614780.smt2                   |   21.908s | 1758.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.825782.smt2               |   21.913s | 1256.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.820023.smt2                   |   21.923s | 1241.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.821053.smt2                   |   21.932s | 1242.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.876764.smt2               |   21.933s | 1252.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.844945.smt2                   |   21.945s | 1316.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.692734.smt2                   |   21.950s | 1217.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/quantified_pointer_why.smt2 |   21.965s | 1803.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.712193.smt2               |   21.969s | 1859.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.955746.smt2                   |   21.976s | 1338.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.872800.smt2               |   21.987s | 1236.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.779430.smt2                   |   21.989s | 2073.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.772111.smt2               |   21.990s | 1284.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.667166.smt2                   |   21.997s | 1684.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.561997.smt2                   |   22.005s | 2199.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.697344.smt2                   |   22.016s | 2066.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.944289.smt2                   |   22.017s | 1243.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.877339.smt2                   |   22.018s | 1971.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.857109.smt2                   |   22.023s | 2083.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.657075.smt2               |   22.034s | 1353.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.661347.smt2                   |   22.034s | 1142.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.663327.smt2                   |   22.043s | 1142.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.654080.smt2               |   22.045s | 1887.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.746428.smt2               |   22.046s | 1311.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.864684.smt2                   |   22.046s | 1382.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.801047.smt2                   |   22.050s | 2117.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.854640.smt2               |   22.050s | 1842.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.767657.smt2                   |   22.053s | 1310.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.714184.smt2                   |   22.053s | 1311.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.838638.smt2               |   22.055s | 2046.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.827926.smt2                   |   22.061s | 1316.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.768674.smt2               |   22.064s | 2047.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.662227.smt2               |   22.065s | 1954.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.919084.smt2                   |   22.070s | 2256.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.796779.smt2                   |   22.076s | 2107.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.943691.smt2               |   22.081s | 2049.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.661781.smt2               |   22.094s | 1247.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.663869.smt2                   |   22.102s | 2100.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.685296.smt2                   |   22.107s | 2151.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.747589.smt2               |   22.108s | 2200.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/bts0073_why.smt2            |   22.110s | 2799.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.759141.smt2                   |   22.117s | 2242.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.780306.smt2               |   22.118s | 1321.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.801385.smt2               |   22.120s | 1404.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.655977.smt2                   |   22.121s | 2025.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.758499.smt2                   |   22.121s | 1346.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.869906.smt2               |   22.129s | 2058.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.853412.smt2                   |   22.135s | 2135.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.825014.smt2                   |   22.141s | 1392.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.706191.smt2                   |   22.142s | 2111.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.826803.smt2               |   22.150s | 1368.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.805592.smt2               |   22.158s | 2106.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.858350.smt2               |   22.161s | 1365.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.660068.smt2               |   22.162s | 1607.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.638333.smt2                   |   22.163s | 2088.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.828944.smt2                   |   22.166s | 1529.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.663953.smt2                   |   22.171s | 2368.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.833458.smt2                   |   22.172s | 1336.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.843953.smt2                   |   22.179s | 2159.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.837129.smt2                   |   22.181s | 2013.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.865953.smt2               |   22.182s | 1393.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.783662.smt2                   |   22.184s | 2092.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.753349.smt2                   |   22.186s | 2446.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.756005.smt2               |   22.187s | 2207.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/bts0187_why.smt2            |   22.191s | 2925.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.744873.smt2                   |   22.194s | 2332.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.755062.smt2                   |   22.204s | 2320.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.940390.smt2                   |   22.206s | 2128.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/bug390_why.smt2             |   22.208s | 2396.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.645715.smt2               |   22.208s | 2247.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.743633.smt2               |   22.209s | 2051.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.880725.smt2                   |   22.212s | 1478.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.908122.smt2                   |   22.212s | 1390.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.776019.smt2               |   22.212s | 1507.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.792971.smt2               |   22.224s | 1450.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.877834.smt2               |   22.225s | 2059.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.873672.smt2                   |   22.225s | 2127.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.865313.smt2                   |   22.229s | 1423.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.799236.smt2                   |   22.240s | 1520.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.807772.smt2                   |   22.243s | 1430.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.831243.smt2               |   22.250s | 1487.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.796143.smt2                   |   22.251s | 2048.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.655748.smt2                   |   22.258s | 1999.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/bts5878_why.smt2            |   22.259s | 2524.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.877685.smt2                   |   22.260s | 1456.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.831856.smt2                   |   22.262s | 1470.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.929723.smt2               |   22.263s | 2352.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.818028.smt2                   |   22.267s | 1312.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/bts0199_why.smt2            |   22.275s | 2406.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.876712.smt2                   |   22.276s | 1500.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.786512.smt2                   |   22.276s | 1541.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.647483.smt2               |   22.277s | 1609.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.785903.smt2               |   22.283s | 1549.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.943708.smt2                   |   22.299s | 2048.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.671569.smt2               |   22.300s | 2457.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.761507.smt2                   |   22.303s | 2119.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.664248.smt2               |   22.308s | 1484.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.652843.smt2               |   22.310s | 2019.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.675189.smt2                   |   22.311s | 3797.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.747041.smt2                   |   22.316s | 1541.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.956070.smt2                   |   22.317s | 1688.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.767299.smt2                   |   22.320s | 1541.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.701996.smt2               |   22.325s | 1458.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.635953.smt2                   |   22.328s | 3328.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.825598.smt2                   |   22.339s | 2331.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/jeannin_why.smt2            |   22.344s | 2975.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.865646.smt2                   |   22.345s | 1517.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.821986.smt2                   |   22.346s | 1575.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/return_why.smt2             |   22.349s | 3225.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.803504.smt2                   |   22.357s | 1478.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.711170.smt2                   |   22.358s | 1493.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.861982.smt2               |   22.359s | 1553.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.763220.smt2                   |   22.359s | 1662.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.792511.smt2                   |   22.360s | 2380.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.829638.smt2               |   22.360s | 2343.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.659732.smt2                   |   22.362s | 1467.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.925667.smt2                   |   22.363s | 1433.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.759499.smt2                   |   22.369s | 1503.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.628941.smt2               |   22.370s | 2913.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.923470.smt2                   |   22.373s | 1617.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.815818.smt2                   |   22.374s | 1470.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.872699.smt2                   |   22.376s | 1510.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.858887.smt2               |   22.376s | 2437.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.750959.smt2                   |   22.378s | 1504.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.687278.smt2                   |   22.384s | 1510.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.635849.smt2               |   22.384s | 2841.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/fs252_why.smt2              |   22.385s | 2548.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.647252.smt2                   |   22.399s | 2263.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.661728.smt2                   |   22.400s | 1500.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.873870.smt2               |   22.411s | 1515.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.750318.smt2                   |   22.413s | 1530.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.809917.smt2                   |   22.419s | 1464.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.832874.smt2                   |   22.420s | 1513.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.775261.smt2                   |   22.431s | 1569.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.881798.smt2               |   22.433s | 1517.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.940633.smt2                   |   22.435s | 2328.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.791875.smt2                   |   22.442s | 2524.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.925543.smt2               |   22.444s | 1634.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.633330.smt2               |   22.446s | 4197.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.662069.smt2               |   22.450s | 2701.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.921280.smt2                   |   22.458s | 1442.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.687448.smt2                   |   22.463s | 2857.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.663700.smt2                   |   22.465s | 1500.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.659078.smt2               |   22.478s | 2751.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.821634.smt2                   |   22.495s | 1675.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.640330.smt2                   |   22.499s | 2414.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.649061.smt2                   |   22.500s | 2822.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.629976.smt2                   |   22.509s | 4073.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.763357.smt2               |   22.511s | 1615.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.617112.smt2                   |   22.515s | 2797.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.881352.smt2                   |   22.522s | 2370.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.702400.smt2                   |   22.536s | 1584.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.636226.smt2                   |   22.538s | 2282.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.670862.smt2               |   22.542s | 2744.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/aviation/axiomatic_why.smt2          |   22.543s | 4539.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.770035.smt2                   |   22.544s | 1590.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.777173.smt2               |   22.550s | 1640.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.696888.smt2               |   22.552s | 2945.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.860981.smt2               |   22.573s | 1621.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.776249.smt2                   |   22.577s | 1973.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.910312.smt2                   |   22.595s | 1654.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.746656.smt2                   |   22.599s | 2925.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.635732.smt2               |   22.602s | 2929.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.944599.smt2                   |   22.613s | 2877.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.760228.smt2               |   22.625s | 1811.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.909292.smt2                   |   22.644s | 1999.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.646409.smt2                   |   22.644s | 1993.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.746010.smt2                   |   22.646s | 2802.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.633611.smt2               |   22.650s | 6270.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.780480.smt2                   |   22.653s | 1764.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.673324.smt2               |   22.664s | 1738.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.562301.smt2               |   22.668s | 3367.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.788577.smt2                   |   22.671s | 1731.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.909956.smt2                   |   22.674s | 2478.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.711639.smt2                   |   22.692s | 3019.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.695009.smt2                   |   22.702s | 3062.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.661994.smt2                   |   22.705s | 3130.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.699383.smt2               |   22.708s | 1786.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.647018.smt2               |   22.710s | 2820.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.857642.smt2                   |   22.713s | 2102.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.713145.smt2                   |   22.736s | 2270.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.775888.smt2                   |   22.747s | 1743.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.695337.smt2                   |   22.752s | 2540.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.697961.smt2               |   22.752s | 1775.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.671895.smt2               |   22.764s | 1846.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.665247.smt2               |   22.776s | 1670.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.674024.smt2               |   22.778s | 2939.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.762578.smt2                   |   22.782s | 2048.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.914698.smt2                   |   22.786s | 1820.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.873326.smt2                   |   22.794s | 1760.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.673310.smt2                   |   22.803s | 2102.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.845302.smt2               |   22.830s | 2098.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.806772.smt2               |   22.831s | 2102.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.817734.smt2               |   22.833s | 2054.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.673103.smt2                   |   22.854s | 1746.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.759134.smt2               |   22.859s | 2055.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.655425.smt2                   |   22.863s | 2006.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.678148.smt2                   |   22.866s | 2127.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.781509.smt2               |   22.889s | 1852.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.834515.smt2               |   22.894s | 2067.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.685476.smt2                   |   22.894s | 2006.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.940318.smt2               |   22.898s | 2045.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.798358.smt2               |   22.905s | 2053.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.635501.smt2               |   22.917s | 2075.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.754911.smt2               |   22.921s | 1938.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.863623.smt2                   |   22.926s | 2148.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.765586.smt2                   |   22.926s | 2063.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.809583.smt2                   |   22.927s | 2050.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.742487.smt2               |   22.931s | 2072.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.612465.smt2                   |   22.931s | 2065.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.757428.smt2                   |   22.932s | 2063.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.787622.smt2                   |   22.933s | 2072.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.695462.smt2                   |   22.933s | 2246.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.926856.smt2                   |   22.936s | 1936.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.644770.smt2               |   22.949s | 1823.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.914342.smt2                   |   22.950s | 2175.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.938740.smt2               |   22.953s | 2124.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.697550.smt2               |   22.958s | 2287.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.683368.smt2                   |   22.958s | 2103.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.710520.smt2                   |   22.972s | 2559.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.794151.smt2               |   22.974s | 2066.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.653587.smt2               |   22.978s | 2251.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.816994.smt2                   |   22.985s | 2523.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.659901.smt2               |   22.988s | 1885.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.875663.smt2                   |   22.988s | 2136.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.647389.smt2                   |   22.993s | 2208.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.946545.smt2               |   23.003s | 2137.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.740747.smt2                   |   23.004s | 2086.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.789955.smt2               |   23.008s | 2070.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.633926.smt2                   |   23.010s | 2332.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.817643.smt2                   |   23.012s | 2635.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.645857.smt2               |   23.012s | 2472.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.918728.smt2                   |   23.014s | 2089.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.939846.smt2                   |   23.018s | 2048.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.699441.smt2                   |   23.019s | 3797.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.804679.smt2                   |   23.026s | 2052.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.923114.smt2                   |   23.034s | 2259.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.634134.smt2                   |   23.035s | 1968.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.661907.smt2                   |   23.046s | 2228.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.658206.smt2                   |   23.048s | 2163.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.808947.smt2                   |   23.054s | 2052.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.673421.smt2                   |   23.057s | 1967.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.827387.smt2               |   23.073s | 2051.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.867637.smt2                   |   23.080s | 2134.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.714922.smt2               |   23.081s | 2507.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.751341.smt2                   |   23.083s | 2049.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.861289.smt2                   |   23.101s | 2057.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.823496.smt2               |   23.105s | 2060.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.774116.smt2                   |   23.110s | 2160.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.751753.smt2               |   23.111s | 2063.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.700022.smt2               |   23.123s | 4081.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.636136.smt2                   |   23.128s | 3544.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.939774.smt2               |   23.129s | 2050.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.697561.smt2                   |   23.140s | 2047.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.780093.smt2                   |   23.145s | 2059.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.922450.smt2                   |   23.152s | 2042.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.621866.smt2                   |   23.162s | 2898.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.649261.smt2                   |   23.167s | 1967.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.712540.smt2               |   23.170s | 4508.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.913678.smt2                   |   23.191s | 2008.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.802565.smt2               |   23.202s | 2090.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.845575.smt2                   |   23.212s | 2659.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.788234.smt2                   |   23.213s | 2095.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.665768.smt2               |   23.217s | 2074.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.805315.smt2                   |   23.220s | 2071.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.871650.smt2                   |   23.236s | 2136.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.918064.smt2                   |   23.244s | 2035.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.713843.smt2                   |   23.251s | 2313.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.653905.smt2               |   23.266s | 2058.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.879676.smt2                   |   23.287s | 2135.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.846296.smt2               |   23.300s | 2151.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.698113.smt2               |   23.368s | 2552.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.697673.smt2                   |   23.391s | 2648.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.640466.smt2                   |   23.400s | 2383.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.675244.smt2                   |   23.408s | 3919.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.845939.smt2                   |   23.415s | 2381.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.933524.smt2               |   23.485s | 2476.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/smtlib.647637.smt2               |   23.508s | 3681.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.958311.smt2                   |   23.548s | 3249.0MiB| timeout | 0 |  |  |
|non-incremental/AUFNIRA/FFT/z3.699496.smt2                   |   23.550s | 3919.0MiB| timeout | 0 |  |  |