# . * SAT 15 * UNSAT 95 * TIMEOUT 150 * UNKNOWN 6 * 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 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_U8_sol1.smt2 | 0.023s | 20.364MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U72_sol2.smt2 | 0.024s | 20.0MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U20_sol1.smt2 | 0.026s | 20.216MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U62.smt2 | 0.027s | 21.072MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U82_sol1.smt2 | 0.028s | 20.368MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U23_sol1.smt2 | 0.030s | 20.1MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U39_sol1.smt2 | 0.033s | 20.36MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U23.smt2 | 0.039s | 20.9MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U26_sol2.smt2 | 0.041s | 20.628MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U61_sol1.smt2 | 0.044s | 20.88MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U87_sol2.smt2 | 0.047s | 20.3MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U56_sol2.smt2 | 0.047s | 20.636MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U45_sol1.smt2 | 0.049s | 20.608MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U75.smt2 | 0.052s | 20.604MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U66.smt2 | 0.054s | 20.62MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U89_sol1.smt2 | 0.066s | 20.188MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C4_sol1.smt2 | 0.067s | 20.344MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U7_sol1.smt2 | 0.068s | 19.936MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U90_sol1.smt2 | 0.070s | 20.364MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U10_sol1.smt2 | 0.071s | 20.124MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U5_sol1.smt2 | 0.071s | 20.124MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U8_sol2.smt2 | 0.072s | 20.58MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U66_sol2.smt2 | 0.072s | 20.32MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C10_sol1.smt2 | 0.073s | 20.14MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U67_sol1.smt2 | 0.073s | 20.148MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U49_sol1.smt2 | 0.073s | 20.124MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U46_sol1.smt2 | 0.073s | 19.924MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U48_sol1.smt2 | 0.074s | 20.176MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U68_sol1.smt2 | 0.075s | 20.368MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U75_sol2.smt2 | 0.075s | 20.148MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U41_sol3.smt2 | 0.076s | 20.168MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U56_sol1.smt2 | 0.076s | 20.336MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U62_sol1.smt2 | 0.076s | 20.148MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C13_sol1.smt2 | 0.077s | 20.116MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U64_sol1.smt2 | 0.078s | 20.12MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U75_sol1.smt2 | 0.079s | 20.172MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U50_sol1.smt2 | 0.079s | 20.108MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U4_sol1.smt2 | 0.079s | 20.848MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U81.smt2 | 0.079s | 20.38MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C10.smt2 | 0.079s | 20.424MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U71_sol1.smt2 | 0.080s | 20.116MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U24_sol1.smt2 | 0.081s | 20.12MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U9_sol1.smt2 | 0.082s | 20.328MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U57_sol1.smt2 | 0.082s | 20.42MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U57.smt2 | 0.082s | 20.592MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U3_sol1.smt2 | 0.083s | 20.116MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U27_sol1.smt2 | 0.083s | 20.364MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C9a_sol1.smt2 | 0.083s | 20.108MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U6_sol1.smt2 | 0.084s | 20.108MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U41_sol1.smt2 | 0.085s | 20.132MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U20_sol3.smt2 | 0.085s | 20.144MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U81_sol1.smt2 | 0.085s | 20.432MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U50_sol2.smt2 | 0.085s | 20.14MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U50_sol3.smt2 | 0.086s | 20.144MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U2_sol1.smt2 | 0.086s | 20.16MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U93_sol1.smt2 | 0.086s | 20.644MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U42_sol1.smt2 | 0.086s | 20.108MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U26_sol1.smt2 | 0.087s | 20.404MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U14_sol1.smt2 | 0.087s | 20.62MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U46_sol2.smt2 | 0.088s | 20.32MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U49_sol2.smt2 | 0.089s | 19.932MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U41_sol2.smt2 | 0.089s | 20.332MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U54_sol2.smt2 | 0.089s | 20.408MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C2_sol1.smt2 | 0.090s | 20.108MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U20_sol2.smt2 | 0.090s | 20.112MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C6_sol1.smt2 | 0.091s | 20.108MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U13_sol1.smt2 | 0.091s | 20.352MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U19_sol1.smt2 | 0.091s | 20.264MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U71.smt2 | 0.091s | 20.616MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U48_sol2.smt2 | 0.092s | 20.588MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U66_sol1.smt2 | 0.092s | 20.384MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U17.smt2 | 0.092s | 20.424MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U46.smt2 | 0.093s | 20.784MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U68.smt2 | 0.093s | 20.616MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U87_sol1.smt2 | 0.094s | 20.112MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U76_sol1.smt2 | 0.096s | 20.556MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U44_sol1.smt2 | 0.096s | 20.868MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C9_sol1.smt2 | 0.096s | 20.628MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U44_sol2.smt2 | 0.096s | 20.888MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U72.smt2 | 0.097s | 20.868MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U92_sol1.smt2 | 0.098s | 19.964MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U45_sol2.smt2 | 0.098s | 20.364MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C5.smt2 | 0.099s | 20.504MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C5_sol1.smt2 | 0.100s | 20.568MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U1.smt2 | 0.102s | 21.396MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U11_sol1.smt2 | 0.103s | 20.628MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U20.smt2 | 0.103s | 20.896MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U51.smt2 | 0.104s | 20.852MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C3_sol1.smt2 | 0.109s | 20.26MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U37_sol1.smt2 | 0.109s | 21.228MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U17_sol1.smt2 | 0.109s | 20.372MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U48.smt2 | 0.109s | 20.624MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U72_sol1.smt2 | 0.110s | 20.16MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U25_sol1.smt2 | 0.113s | 20.004MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U4.smt2 | 0.113s | 21.18MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U53_sol1.smt2 | 0.115s | 20.144MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C1_sol1.smt2 | 0.116s | 20.12MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U51_sol1.smt2 | 0.116s | 20.348MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C12_sol1.smt2 | 0.116s | 19.924MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U25_sol2.smt2 | 0.119s | 20.136MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U89.smt2 | 0.122s | 20.616MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U91_sol1.smt2 | 0.125s | 19.888MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U91_sol2.smt2 | 0.126s | 20.152MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U54_sol1.smt2 | 0.127s | 20.756MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U41.smt2 | 0.129s | 20.792MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U11.smt2 | 0.130s | 20.364MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U26.smt2 | 0.158s | 22.404MiB| sat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U79.smt2 | 0.180s | 32.408MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U12_sol1.smt2 | 0.190s | 20.892MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U7.smt2 | 4.360s | 26.792MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C6.smt2 | 5.539s | 45.356MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U14.smt2 | 7.314s | 29.62MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U14.smt2 | 8.129s | 30.388MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U16_sol1.smt2 | 9.916s | 33.208MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U40_sol1.smt2 | 9.977s | 21.328MiB| unsat | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U17.smt2 | 10.721s | 143.0MiB| unknown | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C9.smt2 | 20.018s | 38.94MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C9a.smt2 | 20.022s | 42.796MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U12.smt2 | 20.023s | 29.044MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U7.smt2 | 20.024s | 38.472MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U30.smt2 | 20.037s | 23.94MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U12.smt2 | 20.039s | 35.808MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U76.smt2 | 20.045s | 27.936MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U44.smt2 | 20.050s | 41.972MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U26.smt2 | 20.052s | 33.288MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U88.smt2 | 20.060s | 36.892MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U5.smt2 | 20.066s | 152.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U45.smt2 | 20.068s | 28.376MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U4.smt2 | 20.073s | 556.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C7_sol1.smt2 | 20.074s | 32.788MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U27.smt2 | 20.078s | 25.452MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C7.smt2 | 20.081s | 29.432MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U76.smt2 | 20.081s | 27.792MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U81.smt2 | 20.088s | 57.136MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C9a.smt2 | 20.088s | 66.812MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C8_sol1.smt2 | 20.090s | 39.268MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U23.smt2 | 20.093s | 47.92MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C5.smt2 | 20.093s | 22.98MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U53.smt2 | 20.098s | 40.224MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U93.smt2 | 20.105s | 28.436MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U1.smt2 | 20.107s | 24.096MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C9.smt2 | 20.108s | 55.1MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U66.smt2 | 20.109s | 32.008MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U39.smt2 | 20.110s | 65.924MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U27.smt2 | 20.113s | 23.44MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U1_sol1.smt2 | 20.119s | 26.636MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U11.smt2 | 20.120s | 56.176MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U9.smt2 | 20.124s | 284.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U38.smt2 | 20.125s | 39.712MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U53.smt2 | 20.129s | 49.208MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U57.smt2 | 20.129s | 165.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U47.smt2 | 20.133s | 28.196MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C13.smt2 | 20.133s | 266.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U15_sol1.smt2 | 20.137s | 29.612MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C6.smt2 | 20.137s | 37.144MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U87.smt2 | 20.137s | 70.944MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U10.smt2 | 20.137s | 104.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C4.smt2 | 20.144s | 104.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U34.smt2 | 20.149s | 80.432MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U90.smt2 | 20.149s | 94.772MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U93.smt2 | 20.151s | 28.104MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C3.smt2 | 20.151s | 64.912MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C3.smt2 | 20.153s | 64.356MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U6.smt2 | 20.160s | 123.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U90.smt2 | 20.171s | 97.264MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U9.smt2 | 20.172s | 153.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C7.smt2 | 20.176s | 28.548MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U45.smt2 | 20.199s | 221.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U33.smt2 | 20.201s | 172.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U28.smt2 | 20.213s | 517.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U33.smt2 | 20.218s | 173.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U6.smt2 | 20.218s | 192.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C13.smt2 | 20.221s | 239.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C10.smt2 | 20.231s | 274.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U39.smt2 | 20.251s | 325.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U16.smt2 | 20.262s | 267.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U33_sol1.smt2 | 20.290s | 404.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C4.smt2 | 20.293s | 298.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U72.smt2 | 20.322s | 302.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U44.smt2 | 20.323s | 604.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U10.smt2 | 20.325s | 264.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U68.smt2 | 20.353s | 510.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C8.smt2 | 20.394s | 480.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C2.smt2 | 20.404s | 566.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U19.smt2 | 20.434s | 725.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U70.smt2 | 20.476s | 582.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U91.smt2 | 20.497s | 619.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U16.smt2 | 20.526s | 986.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U71.smt2 | 20.531s | 670.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C8.smt2 | 20.611s | 1240.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U91.smt2 | 20.699s | 1255.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U92.smt2 | 20.847s | 1007.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U43.smt2 | 20.950s | 1985.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U51.smt2 | 20.985s | 1404.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U19.smt2 | 21.050s | 1657.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U87.smt2 | 21.114s | 1800.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U43.smt2 | 21.159s | 1925.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U2.smt2 | 21.230s | 2340.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U21.smt2 | 21.244s | 2314.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U29.smt2 | 21.263s | 2506.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U22.smt2 | 21.281s | 2465.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U67.smt2 | 21.287s | 2547.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U48.smt2 | 21.310s | 2517.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U37.smt2 | 21.315s | 2237.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U61.smt2 | 21.328s | 1994.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U56.smt2 | 21.360s | 2869.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U61.smt2 | 21.378s | 2097.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U40.smt2 | 21.409s | 2348.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U37.smt2 | 21.419s | 2356.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U67.smt2 | 21.443s | 2321.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U13.smt2 | 21.459s | 3211.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U54.smt2 | 21.472s | 3258.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C11.smt2 | 21.477s | 2352.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U40.smt2 | 21.514s | 3624.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U49.smt2 | 21.563s | 3828.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U15.smt2 | 21.587s | 2744.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U8.smt2 | 21.591s | 2770.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U50.smt2 | 21.631s | 3228.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U73.smt2 | 21.638s | 2874.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U46.smt2 | 21.650s | 3257.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U15_sol2.smt2 | 21.670s | 2698.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U21.smt2 | 21.681s | 3521.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U29.smt2 | 21.684s | 3043.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U64.smt2 | 21.692s | 3460.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U56.smt2 | 21.699s | 3056.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U8.smt2 | 21.700s | 3451.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C11.smt2 | 21.731s | 3527.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U21_sol1.smt2 | 21.733s | 3041.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U5.smt2 | 21.739s | 4749.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U31.smt2 | 21.742s | 3061.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U41.smt2 | 21.745s | 2907.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U73.smt2 | 21.750s | 4414.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C12.smt2 | 21.754s | 2867.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U2.smt2 | 21.757s | 4308.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U22.smt2 | 21.763s | 3525.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C2.smt2 | 21.763s | 3923.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U54.smt2 | 21.771s | 3462.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U22_sol1.smt2 | 21.792s | 3426.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_C11_sol1.smt2 | 21.795s | 2911.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U50.smt2 | 21.797s | 3336.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U75.smt2 | 21.806s | 6903.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U82.smt2 | 21.806s | 4058.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U73_sol1.smt2 | 21.823s | 4592.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U3.smt2 | 21.835s | 4225.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U42.smt2 | 21.837s | 3555.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U25.smt2 | 21.844s | 2995.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U65.smt2 | 21.849s | 3641.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U82.smt2 | 21.851s | 3899.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U20.smt2 | 21.875s | 3982.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U62.smt2 | 21.890s | 3844.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U13.smt2 | 21.901s | 4443.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C12.smt2 | 21.907s | 4119.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U64.smt2 | 21.913s | 3252.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U3.smt2 | 21.916s | 4278.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U92.smt2 | 21.922s | 4296.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U25.smt2 | 21.940s | 4487.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U15.smt2 | 21.956s | 3520.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U24.smt2 | 21.969s | 4054.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_C1.smt2 | 21.993s | 3847.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U49.smt2 | 22.005s | 4177.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U89.smt2 | 22.028s | 7370.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U29_sol1.smt2 | 22.113s | 4575.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_U24.smt2 | 22.138s | 4128.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/prove/problem_C1.smt2 | 22.177s | 7344.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/find/problem_U42.smt2 | 22.365s | 4781.0MiB| timeout | 0 | | | |non-incremental/UFNIRA/20240414-funcprobs/check/problem_U43_sol1.smt2 | 22.446s | 8055.0MiB| timeout | 0 | | |