# . * 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-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/AUFBVFP.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/583_ph7.smt2 | 0.340s | 115.0MiB| unsat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/340_oggenc.smt2 | 0.367s | 36.616MiB| sat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/392_oggenc.smt2 | 1.182s | 45.044MiB| sat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/ph7/611_ph7.smt2 | 1.262s | 42.428MiB| unsat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/344_oggenc.smt2 | 2.376s | 47.64MiB| sat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/290_oggenc.smt2 | 2.446s | 338.0MiB| unsat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/455_oggenc.smt2 | 3.343s | 329.0MiB| unsat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/397_oggenc.smt2 | 6.029s | 60.624MiB| unsat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/sqlite3/816_sqlite3.smt2 | 7.116s | 67.264MiB| unsat | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/744_ph7.smt2 | 20.022s | 94.192MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/411_oggenc.smt2 | 20.023s | 47.72MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/384_oggenc.smt2 | 20.033s | 111.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/352_oggenc.smt2 | 20.036s | 253.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/277_oggenc.smt2 | 20.037s | 245.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/295_oggenc.smt2 | 20.043s | 272.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/426_oggenc.smt2 | 20.047s | 339.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/ph7/757_ph7.smt2 | 20.048s | 107.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/342_oggenc.smt2 | 20.048s | 272.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/ph7/568_ph7.smt2 | 20.049s | 89.088MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/374_oggenc.smt2 | 20.053s | 114.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/351_oggenc.smt2 | 20.056s | 36.18MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/322_oggenc.smt2 | 20.057s | 143.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/392_oggenc.smt2 | 20.068s | 120.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/bzip2/001_bzip2.smt2 | 20.070s | 131.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/357_oggenc.smt2 | 20.070s | 119.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/sqlite3/892_sqlite3.smt2 | 20.071s | 101.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/445_oggenc.smt2 | 20.071s | 194.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/422_oggenc.smt2 | 20.077s | 167.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/459_oggenc.smt2 | 20.078s | 550.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/410_oggenc.smt2 | 20.089s | 221.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/449_oggenc.smt2 | 20.091s | 278.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/324_oggenc.smt2 | 20.091s | 270.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/434_oggenc.smt2 | 20.094s | 225.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/368_oggenc.smt2 | 20.100s | 460.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/343_oggenc.smt2 | 20.102s | 239.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/354_oggenc.smt2 | 20.103s | 250.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/300_oggenc.smt2 | 20.107s | 469.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/356_oggenc.smt2 | 20.116s | 319.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/305_oggenc.smt2 | 20.124s | 422.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/303_oggenc.smt2 | 20.131s | 667.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/288_oggenc.smt2 | 20.136s | 353.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/293_oggenc.smt2 | 20.138s | 466.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/369_oggenc.smt2 | 20.141s | 555.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/sqlite3/917_sqlite3.smt2 | 20.143s | 412.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/358_oggenc.smt2 | 20.143s | 807.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/409_oggenc.smt2 | 20.159s | 680.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/386_oggenc.smt2 | 20.173s | 664.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/446_oggenc.smt2 | 20.212s | 1369.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/430_oggenc.smt2 | 20.404s | 3142.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/sqlite3/870_sqlite3.smt2 | 20.520s | 3801.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/453_oggenc.smt2 | 20.561s | 4568.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/461_oggenc.smt2 | 20.751s | 6096.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/385_oggenc.smt2 | 20.827s | 6489.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/346_oggenc.smt2 | 20.892s | 7761.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/oggenc/344_oggenc.smt2 | 20.904s | 7831.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2/oggenc/457_oggenc.smt2 | 20.981s | 8632.0MiB| timeout | 0 | | | |non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/489_ph7.smt2 | 21.052s | 8567.0MiB| timeout | 0 | | |