# . * SAT 70 * UNSAT 0 * TIMEOUT 0 * 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_SNIA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-QF_SNIA.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/QF_SNIA.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1552.corecstrs.readable.smt2 | 0.023s | 20.756MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1590.corecstrs.readable.smt2 | 0.023s | 20.848MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/2008.corecstrs.readable.smt2 | 0.024s | 20.048MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1884.corecstrs.readable.smt2 | 0.024s | 20.472MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1572.corecstrs.readable.smt2 | 0.024s | 20.364MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1567.corecstrs.readable.smt2 | 0.024s | 20.368MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/823.corecstrs.readable.smt2 | 0.025s | 20.512MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1589.corecstrs.readable.smt2 | 0.025s | 20.38MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1573.corecstrs.readable.smt2 | 0.025s | 20.368MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1557.corecstrs.readable.smt2 | 0.025s | 20.264MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1886.corecstrs.readable.smt2 | 0.026s | 20.384MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/846.corecstrs.readable.smt2 | 0.027s | 20.596MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1911.corecstrs.readable.smt2 | 0.027s | 20.62MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1627.corecstrs.readable.smt2 | 0.027s | 20.34MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/849.corecstrs.readable.smt2 | 0.029s | 20.352MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/845.corecstrs.readable.smt2 | 0.029s | 20.348MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1909.corecstrs.readable.smt2 | 0.029s | 20.604MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/843.corecstrs.readable.smt2 | 0.030s | 20.5MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/812.corecstrs.readable.smt2 | 0.031s | 20.352MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/821.corecstrs.readable.smt2 | 0.031s | 20.652MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1594.corecstrs.readable.smt2 | 0.032s | 20.288MiB| sat | 0 | | | |non-incremental/QF_SNIA/20200224-Wu-PyExZ3/bdcb3877984a55b540face066045c4642cba1bc553af78576a41a76e.smt2 | 0.039s | 20.492MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1576.corecstrs.readable.smt2 | 0.039s | 20.376MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1555.corecstrs.readable.smt2 | 0.039s | 20.248MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1551.corecstrs.readable.smt2 | 0.039s | 20.148MiB| sat | 0 | | | |non-incremental/QF_SNIA/20200224-Wu-PyExZ3/5735c9082c3f9cd487c6376032029bb499ba1f87113dc9ca03adc6bc.smt2 | 0.040s | 20.524MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1596.corecstrs.readable.smt2 | 0.040s | 20.156MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1550.corecstrs.readable.smt2 | 0.040s | 20.22MiB| sat | 0 | | | |non-incremental/QF_SNIA/20200224-Wu-PyExZ3/dddb9cc1f86d5738fd85ffa1b430c4e9df9771c0fffa945b9b414772.smt2 | 0.041s | 20.608MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/2010.corecstrs.readable.smt2 | 0.041s | 20.124MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1908.corecstrs.readable.smt2 | 0.041s | 20.3MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1588.corecstrs.readable.smt2 | 0.041s | 20.144MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1556.corecstrs.readable.smt2 | 0.041s | 20.344MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1566.corecstrs.readable.smt2 | 0.041s | 20.38MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/827.corecstrs.readable.smt2 | 0.042s | 20.74MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1997.corecstrs.readable.smt2 | 0.042s | 20.144MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1636.corecstrs.readable.smt2 | 0.042s | 20.14MiB| sat | 0 | | | |non-incremental/QF_SNIA/20200224-Wu-PyExZ3/f72b09bc9444f702ad7cdf3a9075754e71d673f3d134d9f485f6608a.smt2 | 0.043s | 20.704MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/839.corecstrs.readable.smt2 | 0.044s | 20.4MiB| sat | 0 | | | |non-incremental/QF_SNIA/20200224-Wu-PyExZ3/e007cfdcf4dd61007107222cbedbb46ad161a945ab5ee0a68d3f585a.smt2 | 0.045s | 21.104MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/824.corecstrs.readable.smt2 | 0.045s | 20.4MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/840.corecstrs.readable.smt2 | 0.045s | 20.664MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/809.corecstrs.readable.smt2 | 0.045s | 20.368MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1568.corecstrs.readable.smt2 | 0.045s | 20.372MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/2009.corecstrs.readable.smt2 | 0.045s | 20.084MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/2007.corecstrs.readable.smt2 | 0.046s | 20.336MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1626.corecstrs.readable.smt2 | 0.046s | 20.14MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/808.corecstrs.readable.smt2 | 0.047s | 20.408MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/851.corecstrs.readable.smt2 | 0.047s | 20.596MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1553.corecstrs.readable.smt2 | 0.047s | 20.368MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1634.corecstrs.readable.smt2 | 0.048s | 20.144MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1598.corecstrs.readable.smt2 | 0.048s | 20.372MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/820.corecstrs.readable.smt2 | 0.049s | 20.476MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/811.corecstrs.readable.smt2 | 0.049s | 20.292MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1637.corecstrs.readable.smt2 | 0.049s | 20.356MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1628.corecstrs.readable.smt2 | 0.049s | 20.608MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1575.corecstrs.readable.smt2 | 0.049s | 20.264MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/826.corecstrs.readable.smt2 | 0.050s | 20.44MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1597.corecstrs.readable.smt2 | 0.050s | 20.368MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1554.corecstrs.readable.smt2 | 0.050s | 20.632MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1633.corecstrs.readable.smt2 | 0.050s | 20.376MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1907.corecstrs.readable.smt2 | 0.050s | 20.384MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/838.corecstrs.readable.smt2 | 0.051s | 20.364MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1885.corecstrs.readable.smt2 | 0.051s | 20.224MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1574.corecstrs.readable.smt2 | 0.051s | 20.416MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1595.corecstrs.readable.smt2 | 0.051s | 20.38MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/822.corecstrs.readable.smt2 | 0.052s | 20.508MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1635.corecstrs.readable.smt2 | 0.052s | 20.656MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/small/1910.corecstrs.readable.smt2 | 0.052s | 20.176MiB| sat | 0 | | | |non-incremental/QF_SNIA/20180523-Reynolds/kaluza/sat/big/825.corecstrs.readable.smt2 | 0.056s | 20.352MiB| sat | 0 | | |