# . * SAT 0 * UNSAT 114 * TIMEOUT 180 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: rings_with_z3-4.14.0
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: 3c47fd96cf5645d0c42b2c819d9e9a84380aa721
Z3 branch: 
Z3 options: "-T:600 -st"
Z3 inputs: inputs/rings
Z3 commit message: bump timeout for jobs

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |ring_2exp16_4vars_0ite_unsat.smt2 | 0.031s | 20.544MiB| unsat | 0 | | | |ring_2exp8_5vars_0ite_unsat.smt2 | 0.031s | 20.584MiB| unsat | 0 | | | |ring_2exp16_3vars_0ite_unsat.smt2 | 0.032s | 20.352MiB| unsat | 0 | | | |ring_2exp12_4vars_0ite_unsat.smt2 | 0.032s | 20.188MiB| unsat | 0 | | | |ring_2exp6_3vars_0ite_unsat.smt2 | 0.033s | 20.38MiB| unsat | 0 | | | |ring_2exp12_7vars_0ite_unsat.smt2 | 0.034s | 20.652MiB| unsat | 0 | | | |ring_2exp14_4vars_0ite_unsat.smt2 | 0.035s | 20.34MiB| unsat | 0 | | | |ring_2exp6_4vars_0ite_unsat.smt2 | 0.035s | 20.272MiB| unsat | 0 | | | |ring_2exp10_3vars_0ite_unsat.smt2 | 0.036s | 20.512MiB| unsat | 0 | | | |ring_2exp14_5vars_0ite_unsat.smt2 | 0.037s | 20.52MiB| unsat | 0 | | | |ring_2exp8_4vars_0ite_unsat.smt2 | 0.038s | 20.408MiB| unsat | 0 | | | |ring_2exp4_4vars_0ite_unsat.smt2 | 0.038s | 20.168MiB| unsat | 0 | | | |ring_2exp4_5vars_0ite_unsat.smt2 | 0.039s | 20.736MiB| unsat | 0 | | | |ring_2exp14_7vars_0ite_unsat.smt2 | 0.040s | 20.976MiB| unsat | 0 | | | |ring_2exp16_5vars_0ite_unsat.smt2 | 0.040s | 20.524MiB| unsat | 0 | | | |ring_2exp6_8vars_0ite_unsat.smt2 | 0.041s | 20.776MiB| unsat | 0 | | | |ring_2exp16_6vars_0ite_unsat.smt2 | 0.041s | 20.636MiB| unsat | 0 | | | |ring_2exp10_4vars_0ite_unsat.smt2 | 0.041s | 20.516MiB| unsat | 0 | | | |ring_2exp12_3vars_2ite_unsat.smt2 | 0.041s | 20.272MiB| unsat | 0 | | | |ring_2exp10_3vars_2ite_unsat.smt2 | 0.042s | 20.3MiB| unsat | 0 | | | |ring_2exp14_8vars_0ite_unsat.smt2 | 0.044s | 20.904MiB| unsat | 0 | | | |ring_2exp14_6vars_0ite_unsat.smt2 | 0.044s | 20.52MiB| unsat | 0 | | | |ring_2exp10_8vars_0ite_unsat.smt2 | 0.045s | 20.836MiB| unsat | 0 | | | |ring_2exp12_6vars_0ite_unsat.smt2 | 0.045s | 20.456MiB| unsat | 0 | | | |ring_2exp4_3vars_0ite_unsat.smt2 | 0.045s | 20.264MiB| unsat | 0 | | | |ring_2exp8_8vars_0ite_unsat.smt2 | 0.045s | 20.848MiB| unsat | 0 | | | |ring_2exp10_6vars_0ite_unsat.smt2 | 0.046s | 20.596MiB| unsat | 0 | | | |ring_2exp8_9vars_0ite_unsat.smt2 | 0.047s | 20.868MiB| unsat | 0 | | | |ring_2exp10_9vars_0ite_unsat.smt2 | 0.047s | 21.032MiB| unsat | 0 | | | |ring_2exp14_9vars_0ite_unsat.smt2 | 0.048s | 21.036MiB| unsat | 0 | | | |ring_2exp8_3vars_0ite_unsat.smt2 | 0.048s | 20.052MiB| unsat | 0 | | | |ring_2exp16_9vars_0ite_unsat.smt2 | 0.048s | 21.184MiB| unsat | 0 | | | |ring_2exp14_3vars_2ite_unsat.smt2 | 0.048s | 20.604MiB| unsat | 0 | | | |ring_2exp10_5vars_0ite_unsat.smt2 | 0.048s | 20.524MiB| unsat | 0 | | | |ring_2exp4_7vars_0ite_unsat.smt2 | 0.049s | 20.52MiB| unsat | 0 | | | |ring_2exp6_9vars_0ite_unsat.smt2 | 0.049s | 20.736MiB| unsat | 0 | | | |ring_2exp12_8vars_0ite_unsat.smt2 | 0.049s | 20.78MiB| unsat | 0 | | | |ring_2exp12_5vars_0ite_unsat.smt2 | 0.049s | 20.52MiB| unsat | 0 | | | |ring_2exp12_9vars_0ite_unsat.smt2 | 0.050s | 20.96MiB| unsat | 0 | | | |ring_2exp4_6vars_0ite_unsat.smt2 | 0.050s | 20.524MiB| unsat | 0 | | | |ring_2exp4_8vars_0ite_unsat.smt2 | 0.051s | 20.656MiB| unsat | 0 | | | |ring_2exp16_3vars_1ite_unsat.smt2 | 0.051s | 20.384MiB| unsat | 0 | | | |ring_2exp12_3vars_0ite_unsat.smt2 | 0.051s | 20.268MiB| unsat | 0 | | | |ring_2exp8_3vars_2ite_unsat.smt2 | 0.052s | 20.268MiB| unsat | 0 | | | |ring_2exp14_3vars_0ite_unsat.smt2 | 0.053s | 20.324MiB| unsat | 0 | | | |ring_2exp16_7vars_0ite_unsat.smt2 | 0.053s | 20.776MiB| unsat | 0 | | | |ring_2exp8_6vars_0ite_unsat.smt2 | 0.053s | 20.556MiB| unsat | 0 | | | |ring_2exp4_3vars_1ite_unsat.smt2 | 0.054s | 20.328MiB| unsat | 0 | | | |ring_2exp6_6vars_0ite_unsat.smt2 | 0.054s | 20.428MiB| unsat | 0 | | | |ring_2exp6_5vars_0ite_unsat.smt2 | 0.055s | 20.46MiB| unsat | 0 | | | |ring_2exp8_7vars_0ite_unsat.smt2 | 0.055s | 21.036MiB| unsat | 0 | | | |ring_2exp8_3vars_1ite_unsat.smt2 | 0.055s | 20.352MiB| unsat | 0 | | | |ring_2exp14_3vars_1ite_unsat.smt2 | 0.057s | 20.328MiB| unsat | 0 | | | |ring_2exp10_3vars_1ite_unsat.smt2 | 0.057s | 20.328MiB| unsat | 0 | | | |ring_2exp6_3vars_1ite_unsat.smt2 | 0.058s | 20.148MiB| unsat | 0 | | | |ring_2exp10_7vars_0ite_unsat.smt2 | 0.058s | 20.708MiB| unsat | 0 | | | |ring_2exp16_8vars_0ite_unsat.smt2 | 0.058s | 20.684MiB| unsat | 0 | | | |ring_2exp16_3vars_2ite_unsat.smt2 | 0.059s | 20.364MiB| unsat | 0 | | | |ring_2exp12_3vars_1ite_unsat.smt2 | 0.065s | 20.504MiB| unsat | 0 | | | |ring_2exp6_3vars_2ite_unsat.smt2 | 0.067s | 20.26MiB| unsat | 0 | | | |ring_2exp6_7vars_0ite_unsat.smt2 | 0.067s | 20.896MiB| unsat | 0 | | | |ring_2exp4_3vars_2ite_unsat.smt2 | 0.069s | 20.508MiB| unsat | 0 | | | |ring_2exp4_9vars_0ite_unsat.smt2 | 0.077s | 20.844MiB| unsat | 0 | | | |ring_2exp16_4vars_2ite_unsat.smt2 | 0.670s | 20.828MiB| unsat | 0 | | | |ring_2exp14_4vars_3ite_unsat.smt2 | 0.673s | 20.848MiB| unsat | 0 | | | |ring_2exp14_4vars_1ite_unsat.smt2 | 0.740s | 20.808MiB| unsat | 0 | | | |ring_2exp16_4vars_3ite_unsat.smt2 | 0.782s | 21.02MiB| unsat | 0 | | | |ring_2exp10_4vars_3ite_unsat.smt2 | 0.794s | 20.944MiB| unsat | 0 | | | |ring_2exp12_4vars_3ite_unsat.smt2 | 0.799s | 20.924MiB| unsat | 0 | | | |ring_2exp4_4vars_3ite_unsat.smt2 | 0.805s | 20.776MiB| unsat | 0 | | | |ring_2exp10_4vars_2ite_unsat.smt2 | 0.829s | 20.964MiB| unsat | 0 | | | |ring_2exp6_4vars_1ite_unsat.smt2 | 0.837s | 21.368MiB| unsat | 0 | | | |ring_2exp16_4vars_1ite_unsat.smt2 | 0.843s | 20.796MiB| unsat | 0 | | | |ring_2exp8_4vars_1ite_unsat.smt2 | 0.850s | 20.912MiB| unsat | 0 | | | |ring_2exp8_4vars_3ite_unsat.smt2 | 0.869s | 20.988MiB| unsat | 0 | | | |ring_2exp14_4vars_2ite_unsat.smt2 | 0.876s | 20.792MiB| unsat | 0 | | | |ring_2exp12_4vars_2ite_unsat.smt2 | 0.919s | 20.876MiB| unsat | 0 | | | |ring_2exp10_4vars_1ite_unsat.smt2 | 0.935s | 20.988MiB| unsat | 0 | | | |ring_2exp12_4vars_1ite_unsat.smt2 | 0.940s | 20.924MiB| unsat | 0 | | | |ring_2exp4_4vars_2ite_unsat.smt2 | 1.019s | 20.896MiB| unsat | 0 | | | |ring_2exp6_4vars_3ite_unsat.smt2 | 1.028s | 20.892MiB| unsat | 0 | | | |ring_2exp8_4vars_2ite_unsat.smt2 | 1.085s | 21.068MiB| unsat | 0 | | | |ring_2exp4_4vars_1ite_unsat.smt2 | 1.116s | 20.916MiB| unsat | 0 | | | |ring_2exp6_4vars_2ite_unsat.smt2 | 1.412s | 21.124MiB| unsat | 0 | | | |ring_2exp4_5vars_1ite_unsat.smt2 | 9.600s | 23.328MiB| unsat | 0 | | | |ring_2exp4_5vars_3ite_unsat.smt2 | 9.805s | 23.58MiB| unsat | 0 | | | |ring_2exp4_5vars_4ite_unsat.smt2 | 48.541s | 24.68MiB| unsat | 0 | | | |ring_2exp4_5vars_2ite_unsat.smt2 | 53.183s | 24.576MiB| unsat | 0 | | | |ring_2exp8_5vars_4ite_unsat.smt2 | 96.721s | 29.752MiB| unsat | 0 | | | |ring_2exp16_5vars_4ite_unsat.smt2 | 110.515s | 29.12MiB| unsat | 0 | | | |ring_2exp14_5vars_4ite_unsat.smt2 | 113.384s | 27.864MiB| unsat | 0 | | | |ring_2exp12_5vars_4ite_unsat.smt2 | 121.323s | 29.272MiB| unsat | 0 | | | |ring_2exp10_5vars_4ite_unsat.smt2 | 128.815s | 29.572MiB| unsat | 0 | | | |ring_2exp14_5vars_3ite_unsat.smt2 | 129.374s | 30.232MiB| unsat | 0 | | | |ring_2exp16_5vars_1ite_unsat.smt2 | 152.156s | 29.332MiB| unsat | 0 | | | |ring_2exp4_7vars_2ite_unsat.smt2 | 184.007s | 29.856MiB| unsat | 0 | | | |ring_2exp6_5vars_4ite_unsat.smt2 | 193.054s | 32.632MiB| unsat | 0 | | | |ring_2exp4_7vars_1ite_unsat.smt2 | 195.085s | 30.528MiB| unsat | 0 | | | |ring_2exp4_6vars_5ite_unsat.smt2 | 214.575s | 29.536MiB| unsat | 0 | | | |ring_2exp16_5vars_3ite_unsat.smt2 | 219.001s | 30.264MiB| unsat | 0 | | | |ring_2exp4_8vars_1ite_unsat.smt2 | 221.061s | 30.296MiB| unsat | 0 | | | |ring_2exp14_5vars_2ite_unsat.smt2 | 227.846s | 30.624MiB| unsat | 0 | | | |ring_2exp12_5vars_3ite_unsat.smt2 | 231.750s | 30.672MiB| unsat | 0 | | | |ring_2exp10_5vars_2ite_unsat.smt2 | 261.753s | 34.368MiB| unsat | 0 | | | |ring_2exp12_5vars_1ite_unsat.smt2 | 273.655s | 31.088MiB| unsat | 0 | | | |ring_2exp10_5vars_1ite_unsat.smt2 | 300.888s | 32.332MiB| unsat | 0 | | | |ring_2exp8_5vars_1ite_unsat.smt2 | 309.884s | 34.008MiB| unsat | 0 | | | |ring_2exp16_5vars_2ite_unsat.smt2 | 312.307s | 32.38MiB| unsat | 0 | | | |ring_2exp14_5vars_1ite_unsat.smt2 | 356.127s | 32.796MiB| unsat | 0 | | | |ring_2exp4_6vars_4ite_unsat.smt2 | 392.552s | 33.12MiB| unsat | 0 | | | |ring_2exp4_8vars_2ite_unsat.smt2 | 413.221s | 31.128MiB| unsat | 0 | | | |ring_2exp4_6vars_1ite_unsat.smt2 | 417.961s | 34.576MiB| unsat | 0 | | | |ring_2exp4_6vars_2ite_unsat.smt2 | 424.006s | 32.38MiB| unsat | 0 | | | |ring_2exp12_5vars_2ite_unsat.smt2 | 545.965s | 33.252MiB| unsat | 0 | | | |ring_2exp6_8vars_5ite_unsat.smt2 | 597.468s | 37.276MiB| timeout | 0 | | | |ring_2exp4_6vars_3ite_unsat.smt2 | 598.436s | 35.228MiB| timeout | 0 | | | |ring_2exp8_8vars_6ite_unsat.smt2 | 598.471s | 39.612MiB| timeout | 0 | | | |ring_2exp6_9vars_8ite_unsat.smt2 | 598.488s | 34.996MiB| timeout | 0 | | | |ring_2exp8_9vars_8ite_unsat.smt2 | 598.637s | 39.604MiB| timeout | 0 | | | |ring_2exp8_8vars_1ite_unsat.smt2 | 598.651s | 41.248MiB| timeout | 0 | | | |ring_2exp8_9vars_1ite_unsat.smt2 | 598.793s | 44.088MiB| timeout | 0 | | | |ring_2exp8_9vars_2ite_unsat.smt2 | 598.893s | 45.476MiB| timeout | 0 | | | |ring_2exp12_7vars_6ite_unsat.smt2 | 599.111s | 35.552MiB| timeout | 0 | | | |ring_2exp14_8vars_4ite_unsat.smt2 | 599.159s | 37.444MiB| timeout | 0 | | | |ring_2exp16_9vars_5ite_unsat.smt2 | 599.206s | 39.46MiB| timeout | 0 | | | |ring_2exp4_7vars_4ite_unsat.smt2 | 599.207s | 36.424MiB| timeout | 0 | | | |ring_2exp10_5vars_3ite_unsat.smt2 | 599.209s | 34.972MiB| timeout | 0 | | | |ring_2exp10_9vars_1ite_unsat.smt2 | 599.249s | 42.484MiB| timeout | 0 | | | |ring_2exp16_9vars_7ite_unsat.smt2 | 599.298s | 36.496MiB| timeout | 0 | | | |ring_2exp12_8vars_5ite_unsat.smt2 | 599.317s | 39.428MiB| timeout | 0 | | | |ring_2exp14_9vars_4ite_unsat.smt2 | 599.324s | 41.008MiB| timeout | 0 | | | |ring_2exp12_6vars_4ite_unsat.smt2 | 599.326s | 45.452MiB| timeout | 0 | | | |ring_2exp6_9vars_2ite_unsat.smt2 | 599.343s | 42.048MiB| timeout | 0 | | | |ring_2exp6_7vars_1ite_unsat.smt2 | 599.485s | 36.588MiB| timeout | 0 | | | |ring_2exp6_7vars_4ite_unsat.smt2 | 599.489s | 36.536MiB| timeout | 0 | | | |ring_2exp14_6vars_2ite_unsat.smt2 | 599.494s | 38.216MiB| timeout | 0 | | | |ring_2exp12_8vars_7ite_unsat.smt2 | 599.497s | 37.464MiB| timeout | 0 | | | |ring_2exp8_6vars_4ite_unsat.smt2 | 599.508s | 38.604MiB| timeout | 0 | | | |ring_2exp6_8vars_2ite_unsat.smt2 | 599.532s | 38.996MiB| timeout | 0 | | | |ring_2exp14_8vars_5ite_unsat.smt2 | 599.564s | 38.0MiB| timeout | 0 | | | |ring_2exp8_8vars_5ite_unsat.smt2 | 599.567s | 38.86MiB| timeout | 0 | | | |ring_2exp8_5vars_3ite_unsat.smt2 | 599.578s | 34.136MiB| timeout | 0 | | | |ring_2exp12_7vars_1ite_unsat.smt2 | 599.590s | 41.428MiB| timeout | 0 | | | |ring_2exp16_6vars_5ite_unsat.smt2 | 599.591s | 44.252MiB| timeout | 0 | | | |ring_2exp4_8vars_7ite_unsat.smt2 | 599.613s | 30.9MiB| timeout | 0 | | | |ring_2exp10_8vars_4ite_unsat.smt2 | 599.614s | 39.832MiB| timeout | 0 | | | |ring_2exp16_6vars_1ite_unsat.smt2 | 599.617s | 35.192MiB| timeout | 0 | | | |ring_2exp6_8vars_4ite_unsat.smt2 | 599.620s | 37.672MiB| timeout | 0 | | | |ring_2exp12_6vars_1ite_unsat.smt2 | 599.630s | 37.524MiB| timeout | 0 | | | |ring_2exp16_6vars_3ite_unsat.smt2 | 599.636s | 38.08MiB| timeout | 0 | | | |ring_2exp12_6vars_3ite_unsat.smt2 | 599.637s | 40.6MiB| timeout | 0 | | | |ring_2exp14_8vars_2ite_unsat.smt2 | 599.643s | 41.264MiB| timeout | 0 | | | |ring_2exp12_8vars_6ite_unsat.smt2 | 599.675s | 38.336MiB| timeout | 0 | | | |ring_2exp14_6vars_5ite_unsat.smt2 | 599.676s | 41.232MiB| timeout | 0 | | | |ring_2exp6_7vars_2ite_unsat.smt2 | 599.684s | 38.14MiB| timeout | 0 | | | |ring_2exp14_9vars_7ite_unsat.smt2 | 599.689s | 45.72MiB| timeout | 0 | | | |ring_2exp14_7vars_6ite_unsat.smt2 | 599.691s | 38.612MiB| timeout | 0 | | | |ring_2exp12_9vars_5ite_unsat.smt2 | 599.694s | 39.764MiB| timeout | 0 | | | |ring_2exp4_7vars_3ite_unsat.smt2 | 599.697s | 33.952MiB| timeout | 0 | | | |ring_2exp12_9vars_1ite_unsat.smt2 | 599.700s | 47.3MiB| timeout | 0 | | | |ring_2exp6_9vars_5ite_unsat.smt2 | 599.701s | 36.476MiB| timeout | 0 | | | |ring_2exp14_8vars_6ite_unsat.smt2 | 599.703s | 37.624MiB| timeout | 0 | | | |ring_2exp4_9vars_5ite_unsat.smt2 | 599.706s | 33.232MiB| timeout | 0 | | | |ring_2exp4_8vars_3ite_unsat.smt2 | 599.707s | 30.736MiB| timeout | 0 | | | |ring_2exp10_8vars_7ite_unsat.smt2 | 599.713s | 40.296MiB| timeout | 0 | | | |ring_2exp8_9vars_4ite_unsat.smt2 | 599.715s | 43.436MiB| timeout | 0 | | | |ring_2exp14_8vars_3ite_unsat.smt2 | 599.717s | 41.468MiB| timeout | 0 | | | |ring_2exp14_7vars_4ite_unsat.smt2 | 599.730s | 39.076MiB| timeout | 0 | | | |ring_2exp4_7vars_6ite_unsat.smt2 | 599.731s | 39.628MiB| timeout | 0 | | | |ring_2exp10_6vars_4ite_unsat.smt2 | 599.733s | 39.348MiB| timeout | 0 | | | |ring_2exp4_9vars_7ite_unsat.smt2 | 599.733s | 32.64MiB| timeout | 0 | | | |ring_2exp10_7vars_4ite_unsat.smt2 | 599.737s | 39.272MiB| timeout | 0 | | | |ring_2exp10_8vars_6ite_unsat.smt2 | 599.740s | 38.208MiB| timeout | 0 | | | |ring_2exp14_9vars_3ite_unsat.smt2 | 599.744s | 42.364MiB| timeout | 0 | | | |ring_2exp10_7vars_3ite_unsat.smt2 | 599.751s | 39.276MiB| timeout | 0 | | | |ring_2exp16_9vars_6ite_unsat.smt2 | 599.755s | 37.984MiB| timeout | 0 | | | |ring_2exp16_7vars_5ite_unsat.smt2 | 599.762s | 36.376MiB| timeout | 0 | | | |ring_2exp14_6vars_1ite_unsat.smt2 | 599.774s | 38.8MiB| timeout | 0 | | | |ring_2exp6_6vars_2ite_unsat.smt2 | 599.778s | 38.176MiB| timeout | 0 | | | |ring_2exp12_8vars_4ite_unsat.smt2 | 599.778s | 38.904MiB| timeout | 0 | | | |ring_2exp14_7vars_1ite_unsat.smt2 | 599.780s | 38.644MiB| timeout | 0 | | | |ring_2exp10_9vars_3ite_unsat.smt2 | 599.781s | 45.296MiB| timeout | 0 | | | |ring_2exp16_9vars_4ite_unsat.smt2 | 599.781s | 38.884MiB| timeout | 0 | | | |ring_2exp8_5vars_2ite_unsat.smt2 | 599.782s | 34.692MiB| timeout | 0 | | | |ring_2exp10_9vars_4ite_unsat.smt2 | 599.790s | 41.672MiB| timeout | 0 | | | |ring_2exp6_5vars_3ite_unsat.smt2 | 599.792s | 35.008MiB| timeout | 0 | | | |ring_2exp10_7vars_1ite_unsat.smt2 | 599.794s | 41.372MiB| timeout | 0 | | | |ring_2exp10_8vars_1ite_unsat.smt2 | 599.800s | 42.428MiB| timeout | 0 | | | |ring_2exp16_7vars_2ite_unsat.smt2 | 599.803s | 43.448MiB| timeout | 0 | | | |ring_2exp14_7vars_5ite_unsat.smt2 | 599.808s | 39.472MiB| timeout | 0 | | | |ring_2exp8_8vars_3ite_unsat.smt2 | 599.808s | 45.324MiB| timeout | 0 | | | |ring_2exp8_7vars_4ite_unsat.smt2 | 599.811s | 41.22MiB| timeout | 0 | | | |ring_2exp12_6vars_5ite_unsat.smt2 | 599.816s | 42.704MiB| timeout | 0 | | | |ring_2exp6_8vars_1ite_unsat.smt2 | 599.820s | 36.692MiB| timeout | 0 | | | |ring_2exp6_7vars_3ite_unsat.smt2 | 599.823s | 41.672MiB| timeout | 0 | | | |ring_2exp10_8vars_2ite_unsat.smt2 | 599.824s | 40.448MiB| timeout | 0 | | | |ring_2exp8_7vars_5ite_unsat.smt2 | 599.824s | 39.048MiB| timeout | 0 | | | |ring_2exp16_8vars_3ite_unsat.smt2 | 599.827s | 38.944MiB| timeout | 0 | | | |ring_2exp6_9vars_7ite_unsat.smt2 | 599.830s | 37.664MiB| timeout | 0 | | | |ring_2exp6_9vars_4ite_unsat.smt2 | 599.831s | 38.86MiB| timeout | 0 | | | |ring_2exp6_7vars_6ite_unsat.smt2 | 599.832s | 38.144MiB| timeout | 0 | | | |ring_2exp16_7vars_4ite_unsat.smt2 | 599.841s | 40.116MiB| timeout | 0 | | | |ring_2exp16_8vars_5ite_unsat.smt2 | 599.846s | 39.152MiB| timeout | 0 | | | |ring_2exp6_8vars_7ite_unsat.smt2 | 599.847s | 35.844MiB| timeout | 0 | | | |ring_2exp12_9vars_2ite_unsat.smt2 | 599.858s | 46.74MiB| timeout | 0 | | | |ring_2exp8_6vars_5ite_unsat.smt2 | 599.858s | 40.624MiB| timeout | 0 | | | |ring_2exp14_8vars_1ite_unsat.smt2 | 599.863s | 41.424MiB| timeout | 0 | | | |ring_2exp16_9vars_2ite_unsat.smt2 | 599.868s | 49.456MiB| timeout | 0 | | | |ring_2exp16_6vars_2ite_unsat.smt2 | 599.869s | 38.588MiB| timeout | 0 | | | |ring_2exp12_8vars_1ite_unsat.smt2 | 599.870s | 40.204MiB| timeout | 0 | | | |ring_2exp14_9vars_2ite_unsat.smt2 | 599.871s | 44.364MiB| timeout | 0 | | | |ring_2exp6_9vars_6ite_unsat.smt2 | 599.872s | 37.368MiB| timeout | 0 | | | |ring_2exp10_9vars_2ite_unsat.smt2 | 599.879s | 44.22MiB| timeout | 0 | | | |ring_2exp14_7vars_3ite_unsat.smt2 | 599.883s | 36.128MiB| timeout | 0 | | | |ring_2exp14_9vars_5ite_unsat.smt2 | 599.883s | 38.412MiB| timeout | 0 | | | |ring_2exp10_9vars_5ite_unsat.smt2 | 599.885s | 42.48MiB| timeout | 0 | | | |ring_2exp12_8vars_3ite_unsat.smt2 | 599.888s | 39.4MiB| timeout | 0 | | | |ring_2exp12_7vars_3ite_unsat.smt2 | 599.897s | 37.664MiB| timeout | 0 | | | |ring_2exp6_6vars_4ite_unsat.smt2 | 599.898s | 39.024MiB| timeout | 0 | | | |ring_2exp12_9vars_8ite_unsat.smt2 | 599.900s | 37.484MiB| timeout | 0 | | | |ring_2exp16_8vars_4ite_unsat.smt2 | 599.902s | 39.272MiB| timeout | 0 | | | |ring_2exp8_6vars_3ite_unsat.smt2 | 599.903s | 44.768MiB| timeout | 0 | | | |ring_2exp6_6vars_5ite_unsat.smt2 | 599.905s | 38.952MiB| timeout | 0 | | | |ring_2exp10_9vars_6ite_unsat.smt2 | 599.906s | 44.236MiB| timeout | 0 | | | |ring_2exp16_8vars_6ite_unsat.smt2 | 599.910s | 39.08MiB| timeout | 0 | | | |ring_2exp4_7vars_5ite_unsat.smt2 | 599.911s | 35.788MiB| timeout | 0 | | | |ring_2exp14_6vars_3ite_unsat.smt2 | 599.913s | 38.08MiB| timeout | 0 | | | |ring_2exp8_8vars_4ite_unsat.smt2 | 599.914s | 39.776MiB| timeout | 0 | | | |ring_2exp6_5vars_1ite_unsat.smt2 | 599.915s | 33.588MiB| timeout | 0 | | | |ring_2exp6_6vars_3ite_unsat.smt2 | 599.917s | 39.664MiB| timeout | 0 | | | |ring_2exp10_7vars_2ite_unsat.smt2 | 599.919s | 39.124MiB| timeout | 0 | | | |ring_2exp16_6vars_4ite_unsat.smt2 | 599.920s | 40.352MiB| timeout | 0 | | | |ring_2exp16_9vars_1ite_unsat.smt2 | 599.921s | 44.932MiB| timeout | 0 | | | |ring_2exp10_6vars_1ite_unsat.smt2 | 599.921s | 39.248MiB| timeout | 0 | | | |ring_2exp12_6vars_2ite_unsat.smt2 | 599.922s | 42.788MiB| timeout | 0 | | | |ring_2exp8_9vars_5ite_unsat.smt2 | 599.922s | 39.272MiB| timeout | 0 | | | |ring_2exp8_7vars_2ite_unsat.smt2 | 599.924s | 39.528MiB| timeout | 0 | | | |ring_2exp6_6vars_1ite_unsat.smt2 | 599.925s | 36.192MiB| timeout | 0 | | | |ring_2exp10_9vars_8ite_unsat.smt2 | 599.926s | 39.812MiB| timeout | 0 | | | |ring_2exp10_6vars_2ite_unsat.smt2 | 599.927s | 42.756MiB| timeout | 0 | | | |ring_2exp14_6vars_4ite_unsat.smt2 | 599.927s | 41.16MiB| timeout | 0 | | | |ring_2exp4_9vars_4ite_unsat.smt2 | 599.928s | 35.156MiB| timeout | 0 | | | |ring_2exp16_7vars_3ite_unsat.smt2 | 599.933s | 44.96MiB| timeout | 0 | | | |ring_2exp6_8vars_3ite_unsat.smt2 | 599.933s | 35.64MiB| timeout | 0 | | | |ring_2exp10_8vars_3ite_unsat.smt2 | 599.934s | 43.432MiB| timeout | 0 | | | |ring_2exp4_9vars_8ite_unsat.smt2 | 599.935s | 37.876MiB| timeout | 0 | | | |ring_2exp8_8vars_2ite_unsat.smt2 | 599.937s | 46.324MiB| timeout | 0 | | | |ring_2exp4_8vars_5ite_unsat.smt2 | 599.937s | 33.6MiB| timeout | 0 | | | |ring_2exp14_7vars_2ite_unsat.smt2 | 599.938s | 41.808MiB| timeout | 0 | | | |ring_2exp16_8vars_1ite_unsat.smt2 | 599.940s | 52.708MiB| timeout | 0 | | | |ring_2exp16_7vars_6ite_unsat.smt2 | 599.941s | 44.076MiB| timeout | 0 | | | |ring_2exp4_9vars_6ite_unsat.smt2 | 599.942s | 37.252MiB| timeout | 0 | | | |ring_2exp8_9vars_3ite_unsat.smt2 | 599.944s | 50.16MiB| timeout | 0 | | | |ring_2exp12_9vars_6ite_unsat.smt2 | 599.945s | 49.796MiB| timeout | 0 | | | |ring_2exp14_8vars_7ite_unsat.smt2 | 599.946s | 45.912MiB| timeout | 0 | | | |ring_2exp6_7vars_5ite_unsat.smt2 | 599.946s | 36.308MiB| timeout | 0 | | | |ring_2exp8_9vars_6ite_unsat.smt2 | 599.947s | 49.308MiB| timeout | 0 | | | |ring_2exp4_9vars_1ite_unsat.smt2 | 599.947s | 45.012MiB| timeout | 0 | | | |ring_2exp8_7vars_3ite_unsat.smt2 | 599.948s | 39.876MiB| timeout | 0 | | | |ring_2exp14_9vars_8ite_unsat.smt2 | 599.948s | 35.432MiB| timeout | 0 | | | |ring_2exp8_6vars_1ite_unsat.smt2 | 599.948s | 43.88MiB| timeout | 0 | | | |ring_2exp8_7vars_6ite_unsat.smt2 | 599.949s | 42.036MiB| timeout | 0 | | | |ring_2exp4_9vars_2ite_unsat.smt2 | 599.950s | 43.316MiB| timeout | 0 | | | |ring_2exp10_8vars_5ite_unsat.smt2 | 599.950s | 43.356MiB| timeout | 0 | | | |ring_2exp6_8vars_6ite_unsat.smt2 | 599.950s | 43.08MiB| timeout | 0 | | | |ring_2exp6_5vars_2ite_unsat.smt2 | 599.952s | 38.828MiB| timeout | 0 | | | |ring_2exp14_9vars_6ite_unsat.smt2 | 599.952s | 47.392MiB| timeout | 0 | | | |ring_2exp16_8vars_7ite_unsat.smt2 | 599.952s | 39.296MiB| timeout | 0 | | | |ring_2exp4_8vars_6ite_unsat.smt2 | 599.953s | 43.688MiB| timeout | 0 | | | |ring_2exp16_9vars_8ite_unsat.smt2 | 599.954s | 42.916MiB| timeout | 0 | | | |ring_2exp4_9vars_3ite_unsat.smt2 | 599.955s | 42.616MiB| timeout | 0 | | | |ring_2exp10_7vars_6ite_unsat.smt2 | 599.956s | 42.236MiB| timeout | 0 | | | |ring_2exp10_9vars_7ite_unsat.smt2 | 599.956s | 49.764MiB| timeout | 0 | | | |ring_2exp12_7vars_5ite_unsat.smt2 | 599.958s | 42.432MiB| timeout | 0 | | | |ring_2exp12_9vars_3ite_unsat.smt2 | 599.958s | 50.5MiB| timeout | 0 | | | |ring_2exp14_9vars_1ite_unsat.smt2 | 599.958s | 46.648MiB| timeout | 0 | | | |ring_2exp12_9vars_7ite_unsat.smt2 | 599.958s | 45.66MiB| timeout | 0 | | | |ring_2exp12_8vars_2ite_unsat.smt2 | 599.959s | 49.76MiB| timeout | 0 | | | |ring_2exp12_7vars_4ite_unsat.smt2 | 599.960s | 41.668MiB| timeout | 0 | | | |ring_2exp6_9vars_3ite_unsat.smt2 | 599.961s | 43.912MiB| timeout | 0 | | | |ring_2exp6_9vars_1ite_unsat.smt2 | 599.961s | 48.276MiB| timeout | 0 | | | |ring_2exp12_7vars_2ite_unsat.smt2 | 599.961s | 45.212MiB| timeout | 0 | | | |ring_2exp16_8vars_2ite_unsat.smt2 | 599.962s | 47.916MiB| timeout | 0 | | | |ring_2exp10_6vars_5ite_unsat.smt2 | 599.963s | 42.964MiB| timeout | 0 | | | |ring_2exp8_9vars_7ite_unsat.smt2 | 599.963s | 47.216MiB| timeout | 0 | | | |ring_2exp16_7vars_1ite_unsat.smt2 | 599.963s | 45.708MiB| timeout | 0 | | | |ring_2exp10_6vars_3ite_unsat.smt2 | 599.963s | 44.844MiB| timeout | 0 | | | |ring_2exp4_8vars_4ite_unsat.smt2 | 599.964s | 38.816MiB| timeout | 0 | | | |ring_2exp8_8vars_7ite_unsat.smt2 | 599.964s | 42.708MiB| timeout | 0 | | | |ring_2exp16_9vars_3ite_unsat.smt2 | 599.964s | 50.276MiB| timeout | 0 | | | |ring_2exp8_6vars_2ite_unsat.smt2 | 599.965s | 44.172MiB| timeout | 0 | | | |ring_2exp10_7vars_5ite_unsat.smt2 | 599.967s | 47.148MiB| timeout | 0 | | | |ring_2exp12_9vars_4ite_unsat.smt2 | 599.967s | 47.52MiB| timeout | 0 | | | |ring_2exp8_7vars_1ite_unsat.smt2 | 599.971s | 42.344MiB| timeout | 0 | | |