Benchmark

LabelMeaning
SSolution {OPTIMUM FOUND or OPT | UNSATISFIABLE or UNSAT | UNKNOWN | Not available or N/A}
OBest solution found
TCPU time (TO for Time Out)
(out)(err)Standard output and standard error for each solver

ColorMeaning for Complete SolversMeaning for Incomplete Solvers
TextBest solver columnBest solver column
TextOptimal solution with the best CPU timeBest solution with the best CPU time
TextOptimal solution and finished within the Time OutBest solution without the best CPU time
TextOptimal solution and did not finish within the Time OutSolution found but not the best
TextTime OutTime Out
TextBuggy solutionBuggy solution

Instance file name Best solver ISAC+-2016-in
mul_8_11.wcnf O = 64
T = 17.06
O = 64
T = 17.06
mul_8_13.wcnf O = 60
T = 18.24
O = 60
T = 18.24
mul_8_14.wcnf O = 56
T = 14.71
O = 56
T = 14.71
mul_8_3.wcnf O = 36
T = 10.20
O = 36
T = 10.20
mul_8_9.wcnf O = 42
T = 11.90
O = 42
T = 11.90
sbox_4.wcnf O = 22
T = 7.49
O = 22
T = 7.49
sbox_8.wcnf O = 845
T = 25.64
O = 845
T = 25.64
atcoss_mesat_01.wcnf O = 20
T = 185.32
O = 20
T = 185.32
atcoss_mesat_02.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_mesat_03.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_mesat_04.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_mesat_05.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_mesat_06.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_mesat_07.wcnf O = 0
T = 72.60
O = 0
T = 72.60
atcoss_mesat_08.wcnf O = 0
T = 60.46
O = 0
T = 60.46
atcoss_mesat_09.wcnf O = 0
T = 134.54
O = 0
T = 134.54
atcoss_mesat_10.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_mesat_11.wcnf O = 50
T = 129.83
O = 50
T = 129.83
atcoss_mesat_12.wcnf O = 12
T = 84.48
O = 12
T = 84.48
atcoss_mesat_13.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_mesat_14.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_mesat_15.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_mesat_16.wcnf O = 0
T = 95.03
O = 0
T = 95.03
atcoss_mesat_17.wcnf O = 0
T = 154.56
O = 0
T = 154.56
atcoss_mesat_18.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_sugar_01.wcnf O = 20
T = 58.60
O = 20
T = 58.60
atcoss_sugar_02.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_sugar_03.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_sugar_04.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_sugar_05.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_sugar_06.wcnf O = 20
T = 90.98
O = 20
T = 90.98
atcoss_sugar_07.wcnf O = 0
T = 23.32
O = 0
T = 23.32
atcoss_sugar_08.wcnf O = 0
T = 22.20
O = 0
T = 22.20
atcoss_sugar_09.wcnf O = 0
T = 60.51
O = 0
T = 60.51
atcoss_sugar_10.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_sugar_11.wcnf O = 50
T = 21.87
O = 50
T = 21.87
atcoss_sugar_12.wcnf O = 12
T = 42.38
O = 12
T = 42.38
atcoss_sugar_13.wcnf O = 0
T = 83.70
O = 0
T = 83.70
atcoss_sugar_14.wcnf O = 0
T = 100.78
O = 0
T = 100.78
atcoss_sugar_15.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_sugar_16.wcnf O = 0
T = 28.34
O = 0
T = 28.34
atcoss_sugar_17.wcnf O = 0
T = 41.09
O = 0
T = 41.09
atcoss_sugar_18.wcnf O = N/A
T = TO
O = N/A
T = TO
atcoss_sugar_19.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-f20c10b_001_area_delay.wcnf O = 28
T = 9.06
O = 28
T = 9.06
normalized-f20c10b_002_area_delay.wcnf O = 24
T = 7.40
O = 24
T = 7.40
normalized-f20c10b_003_area_delay.wcnf O = 26
T = 7.47
O = 26
T = 7.47
normalized-f20c10b_004_area_delay.wcnf O = 27
T = 7.53
O = 27
T = 7.53
normalized-f20c10b_005_area_delay.wcnf O = 26
T = 7.80
O = 26
T = 7.80
normalized-f20c10b_006_area_delay.wcnf O = 22
T = 7.33
O = 22
T = 7.33
normalized-f20c10b_007_area_delay.wcnf O = 26
T = 9.63
O = 26
T = 9.63
normalized-f20c10b_008_area_delay.wcnf O = 25
T = 7.60
O = 25
T = 7.60
normalized-f20c10b_009_area_delay.wcnf O = 24
T = 7.29
O = 24
T = 7.29
normalized-f20c10b_010_area_delay.wcnf O = 26
T = 11.40
O = 26
T = 11.40
normalized-f20c10b_011_area_delay.wcnf O = 26
T = 7.54
O = 26
T = 7.54
normalized-f20c10b_012_area_delay.wcnf O = 27
T = 7.81
O = 27
T = 7.81
normalized-f20c10b_013_area_delay.wcnf O = 22
T = 11.74
O = 22
T = 11.74
normalized-f20c10b_014_area_delay.wcnf O = 27
T = 8.49
O = 27
T = 8.49
normalized-f20c10b_015_area_delay.wcnf O = 25
T = 7.54
O = 25
T = 7.54
normalized-f20c10b_016_area_delay.wcnf O = 25
T = 7.57
O = 25
T = 7.57
normalized-f20c10b_017_area_delay.wcnf O = 25
T = 8.96
O = 25
T = 8.96
normalized-f20c10b_018_area_delay.wcnf O = 25
T = 7.34
O = 25
T = 7.34
normalized-f20c10b_019_area_delay.wcnf O = 24
T = 7.42
O = 24
T = 7.42
normalized-f20c10b_020_area_delay.wcnf O = 23
T = 7.37
O = 23
T = 7.37
normalized-f20c10b_021_area_delay.wcnf O = 24
T = 7.50
O = 24
T = 7.50
normalized-f20c10b_022_area_delay.wcnf O = 26
T = 7.62
O = 26
T = 7.62
normalized-f20c10b_023_area_delay.wcnf O = 22
T = 11.08
O = 22
T = 11.08
normalized-f20c10b_024_area_delay.wcnf O = 24
T = 7.47
O = 24
T = 7.47
normalized-f20c10b_025_area_delay.wcnf O = 25
T = 8.74
O = 25
T = 8.74
normalized-fir06_area_delay.wcnf O = 15
T = 7.25
O = 15
T = 7.25
normalized-fir07_area_delay.wcnf O = 16
T = 10.00
O = 16
T = 10.00
normalized-fir08_area_delay.wcnf O = 23
T = 43.20
O = 23
T = 43.20
normalized-fir08_area_opers.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-fir08_area_partials.wcnf O = 49
T = 8.58
O = 49
T = 8.58
normalized-fir09_area_delay.wcnf O = 17
T = 8.13
O = 17
T = 8.13
normalized-fir09_area_opers.wcnf O = 34
T = 10.76
O = 34
T = 10.76
simp-ibd_50.01.wcnf O = 53
T = 8.50
O = 53
T = 8.50
simp-ibd_50.02.wcnf O = 56
T = 20.81
O = 56
T = 20.81
simp-ibd_50.03.wcnf O = 54
T = 7.15
O = 54
T = 7.15
simp-ibd_50.04.wcnf O = 55
T = 15.27
O = 55
T = 15.27
simp-ibd_50.05.wcnf O = 59
T = 7.73
O = 59
T = 7.73
simp-ibd_50.06.wcnf O = 55
T = 26.94
O = 55
T = 26.94
simp-ibd_50.07.wcnf O = 57
T = 11.21
O = 57
T = 11.21
simp-ibd_50.08.wcnf O = 59
T = 13.63
O = 59
T = 13.63
simp-ibd_50.09.wcnf O = 57
T = 7.52
O = 57
T = 7.52
simp-test_chr21_YRI_75.wcnf O = 44
T = 12.37
O = 44
T = 12.37
SU1__simp-genos.haps.1.wcnf O = 73
T = 7.48
O = 73
T = 7.48
SU1__simp-genos.haps.10.wcnf O = 90
T = 15.31
O = 90
T = 15.31
SU1__simp-genos.haps.18.wcnf O = 74
T = 7.84
O = 74
T = 7.84
SU1__simp-genos.haps.19.wcnf O = 79
T = 7.75
O = 79
T = 7.75
SU1__simp-genos.haps.26.wcnf O = 81
T = 14.32
O = 81
T = 14.32
SU1__simp-genos.haps.27.wcnf O = 92
T = 7.94
O = 92
T = 7.94
SU1__simp-genos.haps.29.wcnf O = 68
T = 7.90
O = 68
T = 7.90
SU1__simp-genos.haps.30.wcnf O = 69
T = 8.45
O = 69
T = 8.45
SU1__simp-genos.haps.32.wcnf O = 71
T = 9.20
O = 71
T = 9.20
SU1__simp-genos.haps.34.wcnf O = 69
T = 7.75
O = 69
T = 7.75
SU1__simp-genos.haps.37.wcnf O = 77
T = 7.56
O = 77
T = 7.56
SU1__simp-genos.haps.38.wcnf O = 89
T = 8.96
O = 89
T = 8.96
SU1__simp-genos.haps.50.wcnf O = 59
T = 7.63
O = 59
T = 7.63
SU1__simp-genos.haps.54.wcnf O = 72
T = 7.69
O = 72
T = 7.69
SU1__simp-genos.haps.58.wcnf O = 85
T = 8.01
O = 85
T = 8.01
SU1__simp-genos.haps.62.wcnf O = 67
T = 7.96
O = 67
T = 7.96
SU1__simp-genos.haps.69.wcnf O = 76
T = 8.96
O = 76
T = 8.96
SU1__simp-genos.haps.7.wcnf O = 73
T = 144.61
O = 73
T = 144.61
SU1__simp-genos.haps.70.wcnf O = 58
T = 7.67
O = 58
T = 7.67
SU1__simp-genos.haps.8.wcnf O = 63
T = 7.49
O = 63
T = 7.49
SU1__simp-genos.haps.85.wcnf O = 65
T = 7.57
O = 65
T = 7.57
SU1__simp-genos.haps.86.wcnf O = 56
T = 7.83
O = 56
T = 7.83
SU3__simp-genos.haps.21.wcnf O = 116
T = 31.69
O = 116
T = 31.69
SU3__simp-genos.haps.23.wcnf O = 110
T = 7.95
O = 110
T = 7.95
SU3__simp-genos.haps.27.wcnf O = 99
T = 9.24
O = 99
T = 9.24
SU3__simp-genos.haps.33.wcnf O = 113
T = 8.08
O = 113
T = 8.08
SU3__simp-genos.haps.38.wcnf O = 100
T = 12.53
O = 100
T = 12.53
SU3__simp-genos.haps.53.wcnf O = 110
T = 41.71
O = 110
T = 41.71
SU3__simp-genos.haps.58.wcnf O = 101
T = 11.43
O = 101
T = 11.43
SU3__simp-genos.haps.60.wcnf O = 103
T = 10.88
O = 103
T = 10.88
SU3__simp-genos.haps.63.wcnf O = N/A
T = TO
O = N/A
T = TO
SU3__simp-genos.haps.64.wcnf O = 99
T = 13.72
O = 99
T = 13.72
SU3__simp-genos.haps.72.wcnf O = 92
T = 16.25
O = 92
T = 16.25
SU3__simp-genos.haps.74.wcnf O = 102
T = 7.53
O = 102
T = 7.53
SU3__simp-genos.haps.80.wcnf O = N/A
T = TO
O = N/A
T = TO
SU3__simp-genos.haps.86.wcnf O = 102
T = 8.42
O = 102
T = 8.42
SU3__simp-genos.haps.88.wcnf O = 106
T = 93.12
O = 106
T = 93.12
SU3__simp-genos.haps.9.wcnf O = 108
T = 43.86
O = 108
T = 43.86
normalized-f1000.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-f2000.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-f600.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-g125.17.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-g125.18.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-g250.15.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-g250.29.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-hanoi5.wcnf O = 1931
T = 7.87
O = 1931
T = 7.87
normalized-ii16a1.wcnf O = 1129
T = 155.32
O = 1129
T = 155.32
normalized-ii16a2.wcnf O = 1164
T = 19.89
O = 1164
T = 19.89
normalized-ii16b1.wcnf O = 1379
T = 9.91
O = 1379
T = 9.91
normalized-ii16c1.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii16c2.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii16d1.wcnf O = 890
T = 216.70
O = 890
T = 216.70
normalized-ii16d2.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii16e1.wcnf O = 1087
T = 145.55
O = 1087
T = 145.55
normalized-ii32b1.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii32c1.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii32c2.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii32c3.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii32c4.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii32d1.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii32d2.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii32d3.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii32e5.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii8a2.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii8a3.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii8a4.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii8b2.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii8b3.wcnf O = 507
T = 7.46
O = 507
T = 7.46
normalized-ii8b4.wcnf O = 654
T = 7.36
O = 654
T = 7.36
normalized-ii8c2.wcnf O = 525
T = 7.68
O = 525
T = 7.68
normalized-ii8d1.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii8d2.wcnf O = 540
T = 7.19
O = 540
T = 7.19
normalized-ii8e1.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ii8e2.wcnf O = 494
T = 8.27
O = 494
T = 8.27
normalized-par32-1-c.wcnf O = N/A
T = TO
O = 61597
T = 222.69
normalized-par32-1.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-par32-2-c.wcnf O = N/A
T = TO
O = 71321
T = 197.17
normalized-par32-2.wcnf O = N/A
T = TO
O = N/A
T = TO
c1355_F1001gat-1048gat@1.wcnf O = 21
T = 7.26
O = 21
T = 7.26
c1355_F1001gat@1.wcnf O = 21
T = 7.35
O = 21
T = 7.35
c1355_F1036gat-1229gat@1.wcnf O = 13
T = 7.25
O = 13
T = 7.25
c1355_F106gat-409gat@1.wcnf O = 33
T = 7.31
O = 33
T = 7.31
c1355_F106gat@0.wcnf O = 14
T = 7.38
O = 14
T = 7.38
c1355_F113gat-1260gat@1.wcnf O = 13
T = 7.34
O = 13
T = 7.34
c1355_F1150gat@0.wcnf O = 13
T = 7.27
O = 13
T = 7.27
c1355_F1183gat-1262gat@1.wcnf O = 33
T = 7.27
O = 33
T = 7.27
c1355_F120gat-414gat@1.wcnf O = 33
T = 7.33
O = 33
T = 7.33
c1355_F1229gat@1.wcnf O = 33
T = 7.22
O = 33
T = 7.22
c1355_F127gat-418gat@1.wcnf O = 33
T = 7.29
O = 33
T = 7.29
c1355_F141gat@0.wcnf O = 14
T = 7.37
O = 14
T = 7.37
c1355_F155gat@1.wcnf O = 14
T = 7.41
O = 14
T = 7.41
c1355_F176gat-1278gat@1.wcnf O = 13
T = 7.33
O = 13
T = 7.33
c1355_F183gat@0.wcnf O = 14
T = 7.35
O = 14
T = 7.35
c1355_F197gat-308gat@1.wcnf O = 33
T = 7.26
O = 33
T = 7.26
c1355_F1gat@0.wcnf O = 14
T = 7.33
O = 14
T = 7.33
c1355_F43gat@1.wcnf O = 14
T = 7.31
O = 14
T = 7.31
c1355_F50gat@1.wcnf O = 14
T = 7.35
O = 14
T = 7.35
c1355_F543gat@1.wcnf O = 33
T = 7.24
O = 33
T = 7.24
c1355_F57gat@1.wcnf O = 14
T = 7.34
O = 14
T = 7.34
c1355_F71gat@1.wcnf O = 14
T = 7.06
O = 14
T = 7.06
c3540_F20@1.wcnf O = 6
T = 7.39
O = 6
T = 7.39
c3540_F41@1.wcnf O = 7
T = 7.40
O = 7
T = 7.40
c3540_F45@0.wcnf O = 9
T = 7.60
O = 9
T = 7.60
c3540_F45@1.wcnf O = 9
T = 7.92
O = 9
T = 7.92
c6288_F137gat@1.wcnf O = 10
T = 7.08
O = 10
T = 7.08
c6288_F205gat@1.wcnf O = 7
T = 7.95
O = 7
T = 7.95
c6288_F35gat@1.wcnf O = 4
T = 7.33
O = 4
T = 7.33
c6288_F69gat@1.wcnf O = 6
T = 7.43
O = 6
T = 7.43
normalized-C499.a.wcnf O = 64
T = 7.94
O = 64
T = 7.94
normalized-addm4.r.wcnf O = 165
T = 7.41
O = 165
T = 7.41
normalized-alu4.b.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-apex6.b.wcnf O = 148
T = 21.40
O = 148
T = 21.40
normalized-bench1.r.wcnf O = 122
T = 242.90
O = 122
T = 242.90
normalized-des.a.wcnf O = 942
T = 10.92
O = 942
T = 10.92
normalized-duke2.b.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ex1010.pi.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-ex5.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-exam.pi.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-f51m.b.wcnf O = 18
T = 7.28
O = 18
T = 7.28
normalized-fout.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-jac3.wcnf O = 15
T = 7.56
O = 15
T = 7.56
normalized-lin.rom.r.wcnf O = 120
T = 7.87
O = 120
T = 7.87
normalized-m100_100_10_10.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-m100_100_10_15.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-m100_100_10_30.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-m100_100_30_30.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-m100_300_10_10.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-m100_300_10_14.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-m100_300_10_15.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-m100_300_10_20.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-m200_500_10_10.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-m4.r.wcnf O = 90
T = 7.08
O = 90
T = 7.08
normalized-maincont.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-max1024.pi.wcnf O = 259
T = 106.47
O = 259
T = 106.47
normalized-max1024.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-max512.r.wcnf O = 113
T = 7.00
O = 113
T = 7.00
normalized-mlp4.r.wcnf O = 109
T = 7.32
O = 109
T = 7.32
normalized-pdc.r.wcnf O = 94
T = 7.62
O = 94
T = 7.62
normalized-prom2.pi.wcnf O = 287
T = 25.45
O = 287
T = 25.45
normalized-prom2.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-rd84.b.wcnf O = 5
T = 7.66
O = 5
T = 7.66
normalized-rot.b.wcnf O = 115
T = 62.55
O = 115
T = 62.55
normalized-sao2.b.wcnf O = 25
T = 7.25
O = 25
T = 7.25
normalized-saucier.r.wcnf O = N/A
T = TO
O = N/A
T = TO
normalized-test1.r.wcnf O = 111
T = 246.60
O = 111
T = 246.60
normalized-test4.pi.wcnf O = 121
T = 246.89
O = 121
T = 246.89
ctrl.wcnf O = 15
T = 7.45
O = 15
T = 7.45
mrisc_mem2wire.wcnf O = 5
T = 16.16
O = 5
T = 16.16
spi.wcnf O = 46
T = 12.05
O = 46
T = 12.05
sudoku.wcnf O = 13
T = 12.65
O = 13
T = 12.65
SAT02__industrial__biere__dinphil__dp10s10.shuffled.cnf.wcnf.8.wcnf O = 240
T = 14.13
O = 240
T = 14.13
SAT02__industrial__goldberg__fpga_routing__vda_gr_rcs_w9.shuffled.cnf.wcnf.5.wcnf O = 6
T = 7.53
O = 6
T = 7.53
SAT02__industrial__goldberg__fpga_routing__vda_gr_rcs_w9.shuffled.cnf.wcnf.8.wcnf O = 3
T = 7.54
O = 3
T = 7.54
SAT04__industrial__vangelder__cnf-color__abb313GPIA-9-tr.used-as.sat04-321.cnf.wcnf.3.wcnf O = 80
T = 42.88
O = 80
T = 42.88
SAT04__industrial__vangelder__cnf-color__abb313GPIA-9-tr.used-as.sat04-321.cnf.wcnf.6.wcnf O = 25
T = 70.68
O = 25
T = 70.68
SAT04__industrial__velev__pipe-sat-1-1__12pipe_bug4_q0.used-as.sat04-723.cnf.wcnf.1.wcnf O = 179
T = 36.02
O = 179
T = 36.02
SAT04__industrial__velev__pipe-sat-1-1__12pipe_bug4_q0.used-as.sat04-723.cnf.wcnf.8.wcnf O = 86
T = 21.87
O = 86
T = 21.87
SAT04__industrial__velev__pipe-sat-1-1__12pipe_bug6_q0.used-as.sat04-725.cnf.wcnf.10.wcnf O = 50
T = 22.00
O = 50
T = 22.00
SAT04__industrial__velev__pipe-sat-1-1__12pipe_bug6_q0.used-as.sat04-725.cnf.wcnf.5.wcnf O = 53
T = 18.62
O = 53
T = 18.62
SAT07__industrial__vliw_sat_4.0__9vliw_m_9stages_iq3_C1_bug5.cnf.wcnf.4.wcnf O = 8
T = 36.72
O = 8
T = 36.72
SAT07__industrial__vliw_sat_4.0__9vliw_m_9stages_iq3_C1_bug6.cnf.wcnf.1.wcnf O = 14
T = 35.57
O = 14
T = 35.57
SAT07__industrial__vliw_sat_4.0__9vliw_m_9stages_iq3_C1_bug6.cnf.wcnf.4.wcnf O = 24
T = 59.21
O = 24
T = 59.21
SAT07__industrial__vliw_sat_4.0__9vliw_m_9stages_iq3_C1_bug6.cnf.wcnf.7.wcnf O = 3
T = 36.88
O = 3
T = 36.88
SAT09__APPLICATIONS__satComp09_BioInstances__rbcl_xits_15_SAT.cnf.wcnf.9.wcnf O = 26
T = 9.30
O = 26
T = 9.30
SAT09__APPLICATIONS__satComp09_BioInstances__rbcl_xits_18_SAT.cnf.wcnf.2.wcnf O = 7
T = 7.67
O = 7
T = 7.67
SAT11__application__fuhs__AProVE11__AProVE11-09.cnf.wcnf.10.wcnf O = 208
T = 42.61
O = 208
T = 42.61
SAT11__application__fuhs__AProVE11__AProVE11-09.cnf.wcnf.4.wcnf O = 1382
T = 71.48
O = 1382
T = 71.48
SAT11__application__fuhs__AProVE11__AProVE11-09.cnf.wcnf.8.wcnf O = 320
T = 54.59
O = 320
T = 54.59
SAT11__application__fuhs__AProVE11__AProVE11-10.cnf.wcnf.3.wcnf O = 1028
T = 173.99
O = 1028
T = 173.99
SAT11__application__fuhs__AProVE11__AProVE11-12.cnf.wcnf.2.wcnf O = 501
T = 20.07
O = 501
T = 20.07
SAT11__application__fuhs__AProVE11__AProVE11-12.cnf.wcnf.4.wcnf O = 180
T = 13.30
O = 180
T = 13.30
SAT11__application__fuhs__AProVE11__AProVE11-16.cnf.wcnf.1.wcnf O = 263
T = 18.59
O = 263
T = 18.59
SAT11__application__jarvisalo__AAAI2010-SATPlanning__aaai10-planning-ipc5-TPP-30-step11.cnf.wcnf.1.wcnf O = 1
T = 60.66
O = 1
T = 60.66
SAT11__application__jarvisalo__AAAI2010-SATPlanning__aaai10-planning-ipc5-pipesworld-12-step16.cnf.wcnf.2.wcnf O = 1
T = 10.05
O = 1
T = 10.05
SAT11__application__jarvisalo__AAAI2010-SATPlanning__aaai10-planning-ipc5-pipesworld-12-step16.cnf.wcnf.7.wcnf O = 1
T = 10.14
O = 1
T = 10.14
SAT11__application__jarvisalo__AAAI2010-SATPlanning__aaai10-planning-ipc5-pipesworld-18-step16.cnf.wcnf.1.wcnf O = 1
T = 42.20
O = 1
T = 42.20
SAT11__application__jarvisalo__AAAI2010-SATPlanning__aaai10-planning-ipc5-pipesworld-18-step16.cnf.wcnf.4.wcnf O = 1
T = 43.60
O = 1
T = 43.60
SAT11__application__jarvisalo__smtqfbv-aigs__smtlib-qfbv-aigs-bin_libmsrpc_vc1225336-tseitin.cnf.wcnf.4.wcnf O = 154
T = 34.28
O = 154
T = 34.28
SAT11__application__jarvisalo__smtqfbv-aigs__smtlib-qfbv-aigs-bin_libsmbsharemodes_vc5759-tseitin.cnf.wcnf.9.wcnf O = 118
T = 195.44
O = 118
T = 195.44
SAT11__application__jarvisalo__smtqfbv-aigs__smtlib-qfbv-aigs-rfunit_flat-64-tseitin.cnf.wcnf.10.wcnf O = 9
T = 9.56
O = 9
T = 9.56
SAT11__application__jarvisalo__smtqfbv-aigs__smtlib-qfbv-aigs-rfunit_flat-64-tseitin.cnf.wcnf.2.wcnf O = 73
T = 12.55
O = 73
T = 12.55
SAT11__application__jarvisalo__smtqfbv-aigs__smtlib-qfbv-aigs-rfunit_flat-64-tseitin.cnf.wcnf.7.wcnf O = 20
T = 10.50
O = 20
T = 10.50
SAT11__application__leberre__2dimensionalstrippacking__E05F18.cnf.wcnf.7.wcnf O = 61
T = 82.96
O = 61
T = 82.96
SAT11__application__leberre__2dimensionalstrippacking__E05F18.cnf.wcnf.9.wcnf O = 82
T = 39.40
O = 82
T = 39.40
SAT11__application__manthey__traffic__traffic_3_uc_sat.cnf.wcnf.8.wcnf O = 77
T = 17.60
O = 77
T = 17.60
SAT11__application__manthey__traffic__traffic_r_sat.cnf.wcnf.4.wcnf O = 78
T = 33.37
O = 78
T = 33.37
SAT11__application__manthey__traffic__traffic_r_sat.cnf.wcnf.6.wcnf O = 120
T = 14.65
O = 120
T = 14.65
SAT11__application__rintanen__SATPlanning__blocks-blocks-36-0.180-SAT.cnf.wcnf.2.wcnf O = 35
T = 81.21
O = 35
T = 81.21
SAT11__application__rintanen__SATPlanning__openstacks-sequencedstrips-nonadl-nonnegated-os-sequencedstrips-p30_3.085-SAT.cnf.wcnf.4.wcnf O = 6
T = 11.51
O = 6
T = 11.51
SAT_RACE06__ibm-2002-21r-k95.cnf.wcnf.4.wcnf O = 2
T = 55.91
O = 2
T = 55.91
SAT_RACE06__velev-pipe-sat-1.0-b9.cnf.wcnf.2.wcnf O = 25
T = 24.03
O = 25
T = 24.03
SAT_RACE06__velev-pipe-sat-1.0-b9.cnf.wcnf.5.wcnf O = 85
T = 26.86
O = 85
T = 26.86
SAT_RACE08__cnf__ibm-2004-01-k90.cnf.wcnf.10.wcnf O = 5
T = 8.24
O = 5
T = 8.24
TEAMS20_l7aa.cnf.wcnf O = 26
T = 17.78
O = 26
T = 17.78
teams16_l7a.cnf.wcnf O = 18
T = 8.88
O = 18
T = 8.88
teams20_l2a.cnf.wcnf O = 12
T = 10.25
O = 12
T = 10.25
teams20_l4a.cnf.wcnf O = 18
T = 12.96
O = 18
T = 12.96
teams20_l6a.cnf.wcnf O = 18
T = 10.36
O = 18
T = 10.36
teams20_l8a.cnf.wcnf O = 16
T = 8.73
O = 16
T = 8.73
teams24_l4a.cnf.wcnf O = 14
T = 16.56
O = 14
T = 16.56
cnf.10.p.10.wcnf O = 10
T = 31.30
O = 10
T = 31.30
cnf.10.p.9.wcnf O = 10
T = 32.46
O = 10
T = 32.46
cnf.11.p.10.wcnf O = 11
T = 29.97
O = 11
T = 29.97
cnf.11.p.9.wcnf O = 11
T = 123.59
O = 11
T = 123.59
cnf.12.p.10.wcnf O = 12
T = 77.63
O = 12
T = 77.63
cnf.12.p.8.wcnf O = 12
T = 39.15
O = 12
T = 39.15
cnf.12.p.9.wcnf O = 12
T = 77.08
O = 12
T = 77.08
cnf.12.t.9.wcnf O = 12
T = 17.50
O = 12
T = 17.50
cnf.13.p.10.wcnf O = 13
T = 49.61
O = 13
T = 49.61
cnf.13.p.8.wcnf O = 13
T = 67.32
O = 13
T = 67.32
cnf.13.p.9.wcnf O = 13
T = 39.49
O = 13
T = 39.49
cnf.14.d.10.wcnf O = 14
T = 24.70
O = 14
T = 24.70
cnf.14.p.10.wcnf O = 14
T = 96.12
O = 14
T = 96.12
cnf.14.p.9.wcnf O = 14
T = 71.76
O = 14
T = 71.76
cnf.14.t.7.wcnf O = 14
T = 15.72
O = 14
T = 15.72
cnf.14.t.9.wcnf O = 14
T = 19.10
O = 14
T = 19.10
cnf.15.p.10.wcnf O = 15
T = 94.43
O = 15
T = 94.43
cnf.15.p.8.wcnf O = 15
T = 56.23
O = 15
T = 56.23
cnf.15.p.9.wcnf O = 15
T = 98.59
O = 15
T = 98.59
cnf.15.t.10.wcnf O = 15
T = 28.79
O = 15
T = 28.79
cnf.16.p.10.wcnf O = 16
T = 136.90
O = 16
T = 136.90
cnf.16.p.8.wcnf O = 16
T = 95.35
O = 16
T = 95.35
cnf.16.p.9.wcnf O = 16
T = 172.87
O = 16
T = 172.87
cnf.16.t.9.wcnf O = 16
T = 25.74
O = 16
T = 25.74
cnf.17.d.10.wcnf O = 17
T = 24.89
O = 17
T = 24.89
cnf.17.d.9.wcnf O = 17
T = 17.34
O = 17
T = 17.34
cnf.17.p.10.wcnf O = 17
T = 127.61
O = 17
T = 127.61
cnf.17.p.9.wcnf O = 17
T = 167.60
O = 17
T = 167.60
cnf.17.t.10.wcnf O = 17
T = 25.14
O = 17
T = 25.14
cnf.17.t.8.wcnf O = 17
T = 16.48
O = 17
T = 16.48
cnf.18.d.7.wcnf O = 18
T = 18.93
O = 18
T = 18.93
cnf.18.p.10.wcnf O = 18
T = 232.99
O = 18
T = 232.99
cnf.18.p.8.wcnf O = 18
T = 96.45
O = 18
T = 96.45
cnf.18.p.9.wcnf O = 18
T = 145.20
O = 18
T = 145.20
cnf.18.t.9.wcnf O = 18
T = 25.66
O = 18
T = 25.66
cnf.19.d.10.wcnf O = 19
T = 22.98
O = 19
T = 22.98
cnf.19.p.10.wcnf O = 19
T = 195.41
O = 19
T = 195.41
cnf.19.p.8.wcnf O = 19
T = 70.83
O = 19
T = 70.83
cnf.19.p.9.wcnf O = 19
T = 206.42
O = 19
T = 206.42
cnf.19.t.7.wcnf O = 19
T = 26.58
O = 19
T = 26.58
cnf.20.d.10.wcnf O = 20
T = 23.24
O = 20
T = 23.24
cnf.20.d.9.wcnf O = 20
T = 24.06
O = 20
T = 24.06
cnf.20.p.10.wcnf O = N/A
T = TO
O = N/A
T = TO
cnf.20.p.9.wcnf O = N/A
T = TO
O = N/A
T = TO
cnf.20.t.10.wcnf O = 20
T = 42.20
O = 20
T = 42.20
cnf.20.t.8.wcnf O = 20
T = 28.41
O = 20
T = 28.41
cnf.8.p.10.wcnf O = 8
T = 23.25
O = 8
T = 23.25
cnf.8.p.9.wcnf O = 8
T = 14.67
O = 8
T = 14.67
cnf.9.p.10.wcnf O = 9
T = 32.65
O = 9
T = 32.65
cnf.9.p.9.wcnf O = 9
T = 30.73
O = 9
T = 30.73
splitedReads_0.matrix.wcnf O = 2907
T = 37.16
O = 2907
T = 37.16
splitedReads_137.matrix.wcnf O = 90
T = 7.53
O = 90
T = 7.53
splitedReads_158.matrix.wcnf O = 173
T = 7.87
O = 173
T = 7.87
splitedReads_160.matrix.wcnf O = 186
T = 7.89
O = 186
T = 7.89
splitedReads_18.matrix.wcnf O = 138
T = 7.68
O = 138
T = 7.68
splitedReads_414.matrix.wcnf O = 171
T = 7.69
O = 171
T = 7.69
GreeceWesternGreeceUniversityInstance4.xml.wcnf O = N/A
T = TO
O = N/A
T = TO
SouthAfricaWoodlands2009.xml.wcnf O = 0
T = 22.87
O = 0
T = 22.87
b14_C-mbd14-0209.wcnf O = 25
T = 66.45
O = 25
T = 66.45
b14_C-mbd14-0213.wcnf O = 27
T = 15.98
O = 27
T = 15.98
b14_C-mbd14-0218.wcnf O = 25
T = 26.46
O = 25
T = 26.46
b14_C-mbd14-0225.wcnf O = 24
T = 44.20
O = 24
T = 44.20
b14_C-mbd14-0231.wcnf O = 22
T = 39.31
O = 22
T = 39.31
b14_C-mbd14-0248.wcnf O = 25
T = 13.54
O = 25
T = 13.54
b14_C-mbd14-0256.wcnf O = 22
T = 13.42
O = 22
T = 13.42
b14_C-mbd14-0259.wcnf O = 21
T = 7.41
O = 21
T = 7.41
b15_C-mbd14-0240.wcnf O = 21
T = 35.41
O = 21
T = 35.41
b15_C-mbd14-0256.wcnf O = 24
T = 7.62
O = 24
T = 7.62
b15_C-mbd14-0259.wcnf O = 22
T = 7.85
O = 22
T = 7.85
b15_C-mbd14-0288.wcnf O = 26
T = 16.66
O = 26
T = 16.66
b15_C-mbd14-0305.wcnf O = 23
T = 9.48
O = 23
T = 9.48
b15_C-mbd14-0330.wcnf O = 20
T = 8.17
O = 20
T = 8.17
b17_C-mbd14-0205.wcnf O = 22
T = 7.58
O = 22
T = 7.58
b17_C-mbd14-0206.wcnf O = 27
T = 7.76
O = 27
T = 7.76
b17_C-mbd14-0217.wcnf O = 24
T = 7.50
O = 24
T = 7.50
b17_C-mbd14-0218.wcnf O = 27
T = 7.53
O = 27
T = 7.53
b17_C-mbd14-0220.wcnf O = 24
T = 7.85
O = 24
T = 7.85
b17_C-mbd14-0224.wcnf O = 23
T = 7.60
O = 23
T = 7.60
b17_C-mbd14-0229.wcnf O = 19
T = 7.80
O = 19
T = 7.80
b17_C-mbd14-0230.wcnf O = 24
T = 7.39
O = 24
T = 7.39
b20_C-mbd14-0202.wcnf O = 21
T = 7.51
O = 21
T = 7.51
b20_C-mbd14-0211.wcnf O = 23
T = 10.97
O = 23
T = 10.97
b20_C-mbd14-0213.wcnf O = 22
T = 8.33
O = 22
T = 8.33
b20_C-mbd14-0214.wcnf O = 17
T = 8.49
O = 17
T = 8.49
b20_C-mbd14-0216.wcnf O = 26
T = 8.00
O = 26
T = 8.00
b20_C-mbd14-0217.wcnf O = 21
T = 8.01
O = 21
T = 8.01
b20_C-mbd14-0221.wcnf O = 22
T = 8.08
O = 22
T = 8.08
b20_C-mbd14-0222.wcnf O = 28
T = 27.53
O = 28
T = 27.53
b21_C-mbd14-0203.wcnf O = 27
T = 12.90
O = 27
T = 12.90
b21_C-mbd14-0204.wcnf O = 22
T = 7.65
O = 22
T = 7.65
b21_C-mbd14-0205.wcnf O = 21
T = 11.42
O = 21
T = 11.42
b21_C-mbd14-0217.wcnf O = 21
T = 7.98
O = 21
T = 7.98
b21_C-mbd14-0218.wcnf O = N/A
T = TO
O = N/A
T = TO
b21_C-mbd14-0221.wcnf O = 19
T = 7.45
O = 19
T = 7.45
b21_C-mbd14-0224.wcnf O = 16
T = 7.43
O = 16
T = 7.43
b21_C-mbd14-0227.wcnf O = 24
T = 7.56
O = 24
T = 7.56
b22_C-mbd14-0204.wcnf O = 23
T = 7.76
O = 23
T = 7.76
b22_C-mbd14-0205.wcnf O = 28
T = 7.80
O = 28
T = 7.80
b22_C-mbd14-0207.wcnf O = 25
T = 7.54
O = 25
T = 7.54
b22_C-mbd14-0208.wcnf O = 23
T = 7.56
O = 23
T = 7.56
b22_C-mbd14-0210.wcnf O = 26
T = 8.14
O = 26
T = 8.14
b22_C-mbd14-0211.wcnf O = 22
T = 7.61
O = 22
T = 7.61
b22_C-mbd14-0213.wcnf O = 26
T = 7.63
O = 26
T = 7.63
b22_C-mbd14-0215.wcnf O = 22
T = 7.66
O = 22
T = 7.66
1aabfc32-d491-11df-9a24-00163e3d3b7c_l3.wcnf O = 2236
T = 14.96
O = 2236
T = 14.96
2c3aece6-c8b2-11df-a040-00163e3d3b7c_l3.wcnf O = 814
T = 7.66
O = 814
T = 7.66
4ede8d96-c17a-11df-a7c5-00163e3d3b7c_l3.wcnf O = 631
T = 8.12
O = 631
T = 8.12
7f80e4f0-4fe9-11e0-acd7-00163e1e087d_l3.wcnf O = 404
T = 7.47
O = 404
T = 7.47
ff4a1d84-d490-11df-9e6c-00163e3d3b7c_l3.wcnf O = 2236
T = 16.43
O = 2236
T = 16.43
rand118_l2.wcnf O = 447
T = 8.04
O = 447
T = 8.04
rand172_l2.wcnf O = 670
T = 9.07
O = 670
T = 9.07
rand179_l2.wcnf O = 1088
T = 10.09
O = 1088
T = 10.09
rand196_l2.wcnf O = 1298
T = 11.05
O = 1298
T = 11.05
rand208_l2.wcnf O = 349
T = 8.07
O = 349
T = 8.07
rand209_l2.wcnf O = 1199
T = 9.99
O = 1199
T = 9.99
rand21_l2.wcnf O = 1465
T = 12.11
O = 1465
T = 12.11
rand242_l2.wcnf O = 388
T = 8.22
O = 388
T = 8.22
rand289_l2.wcnf O = 350
T = 8.01
O = 350
T = 8.01
rand290_l2.wcnf O = 1017
T = 9.98
O = 1017
T = 9.98
rand308_l2.wcnf O = 1235
T = 9.98
O = 1235
T = 9.98
rand30_l2.wcnf O = 512
T = 8.26
O = 512
T = 8.26
rand313_l2.wcnf O = 1595
T = 11.71
O = 1595
T = 11.71
rand377_l2.wcnf O = 574
T = 8.01
O = 574
T = 8.01
rand411_l2.wcnf O = 578
T = 8.36
O = 578
T = 8.36
rand414_l2.wcnf O = 1259
T = 9.61
O = 1259
T = 9.61
rand425_l2.wcnf O = 694
T = 8.80
O = 694
T = 8.80
rand446_l2.wcnf O = 416
T = 8.30
O = 416
T = 8.30
rand484_l2.wcnf O = 331
T = 7.94
O = 331
T = 7.94
rand507_l2.wcnf O = 1197
T = 9.35
O = 1197
T = 9.35
rand695_l2.wcnf O = 974
T = 8.79
O = 974
T = 8.79
rand717_l2.wcnf O = 1120
T = 10.19
O = 1120
T = 10.19
rand736_l2.wcnf O = 1232
T = 9.64
O = 1232
T = 9.64
rand736_l3.wcnf O = 1481
T = 7.51
O = 1481
T = 7.51
rand794_l2.wcnf O = 472
T = 8.30
O = 472
T = 8.30
rand7_l2.wcnf O = 971
T = 9.63
O = 971
T = 9.63
rand813_l2.wcnf O = 1192
T = 9.41
O = 1192
T = 9.41
rand869_l2.wcnf O = 459
T = 8.29
O = 459
T = 8.29
rand874_l2.wcnf O = 863
T = 9.31
O = 863
T = 9.31
rand892_l2.wcnf O = 1119
T = 9.36
O = 1119
T = 9.36
rand937_l2.wcnf O = 439
T = 7.84
O = 439
T = 7.84
rand943_l2.wcnf O = 829
T = 9.00
O = 829
T = 9.00
rand954_l2.wcnf O = 700
T = 8.66
O = 700
T = 8.66
rand96_l2.wcnf O = 392
T = 8.16
O = 392
T = 8.16
rand984_l2.wcnf O = 839
T = 9.40
O = 839
T = 9.40
10tree110p.wcnf O = 20
T = 8.59
O = 20
T = 8.59
10tree120p.wcnf O = 41
T = 8.56
O = 41
T = 8.56
10tree130p.wcnf O = 63
T = 16.06
O = 63
T = 16.06
10tree215p.wcnf O = 31
T = 8.22
O = 31
T = 8.22
10tree225p.wcnf O = 52
T = 14.67
O = 52
T = 14.67
10tree305p.wcnf O = 9
T = 8.42
O = 9
T = 8.42
10tree315p.wcnf O = 30
T = 12.51
O = 30
T = 12.51
10tree325p.wcnf O = 48
T = 8.87
O = 48
T = 8.87
10tree405p.wcnf O = 9
T = 7.93
O = 9
T = 7.93
10tree410p.wcnf O = 21
T = 8.33
O = 21
T = 8.33
10tree420p.wcnf O = 41
T = 18.77
O = 41
T = 18.77
10tree430p.wcnf O = 62
T = 12.54
O = 62
T = 12.54
10tree505posib.wcnf O = 10
T = 7.96
O = 10
T = 7.96
10tree515p.wcnf O = 29
T = 9.88
O = 29
T = 9.88
10tree525p.wcnf O = 52
T = 12.36
O = 52
T = 12.36
15tree1001p.wcnf O = 13
T = 26.06
O = 13
T = 26.06
15tree101p.wcnf O = 13
T = 14.65
O = 13
T = 14.65
15tree201p.wcnf O = 13
T = 11.19
O = 13
T = 11.19
15tree301p.wcnf O = 13
T = 19.95
O = 13
T = 19.95
15tree401p.wcnf O = 13
T = 18.55
O = 13
T = 18.55
15tree501p.wcnf O = 13
T = 23.05
O = 13
T = 23.05
15tree601p.wcnf O = 13
T = 10.23
O = 13
T = 10.23
15tree701p.wcnf O = 13
T = 14.40
O = 13
T = 14.40
15tree801p.wcnf O = 13
T = 13.72
O = 13
T = 13.72
15tree901p.wcnf O = 13
T = 14.17
O = 13
T = 14.17
10tree115p.wcnf O = 31
T = 8.81
O = 31
T = 8.81
10tree125p.wcnf O = 52
T = 9.70
O = 52
T = 9.70
10tree210p.wcnf O = 21
T = 7.44
O = 21
T = 7.44
10tree220p.wcnf O = 42
T = 8.84
O = 42
T = 8.84
10tree230p.wcnf O = 63
T = 14.96
O = 63
T = 14.96
10tree310p.wcnf O = 21
T = 8.05
O = 21
T = 8.05
10tree320p.wcnf O = 42
T = 8.33
O = 42
T = 8.33
10tree330p.wcnf O = 63
T = 11.17
O = 63
T = 11.17
10tree405posib.wcnf O = 10
T = 7.39
O = 10
T = 7.39
10tree415p.wcnf O = 31
T = 8.56
O = 31
T = 8.56
10tree425p.wcnf O = 52
T = 8.45
O = 52
T = 8.45
10tree505p.wcnf O = 10
T = 8.00
O = 10
T = 8.00
10tree510p.wcnf O = 21
T = 8.29
O = 21
T = 8.29
10tree520p.wcnf O = 42
T = 9.27
O = 42
T = 9.27
10tree530p.wcnf O = 63
T = 8.18
O = 63
T = 8.18
15tree1001posib.wcnf O = 13
T = 8.07
O = 13
T = 8.07
15tree101posib.wcnf O = 13
T = 9.29
O = 13
T = 9.29
15tree201posib.wcnf O = 13
T = 8.69
O = 13
T = 8.69
15tree301posib.wcnf O = 13
T = 9.50
O = 13
T = 9.50
15tree401posib.wcnf O = 13
T = 8.79
O = 13
T = 8.79
15tree501posib.wcnf O = 13
T = 8.28
O = 13
T = 8.28
15tree601posib.wcnf O = 13
T = 8.46
O = 13
T = 8.46
15tree701posib.wcnf O = 13
T = 8.19
O = 13
T = 8.19
15tree801posib.wcnf O = 13
T = 9.67
O = 13
T = 9.67
15tree901posib.wcnf O = 13
T = 8.31
O = 13
T = 8.31
normalized-s3-3-3-1pb.wcnf O = 36
T = 6.92
O = 36
T = 6.92
normalized-s3-3-3-2pb.wcnf O = 36
T = 6.98
O = 36
T = 6.98
normalized-s3-3-3-3pb.wcnf O = 36
T = 6.97
O = 36
T = 6.97
normalized-s3-3-3-4pb.wcnf O = 36
T = 6.96
O = 36
T = 6.96
normalized-s3-3-3-5pb.wcnf O = 34
T = 7.26
O = 34
T = 7.26
normalized-s4-4-3-10pb.wcnf O = 70
T = 7.28
O = 70
T = 7.28
normalized-s4-4-3-1pb.wcnf O = 62
T = 7.46
O = 62
T = 7.46
normalized-s4-4-3-2pb.wcnf O = 64
T = 7.59
O = 64
T = 7.59
normalized-s4-4-3-3pb.wcnf O = 62
T = 8.27
O = 62
T = 8.27
normalized-s4-4-3-4pb.wcnf O = 60
T = 7.59
O = 60
T = 7.59
normalized-s4-4-3-5pb.wcnf O = 60
T = 7.69
O = 60
T = 7.69
normalized-s4-4-3-6pb.wcnf O = 66
T = 7.46
O = 66
T = 7.46
normalized-s4-4-3-7pb.wcnf O = 64
T = 7.99
O = 64
T = 7.99
normalized-s4-4-3-8pb.wcnf O = 36
T = 7.33
O = 36
T = 7.33
normalized-s4-4-3-9pb.wcnf O = 68
T = 7.93
O = 68
T = 7.93
1bpi_.2knt_.g.wcnf.t.wcnf O = 35
T = 13.57
O = 35
T = 13.57
1bpi_.5pti_.g.wcnf.t.wcnf O = 29
T = 18.02
O = 29
T = 18.02
1knt_.1bpi_.g.wcnf.t.wcnf O = 35
T = 14.62
O = 35
T = 14.62
1knt_.2knt_.g.wcnf.t.wcnf O = 16
T = 10.13
O = 16
T = 10.13
1knt_.5pti_.g.wcnf.t.wcnf O = N/A
T = TO
O = N/A
T = TO
1vii_.1cph_.g.wcnf.t.wcnf O = N/A
T = TO
O = N/A
T = TO
2knt_.5pti_.g.wcnf.t.wcnf O = N/A
T = TO
O = N/A
T = TO
3ebx_.1era_.g.wcnf.t.wcnf O = 34
T = 13.99
O = 34
T = 13.99
3ebx_.6ebx_.g.wcnf.t.wcnf O = N/A
T = TO
O = N/A
T = TO
6ebx_.1era_.g.wcnf.t.wcnf O = N/A
T = TO
O = N/A
T = TO
p1.wcnf.t.wcnf O = 35
T = 13.81
O = 35
T = 13.81
sandiaprotein.g.wcnf.t.wcnf O = 28
T = 13.25
O = 28
T = 13.25
b18-s_PathRelaxation_Set_FS_1.wcnf O = 148
T = 14.30
O = 148
T = 14.30
b18-s_PathRelaxation_Set_FS_10.wcnf O = 113
T = 80.59
O = 113
T = 80.59
b18-s_PathRelaxation_Set_FS_11.wcnf O = 113
T = 43.44
O = 113
T = 43.44
b18-s_PathRelaxation_Set_FS_12.wcnf O = 113
T = 53.09
O = 113
T = 53.09
b18-s_PathRelaxation_Set_FS_2.wcnf O = 145
T = 36.88
O = 145
T = 36.88
b18-s_PathRelaxation_Set_FS_3.wcnf O = 145
T = 55.23
O = 145
T = 55.23
b18-s_PathRelaxation_Set_FS_4.wcnf O = 145
T = 259.40
O = 145
T = 259.40
b18-s_PathRelaxation_Set_FS_5.wcnf O = 145
T = 187.47
O = 145
T = 187.47
b18-s_PathRelaxation_Set_FS_6.wcnf O = 145
T = 275.61
O = 145
T = 275.61
b18-s_PathRelaxation_Set_FS_7.wcnf O = 145
T = 168.98
O = 145
T = 168.98
b18-s_PathRelaxation_Set_FS_8.wcnf O = 145
T = 260.80
O = 145
T = 260.80
b18-s_PathRelaxation_Set_FS_9.wcnf O = 145
T = 262.39
O = 145
T = 262.39
b20-s_PathRelaxation_Set_FS_1.wcnf O = 84
T = 9.70
O = 84
T = 9.70
b20-s_PathRelaxation_Set_FS_10.wcnf O = 83
T = 15.80
O = 83
T = 15.80
b20-s_PathRelaxation_Set_FS_11.wcnf O = 83
T = 12.15
O = 83
T = 12.15
b20-s_PathRelaxation_Set_FS_12.wcnf O = 83
T = 12.12
O = 83
T = 12.12
b20-s_PathRelaxation_Set_FS_2.wcnf O = 83
T = 10.02
O = 83
T = 10.02
b20-s_PathRelaxation_Set_FS_3.wcnf O = 83
T = 14.91
O = 83
T = 14.91
b20-s_PathRelaxation_Set_FS_4.wcnf O = 83
T = 16.42
O = 83
T = 16.42
b20-s_PathRelaxation_Set_FS_5.wcnf O = 83
T = 13.23
O = 83
T = 13.23
b20-s_PathRelaxation_Set_FS_6.wcnf O = 83
T = 13.72
O = 83
T = 13.72
b20-s_PathRelaxation_Set_FS_7.wcnf O = 83
T = 13.25
O = 83
T = 13.25
b20-s_PathRelaxation_Set_FS_8.wcnf O = 83
T = 16.76
O = 83
T = 16.76
b20-s_PathRelaxation_Set_FS_9.wcnf O = 83
T = 12.20
O = 83
T = 12.20
b21-s_PathRelaxation_Set_FS_1.wcnf O = 89
T = 10.52
O = 89
T = 10.52
b21-s_PathRelaxation_Set_FS_10.wcnf O = 88
T = 21.95
O = 88
T = 21.95
b21-s_PathRelaxation_Set_FS_11.wcnf O = 88
T = 23.87
O = 88
T = 23.87
b21-s_PathRelaxation_Set_FS_12.wcnf O = 88
T = 25.85
O = 88
T = 25.85
b21-s_PathRelaxation_Set_FS_2.wcnf O = 89
T = 34.91
O = 89
T = 34.91
b21-s_PathRelaxation_Set_FS_3.wcnf O = 89
T = 23.55
O = 89
T = 23.55
b21-s_PathRelaxation_Set_FS_4.wcnf O = 89
T = 25.17
O = 89
T = 25.17
b21-s_PathRelaxation_Set_FS_5.wcnf O = 89
T = 30.48
O = 89
T = 30.48
b21-s_PathRelaxation_Set_FS_6.wcnf O = 88
T = 29.70
O = 88
T = 29.70
b21-s_PathRelaxation_Set_FS_7.wcnf O = 88
T = 30.31
O = 88
T = 30.31
b21-s_PathRelaxation_Set_FS_8.wcnf O = 88
T = 29.20
O = 88
T = 29.20
b21-s_PathRelaxation_Set_FS_9.wcnf O = 88
T = 25.80
O = 88
T = 25.80
b21-s_PathRelaxation_FS_1.wcnf O = 89
T = 9.17
O = 89
T = 9.17
b21-s_PathRelaxation_FS_10.wcnf O = 89
T = 9.39
O = 89
T = 9.39
b21-s_PathRelaxation_FS_11.wcnf O = 88
T = 8.78
O = 88
T = 8.78
b21-s_PathRelaxation_FS_12.wcnf O = 88
T = 9.09
O = 88
T = 9.09
b21-s_PathRelaxation_FS_13.wcnf O = 89
T = 8.80
O = 89
T = 8.80
b21-s_PathRelaxation_FS_14.wcnf O = 89
T = 8.97
O = 89
T = 8.97
b21-s_PathRelaxation_FS_15.wcnf O = 89
T = 9.99
O = 89
T = 9.99
b21-s_PathRelaxation_FS_16.wcnf O = 88
T = 12.10
O = 88
T = 12.10
b21-s_PathRelaxation_FS_17.wcnf O = 88
T = 8.86
O = 88
T = 8.86
b21-s_PathRelaxation_FS_18.wcnf O = 88
T = 9.17
O = 88
T = 9.17
b21-s_PathRelaxation_FS_19.wcnf O = 88
T = 9.66
O = 88
T = 9.66
b21-s_PathRelaxation_FS_2.wcnf O = 90
T = 11.23
O = 90
T = 11.23
b21-s_PathRelaxation_FS_20.wcnf O = 88
T = 9.36
O = 88
T = 9.36
b21-s_PathRelaxation_FS_21.wcnf O = 88
T = 12.61
O = 88
T = 12.61
b21-s_PathRelaxation_FS_22.wcnf O = 88
T = 9.74
O = 88
T = 9.74
b21-s_PathRelaxation_FS_23.wcnf O = 88
T = 12.35
O = 88
T = 12.35
b21-s_PathRelaxation_FS_24.wcnf O = 88
T = 11.75
O = 88
T = 11.75
b21-s_PathRelaxation_FS_25.wcnf O = 88
T = 8.56
O = 88
T = 8.56
b21-s_PathRelaxation_FS_3.wcnf O = 90
T = 13.57
O = 90
T = 13.57
b21-s_PathRelaxation_FS_4.wcnf O = 92
T = 9.33
O = 92
T = 9.33
b21-s_PathRelaxation_FS_5.wcnf O = 89
T = 10.27
O = 89
T = 10.27
b21-s_PathRelaxation_FS_6.wcnf O = 88
T = 10.74
O = 88
T = 10.74
b21-s_PathRelaxation_FS_7.wcnf O = 89
T = 10.36
O = 89
T = 10.36
b21-s_PathRelaxation_FS_8.wcnf O = 89
T = 9.70
O = 89
T = 9.70
b21-s_PathRelaxation_FS_9.wcnf O = 88
T = 9.90
O = 88
T = 9.90
TWComp_1c75_N69.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_1dj7_N73.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_1dp_N76.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_1en2_N69.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_alarm_N37.wcnf O = 4
T = 7.38
O = 4
T = 7.38
TWComp_barle_N48.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_barley-pp_N26.wcnf O = 7
T = 7.63
O = 7
T = 7.63
TWComp_barley2_N48.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_celar02_N100.wcnf O = 10
T = 13.84
O = 10
T = 13.84
TWComp_celar09pp_N67.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_david-pp_N29.wcnf O = 13
T = 9.51
O = 13
T = 9.51
TWComp_david_N87.wcnf O = 13
T = 26.24
O = 13
T = 26.24
TWComp_eil51.tsp_N51.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_hailfinder_N56.wcnf O = 4
T = 8.22
O = 4
T = 8.22
TWComp_hepar2_N70.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_huck_N74.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_jean_N77.wcnf O = 9
T = 9.87
O = 9
T = 9.87
TWComp_mainuk_N48.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_mildew_35.wcnf O = 4
T = 7.50
O = 4
T = 7.50
TWComp_miles500_N128.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_mulsol.i.5-pp_N119.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_myciel4_N23.wcnf O = 10
T = 20.59
O = 10
T = 20.59
TWComp_myciel5_N47.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_oesoca+_N67.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_oesoca4_N42.wcnf O = 3
T = 7.67
O = 3
T = 7.67
TWComp_oesoca_N39.wcnf O = 3
T = 7.42
O = 3
T = 7.42
TWComp_pathfinder_N109.wcnf O = 6
T = 14.05
O = 6
T = 14.05
TWComp_queen5_5_N25.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_queen6_6_N36.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_queen7_7_N49.wcnf O = N/A
T = TO
O = N/A
T = TO
TWComp_ship-ship-pp_N30.wcnf O = 8
T = 44.04
O = 8
T = 44.04
TWComp_water_N32.wcnf O = 9
T = 8.37
O = 9
T = 8.37
TWComp_win95pts_N76.wcnf O = 8
T = 10.84
O = 8
T = 10.84