# . * SAT 0 * UNSAT 283 * TIMEOUT 11 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: rings_with_dio
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: dd211bade9ecb681c2714d6de997f4c91bdf7a2e
Z3 branch: 
Z3 options: "-T:600 -st"
Z3 inputs: inputs/rings
Z3 commit message: filter out terms that are not solved
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |ring_2exp8_4vars_0ite_unsat.smt2 | 0.030s | 20.2MiB| unsat | 0 | | | |ring_2exp4_5vars_0ite_unsat.smt2 | 0.031s | 20.536MiB| unsat | 0 | | | |ring_2exp8_3vars_0ite_unsat.smt2 | 0.031s | 20.352MiB| unsat | 0 | | | |ring_2exp4_3vars_0ite_unsat.smt2 | 0.031s | 20.168MiB| unsat | 0 | | | |ring_2exp12_4vars_0ite_unsat.smt2 | 0.031s | 20.208MiB| unsat | 0 | | | |ring_2exp4_4vars_0ite_unsat.smt2 | 0.032s | 20.216MiB| unsat | 0 | | | |ring_2exp10_4vars_0ite_unsat.smt2 | 0.032s | 20.384MiB| unsat | 0 | | | |ring_2exp16_3vars_0ite_unsat.smt2 | 0.033s | 20.072MiB| unsat | 0 | | | |ring_2exp12_3vars_0ite_unsat.smt2 | 0.033s | 20.24MiB| unsat | 0 | | | |ring_2exp16_4vars_0ite_unsat.smt2 | 0.033s | 20.164MiB| unsat | 0 | | | |ring_2exp8_5vars_0ite_unsat.smt2 | 0.034s | 20.372MiB| unsat | 0 | | | |ring_2exp10_3vars_0ite_unsat.smt2 | 0.035s | 20.116MiB| unsat | 0 | | | |ring_2exp6_4vars_0ite_unsat.smt2 | 0.035s | 20.376MiB| unsat | 0 | | | |ring_2exp6_3vars_0ite_unsat.smt2 | 0.036s | 20.524MiB| unsat | 0 | | | |ring_2exp16_5vars_0ite_unsat.smt2 | 0.036s | 20.56MiB| unsat | 0 | | | |ring_2exp14_6vars_0ite_unsat.smt2 | 0.036s | 20.468MiB| unsat | 0 | | | |ring_2exp8_6vars_0ite_unsat.smt2 | 0.036s | 20.464MiB| unsat | 0 | | | |ring_2exp12_6vars_0ite_unsat.smt2 | 0.037s | 20.456MiB| unsat | 0 | | | |ring_2exp16_6vars_0ite_unsat.smt2 | 0.037s | 20.516MiB| unsat | 0 | | | |ring_2exp14_4vars_0ite_unsat.smt2 | 0.038s | 20.36MiB| unsat | 0 | | | |ring_2exp6_8vars_0ite_unsat.smt2 | 0.039s | 20.796MiB| unsat | 0 | | | |ring_2exp14_3vars_1ite_unsat.smt2 | 0.039s | 20.356MiB| unsat | 0 | | | |ring_2exp4_8vars_0ite_unsat.smt2 | 0.042s | 20.844MiB| unsat | 0 | | | |ring_2exp6_9vars_0ite_unsat.smt2 | 0.042s | 20.76MiB| unsat | 0 | | | |ring_2exp8_9vars_0ite_unsat.smt2 | 0.042s | 20.692MiB| unsat | 0 | | | |ring_2exp10_6vars_0ite_unsat.smt2 | 0.042s | 20.768MiB| unsat | 0 | | | |ring_2exp14_7vars_0ite_unsat.smt2 | 0.043s | 20.632MiB| unsat | 0 | | | |ring_2exp14_8vars_0ite_unsat.smt2 | 0.044s | 20.832MiB| unsat | 0 | | | |ring_2exp10_8vars_0ite_unsat.smt2 | 0.045s | 20.768MiB| unsat | 0 | | | |ring_2exp16_8vars_0ite_unsat.smt2 | 0.045s | 20.924MiB| unsat | 0 | | | |ring_2exp16_3vars_1ite_unsat.smt2 | 0.046s | 20.272MiB| unsat | 0 | | | |ring_2exp12_5vars_0ite_unsat.smt2 | 0.046s | 20.632MiB| unsat | 0 | | | |ring_2exp8_8vars_0ite_unsat.smt2 | 0.046s | 20.764MiB| unsat | 0 | | | |ring_2exp16_3vars_2ite_unsat.smt2 | 0.047s | 20.776MiB| unsat | 0 | | | |ring_2exp8_3vars_1ite_unsat.smt2 | 0.047s | 20.124MiB| unsat | 0 | | | |ring_2exp4_4vars_1ite_unsat.smt2 | 0.047s | 20.736MiB| unsat | 0 | | | |ring_2exp14_3vars_0ite_unsat.smt2 | 0.049s | 20.208MiB| unsat | 0 | | | |ring_2exp4_7vars_0ite_unsat.smt2 | 0.049s | 20.78MiB| unsat | 0 | | | |ring_2exp8_3vars_2ite_unsat.smt2 | 0.049s | 20.516MiB| unsat | 0 | | | |ring_2exp12_8vars_0ite_unsat.smt2 | 0.049s | 20.804MiB| unsat | 0 | | | |ring_2exp10_9vars_0ite_unsat.smt2 | 0.049s | 20.992MiB| unsat | 0 | | | |ring_2exp12_3vars_2ite_unsat.smt2 | 0.049s | 20.32MiB| unsat | 0 | | | |ring_2exp8_7vars_0ite_unsat.smt2 | 0.050s | 20.728MiB| unsat | 0 | | | |ring_2exp12_9vars_0ite_unsat.smt2 | 0.050s | 21.04MiB| unsat | 0 | | | |ring_2exp14_3vars_2ite_unsat.smt2 | 0.050s | 20.184MiB| unsat | 0 | | | |ring_2exp4_3vars_1ite_unsat.smt2 | 0.051s | 20.364MiB| unsat | 0 | | | |ring_2exp10_3vars_1ite_unsat.smt2 | 0.051s | 20.248MiB| unsat | 0 | | | |ring_2exp6_3vars_2ite_unsat.smt2 | 0.052s | 20.316MiB| unsat | 0 | | | |ring_2exp16_9vars_0ite_unsat.smt2 | 0.053s | 20.892MiB| unsat | 0 | | | |ring_2exp12_7vars_0ite_unsat.smt2 | 0.054s | 20.868MiB| unsat | 0 | | | |ring_2exp14_5vars_0ite_unsat.smt2 | 0.054s | 20.504MiB| unsat | 0 | | | |ring_2exp14_9vars_0ite_unsat.smt2 | 0.057s | 20.98MiB| unsat | 0 | | | |ring_2exp6_3vars_1ite_unsat.smt2 | 0.057s | 20.552MiB| unsat | 0 | | | |ring_2exp16_7vars_0ite_unsat.smt2 | 0.061s | 20.892MiB| unsat | 0 | | | |ring_2exp10_3vars_2ite_unsat.smt2 | 0.061s | 20.48MiB| unsat | 0 | | | |ring_2exp14_4vars_1ite_unsat.smt2 | 0.065s | 20.468MiB| unsat | 0 | | | |ring_2exp4_6vars_0ite_unsat.smt2 | 0.067s | 20.496MiB| unsat | 0 | | | |ring_2exp6_4vars_1ite_unsat.smt2 | 0.069s | 20.72MiB| unsat | 0 | | | |ring_2exp6_5vars_0ite_unsat.smt2 | 0.072s | 20.456MiB| unsat | 0 | | | |ring_2exp10_4vars_1ite_unsat.smt2 | 0.073s | 20.524MiB| unsat | 0 | | | |ring_2exp6_5vars_1ite_unsat.smt2 | 0.075s | 20.576MiB| unsat | 0 | | | |ring_2exp16_4vars_1ite_unsat.smt2 | 0.075s | 20.488MiB| unsat | 0 | | | |ring_2exp8_4vars_1ite_unsat.smt2 | 0.076s | 20.536MiB| unsat | 0 | | | |ring_2exp6_7vars_0ite_unsat.smt2 | 0.078s | 20.788MiB| unsat | 0 | | | |ring_2exp12_3vars_1ite_unsat.smt2 | 0.081s | 20.512MiB| unsat | 0 | | | |ring_2exp6_6vars_0ite_unsat.smt2 | 0.082s | 20.5MiB| unsat | 0 | | | |ring_2exp12_5vars_1ite_unsat.smt2 | 0.083s | 20.64MiB| unsat | 0 | | | |ring_2exp4_4vars_2ite_unsat.smt2 | 0.084s | 20.536MiB| unsat | 0 | | | |ring_2exp6_4vars_2ite_unsat.smt2 | 0.084s | 20.56MiB| unsat | 0 | | | |ring_2exp10_5vars_0ite_unsat.smt2 | 0.084s | 20.48MiB| unsat | 0 | | | |ring_2exp12_4vars_1ite_unsat.smt2 | 0.085s | 20.392MiB| unsat | 0 | | | |ring_2exp4_9vars_0ite_unsat.smt2 | 0.086s | 20.776MiB| unsat | 0 | | | |ring_2exp4_3vars_2ite_unsat.smt2 | 0.088s | 20.368MiB| unsat | 0 | | | |ring_2exp4_5vars_1ite_unsat.smt2 | 0.090s | 20.832MiB| unsat | 0 | | | |ring_2exp10_7vars_0ite_unsat.smt2 | 0.090s | 21.024MiB| unsat | 0 | | | |ring_2exp14_4vars_2ite_unsat.smt2 | 0.091s | 20.476MiB| unsat | 0 | | | |ring_2exp10_4vars_2ite_unsat.smt2 | 0.094s | 20.52MiB| unsat | 0 | | | |ring_2exp8_5vars_1ite_unsat.smt2 | 0.099s | 20.744MiB| unsat | 0 | | | |ring_2exp12_4vars_2ite_unsat.smt2 | 0.104s | 20.52MiB| unsat | 0 | | | |ring_2exp8_4vars_2ite_unsat.smt2 | 0.106s | 20.588MiB| unsat | 0 | | | |ring_2exp10_5vars_1ite_unsat.smt2 | 0.108s | 20.624MiB| unsat | 0 | | | |ring_2exp14_5vars_1ite_unsat.smt2 | 0.109s | 20.728MiB| unsat | 0 | | | |ring_2exp16_4vars_3ite_unsat.smt2 | 0.112s | 20.48MiB| unsat | 0 | | | |ring_2exp16_4vars_2ite_unsat.smt2 | 0.115s | 20.456MiB| unsat | 0 | | | |ring_2exp8_5vars_2ite_unsat.smt2 | 0.115s | 20.78MiB| unsat | 0 | | | |ring_2exp4_5vars_2ite_unsat.smt2 | 0.116s | 20.808MiB| unsat | 0 | | | |ring_2exp6_8vars_1ite_unsat.smt2 | 0.117s | 21.128MiB| unsat | 0 | | | |ring_2exp16_5vars_1ite_unsat.smt2 | 0.117s | 20.52MiB| unsat | 0 | | | |ring_2exp14_4vars_3ite_unsat.smt2 | 0.118s | 20.768MiB| unsat | 0 | | | |ring_2exp10_5vars_2ite_unsat.smt2 | 0.119s | 20.824MiB| unsat | 0 | | | |ring_2exp4_5vars_3ite_unsat.smt2 | 0.123s | 20.848MiB| unsat | 0 | | | |ring_2exp12_7vars_1ite_unsat.smt2 | 0.125s | 21.004MiB| unsat | 0 | | | |ring_2exp14_8vars_1ite_unsat.smt2 | 0.127s | 21.392MiB| unsat | 0 | | | |ring_2exp4_7vars_1ite_unsat.smt2 | 0.127s | 21.08MiB| unsat | 0 | | | |ring_2exp6_5vars_2ite_unsat.smt2 | 0.129s | 20.744MiB| unsat | 0 | | | |ring_2exp4_6vars_2ite_unsat.smt2 | 0.131s | 20.784MiB| unsat | 0 | | | |ring_2exp14_6vars_1ite_unsat.smt2 | 0.134s | 20.764MiB| unsat | 0 | | | |ring_2exp4_7vars_2ite_unsat.smt2 | 0.134s | 21.136MiB| unsat | 0 | | | |ring_2exp14_7vars_1ite_unsat.smt2 | 0.137s | 20.992MiB| unsat | 0 | | | |ring_2exp12_6vars_2ite_unsat.smt2 | 0.141s | 20.928MiB| unsat | 0 | | | |ring_2exp16_6vars_1ite_unsat.smt2 | 0.141s | 21.032MiB| unsat | 0 | | | |ring_2exp8_6vars_1ite_unsat.smt2 | 0.144s | 20.804MiB| unsat | 0 | | | |ring_2exp6_7vars_1ite_unsat.smt2 | 0.148s | 21.044MiB| unsat | 0 | | | |ring_2exp10_6vars_1ite_unsat.smt2 | 0.153s | 20.848MiB| unsat | 0 | | | |ring_2exp10_4vars_3ite_unsat.smt2 | 0.155s | 20.672MiB| unsat | 0 | | | |ring_2exp16_5vars_2ite_unsat.smt2 | 0.155s | 20.736MiB| unsat | 0 | | | |ring_2exp8_8vars_1ite_unsat.smt2 | 0.158s | 21.384MiB| unsat | 0 | | | |ring_2exp8_4vars_3ite_unsat.smt2 | 0.158s | 20.52MiB| unsat | 0 | | | |ring_2exp12_6vars_1ite_unsat.smt2 | 0.160s | 21.012MiB| unsat | 0 | | | |ring_2exp8_7vars_1ite_unsat.smt2 | 0.170s | 21.148MiB| unsat | 0 | | | |ring_2exp14_5vars_2ite_unsat.smt2 | 0.172s | 20.892MiB| unsat | 0 | | | |ring_2exp6_5vars_3ite_unsat.smt2 | 0.173s | 20.756MiB| unsat | 0 | | | |ring_2exp10_7vars_2ite_unsat.smt2 | 0.181s | 21.084MiB| unsat | 0 | | | |ring_2exp6_6vars_1ite_unsat.smt2 | 0.185s | 20.876MiB| unsat | 0 | | | |ring_2exp12_5vars_2ite_unsat.smt2 | 0.187s | 20.716MiB| unsat | 0 | | | |ring_2exp6_6vars_2ite_unsat.smt2 | 0.190s | 21.016MiB| unsat | 0 | | | |ring_2exp4_8vars_1ite_unsat.smt2 | 0.196s | 21.428MiB| unsat | 0 | | | |ring_2exp16_7vars_1ite_unsat.smt2 | 0.196s | 21.104MiB| unsat | 0 | | | |ring_2exp6_4vars_3ite_unsat.smt2 | 0.198s | 20.54MiB| unsat | 0 | | | |ring_2exp4_6vars_3ite_unsat.smt2 | 0.201s | 21.012MiB| unsat | 0 | | | |ring_2exp8_5vars_3ite_unsat.smt2 | 0.202s | 20.696MiB| unsat | 0 | | | |ring_2exp14_7vars_2ite_unsat.smt2 | 0.202s | 21.128MiB| unsat | 0 | | | |ring_2exp8_7vars_2ite_unsat.smt2 | 0.205s | 21.052MiB| unsat | 0 | | | |ring_2exp8_6vars_2ite_unsat.smt2 | 0.206s | 21.012MiB| unsat | 0 | | | |ring_2exp4_6vars_1ite_unsat.smt2 | 0.210s | 20.916MiB| unsat | 0 | | | |ring_2exp10_7vars_1ite_unsat.smt2 | 0.211s | 21.048MiB| unsat | 0 | | | |ring_2exp12_4vars_3ite_unsat.smt2 | 0.213s | 20.56MiB| unsat | 0 | | | |ring_2exp12_8vars_1ite_unsat.smt2 | 0.214s | 21.224MiB| unsat | 0 | | | |ring_2exp4_8vars_2ite_unsat.smt2 | 0.217s | 21.292MiB| unsat | 0 | | | |ring_2exp4_4vars_3ite_unsat.smt2 | 0.218s | 20.724MiB| unsat | 0 | | | |ring_2exp6_7vars_2ite_unsat.smt2 | 0.221s | 21.228MiB| unsat | 0 | | | |ring_2exp10_5vars_3ite_unsat.smt2 | 0.223s | 20.904MiB| unsat | 0 | | | |ring_2exp12_5vars_3ite_unsat.smt2 | 0.227s | 20.88MiB| unsat | 0 | | | |ring_2exp12_6vars_3ite_unsat.smt2 | 0.230s | 21.02MiB| unsat | 0 | | | |ring_2exp16_5vars_3ite_unsat.smt2 | 0.230s | 20.664MiB| unsat | 0 | | | |ring_2exp14_5vars_3ite_unsat.smt2 | 0.231s | 20.66MiB| unsat | 0 | | | |ring_2exp6_9vars_1ite_unsat.smt2 | 0.237s | 21.576MiB| unsat | 0 | | | |ring_2exp16_6vars_2ite_unsat.smt2 | 0.239s | 20.936MiB| unsat | 0 | | | |ring_2exp6_8vars_2ite_unsat.smt2 | 0.252s | 21.312MiB| unsat | 0 | | | |ring_2exp10_6vars_2ite_unsat.smt2 | 0.253s | 21.108MiB| unsat | 0 | | | |ring_2exp8_9vars_1ite_unsat.smt2 | 0.259s | 21.624MiB| unsat | 0 | | | |ring_2exp4_8vars_3ite_unsat.smt2 | 0.261s | 21.38MiB| unsat | 0 | | | |ring_2exp16_8vars_1ite_unsat.smt2 | 0.262s | 21.364MiB| unsat | 0 | | | |ring_2exp10_8vars_2ite_unsat.smt2 | 0.268s | 21.376MiB| unsat | 0 | | | |ring_2exp8_6vars_3ite_unsat.smt2 | 0.278s | 21.144MiB| unsat | 0 | | | |ring_2exp8_8vars_2ite_unsat.smt2 | 0.286s | 21.412MiB| unsat | 0 | | | |ring_2exp14_6vars_2ite_unsat.smt2 | 0.287s | 21.008MiB| unsat | 0 | | | |ring_2exp10_6vars_3ite_unsat.smt2 | 0.288s | 20.964MiB| unsat | 0 | | | |ring_2exp14_7vars_3ite_unsat.smt2 | 0.309s | 21.116MiB| unsat | 0 | | | |ring_2exp4_9vars_1ite_unsat.smt2 | 0.342s | 21.648MiB| unsat | 0 | | | |ring_2exp6_6vars_3ite_unsat.smt2 | 0.343s | 21.188MiB| unsat | 0 | | | |ring_2exp16_7vars_2ite_unsat.smt2 | 0.349s | 21.108MiB| unsat | 0 | | | |ring_2exp12_7vars_2ite_unsat.smt2 | 0.366s | 21.168MiB| unsat | 0 | | | |ring_2exp8_9vars_2ite_unsat.smt2 | 0.370s | 21.72MiB| unsat | 0 | | | |ring_2exp12_7vars_3ite_unsat.smt2 | 0.377s | 21.344MiB| unsat | 0 | | | |ring_2exp10_8vars_1ite_unsat.smt2 | 0.387s | 21.424MiB| unsat | 0 | | | |ring_2exp14_6vars_3ite_unsat.smt2 | 0.405s | 21.032MiB| unsat | 0 | | | |ring_2exp16_6vars_3ite_unsat.smt2 | 0.420s | 20.908MiB| unsat | 0 | | | |ring_2exp4_7vars_3ite_unsat.smt2 | 0.432s | 21.316MiB| unsat | 0 | | | |ring_2exp12_9vars_1ite_unsat.smt2 | 0.483s | 21.768MiB| unsat | 0 | | | |ring_2exp10_8vars_3ite_unsat.smt2 | 0.486s | 21.552MiB| unsat | 0 | | | |ring_2exp16_8vars_2ite_unsat.smt2 | 0.494s | 21.316MiB| unsat | 0 | | | |ring_2exp12_8vars_2ite_unsat.smt2 | 0.497s | 21.556MiB| unsat | 0 | | | |ring_2exp6_9vars_2ite_unsat.smt2 | 0.498s | 21.608MiB| unsat | 0 | | | |ring_2exp16_9vars_1ite_unsat.smt2 | 0.539s | 21.544MiB| unsat | 0 | | | |ring_2exp6_7vars_3ite_unsat.smt2 | 0.544s | 21.56MiB| unsat | 0 | | | |ring_2exp16_8vars_3ite_unsat.smt2 | 0.583s | 21.54MiB| unsat | 0 | | | |ring_2exp14_8vars_3ite_unsat.smt2 | 0.592s | 21.732MiB| unsat | 0 | | | |ring_2exp14_9vars_1ite_unsat.smt2 | 0.608s | 21.404MiB| unsat | 0 | | | |ring_2exp16_9vars_2ite_unsat.smt2 | 0.615s | 21.644MiB| unsat | 0 | | | |ring_2exp12_9vars_2ite_unsat.smt2 | 0.616s | 21.696MiB| unsat | 0 | | | |ring_2exp14_8vars_2ite_unsat.smt2 | 0.624s | 21.428MiB| unsat | 0 | | | |ring_2exp10_9vars_1ite_unsat.smt2 | 0.685s | 21.448MiB| unsat | 0 | | | |ring_2exp4_9vars_2ite_unsat.smt2 | 0.691s | 21.924MiB| unsat | 0 | | | |ring_2exp16_7vars_3ite_unsat.smt2 | 0.703s | 21.396MiB| unsat | 0 | | | |ring_2exp12_8vars_3ite_unsat.smt2 | 0.710s | 21.736MiB| unsat | 0 | | | |ring_2exp8_7vars_3ite_unsat.smt2 | 0.724s | 21.572MiB| unsat | 0 | | | |ring_2exp6_8vars_3ite_unsat.smt2 | 0.733s | 21.78MiB| unsat | 0 | | | |ring_2exp4_9vars_3ite_unsat.smt2 | 0.796s | 22.028MiB| unsat | 0 | | | |ring_2exp14_9vars_2ite_unsat.smt2 | 0.805s | 21.844MiB| unsat | 0 | | | |ring_2exp14_5vars_4ite_unsat.smt2 | 0.812s | 21.04MiB| unsat | 0 | | | |ring_2exp12_5vars_4ite_unsat.smt2 | 0.888s | 21.056MiB| unsat | 0 | | | |ring_2exp16_5vars_4ite_unsat.smt2 | 0.891s | 21.072MiB| unsat | 0 | | | |ring_2exp10_9vars_2ite_unsat.smt2 | 1.050s | 21.62MiB| unsat | 0 | | | |ring_2exp8_5vars_4ite_unsat.smt2 | 1.145s | 21.12MiB| unsat | 0 | | | |ring_2exp10_9vars_3ite_unsat.smt2 | 1.301s | 22.312MiB| unsat | 0 | | | |ring_2exp16_9vars_3ite_unsat.smt2 | 1.301s | 21.94MiB| unsat | 0 | | | |ring_2exp14_7vars_4ite_unsat.smt2 | 1.435s | 21.6MiB| unsat | 0 | | | |ring_2exp10_7vars_3ite_unsat.smt2 | 1.438s | 22.012MiB| unsat | 0 | | | |ring_2exp14_9vars_3ite_unsat.smt2 | 1.461s | 21.796MiB| unsat | 0 | | | |ring_2exp14_6vars_4ite_unsat.smt2 | 1.480s | 21.324MiB| unsat | 0 | | | |ring_2exp10_5vars_4ite_unsat.smt2 | 1.487s | 21.384MiB| unsat | 0 | | | |ring_2exp4_7vars_4ite_unsat.smt2 | 1.606s | 21.54MiB| unsat | 0 | | | |ring_2exp10_8vars_4ite_unsat.smt2 | 1.646s | 21.94MiB| unsat | 0 | | | |ring_2exp6_9vars_3ite_unsat.smt2 | 1.655s | 22.624MiB| unsat | 0 | | | |ring_2exp4_5vars_4ite_unsat.smt2 | 1.700s | 21.328MiB| unsat | 0 | | | |ring_2exp16_7vars_4ite_unsat.smt2 | 1.727s | 21.752MiB| unsat | 0 | | | |ring_2exp8_9vars_3ite_unsat.smt2 | 1.754s | 22.568MiB| unsat | 0 | | | |ring_2exp16_6vars_4ite_unsat.smt2 | 1.877s | 21.52MiB| unsat | 0 | | | |ring_2exp4_6vars_4ite_unsat.smt2 | 1.885s | 21.472MiB| unsat | 0 | | | |ring_2exp12_9vars_3ite_unsat.smt2 | 2.060s | 22.776MiB| unsat | 0 | | | |ring_2exp6_5vars_4ite_unsat.smt2 | 2.062s | 21.796MiB| unsat | 0 | | | |ring_2exp8_8vars_3ite_unsat.smt2 | 2.082s | 22.82MiB| unsat | 0 | | | |ring_2exp12_6vars_4ite_unsat.smt2 | 2.092s | 21.544MiB| unsat | 0 | | | |ring_2exp4_8vars_4ite_unsat.smt2 | 2.109s | 22.06MiB| unsat | 0 | | | |ring_2exp16_8vars_4ite_unsat.smt2 | 2.371s | 22.14MiB| unsat | 0 | | | |ring_2exp10_6vars_4ite_unsat.smt2 | 2.625s | 22.228MiB| unsat | 0 | | | |ring_2exp4_9vars_4ite_unsat.smt2 | 2.986s | 22.256MiB| unsat | 0 | | | |ring_2exp8_6vars_4ite_unsat.smt2 | 3.198s | 22.164MiB| unsat | 0 | | | |ring_2exp4_6vars_5ite_unsat.smt2 | 3.344s | 21.86MiB| unsat | 0 | | | |ring_2exp14_9vars_4ite_unsat.smt2 | 3.596s | 22.56MiB| unsat | 0 | | | |ring_2exp6_9vars_4ite_unsat.smt2 | 3.661s | 23.28MiB| unsat | 0 | | | |ring_2exp6_8vars_4ite_unsat.smt2 | 3.691s | 22.568MiB| unsat | 0 | | | |ring_2exp12_8vars_4ite_unsat.smt2 | 3.756s | 22.828MiB| unsat | 0 | | | |ring_2exp4_9vars_5ite_unsat.smt2 | 3.951s | 22.604MiB| unsat | 0 | | | |ring_2exp14_8vars_4ite_unsat.smt2 | 4.246s | 22.972MiB| unsat | 0 | | | |ring_2exp4_7vars_5ite_unsat.smt2 | 4.271s | 22.264MiB| unsat | 0 | | | |ring_2exp14_6vars_5ite_unsat.smt2 | 4.385s | 22.076MiB| unsat | 0 | | | |ring_2exp10_9vars_4ite_unsat.smt2 | 4.400s | 23.532MiB| unsat | 0 | | | |ring_2exp10_7vars_4ite_unsat.smt2 | 12.408s | 23.376MiB| unsat | 0 | | | |ring_2exp16_9vars_4ite_unsat.smt2 | 13.620s | 23.944MiB| unsat | 0 | | | |ring_2exp8_8vars_4ite_unsat.smt2 | 13.977s | 24.348MiB| unsat | 0 | | | |ring_2exp6_6vars_4ite_unsat.smt2 | 14.491s | 23.576MiB| unsat | 0 | | | |ring_2exp16_7vars_5ite_unsat.smt2 | 15.445s | 24.356MiB| unsat | 0 | | | |ring_2exp10_7vars_5ite_unsat.smt2 | 15.656s | 24.768MiB| unsat | 0 | | | |ring_2exp4_8vars_5ite_unsat.smt2 | 16.058s | 23.432MiB| unsat | 0 | | | |ring_2exp6_7vars_5ite_unsat.smt2 | 16.385s | 24.596MiB| unsat | 0 | | | |ring_2exp12_7vars_4ite_unsat.smt2 | 16.456s | 23.48MiB| unsat | 0 | | | |ring_2exp10_6vars_5ite_unsat.smt2 | 18.283s | 24.208MiB| unsat | 0 | | | |ring_2exp6_7vars_4ite_unsat.smt2 | 18.298s | 24.24MiB| unsat | 0 | | | |ring_2exp16_6vars_5ite_unsat.smt2 | 18.671s | 23.768MiB| unsat | 0 | | | |ring_2exp8_7vars_4ite_unsat.smt2 | 18.858s | 24.424MiB| unsat | 0 | | | |ring_2exp8_6vars_5ite_unsat.smt2 | 19.080s | 24.88MiB| unsat | 0 | | | |ring_2exp8_8vars_5ite_unsat.smt2 | 19.781s | 25.592MiB| unsat | 0 | | | |ring_2exp12_9vars_4ite_unsat.smt2 | 19.828s | 25.504MiB| unsat | 0 | | | |ring_2exp12_7vars_5ite_unsat.smt2 | 19.865s | 24.54MiB| unsat | 0 | | | |ring_2exp12_8vars_5ite_unsat.smt2 | 20.140s | 25.04MiB| unsat | 0 | | | |ring_2exp12_6vars_5ite_unsat.smt2 | 20.897s | 24.412MiB| unsat | 0 | | | |ring_2exp6_6vars_5ite_unsat.smt2 | 22.492s | 24.72MiB| unsat | 0 | | | |ring_2exp14_7vars_5ite_unsat.smt2 | 22.995s | 25.776MiB| unsat | 0 | | | |ring_2exp8_7vars_5ite_unsat.smt2 | 23.116s | 26.552MiB| unsat | 0 | | | |ring_2exp8_9vars_4ite_unsat.smt2 | 26.453s | 27.428MiB| unsat | 0 | | | |ring_2exp16_8vars_5ite_unsat.smt2 | 27.547s | 26.456MiB| unsat | 0 | | | |ring_2exp14_8vars_5ite_unsat.smt2 | 27.675s | 26.356MiB| unsat | 0 | | | |ring_2exp10_8vars_5ite_unsat.smt2 | 28.308s | 26.548MiB| unsat | 0 | | | |ring_2exp16_9vars_5ite_unsat.smt2 | 28.473s | 26.58MiB| unsat | 0 | | | |ring_2exp6_9vars_5ite_unsat.smt2 | 28.563s | 26.14MiB| unsat | 0 | | | |ring_2exp8_9vars_5ite_unsat.smt2 | 28.582s | 27.396MiB| unsat | 0 | | | |ring_2exp12_9vars_5ite_unsat.smt2 | 28.863s | 26.928MiB| unsat | 0 | | | |ring_2exp14_9vars_5ite_unsat.smt2 | 28.988s | 26.112MiB| unsat | 0 | | | |ring_2exp10_9vars_5ite_unsat.smt2 | 29.691s | 27.272MiB| unsat | 0 | | | |ring_2exp12_7vars_6ite_unsat.smt2 | 45.937s | 25.276MiB| unsat | 0 | | | |ring_2exp16_7vars_6ite_unsat.smt2 | 46.918s | 26.116MiB| unsat | 0 | | | |ring_2exp8_7vars_6ite_unsat.smt2 | 47.794s | 26.916MiB| unsat | 0 | | | |ring_2exp6_7vars_6ite_unsat.smt2 | 47.992s | 25.7MiB| unsat | 0 | | | |ring_2exp14_7vars_6ite_unsat.smt2 | 48.787s | 26.228MiB| unsat | 0 | | | |ring_2exp10_7vars_6ite_unsat.smt2 | 48.892s | 26.736MiB| unsat | 0 | | | |ring_2exp12_8vars_6ite_unsat.smt2 | 67.926s | 26.984MiB| unsat | 0 | | | |ring_2exp6_9vars_6ite_unsat.smt2 | 69.460s | 26.764MiB| unsat | 0 | | | |ring_2exp14_8vars_6ite_unsat.smt2 | 70.877s | 26.288MiB| unsat | 0 | | | |ring_2exp16_8vars_6ite_unsat.smt2 | 71.552s | 26.232MiB| unsat | 0 | | | |ring_2exp8_8vars_6ite_unsat.smt2 | 73.359s | 26.936MiB| unsat | 0 | | | |ring_2exp10_8vars_6ite_unsat.smt2 | 74.571s | 27.38MiB| unsat | 0 | | | |ring_2exp14_9vars_6ite_unsat.smt2 | 75.204s | 27.38MiB| unsat | 0 | | | |ring_2exp16_9vars_6ite_unsat.smt2 | 75.833s | 26.744MiB| unsat | 0 | | | |ring_2exp8_9vars_6ite_unsat.smt2 | 78.337s | 27.552MiB| unsat | 0 | | | |ring_2exp12_9vars_6ite_unsat.smt2 | 85.030s | 27.556MiB| unsat | 0 | | | |ring_2exp4_8vars_6ite_unsat.smt2 | 88.769s | 25.948MiB| unsat | 0 | | | |ring_2exp6_8vars_6ite_unsat.smt2 | 90.506s | 27.144MiB| unsat | 0 | | | |ring_2exp10_9vars_6ite_unsat.smt2 | 91.193s | 29.34MiB| unsat | 0 | | | |ring_2exp10_8vars_7ite_unsat.smt2 | 107.134s | 27.348MiB| unsat | 0 | | | |ring_2exp8_8vars_7ite_unsat.smt2 | 111.120s | 28.188MiB| unsat | 0 | | | |ring_2exp12_8vars_7ite_unsat.smt2 | 112.869s | 27.404MiB| unsat | 0 | | | |ring_2exp16_8vars_7ite_unsat.smt2 | 120.776s | 27.52MiB| unsat | 0 | | | |ring_2exp14_8vars_7ite_unsat.smt2 | 121.756s | 27.936MiB| unsat | 0 | | | |ring_2exp14_9vars_7ite_unsat.smt2 | 143.201s | 28.792MiB| unsat | 0 | | | |ring_2exp16_9vars_7ite_unsat.smt2 | 143.278s | 28.264MiB| unsat | 0 | | | |ring_2exp10_9vars_7ite_unsat.smt2 | 144.675s | 30.036MiB| unsat | 0 | | | |ring_2exp8_9vars_7ite_unsat.smt2 | 146.661s | 30.72MiB| unsat | 0 | | | |ring_2exp12_9vars_7ite_unsat.smt2 | 160.196s | 29.108MiB| unsat | 0 | | | |ring_2exp4_8vars_7ite_unsat.smt2 | 165.720s | 28.916MiB| unsat | 0 | | | |ring_2exp4_9vars_7ite_unsat.smt2 | 297.943s | 29.904MiB| unsat | 0 | | | |ring_2exp4_7vars_6ite_unsat.smt2 | 494.179s | 45.188MiB| unsat | 0 | | | |ring_2exp6_8vars_5ite_unsat.smt2 | 599.922s | 37.996MiB| timeout | 0 | | | |ring_2exp10_9vars_8ite_unsat.smt2 | 599.938s | 48.652MiB| timeout | 0 | | | |ring_2exp14_9vars_8ite_unsat.smt2 | 599.945s | 41.16MiB| timeout | 0 | | | |ring_2exp12_9vars_8ite_unsat.smt2 | 599.952s | 50.448MiB| timeout | 0 | | | |ring_2exp4_9vars_6ite_unsat.smt2 | 599.958s | 38.088MiB| timeout | 0 | | | |ring_2exp6_8vars_7ite_unsat.smt2 | 599.961s | 40.056MiB| timeout | 0 | | | |ring_2exp6_9vars_8ite_unsat.smt2 | 599.964s | 42.08MiB| timeout | 0 | | | |ring_2exp16_9vars_8ite_unsat.smt2 | 599.967s | 43.064MiB| timeout | 0 | | | |ring_2exp6_9vars_7ite_unsat.smt2 | 599.971s | 46.96MiB| timeout | 0 | | | |ring_2exp8_9vars_8ite_unsat.smt2 | 599.971s | 46.404MiB| timeout | 0 | | | |ring_2exp4_9vars_8ite_unsat.smt2 | 599.973s | 37.996MiB| timeout | 0 | | |