This is the companion web site for a paper on Efficient Certified RAT Verification: paper.pdf
The source code of all executables is available: Coq checker, ACL2 checker, drat-trim, CryptoMiniSat v5
To replicate the experiments, download, compile, and install all executables in a suitable directory $BIN. Then, for each example $EXAMPLE, execute this Bash script: verify.sh.
The SAT instances used are available from the competition website: 2016/app (1.6 GByte), 2016/crafted (0.9 GBytes), 2015/main (0.6 GByte), 2015/parallel (0.3 Gbyte)
The following table presents detailed runtimes on the set of 241 unsatisfiable (within 5000 seconds on Abacus 2.0) instances. For each instance the original CNF, the DRAT and LRAT proofs as well as all the log files (click on the runtimes) can be accessed. The columns can be sorted by clicking the headers (click twice for reverse sort). Beware that some downloads are huge (some more than 1 GByte). Success results are given in green, failures in red, time-outs in red, and errors in blue.
Instance | cmsat5 | drat-trim | coq checker | acl2 checker |
---|---|---|---|---|
2015/main/manthey_single-ordered-initialized-w24-b9 (cnf) (drat) (lrat) | 0.78 | 0.69 | 1.43 | 0.33 |
2015/main/dated-5-13-u (cnf) (drat) (lrat) | 1711.22 | 4550.49 | 86400 (TIME) | 454.57 |
2015/main/dated-10-17-u (cnf) (drat) (lrat) | 2128.51 | 5402.62 | 86400 (TIME) | 443.92 |
2015/main/6s165-nonopt (cnf) (drat) (lrat) | 13.84 | 7.11 | 10.00 | 1.64 |
2015/main/7pipe_k (cnf) (drat) (lrat) | 178.36 | 542.26 | 20411.37 | 184.46 |
2015/main/manthey_single-ordered-initialized-w44-b8 (cnf) (drat) (lrat) | 363.26 | 543.58 | 7745.33 | 79.75 |
2015/main/6s16 (cnf) (drat) (lrat) | 330.34 | 366.39 | 4484.84 | 36.88 |
2015/main/9dlx_vliw_at_b_iq8.used-as.sat04-718 (cnf) (drat) (lrat) | 878.38 | 8194.64 | 86400 (TIME) | 1154.02 |
2015/main/atco_enc1_opt2_20_12 (cnf) (drat) (lrat) | 2282.45 | 1718.95 | 10109.99 | 115.22 |
2015/main/hitag2-8-60-0-0x1eb82244d7f1c3c-47 (cnf) (drat) (lrat) | 4260.83 | 5208.76 | 16405.45 (ERROR) | 622.23 |
2015/main/beempgsol5b1 (cnf) (drat) (lrat) | 83.82 | 49.90 | 530.84 | 7.48 |
2015/main/6s13-opt (cnf) (drat) (lrat) | 304.68 | 383.26 | 6141.31 | 41.01 |
2015/main/6s133 (cnf) (drat) (lrat) | 249.72 | 264.36 | 7594.09 | 42.25 |
2015/main/10pipe_q0_k (cnf) (drat) (lrat) | 1462.93 | 4539.33 | 86400 (TIME) | 1737.84 |
2015/main/6s9 (cnf) (drat) (lrat) | 345.47 | 401.92 | 5024.76 | 40.99 |
2015/main/aaai10-planning-ipc5-pathways-13-step17 (cnf) (drat) (lrat) | 85.69 | 235.10 | 2143.87 | 34.27 |
2015/main/aaai10-planning-ipc5-pathways-17-step20 (cnf) (drat) (lrat) | 76.70 | 416.88 | 2747.75 | 27.32 |
2015/main/atco_enc1_opt2_10_14 (cnf) (drat) (lrat) | 351.54 | 503.55 | 4541.65 | 56.54 |
2015/main/6s11-opt (cnf) (drat) (lrat) | 398.98 | 399.12 | 4103.16 | 38.04 |
2015/main/6s130-opt (cnf) (drat) (lrat) | 304.25 | 281.83 | 6714.51 | 43.18 |
2015/main/k2fix_gr_rcs_w9.shuffled (cnf) (drat) (lrat) | 37.13 | 40.50 | 115.14 | 7.73 |
2015/main/bob12m02-opt (cnf) (drat) (lrat) | 1537.27 | 948.14 | 4383.39 | 26.32 |
2015/main/6s168-opt (cnf) (drat) (lrat) | 31.87 | 14.09 | 45.19 | 3.16 |
2015/main/6s16-opt (cnf) (drat) (lrat) | 386.26 | 372.58 | 3448.13 | 34.76 |
2015/main/manthey_single-ordered-initialized-w40-b10 (cnf) (drat) (lrat) | 85.06 | 114.43 | 1318.87 | 21.38 |
2015/main/aaai10-planning-ipc5-TPP-21-step11 (cnf) (drat) (lrat) | 339.29 | 1913.44 | 19228.79 (FAIL) | 66.81 (FAIL) |
2015/main/ACG-15-10p0 (cnf) (drat) (lrat) | 315.50 | 2491.63 | 45315.43 | 248.39 |
2015/main/6s17-opt (cnf) (drat) (lrat) | 319.09 | 340.31 | 5610.59 | 38.45 |
2015/main/ACG-20-5p0 (cnf) (drat) (lrat) | 263.55 | 2195.64 | 29654.28 (FAIL) | 125.27 (FAIL) |
2015/main/bjrb07amba10andenv (cnf) (drat) (lrat) | 420.01 | 2107.70 | 86400 (TIME) | 433.92 |
2015/main/post-cbmc-aes-ee-r2-noholes (cnf) (drat) (lrat) | 149.63 | 728.14 | 82208.09 | 165.22 |
2015/main/countbitssrl032 (cnf) (drat) (lrat) | 341.52 | 605.53 | 34202.13 | 150.66 |
2015/main/jgiraldezlevy.2200.9086.08.40.109 (cnf) (drat) (lrat) | 1275.22 | 1667.06 | 23874.55 | 181.49 |
2015/main/hitag2-10-60-0-0x8edc44db7837bbf-65 (cnf) (drat) (lrat) | 4735.28 | 5586.10 | 16227.20 (ERROR) | 667.25 |
2015/main/jgiraldezlevy.2200.9086.08.40.135 (cnf) (drat) (lrat) | 3052.78 | 2525.37 | 86400 (TIME) | 446.14 |
2015/main/bob12m09-opt (cnf) (drat) (lrat) | 212.76 | 442.52 | 10626.28 | 62.00 |
2015/main/jgiraldezlevy.2200.9086.08.40.46 (cnf) (drat) (lrat) | 624.38 | 739.02 | 10567.26 | 103.85 |
2015/main/jgiraldezlevy.2200.9086.08.40.108 (cnf) (drat) (lrat) | 4136.43 | 3345.95 | 86400 (TIME) | 516.25 |
2015/main/dated-10-13-u (cnf) (drat) (lrat) | 144.54 | 964.55 | 8191.85 | 73.01 |
2015/main/group_mulr (cnf) (drat) (lrat) | 699.22 | 31.07 | 540.13 | 14.23 |
2015/main/6s131-opt (cnf) (drat) (lrat) | 279.06 | 238.93 | 5904.63 | 38.30 |
2015/main/hwmcc10-timeframe-expansion-k50-pdtpmsns2-tseitin (cnf) (drat) (lrat) | 353.00 | 664.16 | 30078.89 | 114.50 |
2015/main/manthey_single-ordered-initialized-w20-b7 (cnf) (drat) (lrat) | 0.22 | 0.23 | 0.47 | 0.14 |
2015/main/6s167-opt (cnf) (drat) (lrat) | 56.76 | 38.80 | 97.74 | 6.97 |
2015/main/6s169-opt (cnf) (drat) (lrat) | 164.98 | 104.10 | 417.04 | 15.05 |
2015/main/manthey_single-ordered-initialized-w28-b8 (cnf) (drat) (lrat) | 2.87 | 2.64 | 5.68 | 1.06 |
2015/main/manthey_single-ordered-initialized-w50-b6 (cnf) (drat) (lrat) | 327.06 | 561.92 | 7774.95 | 80.05 |
2015/main/manthey_single-ordered-initialized-w44-b9 (cnf) (drat) (lrat) | 352.44 | 541.58 | 7774.55 | 79.34 |
2015/main/manthey_single-ordered-initialized-w48-b9 (cnf) (drat) (lrat) | 1148.06 | 1715.72 | 44318.61 | 251.53 |
2015/main/manthey_single-ordered-initialized-w18-b7 (cnf) (drat) (lrat) | 0.12 | 0.14 | 0.21 | 0.09 |
2015/main/manthey_single-ordered-initialized-w40-b8 (cnf) (drat) (lrat) | 116.72 | 162.84 | 1701.75 | 29.36 |
2015/main/manthey_single-ordered-initialized-w24-b7 (cnf) (drat) (lrat) | 0.66 | 0.64 | 1.33 | 0.31 |
2015/main/manthey_single-ordered-initialized-w46-b9 (cnf) (drat) (lrat) | 728.64 | 1137.85 | 22725.41 | 154.29 |
2015/main/manthey_single-ordered-initialized-w52-b6 (cnf) (drat) (lrat) | 541.04 | 777.34 | 15455.43 | 127.36 |
2015/main/manthey_single-ordered-initialized-w42-b8 (cnf) (drat) (lrat) | 203.69 | 291.96 | 3431.86 | 47.11 |
2015/main/manthey_single-ordered-initialized-w46-b8 (cnf) (drat) (lrat) | 589.42 | 766.40 | 15672.45 | 134.53 |
2015/main/AProVE07-03 (cnf) (drat) (lrat) | 188.23 | 272.64 | 5287.02 | 57.80 |
2015/main/post-c32s-ss-8 (cnf) (drat) (lrat) | 126.56 | 121.30 | 1812.59 | 15.07 |
2015/main/q_query_3_L80_coli.sat (cnf) (drat) (lrat) | 60.62 | 572.95 | 7958.01 | 29.48 |
2015/main/q_query_3_L150_coli.sat (cnf) (drat) (lrat) | 296.74 | 2630.55 | 67010.25 | 176.76 |
2015/main/atco_enc2_opt2_20_11 (cnf) (drat) (lrat) | 596.96 | 523.85 | 2923.39 | 54.88 |
2015/main/atco_enc3_opt2_10_12 (cnf) (drat) (lrat) | 443.36 | 588.82 | 1135.57 | 27.11 |
2015/main/bob12s02 (cnf) (drat) (lrat) | 510.42 | 437.84 | 2630.14 | 14.74 |
2015/main/AProVE07-27 (cnf) (drat) (lrat) | 421.32 | 1040.83 | 66052.93 | 276.30 |
2015/main/post-cbmc-aes-d-r2 (cnf) (drat) (lrat) | 117.55 | 1326.41 | 86400 (TIME) | 334.26 |
2015/main/SAT_dat.k95-24_1_rule_3 (cnf) (drat) (lrat) | 3334.10 | 20000 (TIME) | (NO RUN) | (NO RUN) |
2015/main/SAT_dat.k90.debugged (cnf) (drat) (lrat) | 2930.81 | 20000 (TIME) | (NO RUN) | (NO RUN) |
2015/main/SAT_dat.k70-24_1_rule_3 (cnf) (drat) (lrat) | 1235.11 | 20000 (TIME) | (NO RUN) | (NO RUN) |
2015/main/velev-vliw-uns-4.0-9-i1 (cnf) (drat) (lrat) | 417.03 | 2396.14 | 86400 (TIME) | 368.47 |
2015/main/UR-20-10p0 (cnf) (drat) (lrat) | 1006.32 | 7879.64 | 86400 (TIME) | 692.30 (FAIL) |
2015/main/beempgsol2b1 (cnf) (drat) (lrat) | 92.74 | 55.00 | 626.25 | 8.04 |
2015/main/atco_enc3_opt2_10_14 (cnf) (drat) (lrat) | 552.55 | 688.82 | 1322.80 | 31.16 |
2015/main/manthey_single-ordered-initialized-w18-b8 (cnf) (drat) (lrat) | 0.14 | 0.14 | 0.27 | 0.10 |
2015/main/manthey_single-ordered-initialized-w26-b8 (cnf) (drat) (lrat) | 1.40 | 1.20 | 2.48 | 0.55 |
2015/main/manol-pipe-c10nid_i (cnf) (drat) (lrat) | 143.82 | 888.01 | 25395.20 | 85.41 |
2015/main/manthey_single-ordered-initialized-w22-b8 (cnf) (drat) (lrat) | 0.39 | 0.36 | 0.82 | 0.20 |
2015/main/manthey_single-ordered-initialized-w48-b6 (cnf) (drat) (lrat) | 223.30 | 362.46 | 4381.83 | 54.74 |
2015/main/manthey_single-ordered-initialized-w20-b8 (cnf) (drat) (lrat) | 0.23 | 0.24 | 0.52 | 0.14 |
2015/main/manthey_single-ordered-initialized-w32-b9 (cnf) (drat) (lrat) | 11.75 | 13.11 | 66.24 | 2.89 |
2015/main/manthey_single-ordered-initialized-w22-b6 (cnf) (drat) (lrat) | 0.32 | 0.32 | 0.70 | 0.19 |
2015/main/manthey_single-ordered-initialized-w26-b7 (cnf) (drat) (lrat) | 1.56 | 1.49 | 2.89 | 0.65 |
2015/main/manthey_single-ordered-initialized-w42-b9 (cnf) (drat) (lrat) | 175.40 | 253.70 | 3142.20 | 41.53 |
2015/main/manthey_single-ordered-initialized-w44-b6 (cnf) (drat) (lrat) | 90.88 | 140.40 | 1394.39 | 25.00 |
2015/main/manthey_single-ordered-initialized-w50-b7 (cnf) (drat) (lrat) | 1057.58 | 1496.28 | 39141.28 | 253.40 |
2015/main/minxorminand064 (cnf) (drat) (lrat) | 184.83 | 521.60 | 35061.91 | 151.15 |
2015/main/manthey_single-ordered-initialized-w46-b7 (cnf) (drat) (lrat) | 352.89 | 564.98 | 8046.43 | 82.05 |
2015/main/manthey_single-ordered-initialized-w44-b7 (cnf) (drat) (lrat) | 216.13 | 305.71 | 4061.74 | 51.85 |
2015/main/manthey_single-ordered-initialized-w48-b7 (cnf) (drat) (lrat) | 620.63 | 1004.31 | 18298.23 | 142.48 |
2015/main/minandmaxor128 (cnf) (drat) (lrat) | 3304.40 | 6966.56 | 86400 (TIME) | 1902.33 |
2015/main/velev-vliw-uns-2.0-uq5 (cnf) (drat) (lrat) | 254.94 | 2999.63 | 86400 (TIME) | 437.71 |
2015/main/UCG-20-5p0 (cnf) (drat) (lrat) | 110.00 | 419.30 | 5886.52 | 40.40 |
2015/main/SAT_dat.k85-24_1_rule_3 (cnf) (drat) (lrat) | 2473.49 | 20000 (TIME) | (NO RUN) | (NO RUN) |
2015/main/post-cbmc-aes-d-r2-noholes (cnf) (drat) (lrat) | 145.53 | 914.35 | 86400 (TIME) | 216.54 |
2015/main/SAT_dat.k80-24_1_rule_1 (cnf) (drat) (lrat) | 2241.44 | 20000 (TIME) | (NO RUN) | (NO RUN) |
2015/main/q_query_3_L200_coli.sat (cnf) (drat) (lrat) | 249.61 | 1453.31 | 9670.47 | 39.69 |
2015/main/UCG-20-10p0 (cnf) (drat) (lrat) | 506.83 | 8253.63 | 86400 (TIME) | 1301.94 |
2015/parallel/SAT_dat.k70-24_1_rule_3 (cnf) (drat) (lrat) | 1147.71 | 20000 (TIME) | (NO RUN) | (NO RUN) |
2015/parallel/6s17-opt (cnf) (drat) (lrat) | 320.42 | 339.24 | 5612.98 | 38.40 |
2015/parallel/jgiraldezlevy.2200.9086.08.40.135 (cnf) (drat) (lrat) | 3013.09 | 2477.63 | 86400 (TIME) | 446.70 |
2015/parallel/dated-10-17-u (cnf) (drat) (lrat) | 2081.00 | 5921.71 | 84667.48 | 442.59 |
2015/parallel/jgiraldezlevy.2200.9086.08.40.46 (cnf) (drat) (lrat) | 624.14 | 718.62 | 10591.20 | 103.58 |
2015/parallel/group_mulr (cnf) (drat) (lrat) | 698.13 | 31.22 | 528.96 | 14.18 |
2015/parallel/jgiraldezlevy.2200.9086.08.40.109 (cnf) (drat) (lrat) | 1298.09 | 1577.73 | 24274.55 | 179.58 |
2015/parallel/6s16-opt (cnf) (drat) (lrat) | 385.05 | 375.35 | 3441.48 | 34.78 |
2015/parallel/atco_enc1_opt2_20_12 (cnf) (drat) (lrat) | 2281.60 | 1435.66 | 10156.90 | 120.01 |
2015/parallel/9dlx_vliw_at_b_iq8.used-as.sat04-718 (cnf) (drat) (lrat) | 876.59 | 8304.15 | 86400 (TIME) | 1157.25 |
2015/parallel/SAT_dat.k90.debugged (cnf) (drat) (lrat) | 2890.55 | 20000 (TIME) | (NO RUN) | (NO RUN) |
2015/parallel/SAT_dat.k80-24_1_rule_1 (cnf) (drat) (lrat) | 2285.24 | 20000 (TIME) | (NO RUN) | (NO RUN) |
2015/parallel/UR-20-10p0 (cnf) (drat) (lrat) | 989.38 | 8152.12 | 86400 (TIME) | 685.30 (FAIL) |
2015/parallel/bob12m02-opt (cnf) (drat) (lrat) | 1536.26 | 911.55 | 4399.07 | 26.16 |
2015/parallel/manthey_single-ordered-initialized-w50-b7 (cnf) (drat) (lrat) | 1076.95 | 1745.22 | 39229.40 | 243.89 |
2015/parallel/dated-5-13-u (cnf) (drat) (lrat) | 1718.44 | 4439.18 | 86400 (TIME) | 454.80 |
2015/parallel/hitag2-8-60-0-0x1eb82244d7f1c3c-47 (cnf) (drat) (lrat) | 4281.02 | 5780.91 | 16347.91 (ERROR) | 610.04 |
2015/parallel/6s13-opt (cnf) (drat) (lrat) | 304.44 | 383.13 | 6154.10 | 40.73 |
2015/parallel/manthey_single-ordered-initialized-w48-b9 (cnf) (drat) (lrat) | 1124.01 | 1723.02 | 44858.16 | 267.58 |
2015/parallel/6s130-opt (cnf) (drat) (lrat) | 298.61 | 281.99 | 6865.57 | 43.60 |
2015/parallel/hitag2-10-60-0-0x8edc44db7837bbf-65 (cnf) (drat) (lrat) | 4771.27 | 5887.64 | 16181.89 (ERROR) | 662.18 |
2015/parallel/SAT_dat.k95-24_1_rule_3 (cnf) (drat) (lrat) | 3570.71 | 20000 (TIME) | (NO RUN) | (NO RUN) |
2015/parallel/minandmaxor128 (cnf) (drat) (lrat) | 3362.06 | 6899.13 | 86400 (TIME) | 2091.32 |
2015/parallel/jgiraldezlevy.2200.9086.08.40.108 (cnf) (drat) (lrat) | 4187.30 | 4084.75 | 86400 (TIME) | 524.59 |
2015/parallel/SAT_dat.k85-24_1_rule_3 (cnf) (drat) (lrat) | 2533.17 | 20000 (TIME) | (NO RUN) | (NO RUN) |
2016/crafted/peb-pyrofpyr-11-neq-3_shuffled (cnf) (drat) (lrat) | 44.37 | 1016.65 | 69286.79 | 701.75 |
2016/crafted/peb-pyrofpyr-12-neq-3_shuffled (cnf) (drat) (lrat) | 68.28 | 2326.65 | 86400 (TIME) | 1438.32 |
2016/crafted/rphp4_065_shuffled (cnf) (drat) (lrat) | 2250.64 | 1256.33 | 66614.46 (ERROR) | 509.93 |
2016/crafted/Schur_161_5_d42 (cnf) (drat) (lrat) | 1174.97 | 691.09 | 20686.20 | 153.62 |
2016/crafted/Schur_161_5_d43 (cnf) (drat) (lrat) | 462.39 | 288.88 | 7106.42 | 81.01 |
2016/crafted/stone-width3chain-nmarkers-08_shuffled (cnf) (drat) (lrat) | 51.03 | 56.45 | 1069.47 | 7.24 |
2016/crafted/ecgrid6x210_shuffled (cnf) (drat) (lrat) | 4808.28 | 253.54 | 899.17 | 20.70 |
2016/crafted/peb-pyrofpyr-13-neq-3_shuffled (cnf) (drat) (lrat) | 99.62 | 4644.33 | 86400 (TIME) | 2413.95 |
2016/crafted/peb-pyrofpyr-14-neq-3_shuffled (cnf) (drat) (lrat) | 155.01 | 8567.68 | 86400 (TIME) | 4226.44 |
2016/crafted/peb-pyrofpyr-15-neq-3_shuffled (cnf) (drat) (lrat) | 227.93 | 14004.52 | 86400 (TIME) | 6707.85 |
2016/crafted/pop90_shuffled (cnf) (drat) (lrat) | 12.27 | 3.97 | 29.62 | 2.97 |
2016/crafted/pop93_shuffled (cnf) (drat) (lrat) | 871.24 | 167.44 | 2922.48 | 51.77 |
2016/crafted/pop99_shuffled (cnf) (drat) (lrat) | 1057.99 | 203.46 | 3522.38 | 56.16 |
2016/crafted/stone-width3chain-nmarkers-10_shuffled (cnf) (drat) (lrat) | 128.95 | 199.42 | 1518.73 | 14.08 |
2016/crafted/stone-width3chain-nmarkers-11_shuffled (cnf) (drat) (lrat) | 200.38 | 383.93 | 3604.55 | 21.78 |
2016/crafted/stone-width3chain-nmarkers-12_shuffled (cnf) (drat) (lrat) | 386.22 | 755.03 | 26928.70 | 35.54 |
2016/crafted/stone-width3chain-nmarkers-13_shuffled (cnf) (drat) (lrat) | 601.05 | 1153.94 | 86400 (TIME) | 150.21 |
2016/crafted/stone-width3chain-nmarkers-14_shuffled (cnf) (drat) (lrat) | 913.33 | 1537.06 | 86400 (TIME) | 98.90 |
2016/crafted/stone-width3chain-nmarkers-15_shuffled (cnf) (drat) (lrat) | 1480.60 | 3336.71 | 86400 (TIME) | 234.77 |
2016/crafted/stone-width3chain-nmarkers-16_shuffled (cnf) (drat) (lrat) | 2471.07 | 4508.13 | 86400 (TIME) | 282.42 |
2016/crafted/stone-width3chain-nmarkers-17_shuffled (cnf) (drat) (lrat) | 3340.58 | 4458.70 | 86400 (TIME) | 409.39 |
2016/crafted/tseitingrid4x185_shuffled (cnf) (drat) (lrat) | 27.81 | 9.84 | 35.34 | 3.39 |
2016/crafted/tseitingrid4x190_shuffled (cnf) (drat) (lrat) | 27.54 | 9.64 | 30.94 | 3.20 |
2016/crafted/tseitingrid4x195_shuffled (cnf) (drat) (lrat) | 27.64 | 9.34 | 31.34 | 3.28 |
2016/crafted/tseitingrid4x200_shuffled (cnf) (drat) (lrat) | 37.67 | 12.08 | 38.70 | 3.58 |
2016/crafted/stone-width3chain-nmarkers-09_shuffled (cnf) (drat) (lrat) | 84.53 | 109.81 | 1013.25 | 10.73 |
2016/app/AProVE11-06 (cnf) (drat) (lrat) | 1944.73 | 2291.16 | 63973.79 (FAIL) | 135.65 (FAIL) |
2016/app/9dlx_vliw_at_b_iq4.used-as.sat04-345 (cnf) (drat) (lrat) | 181.61 | 2203.37 | 86400 (TIME) | 464.68 |
2016/app/9dlx_vliw_at_b_iq9.used-as.sat04-719 (cnf) (drat) (lrat) | 1362.52 | 11029.16 | 86400 (TIME) | 1545.30 |
2016/app/ACG-20-10p0 (cnf) (drat) (lrat) | 717.07 | 11826.32 | 86400 (TIME) | 1539.36 (FAIL) |
2016/app/E00N23 (cnf) (drat) (lrat) | 3318.65 | 2766.74 | 86400 (TIME) | 639.67 |
2016/app/9dlx_vliw_at_b_iq8.used-as.sat04-718 (cnf) (drat) (lrat) | 871.84 | 8269.31 | 86400 (TIME) | 1152.12 |
2016/app/Sz512_15127_3.smt2-cvc4 (cnf) (drat) (lrat) | 201.24 | 379.58 | 4020.70 | 48.77 |
2016/app/UR-15-10p0 (cnf) (drat) (lrat) | 158.91 | 1549.04 | 26203.27 | 156.85 |
2016/app/ablmulub16x4o (cnf) (drat) (lrat) | 336.60 | 858.26 | 25959.94 | 191.27 |
2016/app/ablmulub2x32o (cnf) (drat) (lrat) | 556.27 | 1737.80 | 86400 (TIME) | 433.53 |
2016/app/add_01_1000_4.smt2-cvc4 (cnf) (drat) (lrat) | 10.83 | 14.02 | 129.12 | 4.39 |
2016/app/ak016modbtsimpbisc (cnf) (drat) (lrat) | 2642.94 | 1421.63 | 15791.01 | 122.40 |
2016/app/ak032diagodiagoisc (cnf) (drat) (lrat) | 850.99 | 277.61 | 2784.43 | 23.71 |
2016/app/ak032modbtmodbtisc (cnf) (drat) (lrat) | 2962.26 | 936.80 | 11939.45 | 75.50 |
2016/app/ak064paralparalisc (cnf) (drat) (lrat) | 2435.85 | 2194.19 | 55838.01 | 239.82 |
2016/app/barman-pfile06-022.sas.ex.7 (cnf) (drat) (lrat) | 23.75 | 22.80 | 39.11 | 17.99 |
2016/app/barman-pfile07-027.sas.cr.37 (cnf) (drat) (lrat) | 44.97 | 29.69 | 928.11 | 20.69 |
2016/app/barman-pfile07-028.sas.ex.15 (cnf) (drat) (lrat) | 144.07 | 104.16 | 463.21 | 65.52 |
2016/app/barman-pfile08-030.sas.cr.27 (cnf) (drat) (lrat) | 8.22 | 6.45 | 834.57 | 16.06 |
2016/app/barman-pfile08-032.sas.ex.7 (cnf) (drat) (lrat) | 24.69 | 20.96 | 113.36 | 47.92 |
2016/app/barman-pfile09-036.sas.cr.33 (cnf) (drat) (lrat) | 23.23 | 17.76 | 2172.77 | 31.20 |
2016/app/barman-pfile10-037.sas.ex.7 (cnf) (drat) (lrat) | 33.42 | 28.93 | 212.20 | 79.80 |
2016/app/barman-pfile10-038.sas.cr.25 (cnf) (drat) (lrat) | 11.03 | 8.97 | 1317.49 | 23.84 |
2016/app/barman-pfile10-038.sas.ex.15 (cnf) (drat) (lrat) | 26.87 | 12.59 | 993.26 | 175.35 |
2016/app/barman-pfile10-039.sas.ex.15 (cnf) (drat) (lrat) | 31.18 | 13.92 | 954.87 | 174.61 |
2016/app/barman-pfile10-040.sas.cr.21 (cnf) (drat) (lrat) | 7.77 | 6.33 | 1089.23 | 18.73 |
2016/app/barman-pfile10-040.sas.ex.15 (cnf) (drat) (lrat) | 31.89 | 13.86 | 1192.02 | 175.61 |
2016/app/cube-11-h13-unsat (cnf) (drat) (lrat) | 331.01 | 389.95 | 86400 (TIME) | 90.85 |
2016/app/eq.atree.braun.11.unsat (cnf) (drat) (lrat) | 1081.97 | 1538.09 | 15855.05 | 133.83 |
2016/app/gus-md5-10 (cnf) (drat) (lrat) | 646.24 | 934.73 | 1668.56 (ERROR) | 87.78 (ERROR) |
2016/app/homer17 (cnf) (drat) (lrat) | 1936.21 | 3169.54 | 15692.04 (ERROR) | 676.25 |
2016/app/k2mul.miter (cnf) (drat) (lrat) | 278.32 | 887.87 | 15828.16 | 108.29 |
2016/app/maxxororand032 (cnf) (drat) (lrat) | 203.44 | 213.61 | 6090.11 | 50.17 |
2016/app/modgen-n200-m90860q08c40-12992 (cnf) (drat) (lrat) | 0.04 | 0.08 | 0.08 | 0.04 |
2016/app/modgen-n200-m90860q08c40-14424 (cnf) (drat) (lrat) | 23.45 | 22.92 | 67.92 | 5.81 |
2016/app/modgen-n200-m90860q08c40-15163 (cnf) (drat) (lrat) | 0.03 | 0.09 | 0.09 | 0.04 |
2016/app/modgen-n200-m90860q08c40-21438 (cnf) (drat) (lrat) | 0.03 | 0.08 | 0.10 | 0.04 |
2016/app/modgen-n200-m90860q08c40-28046 (cnf) (drat) (lrat) | 2.13 | 1.57 | 4.52 | 0.74 |
2016/app/modgen-n200-m90860q08c40-29020 (cnf) (drat) (lrat) | 0.03 | 0.08 | 0.10 | 0.03 |
2016/app/modgen-n200-m90860q08c40-3866 (cnf) (drat) (lrat) | 0.04 | 0.08 | 0.09 | 0.05 |
2016/app/modgen-n200-m90860q08c40-5377 (cnf) (drat) (lrat) | 0.05 | 0.08 | 0.10 | 0.04 |
2016/app/modgen-n200-m90860q08c40-6295 (cnf) (drat) (lrat) | 0.03 | 0.08 | 0.10 | 0.04 |
2016/app/ndhf_xits_09_UNSAT (cnf) (drat) (lrat) | 825.51 | 943.80 | 24940.67 | 206.76 |
2016/app/newton.2.2.i.smt2-cvc4 (cnf) (drat) (lrat) | 228.87 | 2581.57 | 86400 (TIME) | 203.30 (FAIL) |
2016/app/newton.2.3.i.smt2-stp212 (cnf) (drat) (lrat) | 303.88 | 716.02 | 50917.57 | 179.85 |
2016/app/newton.3.3.i.smt2-stp212 (cnf) (drat) (lrat) | 377.37 | 901.43 | 71040.05 | 214.87 |
2016/app/newton.4.3.i.smt2-stp212 (cnf) (drat) (lrat) | 317.91 | 808.32 | 86400 (TIME) | 238.62 |
2016/app/q_query_3_L200_coli.sat (cnf) (drat) (lrat) | 249.05 | 1416.33 | 9682.71 | 39.44 |
2016/app/rpoc_xits_08_UNSAT (cnf) (drat) (lrat) | 452.84 | 572.31 | 10247.91 | 111.19 |
2016/app/rpoc_xits_10_UNKNOWN (cnf) (drat) (lrat) | 3366.35 | 2749.39 | 75717.41 | 420.42 |
2016/app/safe009_pso.oepc_true-unreach-call.i-cbmc-u2 (cnf) (drat) (lrat) | 1.77 | 1.01 | 3.57 | 0.68 |
2016/app/safe027_pso.opt_true-unreach-call.i-cbmc-u2 (cnf) (drat) (lrat) | 4.16 | 2.03 | 9.08 | 1.28 |
2016/app/safe028_tso.oepc_true-unreach-call.i-cbmc-u2 (cnf) (drat) (lrat) | 2.35 | 1.30 | 4.54 | 0.80 |
2016/app/schup-l2s-bc56s-1-k391 (cnf) (drat) (lrat) | 251.87 | 6215.64 | 86400 (TIME) | 966.61 |
2016/app/smtlib-qfbv-aigs-VS3-benchmark-S2-tseitin (cnf) (drat) (lrat) | 3757.85 | 4366.35 | 12646.57 (ERROR) | 822.53 |
2016/app/sncf_model_ixl_bmc_depth_07 (cnf) (drat) (lrat) | 3391.63 | 913.07 (ERROR) | (NO RUN) | (NO RUN) |
2016/app/snw_13_8_CCSEncnopre (cnf) (drat) (lrat) | 287.20 | 857.03 | 45131.46 | 235.04 |
2016/app/snw_13_8_CCSpreOptEncpre (cnf) (drat) (lrat) | 45.86 | 34.59 | 38.99 | 3.66 |
2016/app/snw_13_8_CCSpreOptnopre (cnf) (drat) (lrat) | 59.05 | 107.66 | 2526.98 | 13.06 |
2016/app/snw_13_8_CCSpreOptpre (cnf) (drat) (lrat) | 37.25 | 69.23 | 1083.57 | 8.50 |
2016/app/snw_13_8_pre (cnf) (drat) (lrat) | 822.46 | 2654.93 | 86400 (TIME) | 1044.13 |
2016/app/snw_16_8_nopre (cnf) (drat) (lrat) | 3880.67 | 7899.69 | 86400 (TIME) | 999.79 |
2016/app/snw_16_8_pre (cnf) (drat) (lrat) | 1624.35 | 2308.40 | 49911.23 | 197.86 |
2016/app/snw_16_8_preOpt_pre (cnf) (drat) (lrat) | 242.92 | 240.86 | 1157.31 | 16.58 |
2016/app/sokoban-p01.sas.ex.17 (cnf) (drat) (lrat) | 11.31 | 11.44 | 502.48 | 11.45 |
2016/app/sokoban-p09.sas.cr.25 (cnf) (drat) (lrat) | 0.63 | 1.32 | 20.67 | 1.66 |
2016/app/sokoban-p10.sas.cr.35 (cnf) (drat) (lrat) | 1.40 | 1.38 | 10.31 | 1.13 |
2016/app/sokoban-p16.sas.cr.37 (cnf) (drat) (lrat) | 2410.87 | 20000 (TIME) | (NO RUN) | (NO RUN) |
2016/app/sokoban-p16.sas.ex.15 (cnf) (drat) (lrat) | 1054.68 | 1533.61 | 86400 (TIME) | 1408.93 |
2016/app/sokoban-p16.sas.ex.17 (cnf) (drat) (lrat) | 3465.45 | 1147.61 (FAIL) | (NO RUN) | (NO RUN) |
2016/app/sokoban-p17.sas.ex.11 (cnf) (drat) (lrat) | 4.66 | 4.27 | 85.06 | 6.06 |
2016/app/sokoban-p18.sas.cr.29 (cnf) (drat) (lrat) | 0.85 | 0.71 | 5.72 | 0.76 |
2016/app/sokoban-p19.sas.cr.23 (cnf) (drat) (lrat) | 0.59 | 0.52 | 3.26 | 0.57 |
2016/app/sokoban-p20.sas.cr.21 (cnf) (drat) (lrat) | 217.34 | 5659.21 | 86400 (TIME) | 1288.32 |
2016/app/sokoban-p20.sas.cr.23 (cnf) (drat) (lrat) | 812.00 | 11599.07 | 86400 (TIME) | 2579.37 (FAIL) |
2016/app/sokoban-p20.sas.cr.25 (cnf) (drat) (lrat) | 1332.23 | 18291.17 | 86400 (TIME) | 2795.55 (FAIL) |
2016/app/sokoban-p20.sas.cr.27 (cnf) (drat) (lrat) | 4283.45 | 1020.88 (ERROR) | (NO RUN) | (NO RUN) |
2016/app/sokoban-p20.sas.ex.11 (cnf) (drat) (lrat) | 625.11 | 961.90 | 86400 (TIME) | 1198.10 |
2016/app/sokoban-p20.sas.ex.13 (cnf) (drat) (lrat) | 2451.72 | 891.43 (ERROR) | (NO RUN) | (NO RUN) |
2016/app/square.2.0.i.smt2-cvc4 (cnf) (drat) (lrat) | 2.47 | 1.07 | 21.90 | 0.97 |
2016/app/test_v3_r8_vr5_c1_s8257.smt2-stp212 (cnf) (drat) (lrat) | 29.57 | 84.03 | 9.58 (FAIL) | 3.39 (FAIL) |
2016/app/test_v7_r12_vr1_c1_s22787.smt2-cvc4 (cnf) (drat) (lrat) | 3830.26 | 11557.05 | 78361.26 (ERROR) | 785.67 (FAIL) |
2016/app/test_v7_r17_vr1_c1_s30331.smt2-stp212 (cnf) (drat) (lrat) | 2507.61 | 3826.15 | 86400 (TIME) | 366.63 (FAIL) |
2016/app/total-10-13-u (cnf) (drat) (lrat) | 164.92 | 805.18 | 7226.23 | 71.27 |
2016/app/uum8.smt2-stp212 (cnf) (drat) (lrat) | 9.64 | 13.43 | 99.12 | 6.70 |
2016/app/valves-gates-1-k617-unsat (cnf) (drat) (lrat) | 1157.36 | 20000 (TIME) | (NO RUN) | (NO RUN) |
2016/app/velev-vliw-uns-2.0-uq5 (cnf) (drat) (lrat) | 257.03 | 2945.99 | 86400 (TIME) | 435.10 |
2016/app/barman-pfile08-032.sas.ex.15 (cnf) (drat) (lrat) | 40.70 | 26.45 | 534.62 | 107.13 |
2016/app/ctl_4291_567_8_unsat (cnf) (drat) (lrat) | 2650.06 | 2709.55 | 86400 (TIME) | 428.59 |
2016/app/arcfour_initialPermutation_6_14 (cnf) (drat) (lrat) | 115.89 | 91.57 | 86400 (TIME) | 186.07 |
2016/app/sokoban-p04.sas.ex.13 (cnf) (drat) (lrat) | 7.44 | 6.64 | 120.71 | 5.83 |
2016/app/barman-pfile10-040.sas.cr.17 (cnf) (drat) (lrat) | 5.57 | 4.85 | 672.06 | 14.41 |
2016/app/newton.2.3.i.smt2-cvc4 (cnf) (drat) (lrat) | 555.28 | 6074.56 | 86400 (TIME) | 1726.42 |
2016/app/1dlx_c_iq57_a (cnf) (drat) (lrat) | 397.13 | 1746.48 | 80384.97 | 188.88 |