# . * SAT 0 * UNSAT 114 * TIMEOUT 180 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: rings_without_dio
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: dd211bade9ecb681c2714d6de997f4c91bdf7a2e
Z3 branch: 
Z3 options: "-T:600 -st lp.dio=false"
Z3 inputs: inputs/rings
Z3 commit message: filter out terms that are not solved
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |ring_2exp6_4vars_0ite_unsat.smt2 | 0.028s | 20.26MiB| unsat | 0 | | | |ring_2exp10_3vars_0ite_unsat.smt2 | 0.030s | 20.372MiB| unsat | 0 | | | |ring_2exp16_3vars_0ite_unsat.smt2 | 0.031s | 20.508MiB| unsat | 0 | | | |ring_2exp8_4vars_0ite_unsat.smt2 | 0.031s | 20.132MiB| unsat | 0 | | | |ring_2exp6_3vars_0ite_unsat.smt2 | 0.032s | 20.176MiB| unsat | 0 | | | |ring_2exp14_4vars_0ite_unsat.smt2 | 0.032s | 20.24MiB| unsat | 0 | | | |ring_2exp16_4vars_0ite_unsat.smt2 | 0.032s | 20.544MiB| unsat | 0 | | | |ring_2exp6_5vars_0ite_unsat.smt2 | 0.033s | 20.556MiB| unsat | 0 | | | |ring_2exp14_8vars_0ite_unsat.smt2 | 0.033s | 20.924MiB| unsat | 0 | | | |ring_2exp14_5vars_0ite_unsat.smt2 | 0.033s | 20.768MiB| unsat | 0 | | | |ring_2exp12_3vars_0ite_unsat.smt2 | 0.035s | 20.112MiB| unsat | 0 | | | |ring_2exp12_4vars_0ite_unsat.smt2 | 0.035s | 20.256MiB| unsat | 0 | | | |ring_2exp4_5vars_0ite_unsat.smt2 | 0.036s | 20.388MiB| unsat | 0 | | | |ring_2exp10_4vars_0ite_unsat.smt2 | 0.036s | 20.512MiB| unsat | 0 | | | |ring_2exp4_3vars_0ite_unsat.smt2 | 0.037s | 20.276MiB| unsat | 0 | | | |ring_2exp8_5vars_0ite_unsat.smt2 | 0.038s | 20.524MiB| unsat | 0 | | | |ring_2exp4_7vars_0ite_unsat.smt2 | 0.039s | 20.776MiB| unsat | 0 | | | |ring_2exp10_6vars_0ite_unsat.smt2 | 0.039s | 20.552MiB| unsat | 0 | | | |ring_2exp16_6vars_0ite_unsat.smt2 | 0.039s | 20.58MiB| unsat | 0 | | | |ring_2exp14_7vars_0ite_unsat.smt2 | 0.040s | 21.244MiB| unsat | 0 | | | |ring_2exp6_8vars_0ite_unsat.smt2 | 0.040s | 20.804MiB| unsat | 0 | | | |ring_2exp16_5vars_0ite_unsat.smt2 | 0.040s | 20.524MiB| unsat | 0 | | | |ring_2exp4_4vars_0ite_unsat.smt2 | 0.040s | 20.272MiB| unsat | 0 | | | |ring_2exp10_8vars_0ite_unsat.smt2 | 0.041s | 20.772MiB| unsat | 0 | | | |ring_2exp8_7vars_0ite_unsat.smt2 | 0.041s | 20.756MiB| unsat | 0 | | | |ring_2exp12_7vars_0ite_unsat.smt2 | 0.042s | 21.024MiB| unsat | 0 | | | |ring_2exp8_8vars_0ite_unsat.smt2 | 0.043s | 20.892MiB| unsat | 0 | | | |ring_2exp12_5vars_0ite_unsat.smt2 | 0.044s | 20.468MiB| unsat | 0 | | | |ring_2exp8_3vars_0ite_unsat.smt2 | 0.045s | 20.124MiB| unsat | 0 | | | |ring_2exp12_6vars_0ite_unsat.smt2 | 0.045s | 20.62MiB| unsat | 0 | | | |ring_2exp10_9vars_0ite_unsat.smt2 | 0.046s | 20.988MiB| unsat | 0 | | | |ring_2exp14_6vars_0ite_unsat.smt2 | 0.046s | 20.636MiB| unsat | 0 | | | |ring_2exp8_6vars_0ite_unsat.smt2 | 0.046s | 20.584MiB| unsat | 0 | | | |ring_2exp14_3vars_0ite_unsat.smt2 | 0.047s | 20.508MiB| unsat | 0 | | | |ring_2exp16_9vars_0ite_unsat.smt2 | 0.047s | 20.828MiB| unsat | 0 | | | |ring_2exp8_9vars_0ite_unsat.smt2 | 0.049s | 20.876MiB| unsat | 0 | | | |ring_2exp8_3vars_2ite_unsat.smt2 | 0.049s | 20.268MiB| unsat | 0 | | | |ring_2exp12_9vars_0ite_unsat.smt2 | 0.049s | 21.096MiB| unsat | 0 | | | |ring_2exp4_8vars_0ite_unsat.smt2 | 0.050s | 20.672MiB| unsat | 0 | | | |ring_2exp14_3vars_2ite_unsat.smt2 | 0.050s | 20.328MiB| unsat | 0 | | | |ring_2exp14_9vars_0ite_unsat.smt2 | 0.051s | 20.952MiB| unsat | 0 | | | |ring_2exp6_9vars_0ite_unsat.smt2 | 0.051s | 20.888MiB| unsat | 0 | | | |ring_2exp6_3vars_1ite_unsat.smt2 | 0.051s | 20.616MiB| unsat | 0 | | | |ring_2exp10_3vars_2ite_unsat.smt2 | 0.051s | 20.192MiB| unsat | 0 | | | |ring_2exp12_8vars_0ite_unsat.smt2 | 0.052s | 21.06MiB| unsat | 0 | | | |ring_2exp16_3vars_1ite_unsat.smt2 | 0.055s | 20.32MiB| unsat | 0 | | | |ring_2exp10_3vars_1ite_unsat.smt2 | 0.055s | 20.296MiB| unsat | 0 | | | |ring_2exp12_3vars_2ite_unsat.smt2 | 0.058s | 20.252MiB| unsat | 0 | | | |ring_2exp4_9vars_0ite_unsat.smt2 | 0.059s | 21.028MiB| unsat | 0 | | | |ring_2exp4_3vars_1ite_unsat.smt2 | 0.059s | 20.38MiB| unsat | 0 | | | |ring_2exp8_3vars_1ite_unsat.smt2 | 0.059s | 20.396MiB| unsat | 0 | | | |ring_2exp16_8vars_0ite_unsat.smt2 | 0.060s | 20.776MiB| unsat | 0 | | | |ring_2exp4_6vars_0ite_unsat.smt2 | 0.060s | 20.496MiB| unsat | 0 | | | |ring_2exp6_3vars_2ite_unsat.smt2 | 0.061s | 20.32MiB| unsat | 0 | | | |ring_2exp14_3vars_1ite_unsat.smt2 | 0.062s | 20.392MiB| unsat | 0 | | | |ring_2exp16_7vars_0ite_unsat.smt2 | 0.065s | 20.78MiB| unsat | 0 | | | |ring_2exp6_6vars_0ite_unsat.smt2 | 0.067s | 20.6MiB| unsat | 0 | | | |ring_2exp4_3vars_2ite_unsat.smt2 | 0.071s | 20.496MiB| unsat | 0 | | | |ring_2exp6_7vars_0ite_unsat.smt2 | 0.073s | 21.028MiB| unsat | 0 | | | |ring_2exp10_5vars_0ite_unsat.smt2 | 0.077s | 20.516MiB| unsat | 0 | | | |ring_2exp10_7vars_0ite_unsat.smt2 | 0.079s | 20.776MiB| unsat | 0 | | | |ring_2exp16_3vars_2ite_unsat.smt2 | 0.084s | 20.508MiB| unsat | 0 | | | |ring_2exp12_3vars_1ite_unsat.smt2 | 0.088s | 20.272MiB| unsat | 0 | | | |ring_2exp8_4vars_1ite_unsat.smt2 | 0.684s | 20.852MiB| unsat | 0 | | | |ring_2exp4_4vars_2ite_unsat.smt2 | 0.802s | 21.032MiB| unsat | 0 | | | |ring_2exp14_4vars_3ite_unsat.smt2 | 0.874s | 20.832MiB| unsat | 0 | | | |ring_2exp14_4vars_1ite_unsat.smt2 | 0.882s | 20.86MiB| unsat | 0 | | | |ring_2exp12_4vars_3ite_unsat.smt2 | 0.910s | 20.724MiB| unsat | 0 | | | |ring_2exp14_4vars_2ite_unsat.smt2 | 0.919s | 21.032MiB| unsat | 0 | | | |ring_2exp16_4vars_3ite_unsat.smt2 | 0.934s | 20.916MiB| unsat | 0 | | | |ring_2exp4_4vars_3ite_unsat.smt2 | 0.946s | 20.848MiB| unsat | 0 | | | |ring_2exp10_4vars_3ite_unsat.smt2 | 0.954s | 20.792MiB| unsat | 0 | | | |ring_2exp12_4vars_1ite_unsat.smt2 | 0.988s | 20.78MiB| unsat | 0 | | | |ring_2exp8_4vars_3ite_unsat.smt2 | 1.015s | 21.024MiB| unsat | 0 | | | |ring_2exp16_4vars_1ite_unsat.smt2 | 1.025s | 21.072MiB| unsat | 0 | | | |ring_2exp16_4vars_2ite_unsat.smt2 | 1.045s | 20.76MiB| unsat | 0 | | | |ring_2exp12_4vars_2ite_unsat.smt2 | 1.057s | 20.916MiB| unsat | 0 | | | |ring_2exp10_4vars_1ite_unsat.smt2 | 1.098s | 21.032MiB| unsat | 0 | | | |ring_2exp6_4vars_3ite_unsat.smt2 | 1.195s | 21.084MiB| unsat | 0 | | | |ring_2exp8_4vars_2ite_unsat.smt2 | 1.224s | 21.004MiB| unsat | 0 | | | |ring_2exp10_4vars_2ite_unsat.smt2 | 1.360s | 20.92MiB| unsat | 0 | | | |ring_2exp4_4vars_1ite_unsat.smt2 | 1.372s | 21.128MiB| unsat | 0 | | | |ring_2exp6_4vars_1ite_unsat.smt2 | 1.437s | 20.964MiB| unsat | 0 | | | |ring_2exp6_4vars_2ite_unsat.smt2 | 1.593s | 21.06MiB| unsat | 0 | | | |ring_2exp4_5vars_4ite_unsat.smt2 | 51.358s | 24.008MiB| unsat | 0 | | | |ring_2exp4_5vars_1ite_unsat.smt2 | 53.935s | 24.472MiB| unsat | 0 | | | |ring_2exp4_5vars_2ite_unsat.smt2 | 55.513s | 24.152MiB| unsat | 0 | | | |ring_2exp4_5vars_3ite_unsat.smt2 | 58.563s | 24.424MiB| unsat | 0 | | | |ring_2exp16_5vars_4ite_unsat.smt2 | 117.661s | 29.144MiB| unsat | 0 | | | |ring_2exp14_5vars_4ite_unsat.smt2 | 120.690s | 27.792MiB| unsat | 0 | | | |ring_2exp12_5vars_4ite_unsat.smt2 | 129.757s | 29.232MiB| unsat | 0 | | | |ring_2exp10_5vars_4ite_unsat.smt2 | 136.456s | 29.628MiB| unsat | 0 | | | |ring_2exp14_5vars_3ite_unsat.smt2 | 138.338s | 30.264MiB| unsat | 0 | | | |ring_2exp8_5vars_4ite_unsat.smt2 | 140.395s | 29.828MiB| unsat | 0 | | | |ring_2exp16_5vars_1ite_unsat.smt2 | 159.168s | 29.316MiB| unsat | 0 | | | |ring_2exp4_6vars_5ite_unsat.smt2 | 182.982s | 29.708MiB| unsat | 0 | | | |ring_2exp4_7vars_2ite_unsat.smt2 | 190.647s | 29.524MiB| unsat | 0 | | | |ring_2exp16_5vars_3ite_unsat.smt2 | 231.711s | 30.228MiB| unsat | 0 | | | |ring_2exp14_5vars_2ite_unsat.smt2 | 238.363s | 30.64MiB| unsat | 0 | | | |ring_2exp4_8vars_1ite_unsat.smt2 | 242.171s | 30.416MiB| unsat | 0 | | | |ring_2exp12_5vars_3ite_unsat.smt2 | 242.836s | 30.528MiB| unsat | 0 | | | |ring_2exp6_5vars_4ite_unsat.smt2 | 246.184s | 32.616MiB| unsat | 0 | | | |ring_2exp10_5vars_2ite_unsat.smt2 | 253.529s | 34.336MiB| unsat | 0 | | | |ring_2exp4_7vars_1ite_unsat.smt2 | 255.863s | 30.528MiB| unsat | 0 | | | |ring_2exp12_5vars_1ite_unsat.smt2 | 286.601s | 31.172MiB| unsat | 0 | | | |ring_2exp10_5vars_1ite_unsat.smt2 | 313.179s | 32.12MiB| unsat | 0 | | | |ring_2exp8_5vars_1ite_unsat.smt2 | 315.602s | 34.052MiB| unsat | 0 | | | |ring_2exp16_5vars_2ite_unsat.smt2 | 320.020s | 32.352MiB| unsat | 0 | | | |ring_2exp14_5vars_1ite_unsat.smt2 | 364.475s | 32.904MiB| unsat | 0 | | | |ring_2exp4_6vars_1ite_unsat.smt2 | 397.529s | 34.492MiB| unsat | 0 | | | |ring_2exp4_6vars_4ite_unsat.smt2 | 411.767s | 33.116MiB| unsat | 0 | | | |ring_2exp4_8vars_2ite_unsat.smt2 | 440.809s | 31.376MiB| unsat | 0 | | | |ring_2exp4_6vars_2ite_unsat.smt2 | 442.251s | 32.376MiB| unsat | 0 | | | |ring_2exp12_5vars_2ite_unsat.smt2 | 571.003s | 33.068MiB| unsat | 0 | | | |ring_2exp6_5vars_1ite_unsat.smt2 | 595.633s | 33.42MiB| timeout | 0 | | | |ring_2exp16_8vars_3ite_unsat.smt2 | 596.950s | 40.032MiB| timeout | 0 | | | |ring_2exp4_6vars_3ite_unsat.smt2 | 598.038s | 34.78MiB| timeout | 0 | | | |ring_2exp12_6vars_5ite_unsat.smt2 | 598.251s | 42.376MiB| timeout | 0 | | | |ring_2exp14_6vars_5ite_unsat.smt2 | 598.538s | 40.26MiB| timeout | 0 | | | |ring_2exp6_6vars_2ite_unsat.smt2 | 598.604s | 37.264MiB| timeout | 0 | | | |ring_2exp4_7vars_4ite_unsat.smt2 | 598.749s | 35.952MiB| timeout | 0 | | | |ring_2exp10_7vars_3ite_unsat.smt2 | 599.084s | 38.696MiB| timeout | 0 | | | |ring_2exp10_7vars_4ite_unsat.smt2 | 599.144s | 38.54MiB| timeout | 0 | | | |ring_2exp4_9vars_7ite_unsat.smt2 | 599.176s | 32.112MiB| timeout | 0 | | | |ring_2exp14_8vars_4ite_unsat.smt2 | 599.207s | 36.316MiB| timeout | 0 | | | |ring_2exp10_7vars_2ite_unsat.smt2 | 599.239s | 39.024MiB| timeout | 0 | | | |ring_2exp10_6vars_4ite_unsat.smt2 | 599.273s | 38.268MiB| timeout | 0 | | | |ring_2exp8_8vars_1ite_unsat.smt2 | 599.276s | 40.836MiB| timeout | 0 | | | |ring_2exp10_9vars_4ite_unsat.smt2 | 599.281s | 41.116MiB| timeout | 0 | | | |ring_2exp16_9vars_1ite_unsat.smt2 | 599.296s | 43.784MiB| timeout | 0 | | | |ring_2exp8_5vars_3ite_unsat.smt2 | 599.373s | 33.892MiB| timeout | 0 | | | |ring_2exp14_9vars_2ite_unsat.smt2 | 599.411s | 43.956MiB| timeout | 0 | | | |ring_2exp16_9vars_5ite_unsat.smt2 | 599.416s | 39.3MiB| timeout | 0 | | | |ring_2exp12_8vars_7ite_unsat.smt2 | 599.426s | 36.948MiB| timeout | 0 | | | |ring_2exp10_7vars_1ite_unsat.smt2 | 599.496s | 41.28MiB| timeout | 0 | | | |ring_2exp10_8vars_6ite_unsat.smt2 | 599.501s | 38.312MiB| timeout | 0 | | | |ring_2exp8_9vars_4ite_unsat.smt2 | 599.517s | 39.364MiB| timeout | 0 | | | |ring_2exp14_7vars_5ite_unsat.smt2 | 599.541s | 39.34MiB| timeout | 0 | | | |ring_2exp12_9vars_2ite_unsat.smt2 | 599.570s | 45.272MiB| timeout | 0 | | | |ring_2exp8_8vars_5ite_unsat.smt2 | 599.584s | 38.776MiB| timeout | 0 | | | |ring_2exp6_6vars_5ite_unsat.smt2 | 599.601s | 38.288MiB| timeout | 0 | | | |ring_2exp10_9vars_3ite_unsat.smt2 | 599.603s | 44.324MiB| timeout | 0 | | | |ring_2exp10_6vars_1ite_unsat.smt2 | 599.604s | 39.108MiB| timeout | 0 | | | |ring_2exp16_9vars_4ite_unsat.smt2 | 599.623s | 38.852MiB| timeout | 0 | | | |ring_2exp6_7vars_6ite_unsat.smt2 | 599.626s | 36.852MiB| timeout | 0 | | | |ring_2exp6_8vars_1ite_unsat.smt2 | 599.644s | 36.42MiB| timeout | 0 | | | |ring_2exp10_8vars_7ite_unsat.smt2 | 599.648s | 37.248MiB| timeout | 0 | | | |ring_2exp14_7vars_1ite_unsat.smt2 | 599.661s | 38.436MiB| timeout | 0 | | | |ring_2exp8_6vars_5ite_unsat.smt2 | 599.667s | 39.92MiB| timeout | 0 | | | |ring_2exp14_8vars_3ite_unsat.smt2 | 599.669s | 40.748MiB| timeout | 0 | | | |ring_2exp16_9vars_7ite_unsat.smt2 | 599.673s | 36.128MiB| timeout | 0 | | | |ring_2exp6_9vars_2ite_unsat.smt2 | 599.684s | 41.776MiB| timeout | 0 | | | |ring_2exp6_7vars_4ite_unsat.smt2 | 599.690s | 35.628MiB| timeout | 0 | | | |ring_2exp12_6vars_4ite_unsat.smt2 | 599.697s | 35.692MiB| timeout | 0 | | | |ring_2exp12_7vars_1ite_unsat.smt2 | 599.712s | 40.352MiB| timeout | 0 | | | |ring_2exp6_8vars_3ite_unsat.smt2 | 599.712s | 35.272MiB| timeout | 0 | | | |ring_2exp6_8vars_4ite_unsat.smt2 | 599.723s | 37.092MiB| timeout | 0 | | | |ring_2exp10_9vars_6ite_unsat.smt2 | 599.727s | 43.088MiB| timeout | 0 | | | |ring_2exp8_9vars_8ite_unsat.smt2 | 599.728s | 38.428MiB| timeout | 0 | | | |ring_2exp10_8vars_4ite_unsat.smt2 | 599.729s | 41.408MiB| timeout | 0 | | | |ring_2exp14_9vars_8ite_unsat.smt2 | 599.738s | 36.144MiB| timeout | 0 | | | |ring_2exp8_7vars_5ite_unsat.smt2 | 599.739s | 38.688MiB| timeout | 0 | | | |ring_2exp14_7vars_3ite_unsat.smt2 | 599.741s | 36.096MiB| timeout | 0 | | | |ring_2exp6_8vars_2ite_unsat.smt2 | 599.751s | 38.156MiB| timeout | 0 | | | |ring_2exp12_8vars_4ite_unsat.smt2 | 599.754s | 38.828MiB| timeout | 0 | | | |ring_2exp10_9vars_8ite_unsat.smt2 | 599.755s | 40.54MiB| timeout | 0 | | | |ring_2exp16_8vars_5ite_unsat.smt2 | 599.759s | 38.32MiB| timeout | 0 | | | |ring_2exp6_8vars_7ite_unsat.smt2 | 599.763s | 35.644MiB| timeout | 0 | | | |ring_2exp14_6vars_2ite_unsat.smt2 | 599.765s | 37.712MiB| timeout | 0 | | | |ring_2exp6_6vars_4ite_unsat.smt2 | 599.766s | 38.476MiB| timeout | 0 | | | |ring_2exp6_7vars_1ite_unsat.smt2 | 599.767s | 36.064MiB| timeout | 0 | | | |ring_2exp6_9vars_7ite_unsat.smt2 | 599.768s | 39.076MiB| timeout | 0 | | | |ring_2exp14_8vars_2ite_unsat.smt2 | 599.769s | 40.576MiB| timeout | 0 | | | |ring_2exp8_8vars_3ite_unsat.smt2 | 599.770s | 45.044MiB| timeout | 0 | | | |ring_2exp10_9vars_5ite_unsat.smt2 | 599.774s | 40.46MiB| timeout | 0 | | | |ring_2exp14_8vars_1ite_unsat.smt2 | 599.778s | 41.232MiB| timeout | 0 | | | |ring_2exp6_9vars_5ite_unsat.smt2 | 599.779s | 35.676MiB| timeout | 0 | | | |ring_2exp12_6vars_2ite_unsat.smt2 | 599.783s | 42.72MiB| timeout | 0 | | | |ring_2exp16_6vars_3ite_unsat.smt2 | 599.784s | 37.7MiB| timeout | 0 | | | |ring_2exp6_7vars_2ite_unsat.smt2 | 599.797s | 37.856MiB| timeout | 0 | | | |ring_2exp4_7vars_6ite_unsat.smt2 | 599.797s | 39.184MiB| timeout | 0 | | | |ring_2exp12_7vars_3ite_unsat.smt2 | 599.803s | 37.432MiB| timeout | 0 | | | |ring_2exp4_7vars_3ite_unsat.smt2 | 599.808s | 33.548MiB| timeout | 0 | | | |ring_2exp10_8vars_1ite_unsat.smt2 | 599.809s | 41.568MiB| timeout | 0 | | | |ring_2exp14_6vars_3ite_unsat.smt2 | 599.814s | 37.656MiB| timeout | 0 | | | |ring_2exp6_9vars_6ite_unsat.smt2 | 599.817s | 37.548MiB| timeout | 0 | | | |ring_2exp12_9vars_5ite_unsat.smt2 | 599.818s | 39.096MiB| timeout | 0 | | | |ring_2exp14_6vars_1ite_unsat.smt2 | 599.819s | 38.372MiB| timeout | 0 | | | |ring_2exp16_6vars_4ite_unsat.smt2 | 599.825s | 40.22MiB| timeout | 0 | | | |ring_2exp8_7vars_2ite_unsat.smt2 | 599.827s | 38.808MiB| timeout | 0 | | | |ring_2exp6_6vars_1ite_unsat.smt2 | 599.827s | 35.944MiB| timeout | 0 | | | |ring_2exp14_9vars_4ite_unsat.smt2 | 599.829s | 40.024MiB| timeout | 0 | | | |ring_2exp8_5vars_2ite_unsat.smt2 | 599.832s | 34.824MiB| timeout | 0 | | | |ring_2exp12_7vars_6ite_unsat.smt2 | 599.832s | 35.332MiB| timeout | 0 | | | |ring_2exp4_9vars_4ite_unsat.smt2 | 599.835s | 32.74MiB| timeout | 0 | | | |ring_2exp12_8vars_1ite_unsat.smt2 | 599.838s | 39.636MiB| timeout | 0 | | | |ring_2exp16_7vars_5ite_unsat.smt2 | 599.840s | 36.2MiB| timeout | 0 | | | |ring_2exp16_6vars_2ite_unsat.smt2 | 599.841s | 38.336MiB| timeout | 0 | | | |ring_2exp4_7vars_5ite_unsat.smt2 | 599.843s | 35.656MiB| timeout | 0 | | | |ring_2exp14_7vars_4ite_unsat.smt2 | 599.844s | 38.212MiB| timeout | 0 | | | |ring_2exp4_9vars_5ite_unsat.smt2 | 599.853s | 33.0MiB| timeout | 0 | | | |ring_2exp14_8vars_5ite_unsat.smt2 | 599.854s | 37.336MiB| timeout | 0 | | | |ring_2exp6_8vars_5ite_unsat.smt2 | 599.857s | 36.992MiB| timeout | 0 | | | |ring_2exp4_8vars_4ite_unsat.smt2 | 599.858s | 34.72MiB| timeout | 0 | | | |ring_2exp6_5vars_3ite_unsat.smt2 | 599.858s | 35.128MiB| timeout | 0 | | | |ring_2exp8_7vars_4ite_unsat.smt2 | 599.867s | 40.148MiB| timeout | 0 | | | |ring_2exp16_7vars_4ite_unsat.smt2 | 599.873s | 39.548MiB| timeout | 0 | | | |ring_2exp12_9vars_1ite_unsat.smt2 | 599.875s | 46.528MiB| timeout | 0 | | | |ring_2exp6_6vars_3ite_unsat.smt2 | 599.876s | 39.056MiB| timeout | 0 | | | |ring_2exp16_7vars_2ite_unsat.smt2 | 599.876s | 42.372MiB| timeout | 0 | | | |ring_2exp12_6vars_1ite_unsat.smt2 | 599.876s | 37.204MiB| timeout | 0 | | | |ring_2exp8_6vars_3ite_unsat.smt2 | 599.878s | 44.128MiB| timeout | 0 | | | |ring_2exp4_8vars_7ite_unsat.smt2 | 599.879s | 30.616MiB| timeout | 0 | | | |ring_2exp14_9vars_7ite_unsat.smt2 | 599.879s | 43.828MiB| timeout | 0 | | | |ring_2exp8_6vars_4ite_unsat.smt2 | 599.885s | 38.264MiB| timeout | 0 | | | |ring_2exp8_9vars_1ite_unsat.smt2 | 599.886s | 43.972MiB| timeout | 0 | | | |ring_2exp12_6vars_3ite_unsat.smt2 | 599.888s | 40.548MiB| timeout | 0 | | | |ring_2exp16_7vars_3ite_unsat.smt2 | 599.894s | 44.66MiB| timeout | 0 | | | |ring_2exp8_8vars_6ite_unsat.smt2 | 599.896s | 39.224MiB| timeout | 0 | | | |ring_2exp12_8vars_5ite_unsat.smt2 | 599.898s | 39.124MiB| timeout | 0 | | | |ring_2exp6_7vars_3ite_unsat.smt2 | 599.898s | 40.788MiB| timeout | 0 | | | |ring_2exp14_9vars_3ite_unsat.smt2 | 599.899s | 42.148MiB| timeout | 0 | | | |ring_2exp16_6vars_5ite_unsat.smt2 | 599.902s | 43.08MiB| timeout | 0 | | | |ring_2exp10_5vars_3ite_unsat.smt2 | 599.902s | 34.576MiB| timeout | 0 | | | |ring_2exp16_9vars_6ite_unsat.smt2 | 599.904s | 37.044MiB| timeout | 0 | | | |ring_2exp10_8vars_2ite_unsat.smt2 | 599.905s | 41.576MiB| timeout | 0 | | | |ring_2exp14_6vars_4ite_unsat.smt2 | 599.905s | 40.116MiB| timeout | 0 | | | |ring_2exp6_9vars_8ite_unsat.smt2 | 599.907s | 34.864MiB| timeout | 0 | | | |ring_2exp16_8vars_1ite_unsat.smt2 | 599.907s | 50.536MiB| timeout | 0 | | | |ring_2exp12_8vars_3ite_unsat.smt2 | 599.909s | 39.26MiB| timeout | 0 | | | |ring_2exp16_9vars_2ite_unsat.smt2 | 599.909s | 47.868MiB| timeout | 0 | | | |ring_2exp6_5vars_2ite_unsat.smt2 | 599.910s | 37.728MiB| timeout | 0 | | | |ring_2exp14_8vars_6ite_unsat.smt2 | 599.911s | 37.432MiB| timeout | 0 | | | |ring_2exp6_7vars_5ite_unsat.smt2 | 599.911s | 35.992MiB| timeout | 0 | | | |ring_2exp10_9vars_2ite_unsat.smt2 | 599.911s | 45.608MiB| timeout | 0 | | | |ring_2exp12_8vars_6ite_unsat.smt2 | 599.913s | 37.528MiB| timeout | 0 | | | |ring_2exp8_9vars_2ite_unsat.smt2 | 599.913s | 44.788MiB| timeout | 0 | | | |ring_2exp4_8vars_5ite_unsat.smt2 | 599.914s | 33.8MiB| timeout | 0 | | | |ring_2exp16_8vars_4ite_unsat.smt2 | 599.915s | 41.108MiB| timeout | 0 | | | |ring_2exp14_9vars_1ite_unsat.smt2 | 599.919s | 47.232MiB| timeout | 0 | | | |ring_2exp14_7vars_6ite_unsat.smt2 | 599.919s | 38.492MiB| timeout | 0 | | | |ring_2exp8_9vars_6ite_unsat.smt2 | 599.921s | 48.068MiB| timeout | 0 | | | |ring_2exp12_9vars_8ite_unsat.smt2 | 599.921s | 35.888MiB| timeout | 0 | | | |ring_2exp16_9vars_3ite_unsat.smt2 | 599.921s | 47.064MiB| timeout | 0 | | | |ring_2exp14_9vars_5ite_unsat.smt2 | 599.921s | 38.356MiB| timeout | 0 | | | |ring_2exp10_6vars_2ite_unsat.smt2 | 599.922s | 42.28MiB| timeout | 0 | | | |ring_2exp8_6vars_1ite_unsat.smt2 | 599.922s | 42.72MiB| timeout | 0 | | | |ring_2exp8_8vars_4ite_unsat.smt2 | 599.922s | 39.14MiB| timeout | 0 | | | |ring_2exp4_9vars_1ite_unsat.smt2 | 599.922s | 43.168MiB| timeout | 0 | | | |ring_2exp8_9vars_7ite_unsat.smt2 | 599.923s | 47.2MiB| timeout | 0 | | | |ring_2exp16_6vars_1ite_unsat.smt2 | 599.923s | 34.988MiB| timeout | 0 | | | |ring_2exp10_9vars_1ite_unsat.smt2 | 599.924s | 41.86MiB| timeout | 0 | | | |ring_2exp8_7vars_1ite_unsat.smt2 | 599.924s | 41.168MiB| timeout | 0 | | | |ring_2exp4_8vars_3ite_unsat.smt2 | 599.925s | 30.64MiB| timeout | 0 | | | |ring_2exp12_9vars_4ite_unsat.smt2 | 599.925s | 45.268MiB| timeout | 0 | | | |ring_2exp12_7vars_5ite_unsat.smt2 | 599.926s | 40.132MiB| timeout | 0 | | | |ring_2exp14_8vars_7ite_unsat.smt2 | 599.927s | 44.092MiB| timeout | 0 | | | |ring_2exp10_7vars_5ite_unsat.smt2 | 599.927s | 46.156MiB| timeout | 0 | | | |ring_2exp6_9vars_4ite_unsat.smt2 | 599.927s | 37.32MiB| timeout | 0 | | | |ring_2exp8_7vars_3ite_unsat.smt2 | 599.928s | 38.988MiB| timeout | 0 | | | |ring_2exp8_8vars_7ite_unsat.smt2 | 599.929s | 41.144MiB| timeout | 0 | | | |ring_2exp4_9vars_3ite_unsat.smt2 | 599.929s | 42.932MiB| timeout | 0 | | | |ring_2exp10_6vars_5ite_unsat.smt2 | 599.930s | 43.04MiB| timeout | 0 | | | |ring_2exp10_9vars_7ite_unsat.smt2 | 599.931s | 48.372MiB| timeout | 0 | | | |ring_2exp12_8vars_2ite_unsat.smt2 | 599.932s | 48.72MiB| timeout | 0 | | | |ring_2exp6_8vars_6ite_unsat.smt2 | 599.933s | 42.588MiB| timeout | 0 | | | |ring_2exp16_8vars_2ite_unsat.smt2 | 599.934s | 46.084MiB| timeout | 0 | | | |ring_2exp8_7vars_6ite_unsat.smt2 | 599.934s | 41.812MiB| timeout | 0 | | | |ring_2exp4_8vars_6ite_unsat.smt2 | 599.934s | 43.112MiB| timeout | 0 | | | |ring_2exp14_7vars_2ite_unsat.smt2 | 599.934s | 41.736MiB| timeout | 0 | | | |ring_2exp10_7vars_6ite_unsat.smt2 | 599.934s | 41.528MiB| timeout | 0 | | | |ring_2exp10_8vars_3ite_unsat.smt2 | 599.935s | 41.228MiB| timeout | 0 | | | |ring_2exp10_8vars_5ite_unsat.smt2 | 599.937s | 41.728MiB| timeout | 0 | | | |ring_2exp6_9vars_3ite_unsat.smt2 | 599.938s | 42.376MiB| timeout | 0 | | | |ring_2exp8_9vars_3ite_unsat.smt2 | 599.939s | 50.092MiB| timeout | 0 | | | |ring_2exp4_9vars_8ite_unsat.smt2 | 599.940s | 37.792MiB| timeout | 0 | | | |ring_2exp8_9vars_5ite_unsat.smt2 | 599.940s | 38.64MiB| timeout | 0 | | | |ring_2exp12_9vars_7ite_unsat.smt2 | 599.940s | 45.116MiB| timeout | 0 | | | |ring_2exp4_9vars_6ite_unsat.smt2 | 599.942s | 37.896MiB| timeout | 0 | | | |ring_2exp4_9vars_2ite_unsat.smt2 | 599.943s | 41.964MiB| timeout | 0 | | | |ring_2exp6_9vars_1ite_unsat.smt2 | 599.943s | 47.7MiB| timeout | 0 | | | |ring_2exp12_7vars_2ite_unsat.smt2 | 599.943s | 44.552MiB| timeout | 0 | | | |ring_2exp14_9vars_6ite_unsat.smt2 | 599.943s | 46.884MiB| timeout | 0 | | | |ring_2exp12_9vars_6ite_unsat.smt2 | 599.944s | 49.244MiB| timeout | 0 | | | |ring_2exp16_7vars_6ite_unsat.smt2 | 599.944s | 43.84MiB| timeout | 0 | | | |ring_2exp16_7vars_1ite_unsat.smt2 | 599.944s | 45.508MiB| timeout | 0 | | | |ring_2exp12_9vars_3ite_unsat.smt2 | 599.945s | 50.712MiB| timeout | 0 | | | |ring_2exp10_6vars_3ite_unsat.smt2 | 599.945s | 44.388MiB| timeout | 0 | | | |ring_2exp8_6vars_2ite_unsat.smt2 | 599.946s | 44.968MiB| timeout | 0 | | | |ring_2exp8_8vars_2ite_unsat.smt2 | 599.946s | 46.044MiB| timeout | 0 | | | |ring_2exp12_7vars_4ite_unsat.smt2 | 599.946s | 41.82MiB| timeout | 0 | | | |ring_2exp16_8vars_7ite_unsat.smt2 | 599.947s | 37.664MiB| timeout | 0 | | | |ring_2exp16_9vars_8ite_unsat.smt2 | 599.948s | 42.196MiB| timeout | 0 | | | |ring_2exp16_8vars_6ite_unsat.smt2 | 599.957s | 38.12MiB| timeout | 0 | | |