# . * SAT 0 * UNSAT 0 * TIMEOUT 0 * UNKNOWN 266 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/UFNIRA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-UFNIRA.tar.zst-dow
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 459629c662eb7abf25a010b7383431a9f729d234
Z3 branch: master
Z3 options: "-T:20 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify sls-smt)" model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/UFNIRA.tar.zst?download=1
Z3 commit message: bugfixes to ho_matcher

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U41_sol1.smt2 | 0.022s | 19.616MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U3_sol1.smt2 | 0.022s | 19.836MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U21_sol1.smt2 | 0.023s | 19.856MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U75_sol1.smt2 | 0.023s | 20.088MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U16_sol1.smt2 | 0.023s | 20.324MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C4_sol1.smt2 | 0.024s | 19.584MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U22.smt2 | 0.024s | 20.472MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C6.smt2 | 0.024s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U14.smt2 | 0.024s | 20.016MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U48.smt2 | 0.026s | 19.844MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U43.smt2 | 0.026s | 20.092MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U61.smt2 | 0.026s | 19.608MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U13.smt2 | 0.026s | 19.608MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U34.smt2 | 0.028s | 19.588MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U40.smt2 | 0.028s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U4.smt2 | 0.028s | 19.636MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U56.smt2 | 0.029s | 19.608MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U6.smt2 | 0.029s | 19.612MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U91_sol2.smt2 | 0.032s | 20.04MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U46.smt2 | 0.032s | 20.1MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U41.smt2 | 0.033s | 19.572MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U30.smt2 | 0.034s | 19.66MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U67.smt2 | 0.034s | 19.592MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U89.smt2 | 0.035s | 19.604MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U25.smt2 | 0.036s | 20.18MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U68.smt2 | 0.037s | 19.904MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C2.smt2 | 0.039s | 20.32MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U61.smt2 | 0.040s | 19.6MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U50_sol1.smt2 | 0.042s | 20.324MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U41.smt2 | 0.043s | 19.832MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U66.smt2 | 0.045s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U75.smt2 | 0.046s | 19.528MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U92_sol1.smt2 | 0.048s | 20.072MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U87.smt2 | 0.057s | 19.848MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U82.smt2 | 0.060s | 20.316MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U40.smt2 | 0.061s | 19.828MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U56_sol1.smt2 | 0.062s | 19.884MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U62_sol1.smt2 | 0.062s | 19.848MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U92.smt2 | 0.064s | 20.088MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U42_sol1.smt2 | 0.065s | 20.324MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U48.smt2 | 0.065s | 19.632MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C9.smt2 | 0.065s | 19.752MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U73_sol1.smt2 | 0.066s | 19.604MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U12.smt2 | 0.066s | 19.708MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U16.smt2 | 0.066s | 19.652MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U22.smt2 | 0.066s | 19.6MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U43_sol1.smt2 | 0.067s | 19.604MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U72_sol2.smt2 | 0.068s | 19.78MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U88.smt2 | 0.068s | 19.828MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U17.smt2 | 0.068s | 19.532MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U45_sol2.smt2 | 0.070s | 20.104MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U29.smt2 | 0.070s | 19.824MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U26_sol1.smt2 | 0.071s | 19.868MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U76.smt2 | 0.071s | 19.66MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U46.smt2 | 0.071s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U51.smt2 | 0.071s | 20.108MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U50_sol3.smt2 | 0.072s | 19.824MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U73.smt2 | 0.072s | 19.844MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U13.smt2 | 0.073s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U11.smt2 | 0.074s | 19.932MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U8.smt2 | 0.074s | 20.196MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U11_sol1.smt2 | 0.075s | 19.632MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U44_sol1.smt2 | 0.076s | 20.08MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U40_sol1.smt2 | 0.076s | 19.772MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U48_sol2.smt2 | 0.076s | 19.644MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U25_sol1.smt2 | 0.076s | 19.716MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C9.smt2 | 0.076s | 19.6MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U72.smt2 | 0.076s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U27_sol1.smt2 | 0.077s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U46_sol2.smt2 | 0.077s | 19.6MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U93.smt2 | 0.077s | 19.652MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C11.smt2 | 0.077s | 19.728MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U37.smt2 | 0.077s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U87.smt2 | 0.077s | 19.584MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U43.smt2 | 0.077s | 19.608MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U53.smt2 | 0.077s | 19.844MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U15.smt2 | 0.077s | 19.672MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U9.smt2 | 0.077s | 19.588MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U93_sol1.smt2 | 0.078s | 19.876MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U26.smt2 | 0.078s | 19.732MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U29.smt2 | 0.078s | 19.876MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U33.smt2 | 0.078s | 19.768MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U92.smt2 | 0.078s | 19.704MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C8.smt2 | 0.078s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U1.smt2 | 0.079s | 19.58MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C1.smt2 | 0.079s | 19.548MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U50.smt2 | 0.079s | 20.092MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U15_sol1.smt2 | 0.080s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U5.smt2 | 0.080s | 20.068MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U8_sol2.smt2 | 0.081s | 19.844MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U51.smt2 | 0.081s | 20.0MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U14.smt2 | 0.081s | 19.896MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U41_sol2.smt2 | 0.082s | 19.844MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U41_sol3.smt2 | 0.082s | 19.828MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U45_sol1.smt2 | 0.082s | 19.604MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U23.smt2 | 0.082s | 19.852MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U20.smt2 | 0.082s | 19.956MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U54.smt2 | 0.082s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U6.smt2 | 0.082s | 19.62MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U56_sol2.smt2 | 0.083s | 19.736MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U93.smt2 | 0.083s | 19.976MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U44.smt2 | 0.083s | 19.6MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U27.smt2 | 0.083s | 19.588MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U89.smt2 | 0.083s | 19.72MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U25.smt2 | 0.083s | 19.648MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U37_sol1.smt2 | 0.084s | 19.756MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U68_sol1.smt2 | 0.084s | 19.764MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U54_sol2.smt2 | 0.084s | 19.8MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U75_sol2.smt2 | 0.084s | 19.612MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U1.smt2 | 0.084s | 20.32MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C1.smt2 | 0.084s | 19.824MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C2.smt2 | 0.084s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U91.smt2 | 0.084s | 19.608MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C4.smt2 | 0.084s | 19.58MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U45.smt2 | 0.084s | 19.7MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U62.smt2 | 0.084s | 19.664MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U20_sol1.smt2 | 0.085s | 19.608MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U17_sol1.smt2 | 0.085s | 19.624MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U50_sol2.smt2 | 0.085s | 19.82MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U62.smt2 | 0.085s | 19.852MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U67.smt2 | 0.085s | 19.804MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U91.smt2 | 0.085s | 19.76MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C13.smt2 | 0.085s | 19.896MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U15_sol2.smt2 | 0.086s | 19.668MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U66_sol2.smt2 | 0.086s | 19.644MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C9a_sol1.smt2 | 0.086s | 19.652MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U39_sol1.smt2 | 0.086s | 19.852MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C7.smt2 | 0.086s | 19.88MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U16.smt2 | 0.086s | 19.864MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U54.smt2 | 0.086s | 20.248MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U10.smt2 | 0.086s | 19.84MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C3.smt2 | 0.086s | 19.708MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U42.smt2 | 0.086s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U56.smt2 | 0.086s | 19.664MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U21.smt2 | 0.086s | 19.76MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U10.smt2 | 0.086s | 19.76MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U31.smt2 | 0.087s | 19.824MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U53_sol1.smt2 | 0.088s | 20.068MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U47.smt2 | 0.088s | 19.6MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U11.smt2 | 0.088s | 19.592MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C6.smt2 | 0.088s | 19.988MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U14_sol1.smt2 | 0.089s | 19.608MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C4.smt2 | 0.089s | 19.64MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U7.smt2 | 0.089s | 19.624MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U29_sol1.smt2 | 0.090s | 19.728MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U48_sol1.smt2 | 0.090s | 19.592MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U12.smt2 | 0.090s | 19.852MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U38.smt2 | 0.090s | 19.868MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C13.smt2 | 0.090s | 20.064MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U9.smt2 | 0.090s | 19.856MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U90.smt2 | 0.090s | 20.232MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U5.smt2 | 0.090s | 19.752MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U82_sol1.smt2 | 0.091s | 19.608MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C13_sol1.smt2 | 0.091s | 19.856MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U50.smt2 | 0.091s | 19.84MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U3.smt2 | 0.091s | 19.628MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C1_sol1.smt2 | 0.092s | 19.68MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U49_sol2.smt2 | 0.092s | 19.772MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U91_sol1.smt2 | 0.092s | 20.068MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U19_sol1.smt2 | 0.092s | 19.884MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U67_sol1.smt2 | 0.093s | 19.852MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U81_sol1.smt2 | 0.093s | 20.068MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U49_sol1.smt2 | 0.093s | 19.636MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U37.smt2 | 0.093s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U81.smt2 | 0.093s | 19.6MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U8.smt2 | 0.094s | 19.636MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C10.smt2 | 0.094s | 19.572MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U9_sol1.smt2 | 0.095s | 19.652MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U8_sol1.smt2 | 0.095s | 19.876MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U19.smt2 | 0.095s | 19.64MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U87_sol2.smt2 | 0.096s | 19.528MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U12_sol1.smt2 | 0.096s | 19.62MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U15.smt2 | 0.096s | 19.612MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U81.smt2 | 0.096s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C3.smt2 | 0.097s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U27.smt2 | 0.097s | 19.64MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U33.smt2 | 0.097s | 19.572MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U72.smt2 | 0.097s | 19.58MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U53.smt2 | 0.097s | 19.604MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U7.smt2 | 0.097s | 19.852MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U49.smt2 | 0.097s | 19.704MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U20.smt2 | 0.098s | 19.78MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U19.smt2 | 0.098s | 19.708MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C8.smt2 | 0.098s | 19.632MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U64.smt2 | 0.098s | 19.892MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C7_sol1.smt2 | 0.099s | 19.824MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U61_sol1.smt2 | 0.099s | 19.776MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U25_sol2.smt2 | 0.099s | 19.832MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U51_sol1.smt2 | 0.099s | 19.852MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U71_sol1.smt2 | 0.099s | 19.6MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U66_sol1.smt2 | 0.099s | 19.552MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U24.smt2 | 0.099s | 19.756MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U64_sol1.smt2 | 0.100s | 19.636MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U2.smt2 | 0.100s | 19.64MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U2.smt2 | 0.100s | 19.88MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C10_sol1.smt2 | 0.101s | 19.676MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U90_sol1.smt2 | 0.101s | 20.036MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U1_sol1.smt2 | 0.101s | 20.2MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U5_sol1.smt2 | 0.101s | 19.632MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U2_sol1.smt2 | 0.101s | 19.656MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U23_sol1.smt2 | 0.101s | 20.024MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U71.smt2 | 0.101s | 19.872MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C7.smt2 | 0.101s | 19.832MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U24.smt2 | 0.101s | 20.016MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U90.smt2 | 0.101s | 19.552MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U20_sol3.smt2 | 0.102s | 19.864MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U6_sol1.smt2 | 0.102s | 19.68MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U72_sol1.smt2 | 0.102s | 19.592MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U13_sol1.smt2 | 0.102s | 19.644MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C11_sol1.smt2 | 0.102s | 19.58MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U26.smt2 | 0.102s | 19.844MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U76.smt2 | 0.102s | 19.62MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C3_sol1.smt2 | 0.103s | 19.6MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U76_sol1.smt2 | 0.103s | 19.82MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C2_sol1.smt2 | 0.103s | 19.592MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U10_sol1.smt2 | 0.103s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C8_sol1.smt2 | 0.103s | 19.716MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U54_sol1.smt2 | 0.103s | 19.836MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U44_sol2.smt2 | 0.103s | 19.6MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C11.smt2 | 0.103s | 19.796MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U82.smt2 | 0.103s | 19.94MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C12.smt2 | 0.103s | 20.144MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U17.smt2 | 0.103s | 19.64MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U57.smt2 | 0.103s | 19.856MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U28.smt2 | 0.103s | 19.736MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U65.smt2 | 0.103s | 19.668MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U68.smt2 | 0.103s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C5.smt2 | 0.103s | 19.876MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U23.smt2 | 0.103s | 19.844MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C12.smt2 | 0.103s | 19.82MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U57.smt2 | 0.103s | 20.016MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C9a.smt2 | 0.103s | 19.66MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U71.smt2 | 0.103s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U57_sol1.smt2 | 0.104s | 19.588MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C12_sol1.smt2 | 0.104s | 19.616MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U26_sol2.smt2 | 0.104s | 19.74MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U24_sol1.smt2 | 0.104s | 19.64MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U20_sol2.smt2 | 0.104s | 19.84MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U39.smt2 | 0.104s | 19.676MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U39.smt2 | 0.104s | 20.232MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C9_sol1.smt2 | 0.105s | 19.58MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U33_sol1.smt2 | 0.105s | 19.852MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U70.smt2 | 0.106s | 19.632MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U79.smt2 | 0.108s | 19.572MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U89_sol1.smt2 | 0.112s | 19.64MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U64.smt2 | 0.112s | 19.656MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U3.smt2 | 0.116s | 19.62MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U7_sol1.smt2 | 0.117s | 19.632MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U42.smt2 | 0.117s | 19.632MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U21.smt2 | 0.117s | 19.756MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U46_sol1.smt2 | 0.118s | 19.6MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U4_sol1.smt2 | 0.118s | 19.712MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C5.smt2 | 0.118s | 19.6MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U73.smt2 | 0.118s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C10.smt2 | 0.118s | 19.724MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U22_sol1.smt2 | 0.119s | 19.768MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U45.smt2 | 0.119s | 19.588MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C9a.smt2 | 0.119s | 19.916MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U4.smt2 | 0.119s | 19.592MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U44.smt2 | 0.120s | 19.764MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U66.smt2 | 0.120s | 19.636MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U75.smt2 | 0.120s | 19.736MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U49.smt2 | 0.134s | 20.056MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C5_sol1.smt2 | 0.146s | 19.596MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C6_sol1.smt2 | 0.154s | 19.828MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U87_sol1.smt2 | 0.154s | 19.596MiB| unknown | 0 | | |