# . * 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 lp.dio=true"
Z3 inputs: inputs/rings
Z3 commit message: filter out terms that are not solved
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |ring_2exp10_3vars_0ite_unsat.smt2 | 0.029s | 20.124MiB| unsat | 0 | | | |ring_2exp4_3vars_0ite_unsat.smt2 | 0.030s | 20.108MiB| unsat | 0 | | | |ring_2exp14_4vars_0ite_unsat.smt2 | 0.030s | 20.24MiB| unsat | 0 | | | |ring_2exp8_3vars_0ite_unsat.smt2 | 0.031s | 20.232MiB| unsat | 0 | | | |ring_2exp6_3vars_0ite_unsat.smt2 | 0.031s | 20.064MiB| unsat | 0 | | | |ring_2exp10_4vars_0ite_unsat.smt2 | 0.031s | 20.28MiB| unsat | 0 | | | |ring_2exp16_3vars_0ite_unsat.smt2 | 0.032s | 20.172MiB| unsat | 0 | | | |ring_2exp4_4vars_0ite_unsat.smt2 | 0.032s | 20.224MiB| unsat | 0 | | | |ring_2exp16_4vars_0ite_unsat.smt2 | 0.033s | 20.332MiB| unsat | 0 | | | |ring_2exp8_5vars_0ite_unsat.smt2 | 0.034s | 20.46MiB| unsat | 0 | | | |ring_2exp12_4vars_0ite_unsat.smt2 | 0.034s | 20.2MiB| unsat | 0 | | | |ring_2exp10_7vars_0ite_unsat.smt2 | 0.035s | 21.048MiB| unsat | 0 | | | |ring_2exp6_4vars_0ite_unsat.smt2 | 0.035s | 20.26MiB| unsat | 0 | | | |ring_2exp6_5vars_0ite_unsat.smt2 | 0.036s | 20.496MiB| unsat | 0 | | | |ring_2exp14_6vars_0ite_unsat.smt2 | 0.036s | 20.444MiB| unsat | 0 | | | |ring_2exp6_8vars_0ite_unsat.smt2 | 0.037s | 20.92MiB| unsat | 0 | | | |ring_2exp12_6vars_0ite_unsat.smt2 | 0.037s | 20.604MiB| unsat | 0 | | | |ring_2exp16_6vars_0ite_unsat.smt2 | 0.037s | 20.64MiB| unsat | 0 | | | |ring_2exp8_6vars_0ite_unsat.smt2 | 0.037s | 20.584MiB| unsat | 0 | | | |ring_2exp14_3vars_0ite_unsat.smt2 | 0.040s | 20.508MiB| unsat | 0 | | | |ring_2exp4_5vars_0ite_unsat.smt2 | 0.040s | 20.416MiB| unsat | 0 | | | |ring_2exp14_7vars_0ite_unsat.smt2 | 0.041s | 20.62MiB| unsat | 0 | | | |ring_2exp6_9vars_0ite_unsat.smt2 | 0.041s | 20.768MiB| unsat | 0 | | | |ring_2exp12_3vars_0ite_unsat.smt2 | 0.041s | 20.116MiB| unsat | 0 | | | |ring_2exp4_8vars_0ite_unsat.smt2 | 0.042s | 20.756MiB| unsat | 0 | | | |ring_2exp8_3vars_2ite_unsat.smt2 | 0.042s | 20.512MiB| unsat | 0 | | | |ring_2exp16_3vars_2ite_unsat.smt2 | 0.042s | 20.264MiB| unsat | 0 | | | |ring_2exp8_9vars_0ite_unsat.smt2 | 0.043s | 20.924MiB| unsat | 0 | | | |ring_2exp8_3vars_1ite_unsat.smt2 | 0.044s | 20.312MiB| unsat | 0 | | | |ring_2exp16_8vars_0ite_unsat.smt2 | 0.044s | 20.916MiB| unsat | 0 | | | |ring_2exp12_5vars_0ite_unsat.smt2 | 0.045s | 20.672MiB| unsat | 0 | | | |ring_2exp10_5vars_0ite_unsat.smt2 | 0.045s | 20.524MiB| unsat | 0 | | | |ring_2exp4_7vars_0ite_unsat.smt2 | 0.047s | 20.556MiB| unsat | 0 | | | |ring_2exp8_4vars_0ite_unsat.smt2 | 0.047s | 20.264MiB| unsat | 0 | | | |ring_2exp14_3vars_2ite_unsat.smt2 | 0.047s | 20.496MiB| unsat | 0 | | | |ring_2exp8_8vars_0ite_unsat.smt2 | 0.047s | 20.848MiB| unsat | 0 | | | |ring_2exp12_3vars_2ite_unsat.smt2 | 0.047s | 20.372MiB| unsat | 0 | | | |ring_2exp16_9vars_0ite_unsat.smt2 | 0.048s | 21.06MiB| unsat | 0 | | | |ring_2exp16_5vars_0ite_unsat.smt2 | 0.048s | 20.392MiB| unsat | 0 | | | |ring_2exp10_6vars_0ite_unsat.smt2 | 0.048s | 20.748MiB| unsat | 0 | | | |ring_2exp14_3vars_1ite_unsat.smt2 | 0.049s | 20.216MiB| unsat | 0 | | | |ring_2exp10_9vars_0ite_unsat.smt2 | 0.049s | 20.832MiB| unsat | 0 | | | |ring_2exp6_6vars_0ite_unsat.smt2 | 0.049s | 20.52MiB| unsat | 0 | | | |ring_2exp6_3vars_1ite_unsat.smt2 | 0.050s | 20.312MiB| unsat | 0 | | | |ring_2exp8_7vars_0ite_unsat.smt2 | 0.050s | 20.68MiB| unsat | 0 | | | |ring_2exp6_3vars_2ite_unsat.smt2 | 0.050s | 20.252MiB| unsat | 0 | | | |ring_2exp4_3vars_1ite_unsat.smt2 | 0.051s | 20.336MiB| unsat | 0 | | | |ring_2exp16_3vars_1ite_unsat.smt2 | 0.051s | 20.252MiB| unsat | 0 | | | |ring_2exp12_8vars_0ite_unsat.smt2 | 0.053s | 20.884MiB| unsat | 0 | | | |ring_2exp14_5vars_0ite_unsat.smt2 | 0.053s | 20.416MiB| unsat | 0 | | | |ring_2exp10_8vars_0ite_unsat.smt2 | 0.056s | 20.664MiB| unsat | 0 | | | |ring_2exp14_9vars_0ite_unsat.smt2 | 0.057s | 21.06MiB| unsat | 0 | | | |ring_2exp12_7vars_0ite_unsat.smt2 | 0.057s | 20.728MiB| unsat | 0 | | | |ring_2exp4_6vars_0ite_unsat.smt2 | 0.057s | 20.724MiB| unsat | 0 | | | |ring_2exp12_3vars_1ite_unsat.smt2 | 0.057s | 20.4MiB| unsat | 0 | | | |ring_2exp10_3vars_2ite_unsat.smt2 | 0.058s | 20.264MiB| unsat | 0 | | | |ring_2exp14_8vars_0ite_unsat.smt2 | 0.059s | 20.788MiB| unsat | 0 | | | |ring_2exp10_3vars_1ite_unsat.smt2 | 0.060s | 20.32MiB| unsat | 0 | | | |ring_2exp12_9vars_0ite_unsat.smt2 | 0.062s | 20.984MiB| unsat | 0 | | | |ring_2exp6_4vars_1ite_unsat.smt2 | 0.064s | 20.492MiB| unsat | 0 | | | |ring_2exp14_4vars_1ite_unsat.smt2 | 0.067s | 20.332MiB| unsat | 0 | | | |ring_2exp16_7vars_0ite_unsat.smt2 | 0.072s | 21.056MiB| unsat | 0 | | | |ring_2exp4_9vars_0ite_unsat.smt2 | 0.073s | 20.756MiB| unsat | 0 | | | |ring_2exp16_4vars_1ite_unsat.smt2 | 0.074s | 20.448MiB| unsat | 0 | | | |ring_2exp6_7vars_0ite_unsat.smt2 | 0.074s | 20.664MiB| unsat | 0 | | | |ring_2exp4_4vars_1ite_unsat.smt2 | 0.076s | 20.592MiB| unsat | 0 | | | |ring_2exp8_4vars_1ite_unsat.smt2 | 0.078s | 20.464MiB| unsat | 0 | | | |ring_2exp4_4vars_2ite_unsat.smt2 | 0.082s | 20.432MiB| unsat | 0 | | | |ring_2exp4_5vars_1ite_unsat.smt2 | 0.082s | 20.764MiB| unsat | 0 | | | |ring_2exp6_5vars_1ite_unsat.smt2 | 0.082s | 20.644MiB| unsat | 0 | | | |ring_2exp10_4vars_1ite_unsat.smt2 | 0.082s | 20.428MiB| unsat | 0 | | | |ring_2exp10_4vars_2ite_unsat.smt2 | 0.084s | 20.492MiB| unsat | 0 | | | |ring_2exp12_5vars_1ite_unsat.smt2 | 0.089s | 20.716MiB| unsat | 0 | | | |ring_2exp12_4vars_1ite_unsat.smt2 | 0.090s | 20.692MiB| unsat | 0 | | | |ring_2exp16_5vars_1ite_unsat.smt2 | 0.092s | 20.908MiB| unsat | 0 | | | |ring_2exp6_4vars_2ite_unsat.smt2 | 0.093s | 20.6MiB| unsat | 0 | | | |ring_2exp4_3vars_2ite_unsat.smt2 | 0.098s | 20.384MiB| unsat | 0 | | | |ring_2exp14_4vars_2ite_unsat.smt2 | 0.101s | 20.52MiB| unsat | 0 | | | |ring_2exp8_5vars_1ite_unsat.smt2 | 0.102s | 20.748MiB| unsat | 0 | | | |ring_2exp10_5vars_1ite_unsat.smt2 | 0.103s | 20.628MiB| unsat | 0 | | | |ring_2exp8_4vars_2ite_unsat.smt2 | 0.104s | 20.66MiB| unsat | 0 | | | |ring_2exp14_5vars_1ite_unsat.smt2 | 0.106s | 20.628MiB| unsat | 0 | | | |ring_2exp16_4vars_2ite_unsat.smt2 | 0.106s | 20.42MiB| unsat | 0 | | | |ring_2exp4_5vars_2ite_unsat.smt2 | 0.106s | 20.644MiB| unsat | 0 | | | |ring_2exp10_5vars_2ite_unsat.smt2 | 0.108s | 20.616MiB| unsat | 0 | | | |ring_2exp12_4vars_2ite_unsat.smt2 | 0.114s | 20.596MiB| unsat | 0 | | | |ring_2exp8_5vars_2ite_unsat.smt2 | 0.115s | 20.76MiB| unsat | 0 | | | |ring_2exp12_7vars_1ite_unsat.smt2 | 0.125s | 21.072MiB| unsat | 0 | | | |ring_2exp6_5vars_2ite_unsat.smt2 | 0.130s | 20.796MiB| unsat | 0 | | | |ring_2exp14_6vars_1ite_unsat.smt2 | 0.132s | 20.82MiB| unsat | 0 | | | |ring_2exp6_8vars_1ite_unsat.smt2 | 0.132s | 21.28MiB| unsat | 0 | | | |ring_2exp16_4vars_3ite_unsat.smt2 | 0.132s | 20.488MiB| unsat | 0 | | | |ring_2exp4_7vars_1ite_unsat.smt2 | 0.134s | 21.092MiB| unsat | 0 | | | |ring_2exp4_7vars_2ite_unsat.smt2 | 0.136s | 21.152MiB| unsat | 0 | | | |ring_2exp14_7vars_1ite_unsat.smt2 | 0.137s | 21.012MiB| unsat | 0 | | | |ring_2exp16_6vars_1ite_unsat.smt2 | 0.137s | 20.776MiB| unsat | 0 | | | |ring_2exp6_7vars_1ite_unsat.smt2 | 0.138s | 21.176MiB| unsat | 0 | | | |ring_2exp14_4vars_3ite_unsat.smt2 | 0.138s | 20.52MiB| unsat | 0 | | | |ring_2exp8_6vars_1ite_unsat.smt2 | 0.143s | 20.876MiB| unsat | 0 | | | |ring_2exp12_6vars_2ite_unsat.smt2 | 0.145s | 20.928MiB| unsat | 0 | | | |ring_2exp16_5vars_2ite_unsat.smt2 | 0.150s | 20.684MiB| unsat | 0 | | | |ring_2exp14_8vars_1ite_unsat.smt2 | 0.152s | 21.2MiB| unsat | 0 | | | |ring_2exp10_6vars_1ite_unsat.smt2 | 0.153s | 20.796MiB| unsat | 0 | | | |ring_2exp6_5vars_3ite_unsat.smt2 | 0.154s | 20.744MiB| unsat | 0 | | | |ring_2exp12_5vars_2ite_unsat.smt2 | 0.155s | 20.732MiB| unsat | 0 | | | |ring_2exp4_8vars_2ite_unsat.smt2 | 0.156s | 21.24MiB| unsat | 0 | | | |ring_2exp4_6vars_2ite_unsat.smt2 | 0.156s | 20.84MiB| unsat | 0 | | | |ring_2exp4_5vars_3ite_unsat.smt2 | 0.158s | 20.888MiB| unsat | 0 | | | |ring_2exp8_8vars_1ite_unsat.smt2 | 0.162s | 21.384MiB| unsat | 0 | | | |ring_2exp8_4vars_3ite_unsat.smt2 | 0.163s | 20.608MiB| unsat | 0 | | | |ring_2exp8_7vars_1ite_unsat.smt2 | 0.170s | 21.008MiB| unsat | 0 | | | |ring_2exp12_6vars_1ite_unsat.smt2 | 0.171s | 20.808MiB| unsat | 0 | | | |ring_2exp6_4vars_3ite_unsat.smt2 | 0.174s | 20.716MiB| unsat | 0 | | | |ring_2exp12_8vars_1ite_unsat.smt2 | 0.176s | 21.312MiB| unsat | 0 | | | |ring_2exp10_4vars_3ite_unsat.smt2 | 0.177s | 20.472MiB| unsat | 0 | | | |ring_2exp6_6vars_2ite_unsat.smt2 | 0.179s | 20.804MiB| unsat | 0 | | | |ring_2exp12_4vars_3ite_unsat.smt2 | 0.179s | 20.632MiB| unsat | 0 | | | |ring_2exp10_7vars_2ite_unsat.smt2 | 0.181s | 21.032MiB| unsat | 0 | | | |ring_2exp10_7vars_1ite_unsat.smt2 | 0.181s | 21.228MiB| unsat | 0 | | | |ring_2exp6_6vars_1ite_unsat.smt2 | 0.185s | 21.016MiB| unsat | 0 | | | |ring_2exp8_5vars_3ite_unsat.smt2 | 0.190s | 20.692MiB| unsat | 0 | | | |ring_2exp16_7vars_1ite_unsat.smt2 | 0.190s | 21.16MiB| unsat | 0 | | | |ring_2exp14_5vars_2ite_unsat.smt2 | 0.192s | 20.84MiB| unsat | 0 | | | |ring_2exp4_4vars_3ite_unsat.smt2 | 0.194s | 20.744MiB| unsat | 0 | | | |ring_2exp4_8vars_1ite_unsat.smt2 | 0.197s | 21.344MiB| unsat | 0 | | | |ring_2exp14_7vars_2ite_unsat.smt2 | 0.204s | 21.016MiB| unsat | 0 | | | |ring_2exp8_6vars_2ite_unsat.smt2 | 0.207s | 21.028MiB| unsat | 0 | | | |ring_2exp16_5vars_3ite_unsat.smt2 | 0.207s | 20.66MiB| unsat | 0 | | | |ring_2exp4_6vars_1ite_unsat.smt2 | 0.213s | 20.996MiB| unsat | 0 | | | |ring_2exp16_6vars_2ite_unsat.smt2 | 0.214s | 20.8MiB| unsat | 0 | | | |ring_2exp6_7vars_2ite_unsat.smt2 | 0.215s | 21.168MiB| unsat | 0 | | | |ring_2exp14_5vars_3ite_unsat.smt2 | 0.225s | 20.732MiB| unsat | 0 | | | |ring_2exp10_5vars_3ite_unsat.smt2 | 0.226s | 20.892MiB| unsat | 0 | | | |ring_2exp12_6vars_3ite_unsat.smt2 | 0.232s | 20.908MiB| unsat | 0 | | | |ring_2exp8_7vars_2ite_unsat.smt2 | 0.240s | 21.036MiB| unsat | 0 | | | |ring_2exp8_9vars_1ite_unsat.smt2 | 0.247s | 21.576MiB| unsat | 0 | | | |ring_2exp8_6vars_3ite_unsat.smt2 | 0.250s | 20.908MiB| unsat | 0 | | | |ring_2exp10_6vars_2ite_unsat.smt2 | 0.250s | 20.996MiB| unsat | 0 | | | |ring_2exp6_8vars_2ite_unsat.smt2 | 0.256s | 21.456MiB| unsat | 0 | | | |ring_2exp12_5vars_3ite_unsat.smt2 | 0.257s | 20.908MiB| unsat | 0 | | | |ring_2exp6_9vars_1ite_unsat.smt2 | 0.258s | 21.632MiB| unsat | 0 | | | |ring_2exp16_8vars_1ite_unsat.smt2 | 0.263s | 21.324MiB| unsat | 0 | | | |ring_2exp4_8vars_3ite_unsat.smt2 | 0.272s | 21.472MiB| unsat | 0 | | | |ring_2exp4_6vars_3ite_unsat.smt2 | 0.274s | 21.088MiB| unsat | 0 | | | |ring_2exp10_8vars_2ite_unsat.smt2 | 0.279s | 21.52MiB| unsat | 0 | | | |ring_2exp8_8vars_2ite_unsat.smt2 | 0.286s | 21.428MiB| unsat | 0 | | | |ring_2exp10_6vars_3ite_unsat.smt2 | 0.293s | 21.048MiB| unsat | 0 | | | |ring_2exp14_6vars_2ite_unsat.smt2 | 0.299s | 21.036MiB| unsat | 0 | | | |ring_2exp14_7vars_3ite_unsat.smt2 | 0.321s | 21.128MiB| unsat | 0 | | | |ring_2exp6_6vars_3ite_unsat.smt2 | 0.345s | 21.352MiB| unsat | 0 | | | |ring_2exp4_9vars_1ite_unsat.smt2 | 0.347s | 21.648MiB| unsat | 0 | | | |ring_2exp12_7vars_2ite_unsat.smt2 | 0.365s | 21.108MiB| unsat | 0 | | | |ring_2exp16_7vars_2ite_unsat.smt2 | 0.376s | 21.292MiB| unsat | 0 | | | |ring_2exp12_7vars_3ite_unsat.smt2 | 0.377s | 21.28MiB| unsat | 0 | | | |ring_2exp8_9vars_2ite_unsat.smt2 | 0.380s | 21.528MiB| unsat | 0 | | | |ring_2exp10_8vars_1ite_unsat.smt2 | 0.394s | 21.332MiB| unsat | 0 | | | |ring_2exp14_6vars_3ite_unsat.smt2 | 0.402s | 21.084MiB| unsat | 0 | | | |ring_2exp16_6vars_3ite_unsat.smt2 | 0.415s | 21.052MiB| unsat | 0 | | | |ring_2exp4_7vars_3ite_unsat.smt2 | 0.433s | 21.276MiB| unsat | 0 | | | |ring_2exp12_9vars_1ite_unsat.smt2 | 0.488s | 21.516MiB| unsat | 0 | | | |ring_2exp10_8vars_3ite_unsat.smt2 | 0.488s | 21.576MiB| unsat | 0 | | | |ring_2exp12_8vars_2ite_unsat.smt2 | 0.488s | 21.46MiB| unsat | 0 | | | |ring_2exp6_9vars_2ite_unsat.smt2 | 0.505s | 21.652MiB| unsat | 0 | | | |ring_2exp16_8vars_2ite_unsat.smt2 | 0.511s | 21.304MiB| unsat | 0 | | | |ring_2exp16_9vars_1ite_unsat.smt2 | 0.522s | 21.456MiB| unsat | 0 | | | |ring_2exp6_7vars_3ite_unsat.smt2 | 0.537s | 21.536MiB| unsat | 0 | | | |ring_2exp12_9vars_2ite_unsat.smt2 | 0.558s | 21.504MiB| unsat | 0 | | | |ring_2exp14_8vars_2ite_unsat.smt2 | 0.594s | 21.6MiB| unsat | 0 | | | |ring_2exp16_9vars_2ite_unsat.smt2 | 0.602s | 21.584MiB| unsat | 0 | | | |ring_2exp14_8vars_3ite_unsat.smt2 | 0.610s | 21.588MiB| unsat | 0 | | | |ring_2exp14_9vars_1ite_unsat.smt2 | 0.614s | 21.54MiB| unsat | 0 | | | |ring_2exp16_8vars_3ite_unsat.smt2 | 0.616s | 21.62MiB| unsat | 0 | | | |ring_2exp16_7vars_3ite_unsat.smt2 | 0.620s | 21.372MiB| unsat | 0 | | | |ring_2exp10_9vars_1ite_unsat.smt2 | 0.644s | 21.5MiB| unsat | 0 | | | |ring_2exp4_9vars_2ite_unsat.smt2 | 0.690s | 21.744MiB| unsat | 0 | | | |ring_2exp8_7vars_3ite_unsat.smt2 | 0.714s | 21.684MiB| unsat | 0 | | | |ring_2exp12_8vars_3ite_unsat.smt2 | 0.729s | 21.676MiB| unsat | 0 | | | |ring_2exp6_8vars_3ite_unsat.smt2 | 0.806s | 21.8MiB| unsat | 0 | | | |ring_2exp14_5vars_4ite_unsat.smt2 | 0.815s | 21.152MiB| unsat | 0 | | | |ring_2exp14_9vars_2ite_unsat.smt2 | 0.825s | 21.8MiB| unsat | 0 | | | |ring_2exp16_5vars_4ite_unsat.smt2 | 0.889s | 20.964MiB| unsat | 0 | | | |ring_2exp12_5vars_4ite_unsat.smt2 | 0.925s | 21.172MiB| unsat | 0 | | | |ring_2exp4_9vars_3ite_unsat.smt2 | 0.932s | 22.004MiB| unsat | 0 | | | |ring_2exp10_9vars_2ite_unsat.smt2 | 1.034s | 21.768MiB| unsat | 0 | | | |ring_2exp8_5vars_4ite_unsat.smt2 | 1.156s | 21.228MiB| unsat | 0 | | | |ring_2exp10_5vars_4ite_unsat.smt2 | 1.234s | 21.2MiB| unsat | 0 | | | |ring_2exp10_9vars_3ite_unsat.smt2 | 1.312s | 22.288MiB| unsat | 0 | | | |ring_2exp16_9vars_3ite_unsat.smt2 | 1.322s | 21.908MiB| unsat | 0 | | | |ring_2exp14_6vars_4ite_unsat.smt2 | 1.397s | 21.536MiB| unsat | 0 | | | |ring_2exp14_9vars_3ite_unsat.smt2 | 1.421s | 21.832MiB| unsat | 0 | | | |ring_2exp14_7vars_4ite_unsat.smt2 | 1.454s | 21.536MiB| unsat | 0 | | | |ring_2exp10_7vars_3ite_unsat.smt2 | 1.466s | 22.036MiB| unsat | 0 | | | |ring_2exp4_7vars_4ite_unsat.smt2 | 1.469s | 21.548MiB| unsat | 0 | | | |ring_2exp16_7vars_4ite_unsat.smt2 | 1.636s | 21.648MiB| unsat | 0 | | | |ring_2exp4_5vars_4ite_unsat.smt2 | 1.707s | 21.24MiB| unsat | 0 | | | |ring_2exp8_9vars_3ite_unsat.smt2 | 1.760s | 22.568MiB| unsat | 0 | | | |ring_2exp10_8vars_4ite_unsat.smt2 | 1.834s | 22.088MiB| unsat | 0 | | | |ring_2exp4_6vars_4ite_unsat.smt2 | 1.928s | 21.688MiB| unsat | 0 | | | |ring_2exp12_9vars_3ite_unsat.smt2 | 1.940s | 22.772MiB| unsat | 0 | | | |ring_2exp16_6vars_4ite_unsat.smt2 | 1.949s | 21.544MiB| unsat | 0 | | | |ring_2exp12_6vars_4ite_unsat.smt2 | 2.100s | 21.676MiB| unsat | 0 | | | |ring_2exp6_9vars_3ite_unsat.smt2 | 2.101s | 22.616MiB| unsat | 0 | | | |ring_2exp4_8vars_4ite_unsat.smt2 | 2.113s | 22.092MiB| unsat | 0 | | | |ring_2exp6_5vars_4ite_unsat.smt2 | 2.311s | 21.644MiB| unsat | 0 | | | |ring_2exp8_8vars_3ite_unsat.smt2 | 2.397s | 22.712MiB| unsat | 0 | | | |ring_2exp4_6vars_5ite_unsat.smt2 | 2.576s | 21.7MiB| unsat | 0 | | | |ring_2exp4_9vars_4ite_unsat.smt2 | 2.668s | 22.424MiB| unsat | 0 | | | |ring_2exp10_6vars_4ite_unsat.smt2 | 2.691s | 22.348MiB| unsat | 0 | | | |ring_2exp16_8vars_4ite_unsat.smt2 | 3.171s | 22.196MiB| unsat | 0 | | | |ring_2exp8_6vars_4ite_unsat.smt2 | 3.234s | 22.128MiB| unsat | 0 | | | |ring_2exp14_9vars_4ite_unsat.smt2 | 3.272s | 22.568MiB| unsat | 0 | | | |ring_2exp12_8vars_4ite_unsat.smt2 | 3.385s | 22.804MiB| unsat | 0 | | | |ring_2exp6_8vars_4ite_unsat.smt2 | 3.678s | 22.668MiB| unsat | 0 | | | |ring_2exp4_7vars_5ite_unsat.smt2 | 3.799s | 22.208MiB| unsat | 0 | | | |ring_2exp12_7vars_4ite_unsat.smt2 | 3.838s | 22.868MiB| unsat | 0 | | | |ring_2exp14_8vars_4ite_unsat.smt2 | 4.285s | 23.22MiB| unsat | 0 | | | |ring_2exp14_6vars_5ite_unsat.smt2 | 4.299s | 22.028MiB| unsat | 0 | | | |ring_2exp10_9vars_4ite_unsat.smt2 | 4.435s | 23.232MiB| unsat | 0 | | | |ring_2exp4_9vars_5ite_unsat.smt2 | 4.827s | 22.716MiB| unsat | 0 | | | |ring_2exp12_6vars_5ite_unsat.smt2 | 5.019s | 22.604MiB| unsat | 0 | | | |ring_2exp6_9vars_4ite_unsat.smt2 | 11.387s | 23.1MiB| unsat | 0 | | | |ring_2exp10_7vars_4ite_unsat.smt2 | 12.403s | 23.508MiB| unsat | 0 | | | |ring_2exp6_6vars_4ite_unsat.smt2 | 12.958s | 24.156MiB| unsat | 0 | | | |ring_2exp16_9vars_4ite_unsat.smt2 | 13.634s | 23.956MiB| unsat | 0 | | | |ring_2exp8_8vars_4ite_unsat.smt2 | 13.975s | 24.328MiB| unsat | 0 | | | |ring_2exp16_7vars_5ite_unsat.smt2 | 15.447s | 24.4MiB| unsat | 0 | | | |ring_2exp10_7vars_5ite_unsat.smt2 | 15.636s | 24.916MiB| unsat | 0 | | | |ring_2exp16_6vars_5ite_unsat.smt2 | 16.045s | 24.392MiB| unsat | 0 | | | |ring_2exp4_8vars_5ite_unsat.smt2 | 16.065s | 23.64MiB| unsat | 0 | | | |ring_2exp6_7vars_4ite_unsat.smt2 | 16.346s | 24.328MiB| unsat | 0 | | | |ring_2exp6_7vars_5ite_unsat.smt2 | 16.375s | 24.94MiB| unsat | 0 | | | |ring_2exp8_7vars_4ite_unsat.smt2 | 16.425s | 24.82MiB| unsat | 0 | | | |ring_2exp10_6vars_5ite_unsat.smt2 | 16.933s | 24.752MiB| unsat | 0 | | | |ring_2exp12_7vars_5ite_unsat.smt2 | 17.886s | 24.912MiB| unsat | 0 | | | |ring_2exp8_6vars_5ite_unsat.smt2 | 19.053s | 24.884MiB| unsat | 0 | | | |ring_2exp12_9vars_4ite_unsat.smt2 | 19.823s | 25.612MiB| unsat | 0 | | | |ring_2exp12_8vars_5ite_unsat.smt2 | 20.168s | 25.4MiB| unsat | 0 | | | |ring_2exp8_8vars_5ite_unsat.smt2 | 21.020s | 25.144MiB| unsat | 0 | | | |ring_2exp6_6vars_5ite_unsat.smt2 | 21.949s | 24.648MiB| unsat | 0 | | | |ring_2exp14_7vars_5ite_unsat.smt2 | 22.871s | 26.056MiB| unsat | 0 | | | |ring_2exp8_9vars_4ite_unsat.smt2 | 26.428s | 27.544MiB| unsat | 0 | | | |ring_2exp8_7vars_5ite_unsat.smt2 | 27.075s | 25.956MiB| unsat | 0 | | | |ring_2exp16_8vars_5ite_unsat.smt2 | 27.561s | 26.076MiB| unsat | 0 | | | |ring_2exp14_8vars_5ite_unsat.smt2 | 27.696s | 26.164MiB| unsat | 0 | | | |ring_2exp10_8vars_5ite_unsat.smt2 | 28.335s | 26.456MiB| unsat | 0 | | | |ring_2exp16_9vars_5ite_unsat.smt2 | 28.467s | 26.588MiB| unsat | 0 | | | |ring_2exp6_9vars_5ite_unsat.smt2 | 28.571s | 26.156MiB| unsat | 0 | | | |ring_2exp8_9vars_5ite_unsat.smt2 | 28.623s | 27.372MiB| unsat | 0 | | | |ring_2exp12_9vars_5ite_unsat.smt2 | 28.880s | 26.912MiB| unsat | 0 | | | |ring_2exp14_9vars_5ite_unsat.smt2 | 28.979s | 26.116MiB| unsat | 0 | | | |ring_2exp10_9vars_5ite_unsat.smt2 | 29.714s | 27.36MiB| unsat | 0 | | | |ring_2exp12_7vars_6ite_unsat.smt2 | 45.992s | 25.624MiB| unsat | 0 | | | |ring_2exp16_7vars_6ite_unsat.smt2 | 46.973s | 25.912MiB| unsat | 0 | | | |ring_2exp8_7vars_6ite_unsat.smt2 | 47.891s | 26.848MiB| unsat | 0 | | | |ring_2exp6_7vars_6ite_unsat.smt2 | 47.923s | 25.848MiB| unsat | 0 | | | |ring_2exp14_7vars_6ite_unsat.smt2 | 48.733s | 25.572MiB| unsat | 0 | | | |ring_2exp10_7vars_6ite_unsat.smt2 | 48.852s | 26.684MiB| unsat | 0 | | | |ring_2exp12_8vars_6ite_unsat.smt2 | 67.912s | 26.272MiB| unsat | 0 | | | |ring_2exp6_9vars_6ite_unsat.smt2 | 69.499s | 26.672MiB| unsat | 0 | | | |ring_2exp14_8vars_6ite_unsat.smt2 | 70.974s | 26.328MiB| unsat | 0 | | | |ring_2exp16_8vars_6ite_unsat.smt2 | 71.768s | 26.336MiB| unsat | 0 | | | |ring_2exp8_8vars_6ite_unsat.smt2 | 73.440s | 26.988MiB| unsat | 0 | | | |ring_2exp10_8vars_6ite_unsat.smt2 | 74.687s | 26.948MiB| unsat | 0 | | | |ring_2exp14_9vars_6ite_unsat.smt2 | 75.324s | 27.476MiB| unsat | 0 | | | |ring_2exp8_9vars_6ite_unsat.smt2 | 78.176s | 27.568MiB| unsat | 0 | | | |ring_2exp16_9vars_6ite_unsat.smt2 | 81.799s | 27.376MiB| unsat | 0 | | | |ring_2exp12_9vars_6ite_unsat.smt2 | 85.377s | 27.432MiB| unsat | 0 | | | |ring_2exp4_8vars_6ite_unsat.smt2 | 89.399s | 26.084MiB| unsat | 0 | | | |ring_2exp6_8vars_6ite_unsat.smt2 | 90.968s | 27.136MiB| unsat | 0 | | | |ring_2exp10_9vars_6ite_unsat.smt2 | 91.634s | 29.492MiB| unsat | 0 | | | |ring_2exp10_8vars_7ite_unsat.smt2 | 107.344s | 27.4MiB| unsat | 0 | | | |ring_2exp8_8vars_7ite_unsat.smt2 | 110.929s | 28.416MiB| unsat | 0 | | | |ring_2exp12_8vars_7ite_unsat.smt2 | 113.270s | 27.48MiB| unsat | 0 | | | |ring_2exp16_8vars_7ite_unsat.smt2 | 121.431s | 27.432MiB| unsat | 0 | | | |ring_2exp14_8vars_7ite_unsat.smt2 | 122.216s | 28.136MiB| unsat | 0 | | | |ring_2exp14_9vars_7ite_unsat.smt2 | 143.606s | 28.756MiB| unsat | 0 | | | |ring_2exp10_9vars_7ite_unsat.smt2 | 144.722s | 30.124MiB| unsat | 0 | | | |ring_2exp8_9vars_7ite_unsat.smt2 | 146.890s | 31.04MiB| unsat | 0 | | | |ring_2exp12_9vars_7ite_unsat.smt2 | 147.861s | 29.476MiB| unsat | 0 | | | |ring_2exp16_9vars_7ite_unsat.smt2 | 157.482s | 29.324MiB| unsat | 0 | | | |ring_2exp4_8vars_7ite_unsat.smt2 | 166.669s | 28.94MiB| unsat | 0 | | | |ring_2exp4_9vars_7ite_unsat.smt2 | 298.197s | 30.0MiB| unsat | 0 | | | |ring_2exp4_7vars_6ite_unsat.smt2 | 495.639s | 45.404MiB| unsat | 0 | | | |ring_2exp6_8vars_7ite_unsat.smt2 | 599.921s | 39.752MiB| timeout | 0 | | | |ring_2exp16_9vars_8ite_unsat.smt2 | 599.935s | 42.824MiB| timeout | 0 | | | |ring_2exp4_9vars_8ite_unsat.smt2 | 599.939s | 37.992MiB| timeout | 0 | | | |ring_2exp4_9vars_6ite_unsat.smt2 | 599.941s | 38.08MiB| timeout | 0 | | | |ring_2exp6_9vars_7ite_unsat.smt2 | 599.944s | 46.856MiB| timeout | 0 | | | |ring_2exp6_8vars_5ite_unsat.smt2 | 599.945s | 38.18MiB| timeout | 0 | | | |ring_2exp6_9vars_8ite_unsat.smt2 | 599.946s | 42.104MiB| timeout | 0 | | | |ring_2exp10_9vars_8ite_unsat.smt2 | 599.951s | 52.084MiB| timeout | 0 | | | |ring_2exp14_9vars_8ite_unsat.smt2 | 599.953s | 41.34MiB| timeout | 0 | | | |ring_2exp8_9vars_8ite_unsat.smt2 | 599.957s | 46.552MiB| timeout | 0 | | | |ring_2exp12_9vars_8ite_unsat.smt2 | 599.961s | 46.144MiB| timeout | 0 | | |