# .

* SAT 46
* UNSAT 697
* TIMEOUT 52
* UNKNOWN 0

* ERRORS 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/AUFDTLIA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-AUFDTLIA.tar.zst-d
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/AUFDTLIA.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german43.smt2 |    0.021s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german49.smt2 |    0.022s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german2.smt2 |    0.022s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree444.smt2 |    0.022s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree25.smt2 |    0.023s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree68.smt2 |    0.023s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree62.smt2 |    0.023s | 19.904MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree150.smt2 |    0.023s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german45.smt2 |    0.024s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree103.smt2 |    0.024s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree219.smt2 |    0.024s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree301.smt2 |    0.024s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree13.smt2 |    0.024s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree423.smt2 |    0.024s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree127.smt2 |    0.024s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree63.smt2 |    0.024s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree232.smt2 |    0.024s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german148.smt2 |    0.025s | 21.132MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree514.smt2 |    0.025s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree420.smt2 |    0.025s | 19.932MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree248.smt2 |    0.025s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree115.smt2 |    0.025s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree204.smt2 |    0.025s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree306.smt2 |    0.027s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree85.smt2 |    0.027s | 19.548MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree17.smt2 |    0.027s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree329.smt2 |    0.027s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree388.smt2 |    0.027s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree129.smt2 |    0.028s | 20.536MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount18.smt2 |    0.028s | 20.528MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree187.smt2 |    0.029s | 19.772MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree271.smt2 |    0.029s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree424.smt2 |    0.029s | 20.416MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree370.smt2 |    0.030s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree14.smt2 |    0.030s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree33.smt2 |    0.031s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree245.smt2 |    0.031s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree414.smt2 |    0.031s | 20.332MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree214.smt2 |    0.031s | 19.944MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree364.smt2 |    0.031s | 19.516MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree394.smt2 |    0.032s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree217.smt2 |    0.032s | 20.42MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree519.smt2 |    0.032s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree110.smt2 |    0.033s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree154.smt2 |    0.033s | 20.628MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german175.smt2 |    0.034s | 21.436MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree275.smt2 |    0.034s | 20.372MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree298.smt2 |    0.034s | 20.16MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree433.smt2 |    0.034s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree427.smt2 |    0.034s | 19.56MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree521.smt2 |    0.034s | 19.536MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree432.smt2 |    0.034s | 20.872MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree90.smt2 |    0.035s | 19.92MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree74.smt2 |    0.035s | 19.728MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree404.smt2 |    0.035s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree108.smt2 |    0.035s | 19.58MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree94.smt2 |    0.035s | 19.552MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree61.smt2 |    0.035s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree453.smt2 |    0.035s | 20.576MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree76.smt2 |    0.035s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree64.smt2 |    0.035s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree356.smt2 |    0.035s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-coninv-f5.ucl-property_correspondence-vobj-0002.smt2 |    0.036s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree460.smt2 |    0.036s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree196.smt2 |    0.036s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree6.smt2 |    0.036s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german107.smt2 |    0.037s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree418.smt2 |    0.037s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree118.smt2 |    0.037s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree213.smt2 |    0.037s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree428.smt2 |    0.037s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree445.smt2 |    0.037s | 20.52MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree224.smt2 |    0.037s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree233.smt2 |    0.037s | 20.66MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree48.smt2 |    0.037s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree362.smt2 |    0.038s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree221.smt2 |    0.038s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree263.smt2 |    0.039s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree402.smt2 |    0.039s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree238.smt2 |    0.039s | 19.528MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree53.smt2 |    0.039s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree7.smt2 |    0.039s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german167.smt2 |    0.040s | 20.96MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german53.smt2 |    0.040s | 20.408MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree200.smt2 |    0.040s | 20.536MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree20.smt2 |    0.040s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree517.smt2 |    0.040s | 20.82MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree454.smt2 |    0.040s | 20.576MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount12.smt2 |    0.040s | 20.516MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree385.smt2 |    0.041s | 20.48MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree87.smt2 |    0.041s | 19.548MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree251.smt2 |    0.041s | 20.488MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree34.smt2 |    0.041s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree463.smt2 |    0.042s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree163.smt2 |    0.042s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree291.smt2 |    0.042s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree235.smt2 |    0.042s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree398.smt2 |    0.043s | 20.58MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree529.smt2 |    0.043s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree120.smt2 |    0.043s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree286.smt2 |    0.043s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree16.smt2 |    0.043s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree8.smt2 |    0.043s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree469.smt2 |    0.043s | 20.42MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree312.smt2 |    0.043s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german128.smt2 |    0.044s | 20.404MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree515.smt2 |    0.044s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree2.smt2 |    0.044s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree51.smt2 |    0.044s | 19.584MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree425.smt2 |    0.044s | 20.468MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree71.smt2 |    0.044s | 19.816MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree194.smt2 |    0.044s | 19.552MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree513.smt2 |    0.044s | 19.488MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree471.smt2 |    0.044s | 19.816MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree426.smt2 |    0.044s | 20.36MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree473.smt2 |    0.045s | 20.196MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount9.smt2 |    0.045s | 20.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree500.smt2 |    0.046s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree405.smt2 |    0.046s | 20.1MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree15.smt2 |    0.047s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree501.smt2 |    0.047s | 20.616MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree182.smt2 |    0.047s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree272.smt2 |    0.047s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree334.smt2 |    0.047s | 20.556MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree195.smt2 |    0.047s | 20.372MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree396.smt2 |    0.047s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree180.smt2 |    0.047s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree39.smt2 |    0.048s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree42.smt2 |    0.048s | 19.912MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree141.smt2 |    0.049s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree462.smt2 |    0.049s | 20.568MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree236.smt2 |    0.049s | 20.396MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-noinv-f5.ucl-property_correspondence-vobj-0003.smt2 |    0.050s | 20.424MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree516.smt2 |    0.050s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree157.smt2 |    0.050s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree456.smt2 |    0.050s | 20.388MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree315.smt2 |    0.051s | 20.648MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree283.smt2 |    0.051s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree379.smt2 |    0.051s | 20.712MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree502.smt2 |    0.051s | 20.588MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount26.smt2 |    0.051s | 20.316MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german147.smt2 |    0.052s | 20.292MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree5.smt2 |    0.052s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree422.smt2 |    0.052s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-noinv-f5.ucl-property_correspondence-vobj-0002.smt2 |    0.053s | 19.864MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree162.smt2 |    0.053s | 20.476MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree70.smt2 |    0.053s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree79.smt2 |    0.053s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree226.smt2 |    0.053s | 20.384MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german120.smt2 |    0.054s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german187.smt2 |    0.054s | 21.1MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree437.smt2 |    0.054s | 20.46MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree52.smt2 |    0.054s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree399.smt2 |    0.054s | 20.84MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree386.smt2 |    0.054s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree434.smt2 |    0.054s | 20.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german117.smt2 |    0.055s | 19.436MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree520.smt2 |    0.055s | 20.824MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree401.smt2 |    0.055s | 20.476MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree317.smt2 |    0.056s | 19.572MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree392.smt2 |    0.056s | 20.776MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree322.smt2 |    0.056s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree505.smt2 |    0.056s | 19.82MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german157.smt2 |    0.057s | 21.0MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german132.smt2 |    0.057s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree289.smt2 |    0.057s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree181.smt2 |    0.057s | 19.916MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount6.smt2 |    0.058s | 20.396MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree206.smt2 |    0.059s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree56.smt2 |    0.059s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree60.smt2 |    0.059s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german110.smt2 |    0.060s | 20.384MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree295.smt2 |    0.060s | 20.16MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree189.smt2 |    0.060s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree480.smt2 |    0.060s | 20.528MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree198.smt2 |    0.061s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree229.smt2 |    0.061s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree440.smt2 |    0.062s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree330.smt2 |    0.062s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree10.smt2 |    0.062s | 19.58MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-coninv-f5.ucl-property_correspondence-vobj-0003.smt2 |    0.063s | 20.844MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree297.smt2 |    0.063s | 19.54MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree417.smt2 |    0.063s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree381.smt2 |    0.063s | 20.084MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree40.smt2 |    0.064s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree47.smt2 |    0.064s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree377.smt2 |    0.064s | 20.676MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree137.smt2 |    0.065s | 20.54MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree203.smt2 |    0.065s | 20.46MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree23.smt2 |    0.065s | 19.52MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree247.smt2 |    0.065s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree254.smt2 |    0.065s | 19.732MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree442.smt2 |    0.065s | 20.08MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-coninv-f5.ucl-property_correspondence-vobj-0004.smt2 |    0.066s | 20.964MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german78.smt2 |    0.066s | 19.864MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree314.smt2 |    0.066s | 20.484MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree310.smt2 |    0.066s | 20.228MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree415.smt2 |    0.066s | 21.796MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree293.smt2 |    0.066s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree409.smt2 |    0.067s | 20.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree478.smt2 |    0.067s | 20.332MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree262.smt2 |    0.067s | 19.524MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree337.smt2 |    0.068s | 19.512MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree246.smt2 |    0.068s | 19.576MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree268.smt2 |    0.068s | 20.66MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german19.smt2 |    0.069s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german152.smt2 |    0.070s | 21.128MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree38.smt2 |    0.070s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree227.smt2 |    0.070s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german115.smt2 |    0.071s | 20.112MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree335.smt2 |    0.071s | 20.868MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree126.smt2 |    0.072s | 20.628MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree412.smt2 |    0.072s | 20.824MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german130.smt2 |    0.073s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german68.smt2 |    0.073s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree308.smt2 |    0.073s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree144.smt2 |    0.073s | 20.048MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree503.smt2 |    0.074s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree31.smt2 |    0.074s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree269.smt2 |    0.074s | 20.756MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree363.smt2 |    0.074s | 20.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree287.smt2 |    0.074s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german46.smt2 |    0.075s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german87.smt2 |    0.076s | 20.088MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree149.smt2 |    0.076s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree26.smt2 |    0.076s | 19.56MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree294.smt2 |    0.076s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree230.smt2 |    0.076s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-noinv-f5.ucl-property_correspondence-vobj-0005.smt2 |    0.077s | 21.128MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-umem-coninv-f5.ucl-property_correspondence-vobj-0005.smt2 |    0.078s | 21.46MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german123.smt2 |    0.078s | 20.42MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree24.smt2 |    0.078s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german109.smt2 |    0.079s | 20.128MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german12.smt2 |    0.079s | 20.148MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree468.smt2 |    0.079s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree278.smt2 |    0.079s | 19.712MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german51.smt2 |    0.080s | 20.58MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german77.smt2 |    0.080s | 20.08MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german97.smt2 |    0.080s | 20.616MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree147.smt2 |    0.080s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount33.smt2 |    0.080s | 20.268MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-coninv-f5.ucl-property_correspondence-vobj-0004.smt2 |    0.081s | 21.024MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german3.smt2 |    0.081s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree138.smt2 |    0.081s | 20.66MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree476.smt2 |    0.081s | 19.908MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german30.smt2 |    0.082s | 19.736MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german10.smt2 |    0.082s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german60.smt2 |    0.082s | 20.516MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german103.smt2 |    0.082s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german56.smt2 |    0.082s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree448.smt2 |    0.082s | 19.548MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree82.smt2 |    0.082s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree367.smt2 |    0.083s | 20.388MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german59.smt2 |    0.084s | 20.284MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german1.smt2 |    0.084s | 20.368MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree123.smt2 |    0.084s | 20.324MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree348.smt2 |    0.084s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree239.smt2 |    0.084s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount39.smt2 |    0.084s | 20.504MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german135.smt2 |    0.085s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree339.smt2 |    0.085s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree265.smt2 |    0.085s | 20.136MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german17.smt2 |    0.086s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree264.smt2 |    0.086s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree146.smt2 |    0.086s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree179.smt2 |    0.086s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german85.smt2 |    0.087s | 20.612MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree489.smt2 |    0.087s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree216.smt2 |    0.087s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree305.smt2 |    0.087s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree86.smt2 |    0.087s | 20.096MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree65.smt2 |    0.087s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree207.smt2 |    0.087s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree186.smt2 |    0.087s | 20.376MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree133.smt2 |    0.088s | 20.184MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree333.smt2 |    0.088s | 20.404MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree508.smt2 |    0.088s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree29.smt2 |    0.088s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree479.smt2 |    0.088s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree397.smt2 |    0.088s | 20.136MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree406.smt2 |    0.088s | 20.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german20.smt2 |    0.089s | 20.068MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree211.smt2 |    0.089s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree136.smt2 |    0.089s | 20.26MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree57.smt2 |    0.089s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree117.smt2 |    0.089s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree421.smt2 |    0.089s | 19.524MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german66.smt2 |    0.090s | 20.748MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german93.smt2 |    0.090s | 19.912MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german96.smt2 |    0.090s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german27.smt2 |    0.090s | 20.324MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree142.smt2 |    0.090s | 20.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree50.smt2 |    0.090s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree58.smt2 |    0.090s | 19.52MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german16.smt2 |    0.091s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree249.smt2 |    0.091s | 20.968MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree257.smt2 |    0.091s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german61.smt2 |    0.092s | 20.208MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german47.smt2 |    0.092s | 20.456MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree98.smt2 |    0.092s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree132.smt2 |    0.092s | 20.656MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree55.smt2 |    0.092s | 19.82MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree282.smt2 |    0.092s | 20.512MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree59.smt2 |    0.092s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree384.smt2 |    0.092s | 20.896MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german178.smt2 |    0.093s | 21.096MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german79.smt2 |    0.093s | 20.192MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german94.smt2 |    0.093s | 20.056MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree250.smt2 |    0.093s | 20.368MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree372.smt2 |    0.093s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree84.smt2 |    0.093s | 20.184MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree419.smt2 |    0.093s | 20.656MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree112.smt2 |    0.094s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree73.smt2 |    0.094s | 20.352MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree121.smt2 |    0.094s | 20.396MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree504.smt2 |    0.094s | 20.616MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german153.smt2 |    0.095s | 20.876MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german7.smt2 |    0.095s | 20.5MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german6.smt2 |    0.095s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree438.smt2 |    0.095s | 19.548MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree27.smt2 |    0.095s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree173.smt2 |    0.095s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree135.smt2 |    0.095s | 19.992MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree231.smt2 |    0.095s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree530.smt2 |    0.095s | 20.96MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree209.smt2 |    0.095s | 20.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree523.smt2 |    0.095s | 20.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german9.smt2 |    0.096s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german169.smt2 |    0.096s | 20.88MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree413.smt2 |    0.096s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree429.smt2 |    0.096s | 20.908MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree522.smt2 |    0.096s | 20.872MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german91.smt2 |    0.097s | 20.272MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german177.smt2 |    0.097s | 21.14MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree183.smt2 |    0.097s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree260.smt2 |    0.097s | 20.876MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree30.smt2 |    0.097s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree528.smt2 |    0.097s | 20.248MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german129.smt2 |    0.098s | 20.624MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree151.smt2 |    0.098s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree139.smt2 |    0.098s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german82.smt2 |    0.099s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german5.smt2 |    0.099s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german26.smt2 |    0.099s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german126.smt2 |    0.099s | 20.584MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree464.smt2 |    0.099s | 20.4MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree1.smt2 |    0.099s | 20.368MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree19.smt2 |    0.099s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree228.smt2 |    0.099s | 20.612MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree72.smt2 |    0.099s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree403.smt2 |    0.099s | 20.848MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree328.smt2 |    0.099s | 21.056MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german28.smt2 |    0.100s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german140.smt2 |    0.100s | 20.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german186.smt2 |    0.100s | 20.912MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree54.smt2 |    0.100s | 19.864MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree353.smt2 |    0.100s | 20.892MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german52.smt2 |    0.101s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german54.smt2 |    0.101s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree518.smt2 |    0.101s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree28.smt2 |    0.101s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree449.smt2 |    0.101s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree107.smt2 |    0.101s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree416.smt2 |    0.101s | 20.588MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree252.smt2 |    0.101s | 20.92MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree354.smt2 |    0.101s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german164.smt2 |    0.102s | 20.104MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree273.smt2 |    0.102s | 20.388MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree156.smt2 |    0.102s | 20.1MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree484.smt2 |    0.102s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree439.smt2 |    0.102s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree255.smt2 |    0.102s | 20.048MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-coninv-f5.ucl-property_correspondence-vobj-0003.smt2 |    0.103s | 21.116MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-noinv-f5.ucl-property_correspondence-vobj-0002.smt2 |    0.103s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german188.smt2 |    0.103s | 21.132MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german67.smt2 |    0.103s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german112.smt2 |    0.103s | 20.372MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german181.smt2 |    0.103s | 21.148MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german35.smt2 |    0.103s | 20.344MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german101.smt2 |    0.103s | 20.836MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german8.smt2 |    0.103s | 20.368MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german145.smt2 |    0.103s | 20.12MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree430.smt2 |    0.103s | 20.552MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree193.smt2 |    0.103s | 19.988MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree368.smt2 |    0.103s | 20.768MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount2.smt2 |    0.103s | 20.212MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german146.smt2 |    0.104s | 20.624MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree35.smt2 |    0.104s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree344.smt2 |    0.104s | 20.808MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree201.smt2 |    0.104s | 20.68MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree96.smt2 |    0.104s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree172.smt2 |    0.104s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree492.smt2 |    0.104s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree380.smt2 |    0.104s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german150.smt2 |    0.105s | 20.908MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german118.smt2 |    0.105s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german172.smt2 |    0.105s | 21.1MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree493.smt2 |    0.105s | 20.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree171.smt2 |    0.105s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree222.smt2 |    0.105s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree128.smt2 |    0.105s | 20.28MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree441.smt2 |    0.105s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree360.smt2 |    0.105s | 21.108MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree174.smt2 |    0.105s | 19.532MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree125.smt2 |    0.105s | 20.156MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount3.smt2 |    0.105s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree320.smt2 |    0.106s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree99.smt2 |    0.106s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree494.smt2 |    0.106s | 20.528MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree105.smt2 |    0.106s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree131.smt2 |    0.106s | 20.864MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree77.smt2 |    0.106s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount38.smt2 |    0.106s | 20.252MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german22.smt2 |    0.107s | 20.344MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german44.smt2 |    0.107s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree188.smt2 |    0.107s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree300.smt2 |    0.107s | 20.076MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount4.smt2 |    0.107s | 20.404MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german42.smt2 |    0.108s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german31.smt2 |    0.108s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german84.smt2 |    0.108s | 20.084MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german57.smt2 |    0.108s | 19.82MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree175.smt2 |    0.108s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree497.smt2 |    0.108s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree276.smt2 |    0.108s | 20.636MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-noinv-f5.ucl-property_correspondence-vobj-0004.smt2 |    0.109s | 21.192MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-coninv-f5.ucl-property_correspondence-vobj-0006.smt2 |    0.109s | 21.904MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german70.smt2 |    0.109s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german144.smt2 |    0.109s | 20.336MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german108.smt2 |    0.109s | 20.576MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german65.smt2 |    0.109s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree159.smt2 |    0.109s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree457.smt2 |    0.109s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree148.smt2 |    0.109s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree152.smt2 |    0.109s | 21.356MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree237.smt2 |    0.109s | 19.816MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree12.smt2 |    0.109s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree178.smt2 |    0.109s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree234.smt2 |    0.109s | 20.38MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree167.smt2 |    0.109s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree93.smt2 |    0.109s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree325.smt2 |    0.109s | 20.296MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german38.smt2 |    0.110s | 20.384MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german74.smt2 |    0.110s | 20.348MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german183.smt2 |    0.110s | 20.908MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german73.smt2 |    0.110s | 20.136MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree311.smt2 |    0.110s | 19.516MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree80.smt2 |    0.110s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree109.smt2 |    0.110s | 20.016MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount20.smt2 |    0.110s | 20.376MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-umem-coninv-f5.ucl-property_correspondence-vobj-0004.smt2 |    0.111s | 21.18MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-noinv-f5.ucl-property_correspondence-vobj-0004.smt2 |    0.111s | 20.972MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german125.smt2 |    0.111s | 20.34MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german33.smt2 |    0.111s | 20.408MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree323.smt2 |    0.111s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount16.smt2 |    0.111s | 20.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount43.smt2 |    0.111s | 20.276MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount8.smt2 |    0.111s | 20.84MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount11.smt2 |    0.111s | 20.24MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount34.smt2 |    0.111s | 20.152MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german149.smt2 |    0.112s | 21.12MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german121.smt2 |    0.112s | 19.496MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree11.smt2 |    0.112s | 20.468MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount7.smt2 |    0.112s | 20.416MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german156.smt2 |    0.113s | 21.116MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree208.smt2 |    0.113s | 20.588MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree130.smt2 |    0.114s | 20.672MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree327.smt2 |    0.114s | 20.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german171.smt2 |    0.115s | 20.908MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german185.smt2 |    0.115s | 20.884MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree316.smt2 |    0.115s | 20.472MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree470.smt2 |    0.115s | 20.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount44.smt2 |    0.115s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-noinv-f5.ucl-property_correspondence-vobj-0003.smt2 |    0.116s | 20.416MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german41.smt2 |    0.116s | 19.788MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-coninv-f5.ucl-property_correspondence-vobj-0005.smt2 |    0.117s | 21.232MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german69.smt2 |    0.117s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree253.smt2 |    0.118s | 20.732MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german133.smt2 |    0.119s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-noinv-f5.ucl-property_correspondence-vobj-0008.smt2 |    0.120s | 22.436MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german104.smt2 |    0.120s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german166.smt2 |    0.120s | 20.936MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german106.smt2 |    0.120s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree124.smt2 |    0.120s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-coninv-f5.ucl-property_correspondence-vobj-0008.smt2 |    0.121s | 22.52MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-coninv-f5.ucl-property_correspondence-vobj-0002.smt2 |    0.121s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german80.smt2 |    0.121s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german95.smt2 |    0.121s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree285.smt2 |    0.121s | 19.988MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree21.smt2 |    0.121s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount30.smt2 |    0.121s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount29.smt2 |    0.121s | 19.936MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount1.smt2 |    0.121s | 20.232MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german83.smt2 |    0.122s | 19.496MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german29.smt2 |    0.122s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german18.smt2 |    0.122s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german141.smt2 |    0.122s | 20.312MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german25.smt2 |    0.122s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german88.smt2 |    0.122s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german81.smt2 |    0.123s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german124.smt2 |    0.123s | 20.368MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german136.smt2 |    0.123s | 20.332MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german14.smt2 |    0.123s | 19.484MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german32.smt2 |    0.123s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german4.smt2 |    0.124s | 19.544MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german122.smt2 |    0.124s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german98.smt2 |    0.124s | 20.424MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german143.smt2 |    0.124s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german21.smt2 |    0.124s | 20.104MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german142.smt2 |    0.124s | 20.36MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german71.smt2 |    0.124s | 20.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german75.smt2 |    0.124s | 20.372MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german55.smt2 |    0.124s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree458.smt2 |    0.124s | 19.92MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-coninv-f5.ucl-property_correspondence-vobj-0005.smt2 |    0.125s | 21.236MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german24.smt2 |    0.125s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german23.smt2 |    0.125s | 20.392MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german100.smt2 |    0.125s | 20.384MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german114.smt2 |    0.125s | 20.156MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german72.smt2 |    0.125s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree524.smt2 |    0.125s | 20.092MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree378.smt2 |    0.125s | 19.52MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree446.smt2 |    0.125s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german137.smt2 |    0.126s | 20.356MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german184.smt2 |    0.126s | 20.916MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german168.smt2 |    0.126s | 21.04MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german163.smt2 |    0.126s | 20.876MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german158.smt2 |    0.126s | 20.788MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german58.smt2 |    0.126s | 20.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german105.smt2 |    0.127s | 20.36MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german102.smt2 |    0.127s | 20.124MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german64.smt2 |    0.127s | 20.148MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german63.smt2 |    0.127s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree365.smt2 |    0.127s | 20.156MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount17.smt2 |    0.127s | 20.276MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount45.smt2 |    0.127s | 20.372MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german134.smt2 |    0.128s | 20.244MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german34.smt2 |    0.128s | 20.856MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german76.smt2 |    0.128s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german155.smt2 |    0.128s | 20.896MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german92.smt2 |    0.128s | 20.148MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german86.smt2 |    0.128s | 20.892MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german111.smt2 |    0.128s | 20.264MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german189.smt2 |    0.128s | 20.932MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german39.smt2 |    0.128s | 20.148MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german138.smt2 |    0.128s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german62.smt2 |    0.128s | 20.368MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german190.smt2 |    0.128s | 20.936MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount21.smt2 |    0.128s | 20.388MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount14.smt2 |    0.128s | 20.36MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german161.smt2 |    0.129s | 20.868MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german11.smt2 |    0.129s | 20.356MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german160.smt2 |    0.129s | 20.884MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german180.smt2 |    0.129s | 21.132MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german99.smt2 |    0.129s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german36.smt2 |    0.129s | 20.424MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german165.smt2 |    0.129s | 21.124MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount15.smt2 |    0.129s | 20.356MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount19.smt2 |    0.129s | 20.368MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount23.smt2 |    0.129s | 20.368MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount25.smt2 |    0.129s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german113.smt2 |    0.130s | 20.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german154.smt2 |    0.130s | 21.1MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german90.smt2 |    0.130s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german40.smt2 |    0.130s | 20.16MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german176.smt2 |    0.130s | 20.932MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german50.smt2 |    0.130s | 20.14MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german13.smt2 |    0.130s | 20.124MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree280.smt2 |    0.130s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount5.smt2 |    0.130s | 20.264MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-noinv-f5.ucl-property_correspondence-vobj-0002.smt2 |    0.131s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-umem-coninv-f5.ucl-property_correspondence-vobj-0002.smt2 |    0.131s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german89.smt2 |    0.131s | 20.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german179.smt2 |    0.131s | 20.872MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german139.smt2 |    0.131s | 20.336MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree318.smt2 |    0.131s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree18.smt2 |    0.131s | 19.584MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree279.smt2 |    0.131s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount10.smt2 |    0.131s | 20.352MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german170.smt2 |    0.132s | 20.876MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german173.smt2 |    0.132s | 20.876MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german182.smt2 |    0.132s | 20.876MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount41.smt2 |    0.132s | 20.64MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-umem-noinv-f5.ucl-property_correspondence-vobj-0002.smt2 |    0.133s | 20.164MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-coninv-f5.ucl-property_correspondence-vobj-0002.smt2 |    0.133s | 20.068MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german151.smt2 |    0.133s | 20.876MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german159.smt2 |    0.133s | 20.936MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german127.smt2 |    0.133s | 20.392MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree122.smt2 |    0.133s | 20.408MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree69.smt2 |    0.134s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree199.smt2 |    0.134s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree452.smt2 |    0.134s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german162.smt2 |    0.135s | 20.904MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree309.smt2 |    0.135s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree197.smt2 |    0.136s | 19.82MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree336.smt2 |    0.137s | 20.48MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree202.smt2 |    0.138s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree373.smt2 |    0.138s | 20.08MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree331.smt2 |    0.138s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree9.smt2 |    0.139s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree145.smt2 |    0.139s | 20.392MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree113.smt2 |    0.139s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount13.smt2 |    0.139s | 19.488MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-noinv-f5.ucl-property_correspondence-vobj-0004.smt2 |    0.140s | 20.964MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german116.smt2 |    0.140s | 20.36MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree510.smt2 |    0.140s | 20.708MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree338.smt2 |    0.140s | 20.552MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-noinv-f5.ucl-property_correspondence-vobj-0006.smt2 |    0.141s | 21.936MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-umem-noinv-f5.ucl-property_correspondence-vobj-0003.smt2 |    0.141s | 20.384MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree346.smt2 |    0.141s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree223.smt2 |    0.141s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree143.smt2 |    0.141s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree411.smt2 |    0.142s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree290.smt2 |    0.143s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree400.smt2 |    0.143s | 20.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree168.smt2 |    0.143s | 20.06MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree95.smt2 |    0.143s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree447.smt2 |    0.143s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount31.smt2 |    0.143s | 20.54MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-coninv-f5.ucl-property_correspondence-vobj-0003.smt2 |    0.144s | 20.628MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-noinv-f5.ucl-property_correspondence-vobj-0003.smt2 |    0.144s | 20.668MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german15.smt2 |    0.144s | 20.104MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german48.smt2 |    0.144s | 20.4MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree4.smt2 |    0.144s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree256.smt2 |    0.144s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree44.smt2 |    0.144s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree83.smt2 |    0.144s | 19.948MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-noinv-f5.ucl-property_correspondence-vobj-0009.smt2 |    0.145s | 22.652MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-noinv-f5.ucl-property_correspondence-vobj-0006.smt2 |    0.145s | 21.98MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree324.smt2 |    0.145s | 20.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree486.smt2 |    0.145s | 20.424MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree389.smt2 |    0.145s | 20.18MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree32.smt2 |    0.145s | 19.916MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-umem-coninv-f5.ucl-property_correspondence-vobj-0003.smt2 |    0.146s | 20.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-coninv-f5.ucl-property_correspondence-vobj-0007.smt2 |    0.146s | 22.156MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german37.smt2 |    0.146s | 20.616MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree191.smt2 |    0.146s | 19.52MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree37.smt2 |    0.146s | 20.068MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree436.smt2 |    0.146s | 19.864MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree106.smt2 |    0.146s | 20.012MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree165.smt2 |    0.146s | 19.488MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree332.smt2 |    0.147s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german119.smt2 |    0.148s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree525.smt2 |    0.149s | 22.444MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree215.smt2 |    0.149s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german131.smt2 |    0.150s | 20.368MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree270.smt2 |    0.150s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree243.smt2 |    0.150s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree155.smt2 |    0.151s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree435.smt2 |    0.151s | 20.248MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree116.smt2 |    0.151s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-coninv-f5.ucl-property_correspondence-vobj-0006.smt2 |    0.152s | 21.928MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-coninv-f5.ucl-property_correspondence-vobj-0009.smt2 |    0.152s | 22.904MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/german/german174.smt2 |    0.152s | 20.736MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree296.smt2 |    0.152s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree3.smt2 |    0.152s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree160.smt2 |    0.152s | 20.244MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree88.smt2 |    0.152s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree205.smt2 |    0.153s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree383.smt2 |    0.153s | 20.588MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree170.smt2 |    0.154s | 19.776MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree75.smt2 |    0.154s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree481.smt2 |    0.154s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-coninv-f5.ucl-property_correspondence-vobj-0004.smt2 |    0.156s | 20.964MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree304.smt2 |    0.156s | 20.864MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree92.smt2 |    0.156s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree284.smt2 |    0.156s | 19.82MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree100.smt2 |    0.156s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree455.smt2 |    0.157s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree349.smt2 |    0.158s | 20.372MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree465.smt2 |    0.158s | 19.728MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree488.smt2 |    0.158s | 20.412MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree140.smt2 |    0.158s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree190.smt2 |    0.159s | 20.008MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree326.smt2 |    0.160s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree495.smt2 |    0.160s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree281.smt2 |    0.161s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree391.smt2 |    0.161s | 20.388MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree376.smt2 |    0.161s | 21.324MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree512.smt2 |    0.161s | 20.564MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree302.smt2 |    0.163s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree67.smt2 |    0.164s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree526.smt2 |    0.164s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree511.smt2 |    0.164s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree472.smt2 |    0.164s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree340.smt2 |    0.164s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree487.smt2 |    0.165s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree352.smt2 |    0.166s | 20.728MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-umem-noinv-f5.ucl-property_correspondence-vobj-0004.smt2 |    0.167s | 21.072MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree43.smt2 |    0.167s | 19.588MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree319.smt2 |    0.167s | 20.652MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree408.smt2 |    0.168s | 20.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree81.smt2 |    0.168s | 20.844MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree104.smt2 |    0.168s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree527.smt2 |    0.168s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree292.smt2 |    0.169s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-noinv-f5.ucl-property_correspondence-vobj-0005.smt2 |    0.170s | 21.192MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree341.smt2 |    0.170s | 26.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree240.smt2 |    0.170s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree321.smt2 |    0.170s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree134.smt2 |    0.171s | 20.64MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree78.smt2 |    0.171s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-noinv-f5.ucl-property_correspondence-vobj-0005.smt2 |    0.172s | 21.076MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree496.smt2 |    0.172s | 20.528MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-coninv-f5.ucl-property_correspondence-vobj-0005.smt2 |    0.173s | 21.208MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree288.smt2 |    0.173s | 20.808MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree241.smt2 |    0.173s | 20.412MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree451.smt2 |    0.173s | 20.424MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree357.smt2 |    0.174s | 20.24MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-noinv-f5.ucl-property_correspondence-vobj-0009.smt2 |    0.175s | 22.528MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree164.smt2 |    0.175s | 19.52MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree66.smt2 |    0.175s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree45.smt2 |    0.175s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree431.smt2 |    0.175s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-noinv-f5.ucl-property_correspondence-vobj-0007.smt2 |    0.176s | 22.172MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree114.smt2 |    0.176s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree36.smt2 |    0.176s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree22.smt2 |    0.176s | 20.1MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree395.smt2 |    0.178s | 20.496MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-noinv-f5.ucl-property_correspondence-vobj-0007.smt2 |    0.182s | 22.18MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-noinv-f5.ucl-property_correspondence-vobj-0006.smt2 |    0.183s | 21.996MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-umem-coninv-f5.ucl-property_correspondence-vobj-0006.smt2 |    0.185s | 21.912MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-coninv-f5.ucl-property_correspondence-vobj-0007.smt2 |    0.190s | 22.244MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-coninv-f5.ucl-property_correspondence-vobj-0006.smt2 |    0.198s | 21.784MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-noinv-f5.ucl-property_correspondence-vobj-0007.smt2 |    0.198s | 22.16MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-coninv-f5.ucl-property_correspondence-vobj-0007.smt2 |    0.200s | 22.256MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-umem-coninv-f5.ucl-property_correspondence-vobj-0007.smt2 |    0.201s | 22.1MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-coninv-f5.ucl-property_correspondence-vobj-0009.smt2 |    0.204s | 22.772MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-coninv-f5.ucl-property_correspondence-vobj-0008.smt2 |    0.204s | 22.436MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree46.smt2 |    0.209s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree102.smt2 |    0.209s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-umem-coninv-f5.ucl-property_correspondence-vobj-0009.smt2 |    0.210s | 22.668MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-noinv-f5.ucl-property_correspondence-vobj-0008.smt2 |    0.210s | 22.344MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-noinv-f5.ucl-property_correspondence-vobj-0008.smt2 |    0.213s | 22.292MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree225.smt2 |    0.213s | 20.452MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-umem-coninv-f5.ucl-property_correspondence-vobj-0008.smt2 |    0.218s | 22.48MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-coninv-f5.ucl-property_correspondence-vobj-0008.smt2 |    0.220s | 22.508MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-noinv-f5.ucl-property_correspondence-vobj-0009.smt2 |    0.226s | 22.736MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-coninv-f5.ucl-property_correspondence-vobj-0009.smt2 |    0.232s | 22.76MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount24.smt2 |    2.004s | 66.292MiB| sat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-umem-coninv-f5.ucl-property_correspondence-vobj-0010.smt2 |    9.012s | 35.4MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-coninv-f5.ucl-property_correspondence-vobj-0010.smt2 |   11.799s | 37.252MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-thrualu-amem-noinv-f5.ucl-property_correspondence-vobj-0010.smt2 |   14.332s | 38.684MiB| unsat | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree119.smt2 |   20.020s | 88.928MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-noinv-f5.ucl-property_correspondence-vobj-0010.smt2 |   20.023s | 37.888MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree387.smt2 |   20.024s | 146.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree371.smt2 |   20.027s | 155.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree261.smt2 |   20.029s | 189.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree166.smt2 |   20.031s | 244.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree506.smt2 |   20.034s | 150.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount35.smt2 |   20.036s | 235.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree474.smt2 |   20.039s | 89.524MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree509.smt2 |   20.041s | 200.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree220.smt2 |   20.042s | 216.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree351.smt2 |   20.042s | 97.316MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree498.smt2 |   20.046s | 151.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree303.smt2 |   20.047s | 136.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree466.smt2 |   20.048s | 91.444MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree343.smt2 |   20.049s | 82.948MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree485.smt2 |   20.057s | 338.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount28.smt2 |   20.057s | 270.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree482.smt2 |   20.058s | 80.104MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree91.smt2 |   20.060s | 367.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree345.smt2 |   20.060s | 92.308MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-uhbexamples/uhb_quantifiers.smt2 |   20.061s | 324.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree375.smt2 |   20.063s | 96.136MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree244.smt2 |   20.064s | 172.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree176.smt2 |   20.069s | 98.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree490.smt2 |   20.072s | 91.072MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree212.smt2 |   20.075s | 352.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree477.smt2 |   20.080s | 338.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree158.smt2 |   20.080s | 242.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree313.smt2 |   20.083s | 271.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-coninv-f5.ucl-property_correspondence-vobj-0010.smt2 |   20.086s | 40.464MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-amem-noinv-f5.ucl-property_correspondence-vobj-0010.smt2 |   20.088s | 38.504MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree101.smt2 |   20.088s | 103.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree410.smt2 |   20.092s | 141.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree184.smt2 |   20.093s | 95.288MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20210304-Y86/run-btfnt-idata-fullalu-umem-coninv-f5.ucl-property_correspondence-vobj-0010.smt2 |   20.100s | 37.98MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree259.smt2 |   20.103s | 276.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree450.smt2 |   20.104s | 83.616MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree277.smt2 |   20.105s | 122.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree347.smt2 |   20.110s | 176.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount36.smt2 |   20.116s | 247.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree267.smt2 |   20.121s | 160.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount40.smt2 |   20.121s | 254.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree355.smt2 |   20.131s | 87.176MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree192.smt2 |   20.131s | 250.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree393.smt2 |   20.132s | 93.712MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree111.smt2 |   20.133s | 87.976MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree461.smt2 |   20.133s | 111.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/refcount/refcount46.smt2 |   20.135s | 257.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree361.smt2 |   20.139s | 124.0MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree369.smt2 |   20.150s | 90.848MiB| timeout | 0 |  |  |
|non-incremental/AUFDTLIA/20172804-Barrett/fmf-cav2013/agreement/agree359.smt2 |   20.173s | 143.0MiB| timeout | 0 |  |  |