Efficient Certified RAT Verification

Efficient Certified RAT Verification

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.

Instancecmsat5drat-trimcoq checkeracl2 checker
2015/main/manthey_single-ordered-initialized-w24-b9 (cnf) (drat) (lrat)0.780.691.430.33
2015/main/dated-5-13-u (cnf) (drat) (lrat)1711.224550.4986400 (TIME)454.57
2015/main/dated-10-17-u (cnf) (drat) (lrat)2128.515402.6286400 (TIME)443.92
2015/main/6s165-nonopt (cnf) (drat) (lrat)13.847.1110.001.64
2015/main/7pipe_k (cnf) (drat) (lrat)178.36542.2620411.37184.46
2015/main/manthey_single-ordered-initialized-w44-b8 (cnf) (drat) (lrat)363.26543.587745.3379.75
2015/main/6s16 (cnf) (drat) (lrat)330.34366.394484.8436.88
2015/main/9dlx_vliw_at_b_iq8.used-as.sat04-718 (cnf) (drat) (lrat)878.388194.6486400 (TIME)1154.02
2015/main/atco_enc1_opt2_20_12 (cnf) (drat) (lrat)2282.451718.9510109.99115.22
2015/main/hitag2-8-60-0-0x1eb82244d7f1c3c-47 (cnf) (drat) (lrat)4260.835208.7616405.45 (ERROR)622.23
2015/main/beempgsol5b1 (cnf) (drat) (lrat)83.8249.90530.847.48
2015/main/6s13-opt (cnf) (drat) (lrat)304.68383.266141.3141.01
2015/main/6s133 (cnf) (drat) (lrat)249.72264.367594.0942.25
2015/main/10pipe_q0_k (cnf) (drat) (lrat)1462.934539.3386400 (TIME)1737.84
2015/main/6s9 (cnf) (drat) (lrat)345.47401.925024.7640.99
2015/main/aaai10-planning-ipc5-pathways-13-step17 (cnf) (drat) (lrat)85.69235.102143.8734.27
2015/main/aaai10-planning-ipc5-pathways-17-step20 (cnf) (drat) (lrat)76.70416.882747.7527.32
2015/main/atco_enc1_opt2_10_14 (cnf) (drat) (lrat)351.54503.554541.6556.54
2015/main/6s11-opt (cnf) (drat) (lrat)398.98399.124103.1638.04
2015/main/6s130-opt (cnf) (drat) (lrat)304.25281.836714.5143.18
2015/main/k2fix_gr_rcs_w9.shuffled (cnf) (drat) (lrat)37.1340.50115.147.73
2015/main/bob12m02-opt (cnf) (drat) (lrat)1537.27948.144383.3926.32
2015/main/6s168-opt (cnf) (drat) (lrat)31.8714.0945.193.16
2015/main/6s16-opt (cnf) (drat) (lrat)386.26372.583448.1334.76
2015/main/manthey_single-ordered-initialized-w40-b10 (cnf) (drat) (lrat)85.06114.431318.8721.38
2015/main/aaai10-planning-ipc5-TPP-21-step11 (cnf) (drat) (lrat)339.291913.4419228.79 (FAIL)66.81 (FAIL)
2015/main/ACG-15-10p0 (cnf) (drat) (lrat)315.502491.6345315.43248.39
2015/main/6s17-opt (cnf) (drat) (lrat)319.09340.315610.5938.45
2015/main/ACG-20-5p0 (cnf) (drat) (lrat)263.552195.6429654.28 (FAIL)125.27 (FAIL)
2015/main/bjrb07amba10andenv (cnf) (drat) (lrat)420.012107.7086400 (TIME)433.92
2015/main/post-cbmc-aes-ee-r2-noholes (cnf) (drat) (lrat)149.63728.1482208.09165.22
2015/main/countbitssrl032 (cnf) (drat) (lrat)341.52605.5334202.13150.66
2015/main/jgiraldezlevy.2200.9086.08.40.109 (cnf) (drat) (lrat)1275.221667.0623874.55181.49
2015/main/hitag2-10-60-0-0x8edc44db7837bbf-65 (cnf) (drat) (lrat)4735.285586.1016227.20 (ERROR)667.25
2015/main/jgiraldezlevy.2200.9086.08.40.135 (cnf) (drat) (lrat)3052.782525.3786400 (TIME)446.14
2015/main/bob12m09-opt (cnf) (drat) (lrat)212.76442.5210626.2862.00
2015/main/jgiraldezlevy.2200.9086.08.40.46 (cnf) (drat) (lrat)624.38739.0210567.26103.85
2015/main/jgiraldezlevy.2200.9086.08.40.108 (cnf) (drat) (lrat)4136.433345.9586400 (TIME)516.25
2015/main/dated-10-13-u (cnf) (drat) (lrat)144.54964.558191.8573.01
2015/main/group_mulr (cnf) (drat) (lrat)699.2231.07540.1314.23
2015/main/6s131-opt (cnf) (drat) (lrat)279.06238.935904.6338.30
2015/main/hwmcc10-timeframe-expansion-k50-pdtpmsns2-tseitin (cnf) (drat) (lrat)353.00664.1630078.89114.50
2015/main/manthey_single-ordered-initialized-w20-b7 (cnf) (drat) (lrat)0.220.230.470.14
2015/main/6s167-opt (cnf) (drat) (lrat)56.7638.8097.746.97
2015/main/6s169-opt (cnf) (drat) (lrat)164.98104.10417.0415.05
2015/main/manthey_single-ordered-initialized-w28-b8 (cnf) (drat) (lrat)2.872.645.681.06
2015/main/manthey_single-ordered-initialized-w50-b6 (cnf) (drat) (lrat)327.06561.927774.9580.05
2015/main/manthey_single-ordered-initialized-w44-b9 (cnf) (drat) (lrat)352.44541.587774.5579.34
2015/main/manthey_single-ordered-initialized-w48-b9 (cnf) (drat) (lrat)1148.061715.7244318.61251.53
2015/main/manthey_single-ordered-initialized-w18-b7 (cnf) (drat) (lrat)0.120.140.210.09
2015/main/manthey_single-ordered-initialized-w40-b8 (cnf) (drat) (lrat)116.72162.841701.7529.36
2015/main/manthey_single-ordered-initialized-w24-b7 (cnf) (drat) (lrat)0.660.641.330.31
2015/main/manthey_single-ordered-initialized-w46-b9 (cnf) (drat) (lrat)728.641137.8522725.41154.29
2015/main/manthey_single-ordered-initialized-w52-b6 (cnf) (drat) (lrat)541.04777.3415455.43127.36
2015/main/manthey_single-ordered-initialized-w42-b8 (cnf) (drat) (lrat)203.69291.963431.8647.11
2015/main/manthey_single-ordered-initialized-w46-b8 (cnf) (drat) (lrat)589.42766.4015672.45134.53
2015/main/AProVE07-03 (cnf) (drat) (lrat)188.23272.645287.0257.80
2015/main/post-c32s-ss-8 (cnf) (drat) (lrat)126.56121.301812.5915.07
2015/main/q_query_3_L80_coli.sat (cnf) (drat) (lrat)60.62572.957958.0129.48
2015/main/q_query_3_L150_coli.sat (cnf) (drat) (lrat)296.742630.5567010.25176.76
2015/main/atco_enc2_opt2_20_11 (cnf) (drat) (lrat)596.96523.852923.3954.88
2015/main/atco_enc3_opt2_10_12 (cnf) (drat) (lrat)443.36588.821135.5727.11
2015/main/bob12s02 (cnf) (drat) (lrat)510.42437.842630.1414.74
2015/main/AProVE07-27 (cnf) (drat) (lrat)421.321040.8366052.93276.30
2015/main/post-cbmc-aes-d-r2 (cnf) (drat) (lrat)117.551326.4186400 (TIME)334.26
2015/main/SAT_dat.k95-24_1_rule_3 (cnf) (drat) (lrat)3334.1020000 (TIME)(NO RUN)(NO RUN)
2015/main/SAT_dat.k90.debugged (cnf) (drat) (lrat)2930.8120000 (TIME)(NO RUN)(NO RUN)
2015/main/SAT_dat.k70-24_1_rule_3 (cnf) (drat) (lrat)1235.1120000 (TIME)(NO RUN)(NO RUN)
2015/main/velev-vliw-uns-4.0-9-i1 (cnf) (drat) (lrat)417.032396.1486400 (TIME)368.47
2015/main/UR-20-10p0 (cnf) (drat) (lrat)1006.327879.6486400 (TIME)692.30 (FAIL)
2015/main/beempgsol2b1 (cnf) (drat) (lrat)92.7455.00626.258.04
2015/main/atco_enc3_opt2_10_14 (cnf) (drat) (lrat)552.55688.821322.8031.16
2015/main/manthey_single-ordered-initialized-w18-b8 (cnf) (drat) (lrat)0.140.140.270.10
2015/main/manthey_single-ordered-initialized-w26-b8 (cnf) (drat) (lrat)1.401.202.480.55
2015/main/manol-pipe-c10nid_i (cnf) (drat) (lrat)143.82888.0125395.2085.41
2015/main/manthey_single-ordered-initialized-w22-b8 (cnf) (drat) (lrat)0.390.360.820.20
2015/main/manthey_single-ordered-initialized-w48-b6 (cnf) (drat) (lrat)223.30362.464381.8354.74
2015/main/manthey_single-ordered-initialized-w20-b8 (cnf) (drat) (lrat)0.230.240.520.14
2015/main/manthey_single-ordered-initialized-w32-b9 (cnf) (drat) (lrat)11.7513.1166.242.89
2015/main/manthey_single-ordered-initialized-w22-b6 (cnf) (drat) (lrat)0.320.320.700.19
2015/main/manthey_single-ordered-initialized-w26-b7 (cnf) (drat) (lrat)1.561.492.890.65
2015/main/manthey_single-ordered-initialized-w42-b9 (cnf) (drat) (lrat)175.40253.703142.2041.53
2015/main/manthey_single-ordered-initialized-w44-b6 (cnf) (drat) (lrat)90.88140.401394.3925.00
2015/main/manthey_single-ordered-initialized-w50-b7 (cnf) (drat) (lrat)1057.581496.2839141.28253.40
2015/main/minxorminand064 (cnf) (drat) (lrat)184.83521.6035061.91151.15
2015/main/manthey_single-ordered-initialized-w46-b7 (cnf) (drat) (lrat)352.89564.988046.4382.05
2015/main/manthey_single-ordered-initialized-w44-b7 (cnf) (drat) (lrat)216.13305.714061.7451.85
2015/main/manthey_single-ordered-initialized-w48-b7 (cnf) (drat) (lrat)620.631004.3118298.23142.48
2015/main/minandmaxor128 (cnf) (drat) (lrat)3304.406966.5686400 (TIME)1902.33
2015/main/velev-vliw-uns-2.0-uq5 (cnf) (drat) (lrat)254.942999.6386400 (TIME)437.71
2015/main/UCG-20-5p0 (cnf) (drat) (lrat)110.00419.305886.5240.40
2015/main/SAT_dat.k85-24_1_rule_3 (cnf) (drat) (lrat)2473.4920000 (TIME)(NO RUN)(NO RUN)
2015/main/post-cbmc-aes-d-r2-noholes (cnf) (drat) (lrat)145.53914.3586400 (TIME)216.54
2015/main/SAT_dat.k80-24_1_rule_1 (cnf) (drat) (lrat)2241.4420000 (TIME)(NO RUN)(NO RUN)
2015/main/q_query_3_L200_coli.sat (cnf) (drat) (lrat)249.611453.319670.4739.69
2015/main/UCG-20-10p0 (cnf) (drat) (lrat)506.838253.6386400 (TIME)1301.94
2015/parallel/SAT_dat.k70-24_1_rule_3 (cnf) (drat) (lrat)1147.7120000 (TIME)(NO RUN)(NO RUN)
2015/parallel/6s17-opt (cnf) (drat) (lrat)320.42339.245612.9838.40
2015/parallel/jgiraldezlevy.2200.9086.08.40.135 (cnf) (drat) (lrat)3013.092477.6386400 (TIME)446.70
2015/parallel/dated-10-17-u (cnf) (drat) (lrat)2081.005921.7184667.48442.59
2015/parallel/jgiraldezlevy.2200.9086.08.40.46 (cnf) (drat) (lrat)624.14718.6210591.20103.58
2015/parallel/group_mulr (cnf) (drat) (lrat)698.1331.22528.9614.18
2015/parallel/jgiraldezlevy.2200.9086.08.40.109 (cnf) (drat) (lrat)1298.091577.7324274.55179.58
2015/parallel/6s16-opt (cnf) (drat) (lrat)385.05375.353441.4834.78
2015/parallel/atco_enc1_opt2_20_12 (cnf) (drat) (lrat)2281.601435.6610156.90120.01
2015/parallel/9dlx_vliw_at_b_iq8.used-as.sat04-718 (cnf) (drat) (lrat)876.598304.1586400 (TIME)1157.25
2015/parallel/SAT_dat.k90.debugged (cnf) (drat) (lrat)2890.5520000 (TIME)(NO RUN)(NO RUN)
2015/parallel/SAT_dat.k80-24_1_rule_1 (cnf) (drat) (lrat)2285.2420000 (TIME)(NO RUN)(NO RUN)
2015/parallel/UR-20-10p0 (cnf) (drat) (lrat)989.388152.1286400 (TIME)685.30 (FAIL)
2015/parallel/bob12m02-opt (cnf) (drat) (lrat)1536.26911.554399.0726.16
2015/parallel/manthey_single-ordered-initialized-w50-b7 (cnf) (drat) (lrat)1076.951745.2239229.40243.89
2015/parallel/dated-5-13-u (cnf) (drat) (lrat)1718.444439.1886400 (TIME)454.80
2015/parallel/hitag2-8-60-0-0x1eb82244d7f1c3c-47 (cnf) (drat) (lrat)4281.025780.9116347.91 (ERROR)610.04
2015/parallel/6s13-opt (cnf) (drat) (lrat)304.44383.136154.1040.73
2015/parallel/manthey_single-ordered-initialized-w48-b9 (cnf) (drat) (lrat)1124.011723.0244858.16267.58
2015/parallel/6s130-opt (cnf) (drat) (lrat)298.61281.996865.5743.60
2015/parallel/hitag2-10-60-0-0x8edc44db7837bbf-65 (cnf) (drat) (lrat)4771.275887.6416181.89 (ERROR)662.18
2015/parallel/SAT_dat.k95-24_1_rule_3 (cnf) (drat) (lrat)3570.7120000 (TIME)(NO RUN)(NO RUN)
2015/parallel/minandmaxor128 (cnf) (drat) (lrat)3362.066899.1386400 (TIME)2091.32
2015/parallel/jgiraldezlevy.2200.9086.08.40.108 (cnf) (drat) (lrat)4187.304084.7586400 (TIME)524.59
2015/parallel/SAT_dat.k85-24_1_rule_3 (cnf) (drat) (lrat)2533.1720000 (TIME)(NO RUN)(NO RUN)
2016/crafted/peb-pyrofpyr-11-neq-3_shuffled (cnf) (drat) (lrat)44.371016.6569286.79701.75
2016/crafted/peb-pyrofpyr-12-neq-3_shuffled (cnf) (drat) (lrat)68.282326.6586400 (TIME)1438.32
2016/crafted/rphp4_065_shuffled (cnf) (drat) (lrat)2250.641256.3366614.46 (ERROR)509.93
2016/crafted/Schur_161_5_d42 (cnf) (drat) (lrat)1174.97691.0920686.20153.62
2016/crafted/Schur_161_5_d43 (cnf) (drat) (lrat)462.39288.887106.4281.01
2016/crafted/stone-width3chain-nmarkers-08_shuffled (cnf) (drat) (lrat)51.0356.451069.477.24
2016/crafted/ecgrid6x210_shuffled (cnf) (drat) (lrat)4808.28253.54899.1720.70
2016/crafted/peb-pyrofpyr-13-neq-3_shuffled (cnf) (drat) (lrat)99.624644.3386400 (TIME)2413.95
2016/crafted/peb-pyrofpyr-14-neq-3_shuffled (cnf) (drat) (lrat)155.018567.6886400 (TIME)4226.44
2016/crafted/peb-pyrofpyr-15-neq-3_shuffled (cnf) (drat) (lrat)227.9314004.5286400 (TIME)6707.85
2016/crafted/pop90_shuffled (cnf) (drat) (lrat)12.273.9729.622.97
2016/crafted/pop93_shuffled (cnf) (drat) (lrat)871.24167.442922.4851.77
2016/crafted/pop99_shuffled (cnf) (drat) (lrat)1057.99203.463522.3856.16
2016/crafted/stone-width3chain-nmarkers-10_shuffled (cnf) (drat) (lrat)128.95199.421518.7314.08
2016/crafted/stone-width3chain-nmarkers-11_shuffled (cnf) (drat) (lrat)200.38383.933604.5521.78
2016/crafted/stone-width3chain-nmarkers-12_shuffled (cnf) (drat) (lrat)386.22755.0326928.7035.54
2016/crafted/stone-width3chain-nmarkers-13_shuffled (cnf) (drat) (lrat)601.051153.9486400 (TIME)150.21
2016/crafted/stone-width3chain-nmarkers-14_shuffled (cnf) (drat) (lrat)913.331537.0686400 (TIME)98.90
2016/crafted/stone-width3chain-nmarkers-15_shuffled (cnf) (drat) (lrat)1480.603336.7186400 (TIME)234.77
2016/crafted/stone-width3chain-nmarkers-16_shuffled (cnf) (drat) (lrat)2471.074508.1386400 (TIME)282.42
2016/crafted/stone-width3chain-nmarkers-17_shuffled (cnf) (drat) (lrat)3340.584458.7086400 (TIME)409.39
2016/crafted/tseitingrid4x185_shuffled (cnf) (drat) (lrat)27.819.8435.343.39
2016/crafted/tseitingrid4x190_shuffled (cnf) (drat) (lrat)27.549.6430.943.20
2016/crafted/tseitingrid4x195_shuffled (cnf) (drat) (lrat)27.649.3431.343.28
2016/crafted/tseitingrid4x200_shuffled (cnf) (drat) (lrat)37.6712.0838.703.58
2016/crafted/stone-width3chain-nmarkers-09_shuffled (cnf) (drat) (lrat)84.53109.811013.2510.73
2016/app/AProVE11-06 (cnf) (drat) (lrat)1944.732291.1663973.79 (FAIL)135.65 (FAIL)
2016/app/9dlx_vliw_at_b_iq4.used-as.sat04-345 (cnf) (drat) (lrat)181.612203.3786400 (TIME)464.68
2016/app/9dlx_vliw_at_b_iq9.used-as.sat04-719 (cnf) (drat) (lrat)1362.5211029.1686400 (TIME)1545.30
2016/app/ACG-20-10p0 (cnf) (drat) (lrat)717.0711826.3286400 (TIME)1539.36 (FAIL)
2016/app/E00N23 (cnf) (drat) (lrat)3318.652766.7486400 (TIME)639.67
2016/app/9dlx_vliw_at_b_iq8.used-as.sat04-718 (cnf) (drat) (lrat)871.848269.3186400 (TIME)1152.12
2016/app/Sz512_15127_3.smt2-cvc4 (cnf) (drat) (lrat)201.24379.584020.7048.77
2016/app/UR-15-10p0 (cnf) (drat) (lrat)158.911549.0426203.27156.85
2016/app/ablmulub16x4o (cnf) (drat) (lrat)336.60858.2625959.94191.27
2016/app/ablmulub2x32o (cnf) (drat) (lrat)556.271737.8086400 (TIME)433.53
2016/app/add_01_1000_4.smt2-cvc4 (cnf) (drat) (lrat)10.8314.02129.124.39
2016/app/ak016modbtsimpbisc (cnf) (drat) (lrat)2642.941421.6315791.01122.40
2016/app/ak032diagodiagoisc (cnf) (drat) (lrat)850.99277.612784.4323.71
2016/app/ak032modbtmodbtisc (cnf) (drat) (lrat)2962.26936.8011939.4575.50
2016/app/ak064paralparalisc (cnf) (drat) (lrat)2435.852194.1955838.01239.82
2016/app/barman-pfile06-022.sas.ex.7 (cnf) (drat) (lrat)23.7522.8039.1117.99
2016/app/barman-pfile07-027.sas.cr.37 (cnf) (drat) (lrat)44.9729.69928.1120.69
2016/app/barman-pfile07-028.sas.ex.15 (cnf) (drat) (lrat)144.07104.16463.2165.52
2016/app/barman-pfile08-030.sas.cr.27 (cnf) (drat) (lrat)8.226.45834.5716.06
2016/app/barman-pfile08-032.sas.ex.7 (cnf) (drat) (lrat)24.6920.96113.3647.92
2016/app/barman-pfile09-036.sas.cr.33 (cnf) (drat) (lrat)23.2317.762172.7731.20
2016/app/barman-pfile10-037.sas.ex.7 (cnf) (drat) (lrat)33.4228.93212.2079.80
2016/app/barman-pfile10-038.sas.cr.25 (cnf) (drat) (lrat)11.038.971317.4923.84
2016/app/barman-pfile10-038.sas.ex.15 (cnf) (drat) (lrat)26.8712.59993.26175.35
2016/app/barman-pfile10-039.sas.ex.15 (cnf) (drat) (lrat)31.1813.92954.87174.61
2016/app/barman-pfile10-040.sas.cr.21 (cnf) (drat) (lrat)7.776.331089.2318.73
2016/app/barman-pfile10-040.sas.ex.15 (cnf) (drat) (lrat)31.8913.861192.02175.61
2016/app/cube-11-h13-unsat (cnf) (drat) (lrat)331.01389.9586400 (TIME)90.85
2016/app/eq.atree.braun.11.unsat (cnf) (drat) (lrat)1081.971538.0915855.05133.83
2016/app/gus-md5-10 (cnf) (drat) (lrat)646.24934.731668.56 (ERROR)87.78 (ERROR)
2016/app/homer17 (cnf) (drat) (lrat)1936.213169.5415692.04 (ERROR)676.25
2016/app/k2mul.miter (cnf) (drat) (lrat)278.32887.8715828.16108.29
2016/app/maxxororand032 (cnf) (drat) (lrat)203.44213.616090.1150.17
2016/app/modgen-n200-m90860q08c40-12992 (cnf) (drat) (lrat)0.040.080.080.04
2016/app/modgen-n200-m90860q08c40-14424 (cnf) (drat) (lrat)23.4522.9267.925.81
2016/app/modgen-n200-m90860q08c40-15163 (cnf) (drat) (lrat)0.030.090.090.04
2016/app/modgen-n200-m90860q08c40-21438 (cnf) (drat) (lrat)0.030.080.100.04
2016/app/modgen-n200-m90860q08c40-28046 (cnf) (drat) (lrat)2.131.574.520.74
2016/app/modgen-n200-m90860q08c40-29020 (cnf) (drat) (lrat)0.030.080.100.03
2016/app/modgen-n200-m90860q08c40-3866 (cnf) (drat) (lrat)0.040.080.090.05
2016/app/modgen-n200-m90860q08c40-5377 (cnf) (drat) (lrat)0.050.080.100.04
2016/app/modgen-n200-m90860q08c40-6295 (cnf) (drat) (lrat)0.030.080.100.04
2016/app/ndhf_xits_09_UNSAT (cnf) (drat) (lrat)825.51943.8024940.67206.76
2016/app/newton.2.2.i.smt2-cvc4 (cnf) (drat) (lrat)228.872581.5786400 (TIME)203.30 (FAIL)
2016/app/newton.2.3.i.smt2-stp212 (cnf) (drat) (lrat)303.88716.0250917.57179.85
2016/app/newton.3.3.i.smt2-stp212 (cnf) (drat) (lrat)377.37901.4371040.05214.87
2016/app/newton.4.3.i.smt2-stp212 (cnf) (drat) (lrat)317.91808.3286400 (TIME)238.62
2016/app/q_query_3_L200_coli.sat (cnf) (drat) (lrat)249.051416.339682.7139.44
2016/app/rpoc_xits_08_UNSAT (cnf) (drat) (lrat)452.84572.3110247.91111.19
2016/app/rpoc_xits_10_UNKNOWN (cnf) (drat) (lrat)3366.352749.3975717.41420.42
2016/app/safe009_pso.oepc_true-unreach-call.i-cbmc-u2 (cnf) (drat) (lrat)1.771.013.570.68
2016/app/safe027_pso.opt_true-unreach-call.i-cbmc-u2 (cnf) (drat) (lrat)4.162.039.081.28
2016/app/safe028_tso.oepc_true-unreach-call.i-cbmc-u2 (cnf) (drat) (lrat)2.351.304.540.80
2016/app/schup-l2s-bc56s-1-k391 (cnf) (drat) (lrat)251.876215.6486400 (TIME)966.61
2016/app/smtlib-qfbv-aigs-VS3-benchmark-S2-tseitin (cnf) (drat) (lrat)3757.854366.3512646.57 (ERROR)822.53
2016/app/sncf_model_ixl_bmc_depth_07 (cnf) (drat) (lrat)3391.63913.07 (ERROR)(NO RUN)(NO RUN)
2016/app/snw_13_8_CCSEncnopre (cnf) (drat) (lrat)287.20857.0345131.46235.04
2016/app/snw_13_8_CCSpreOptEncpre (cnf) (drat) (lrat)45.8634.5938.993.66
2016/app/snw_13_8_CCSpreOptnopre (cnf) (drat) (lrat)59.05107.662526.9813.06
2016/app/snw_13_8_CCSpreOptpre (cnf) (drat) (lrat)37.2569.231083.578.50
2016/app/snw_13_8_pre (cnf) (drat) (lrat)822.462654.9386400 (TIME)1044.13
2016/app/snw_16_8_nopre (cnf) (drat) (lrat)3880.677899.6986400 (TIME)999.79
2016/app/snw_16_8_pre (cnf) (drat) (lrat)1624.352308.4049911.23197.86
2016/app/snw_16_8_preOpt_pre (cnf) (drat) (lrat)242.92240.861157.3116.58
2016/app/sokoban-p01.sas.ex.17 (cnf) (drat) (lrat)11.3111.44502.4811.45
2016/app/sokoban-p09.sas.cr.25 (cnf) (drat) (lrat)0.631.3220.671.66
2016/app/sokoban-p10.sas.cr.35 (cnf) (drat) (lrat)1.401.3810.311.13
2016/app/sokoban-p16.sas.cr.37 (cnf) (drat) (lrat)2410.8720000 (TIME)(NO RUN)(NO RUN)
2016/app/sokoban-p16.sas.ex.15 (cnf) (drat) (lrat)1054.681533.6186400 (TIME)1408.93
2016/app/sokoban-p16.sas.ex.17 (cnf) (drat) (lrat)3465.451147.61 (FAIL)(NO RUN)(NO RUN)
2016/app/sokoban-p17.sas.ex.11 (cnf) (drat) (lrat)4.664.2785.066.06
2016/app/sokoban-p18.sas.cr.29 (cnf) (drat) (lrat)0.850.715.720.76
2016/app/sokoban-p19.sas.cr.23 (cnf) (drat) (lrat)0.590.523.260.57
2016/app/sokoban-p20.sas.cr.21 (cnf) (drat) (lrat)217.345659.2186400 (TIME)1288.32
2016/app/sokoban-p20.sas.cr.23 (cnf) (drat) (lrat)812.0011599.0786400 (TIME)2579.37 (FAIL)
2016/app/sokoban-p20.sas.cr.25 (cnf) (drat) (lrat)1332.2318291.1786400 (TIME)2795.55 (FAIL)
2016/app/sokoban-p20.sas.cr.27 (cnf) (drat) (lrat)4283.451020.88 (ERROR)(NO RUN)(NO RUN)
2016/app/sokoban-p20.sas.ex.11 (cnf) (drat) (lrat)625.11961.9086400 (TIME)1198.10
2016/app/sokoban-p20.sas.ex.13 (cnf) (drat) (lrat)2451.72891.43 (ERROR)(NO RUN)(NO RUN)
2016/app/square.2.0.i.smt2-cvc4 (cnf) (drat) (lrat)2.471.0721.900.97
2016/app/test_v3_r8_vr5_c1_s8257.smt2-stp212 (cnf) (drat) (lrat)29.5784.039.58 (FAIL)3.39 (FAIL)
2016/app/test_v7_r12_vr1_c1_s22787.smt2-cvc4 (cnf) (drat) (lrat)3830.2611557.0578361.26 (ERROR)785.67 (FAIL)
2016/app/test_v7_r17_vr1_c1_s30331.smt2-stp212 (cnf) (drat) (lrat)2507.613826.1586400 (TIME)366.63 (FAIL)
2016/app/total-10-13-u (cnf) (drat) (lrat)164.92805.187226.2371.27
2016/app/uum8.smt2-stp212 (cnf) (drat) (lrat)9.6413.4399.126.70
2016/app/valves-gates-1-k617-unsat (cnf) (drat) (lrat)1157.3620000 (TIME)(NO RUN)(NO RUN)
2016/app/velev-vliw-uns-2.0-uq5 (cnf) (drat) (lrat)257.032945.9986400 (TIME)435.10
2016/app/barman-pfile08-032.sas.ex.15 (cnf) (drat) (lrat)40.7026.45534.62107.13
2016/app/ctl_4291_567_8_unsat (cnf) (drat) (lrat)2650.062709.5586400 (TIME)428.59
2016/app/arcfour_initialPermutation_6_14 (cnf) (drat) (lrat)115.8991.5786400 (TIME)186.07
2016/app/sokoban-p04.sas.ex.13 (cnf) (drat) (lrat)7.446.64120.715.83
2016/app/barman-pfile10-040.sas.cr.17 (cnf) (drat) (lrat)5.574.85672.0614.41
2016/app/newton.2.3.i.smt2-cvc4 (cnf) (drat) (lrat)555.286074.5686400 (TIME)1726.42
2016/app/1dlx_c_iq57_a (cnf) (drat) (lrat)397.131746.4880384.97188.88