# . * SAT 31 * UNSAT 24 * TIMEOUT 3 * 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/QF_UFNRA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-QF_UFNRA.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/QF_UFNRA.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/QF_UFNRA/20190906-CLEARSY/0004/00003.smt2 | 0.025s | 20.112MiB| sat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/modSimpleTest.smt2 | 0.026s | 20.404MiB| sat | 0 | | | |non-incremental/QF_UFNRA/FFT/smtlib.640350.smt2 | 0.028s | 19.608MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/FFT/smtlib.630867.smt2 | 0.032s | 20.196MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/FFT/smtlib.630949.smt2 | 0.033s | 19.932MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/FFT/smtlib.631277.smt2 | 0.034s | 19.856MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/FFT/smtlib.630785.smt2 | 0.036s | 20.252MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/FFT/smtlib.631031.smt2 | 0.050s | 19.932MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/FFT/z3.641736.smt2 | 0.050s | 19.524MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/FFT/z3.630166.smt2 | 0.050s | 20.148MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/l40m.smt2 | 0.051s | 21.46MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/FFT/smtlib.631195.smt2 | 0.051s | 19.992MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/FFT/smtlib.631113.smt2 | 0.051s | 20.116MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStepFinala.smt2 | 0.053s | 21.132MiB| sat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/modInvInitial.smt2 | 0.054s | 20.68MiB| sat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/modInvStep.smt2 | 0.056s | 21.112MiB| sat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/modInvVar1.smt2 | 0.064s | 20.7MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/l40f.smt2 | 0.070s | 21.248MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStepFinal.smt2 | 0.094s | 21.012MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/m40.easy.smt2 | 0.185s | 27.98MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/c40s.smt2 | 0.225s | 29.62MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/40s50.smt2 | 0.231s | 30.536MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/c40f.smt2 | 0.245s | 31.292MiB| sat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep2.smt2 | 0.433s | 21.312MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/cas/40m25.smt2 | 0.466s | 37.46MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/c40m.smt2 | 0.467s | 33.4MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/l40s.smt2 | 0.482s | 40.96MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/40f25.smt2 | 0.538s | 34.5MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/40m50.smt2 | 0.635s | 35.62MiB| sat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep2a.smt2 | 0.742s | 21.412MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/cas/40f10.smt2 | 0.749s | 38.188MiB| sat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep4a.smt2 | 0.766s | 21.416MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/cas/40m99.smt2 | 0.897s | 36.124MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/40s10.smt2 | 0.979s | 40.04MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/40s25.smt2 | 1.065s | 39.612MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/40f50.smt2 | 1.162s | 35.932MiB| sat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep1.smt2 | 1.167s | 21.528MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/cas/20u10.09.smt2 | 1.217s | 31.408MiB| sat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep3a.smt2 | 1.223s | 21.496MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/cas/40s99.smt2 | 1.371s | 40.416MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/40m10.smt2 | 1.546s | 41.232MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/40f99.smt2 | 1.682s | 36.692MiB| sat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep3.smt2 | 1.781s | 21.496MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep6.smt2 | 2.159s | 21.528MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep4.smt2 | 2.239s | 21.68MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep5.smt2 | 2.382s | 21.876MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/cas/s40.smt2 | 5.038s | 37.5MiB| sat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep1a.smt2 | 5.277s | 21.528MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep6a.smt2 | 6.361s | 21.988MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep5a.smt2 | 7.474s | 22.432MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/cas/20revert.u.smt2 | 7.504s | 33.492MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/10u05.04.smt2 | 9.126s | 25.688MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/40u20.19.smt2 | 9.351s | 55.816MiB| sat | 0 | | | |non-incremental/QF_UFNRA/cas/m40.smt2 | 13.232s | 56.912MiB| sat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep7.smt2 | 14.739s | 23.392MiB| unsat | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/sqrtStep7a.smt2 | 20.035s | 22.448MiB| timeout | 0 | | | |non-incremental/QF_UFNRA/cas/30u15.14.smt2 | 20.037s | 40.88MiB| timeout | 0 | | | |non-incremental/QF_UFNRA/20230328-sqrtmodinv-hoenicke/modInvFull.smt2 | 20.109s | 939.0MiB| timeout | 0 | | |