# . * SAT 3 * UNSAT 6 * TIMEOUT 48 * UNKNOWN 0 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/AUFBVFP.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-AUFBVFP.tar.zst-do
Runner: rise-runner-1
Z3 repo: Z3Prover/z3
Z3 commit: 8c989f8840e2c5789cd31aa9465dd2527852d453
Z3 branch: master
Z3 options: "-T:20 model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/AUFBVFP.tar.zst?download=1
Z3 commit message: update tptp front-end
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/583_ph7.smt2 | 0.356s | 114.0MiB| unsat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/340_oggenc.smt2 | 0.456s | 35.668MiB| sat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/392_oggenc.smt2 | 1.662s | 44.492MiB| sat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/ph7/611_ph7.smt2 | 1.755s | 41.64MiB| unsat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/290_oggenc.smt2 | 2.747s | 338.0MiB| unsat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/344_oggenc.smt2 | 3.249s | 46.488MiB| sat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/455_oggenc.smt2 | 3.907s | 328.0MiB| unsat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/397_oggenc.smt2 | 7.476s | 60.112MiB| unsat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/sqlite3/816_sqlite3.smt2 | 9.069s | 66.6MiB| unsat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/ph7/568_ph7.smt2 | 20.029s | 88.188MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/351_oggenc.smt2 | 20.036s | 35.464MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/422_oggenc.smt2 | 20.044s | 166.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/ph7/757_ph7.smt2 | 20.049s | 98.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/411_oggenc.smt2 | 20.054s | 46.884MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/744_ph7.smt2 | 20.054s | 93.412MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/354_oggenc.smt2 | 20.055s | 136.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/sqlite3/892_sqlite3.smt2 | 20.057s | 101.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/384_oggenc.smt2 | 20.059s | 101.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/bzip2/001_bzip2.smt2 | 20.060s | 127.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/392_oggenc.smt2 | 20.060s | 116.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/374_oggenc.smt2 | 20.062s | 106.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/357_oggenc.smt2 | 20.067s | 101.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/426_oggenc.smt2 | 20.077s | 254.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/410_oggenc.smt2 | 20.092s | 221.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/322_oggenc.smt2 | 20.096s | 129.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/445_oggenc.smt2 | 20.101s | 193.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/343_oggenc.smt2 | 20.105s | 238.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/352_oggenc.smt2 | 20.107s | 252.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/434_oggenc.smt2 | 20.110s | 220.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/295_oggenc.smt2 | 20.111s | 267.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/277_oggenc.smt2 | 20.114s | 244.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/356_oggenc.smt2 | 20.115s | 256.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/324_oggenc.smt2 | 20.117s | 269.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/342_oggenc.smt2 | 20.125s | 269.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/449_oggenc.smt2 | 20.128s | 271.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/288_oggenc.smt2 | 20.132s | 352.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/305_oggenc.smt2 | 20.135s | 422.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/sqlite3/917_sqlite3.smt2 | 20.149s | 402.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/368_oggenc.smt2 | 20.152s | 447.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/300_oggenc.smt2 | 20.157s | 463.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/293_oggenc.smt2 | 20.158s | 450.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/369_oggenc.smt2 | 20.161s | 555.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/409_oggenc.smt2 | 20.171s | 680.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/459_oggenc.smt2 | 20.173s | 549.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/386_oggenc.smt2 | 20.185s | 664.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/303_oggenc.smt2 | 20.186s | 666.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/358_oggenc.smt2 | 20.192s | 807.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/430_oggenc.smt2 | 20.240s | 1510.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/446_oggenc.smt2 | 20.255s | 1354.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/sqlite3/870_sqlite3.smt2 | 20.423s | 3656.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/453_oggenc.smt2 | 20.443s | 3851.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/461_oggenc.smt2 | 20.571s | 5648.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/385_oggenc.smt2 | 20.588s | 5784.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/344_oggenc.smt2 | 20.684s | 7115.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/346_oggenc.smt2 | 20.694s | 7136.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/457_oggenc.smt2 | 20.746s | 8093.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/489_ph7.smt2 | 20.751s | 8546.0MiB| timeout | 0 | | |