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-co
mul_8_11.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
mul_8_13.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
mul_8_14.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
mul_8_3.wcnf S = OPT
O = 36
T = 348.29		 S = OPT
O = 36
T = 348.29
mul_8_9.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
sbox_4.wcnf S = OPT
O = 22
T = 10.38		 S = OPT
O = 22
T = 10.38
sbox_8.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_mesat_01.wcnf S = OPT
O = 20
T = 65.82		 S = OPT
O = 20
T = 65.82
atcoss_mesat_02.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_mesat_03.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_mesat_04.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_mesat_05.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_mesat_06.wcnf S = OPT
O = 20
T = 138.65		 S = OPT
O = 20
T = 138.65
atcoss_mesat_07.wcnf S = OPT
O = 0
T = 21.24		 S = OPT
O = 0
T = 21.24
atcoss_mesat_08.wcnf S = OPT
O = 0
T = 22.63		 S = OPT
O = 0
T = 22.63
atcoss_mesat_09.wcnf S = OPT
O = 0
T = 36.02		 S = OPT
O = 0
T = 36.02
atcoss_mesat_10.wcnf S = OPT
O = 13
T = 1233.60		 S = OPT
O = 13
T = 1233.60
atcoss_mesat_11.wcnf S = OPT
O = 50
T = 23.17		 S = OPT
O = 50
T = 23.17
atcoss_mesat_12.wcnf S = OPT
O = 12
T = 19.08		 S = OPT
O = 12
T = 19.08
atcoss_mesat_13.wcnf S = OPT
O = 0
T = 94.85		 S = OPT
O = 0
T = 94.85
atcoss_mesat_14.wcnf S = OPT
O = 0
T = 114.18		 S = OPT
O = 0
T = 114.18
atcoss_mesat_15.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_mesat_16.wcnf S = OPT
O = 0
T = 27.18		 S = OPT
O = 0
T = 27.18
atcoss_mesat_17.wcnf S = OPT
O = 0
T = 37.07		 S = OPT
O = 0
T = 37.07
atcoss_mesat_18.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_sugar_01.wcnf S = OPT
O = 20
T = 47.76		 S = OPT
O = 20
T = 47.76
atcoss_sugar_02.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_sugar_03.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_sugar_04.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_sugar_05.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_sugar_06.wcnf S = OPT
O = 20
T = 76.14		 S = OPT
O = 20
T = 76.14
atcoss_sugar_07.wcnf S = OPT
O = 0
T = 16.39		 S = OPT
O = 0
T = 16.39
atcoss_sugar_08.wcnf S = OPT
O = 0
T = 15.02		 S = OPT
O = 0
T = 15.02
atcoss_sugar_09.wcnf S = OPT
O = 0
T = 24.84		 S = OPT
O = 0
T = 24.84
atcoss_sugar_10.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_sugar_11.wcnf S = OPT
O = 50
T = 12.88		 S = OPT
O = 50
T = 12.88
atcoss_sugar_12.wcnf S = OPT
O = 12
T = 31.08		 S = OPT
O = 12
T = 31.08
atcoss_sugar_13.wcnf S = OPT
O = 0
T = 50.98		 S = OPT
O = 0
T = 50.98
atcoss_sugar_14.wcnf S = OPT
O = 0
T = 59.68		 S = OPT
O = 0
T = 59.68
atcoss_sugar_15.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_sugar_16.wcnf S = OPT
O = 0
T = 16.02		 S = OPT
O = 0
T = 16.02
atcoss_sugar_17.wcnf S = OPT
O = 0
T = 23.59		 S = OPT
O = 0
T = 23.59
atcoss_sugar_18.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
atcoss_sugar_19.wcnf S = OPT
O = 8
T = 226.23		 S = OPT
O = 8
T = 226.23
normalized-f20c10b_001_area_delay.wcnf S = OPT
O = 28
T = 10.42		 S = OPT
O = 28
T = 10.42
normalized-f20c10b_002_area_delay.wcnf S = OPT
O = 24
T = 9.96		 S = OPT
O = 24
T = 9.96
normalized-f20c10b_003_area_delay.wcnf S = OPT
O = 26
T = 10.06		 S = OPT
O = 26
T = 10.06
normalized-f20c10b_004_area_delay.wcnf S = OPT
O = 27
T = 9.95		 S = OPT
O = 27
T = 9.95
normalized-f20c10b_005_area_delay.wcnf S = OPT
O = 26
T = 10.63		 S = OPT
O = 26
T = 10.63
normalized-f20c10b_006_area_delay.wcnf S = OPT
O = 22
T = 9.78		 S = OPT
O = 22
T = 9.78
normalized-f20c10b_007_area_delay.wcnf S = OPT
O = 26
T = 10.62		 S = OPT
O = 26
T = 10.62
normalized-f20c10b_008_area_delay.wcnf S = OPT
O = 25
T = 10.15		 S = OPT
O = 25
T = 10.15
normalized-f20c10b_009_area_delay.wcnf S = OPT
O = 24
T = 9.77		 S = OPT
O = 24
T = 9.77
normalized-f20c10b_010_area_delay.wcnf S = OPT
O = 26
T = 13.53		 S = OPT
O = 26
T = 13.53
normalized-f20c10b_011_area_delay.wcnf S = OPT
O = 26
T = 9.89		 S = OPT
O = 26
T = 9.89
normalized-f20c10b_012_area_delay.wcnf S = OPT
O = 27
T = 10.65		 S = OPT
O = 27
T = 10.65
normalized-f20c10b_013_area_delay.wcnf S = OPT
O = 22
T = 10.53		 S = OPT
O = 22
T = 10.53
normalized-f20c10b_014_area_delay.wcnf S = OPT
O = 27
T = 11.98		 S = OPT
O = 27
T = 11.98
normalized-f20c10b_015_area_delay.wcnf S = OPT
O = 25
T = 10.07		 S = OPT
O = 25
T = 10.07
normalized-f20c10b_016_area_delay.wcnf S = OPT
O = 25
T = 10.07		 S = OPT
O = 25
T = 10.07
normalized-f20c10b_017_area_delay.wcnf S = OPT
O = 25
T = 10.55		 S = OPT
O = 25
T = 10.55
normalized-f20c10b_018_area_delay.wcnf S = OPT
O = 25
T = 9.85		 S = OPT
O = 25
T = 9.85
normalized-f20c10b_019_area_delay.wcnf S = OPT
O = 24
T = 9.77		 S = OPT
O = 24
T = 9.77
normalized-f20c10b_020_area_delay.wcnf S = OPT
O = 23
T = 9.99		 S = OPT
O = 23
T = 9.99
normalized-f20c10b_021_area_delay.wcnf S = OPT
O = 24
T = 9.85		 S = OPT
O = 24
T = 9.85
normalized-f20c10b_022_area_delay.wcnf S = OPT
O = 26
T = 10.05		 S = OPT
O = 26
T = 10.05
normalized-f20c10b_023_area_delay.wcnf S = OPT
O = 22
T = 11.25		 S = OPT
O = 22
T = 11.25
normalized-f20c10b_024_area_delay.wcnf S = OPT
O = 24
T = 9.99		 S = OPT
O = 24
T = 9.99
normalized-f20c10b_025_area_delay.wcnf S = OPT
O = 25
T = 10.47		 S = OPT
O = 25
T = 10.47
normalized-fir06_area_delay.wcnf S = OPT
O = 15
T = 9.93		 S = OPT
O = 15
T = 9.93
normalized-fir07_area_delay.wcnf S = OPT
O = 16
T = 10.74		 S = OPT
O = 16
T = 10.74
normalized-fir08_area_delay.wcnf S = OPT
O = 23
T = 45.34		 S = OPT
O = 23
T = 45.34
normalized-fir08_area_opers.wcnf S = OPT
O = 48
T = 47.79		 S = OPT
O = 48
T = 47.79
normalized-fir08_area_partials.wcnf S = OPT
O = 49
T = 10.70		 S = OPT
O = 49
T = 10.70
normalized-fir09_area_delay.wcnf S = OPT
O = 17
T = 10.27		 S = OPT
O = 17
T = 10.27
normalized-fir09_area_opers.wcnf S = OPT
O = 34
T = 11.80		 S = OPT
O = 34
T = 11.80
simp-ibd_50.01.wcnf S = OPT
O = 53
T = 10.95		 S = OPT
O = 53
T = 10.95
simp-ibd_50.02.wcnf S = OPT
O = 56
T = 14.85		 S = OPT
O = 56
T = 14.85
simp-ibd_50.03.wcnf S = OPT
O = 54
T = 10.03		 S = OPT
O = 54
T = 10.03
simp-ibd_50.04.wcnf S = OPT
O = 55
T = 26.46		 S = OPT
O = 55
T = 26.46
simp-ibd_50.05.wcnf S = OPT
O = 59
T = 10.24		 S = OPT
O = 59
T = 10.24
simp-ibd_50.06.wcnf S = OPT
O = 55
T = 68.25		 S = OPT
O = 55
T = 68.25
simp-ibd_50.07.wcnf S = OPT
O = 57
T = 17.21		 S = OPT
O = 57
T = 17.21
simp-ibd_50.08.wcnf S = OPT
O = 57
T = 1251.85		 S = OPT
O = 57
T = 1251.85
simp-ibd_50.09.wcnf S = OPT
O = 57
T = 10.06		 S = OPT
O = 57
T = 10.06
simp-test_chr21_YRI_75.wcnf S = OPT
O = 44
T = 15.22		 S = OPT
O = 44
T = 15.22
SU1__simp-genos.haps.1.wcnf S = OPT
O = 73
T = 10.07		 S = OPT
O = 73
T = 10.07
SU1__simp-genos.haps.10.wcnf S = OPT
O = 90
T = 16.89		 S = OPT
O = 90
T = 16.89
SU1__simp-genos.haps.18.wcnf S = OPT
O = 74
T = 10.19		 S = OPT
O = 74
T = 10.19
SU1__simp-genos.haps.19.wcnf S = OPT
O = 79
T = 11.02		 S = OPT
O = 79
T = 11.02
SU1__simp-genos.haps.26.wcnf S = OPT
O = 81
T = 16.34		 S = OPT
O = 81
T = 16.34
SU1__simp-genos.haps.27.wcnf S = OPT
O = 92
T = 11.13		 S = OPT
O = 92
T = 11.13
SU1__simp-genos.haps.29.wcnf S = OPT
O = 68
T = 10.38		 S = OPT
O = 68
T = 10.38
SU1__simp-genos.haps.30.wcnf S = OPT
O = 69
T = 11.60		 S = OPT
O = 69
T = 11.60
SU1__simp-genos.haps.32.wcnf S = OPT
O = 71
T = 11.72		 S = OPT
O = 71
T = 11.72
SU1__simp-genos.haps.34.wcnf S = OPT
O = 69
T = 10.37		 S = OPT
O = 69
T = 10.37
SU1__simp-genos.haps.37.wcnf S = OPT
O = 77
T = 10.08		 S = OPT
O = 77
T = 10.08
SU1__simp-genos.haps.38.wcnf S = OPT
O = 89
T = 10.65		 S = OPT
O = 89
T = 10.65
SU1__simp-genos.haps.50.wcnf S = OPT
O = 59
T = 10.35		 S = OPT
O = 59
T = 10.35
SU1__simp-genos.haps.54.wcnf S = OPT
O = 72
T = 10.39		 S = OPT
O = 72
T = 10.39
SU1__simp-genos.haps.58.wcnf S = OPT
O = 85
T = 10.78		 S = OPT
O = 85
T = 10.78
SU1__simp-genos.haps.62.wcnf S = OPT
O = 67
T = 14.13		 S = OPT
O = 67
T = 14.13
SU1__simp-genos.haps.69.wcnf S = OPT
O = 76
T = 10.67		 S = OPT
O = 76
T = 10.67
SU1__simp-genos.haps.7.wcnf S = OPT
O = 73
T = 47.27		 S = OPT
O = 73
T = 47.27
SU1__simp-genos.haps.70.wcnf S = OPT
O = 58
T = 10.12		 S = OPT
O = 58
T = 10.12
SU1__simp-genos.haps.8.wcnf S = OPT
O = 63
T = 10.09		 S = OPT
O = 63
T = 10.09
SU1__simp-genos.haps.85.wcnf S = OPT
O = 65
T = 10.14		 S = OPT
O = 65
T = 10.14
SU1__simp-genos.haps.86.wcnf S = OPT
O = 56
T = 10.49		 S = OPT
O = 56
T = 10.49
SU3__simp-genos.haps.21.wcnf S = OPT
O = 112
T = 471.04		 S = OPT
O = 112
T = 471.04
SU3__simp-genos.haps.23.wcnf S = OPT
O = 110
T = 10.21		 S = OPT
O = 110
T = 10.21
SU3__simp-genos.haps.27.wcnf S = OPT
O = 99
T = 12.20		 S = OPT
O = 99
T = 12.20
SU3__simp-genos.haps.33.wcnf S = OPT
O = 113
T = 14.58		 S = OPT
O = 113
T = 14.58
SU3__simp-genos.haps.38.wcnf S = OPT
O = 100
T = 23.52		 S = OPT
O = 100
T = 23.52
SU3__simp-genos.haps.53.wcnf S = OPT
O = 110
T = 84.37		 S = OPT
O = 110
T = 84.37
SU3__simp-genos.haps.58.wcnf S = OPT
O = 101
T = 16.09		 S = OPT
O = 101
T = 16.09
SU3__simp-genos.haps.60.wcnf S = OPT
O = 103
T = 14.97		 S = OPT
O = 103
T = 14.97
SU3__simp-genos.haps.63.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
SU3__simp-genos.haps.64.wcnf S = OPT
O = 99
T = 13.93		 S = OPT
O = 99
T = 13.93
SU3__simp-genos.haps.72.wcnf S = OPT
O = 92
T = 21.42		 S = OPT
O = 92
T = 21.42
SU3__simp-genos.haps.74.wcnf S = OPT
O = 102
T = 10.23		 S = OPT
O = 102
T = 10.23
SU3__simp-genos.haps.80.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
SU3__simp-genos.haps.86.wcnf S = OPT
O = 102
T = 12.02		 S = OPT
O = 102
T = 12.02
SU3__simp-genos.haps.88.wcnf S = OPT
O = 106
T = 94.23		 S = OPT
O = 106
T = 94.23
SU3__simp-genos.haps.9.wcnf S = OPT
O = 106
T = 1205.19		 S = OPT
O = 106
T = 1205.19
normalized-f1000.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-f2000.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-f600.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-g125.17.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-g125.18.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-g250.15.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-g250.29.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-hanoi5.wcnf S = OPT
O = 1931
T = 11.04		 S = OPT
O = 1931
T = 11.04
normalized-ii16a1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-ii16a2.wcnf S = OPT
O = 1164
T = 1240.88		 S = OPT
O = 1164
T = 1240.88
normalized-ii16b1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-ii16c1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-ii16c2.wcnf S = OPT
O = 861
T = 30.77		 S = OPT
O = 861
T = 30.77
normalized-ii16d1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-ii16d2.wcnf S = OPT
O = 785
T = 26.73		 S = OPT
O = 785
T = 26.73
normalized-ii16e1.wcnf S = OPT
O = 1053
T = 1440.72		 S = OPT
O = 1053
T = 1440.72
normalized-ii32b1.wcnf S = OPT
O = 191
T = 21.20		 S = OPT
O = 191
T = 21.20
normalized-ii32c1.wcnf S = OPT
O = 167
T = 15.59		 S = OPT
O = 167
T = 15.59
normalized-ii32c2.wcnf S = OPT
O = 207
T = 27.39		 S = OPT
O = 207
T = 27.39
normalized-ii32c3.wcnf S = OPT
O = 261
T = 24.00		 S = OPT
O = 261
T = 24.00
normalized-ii32c4.wcnf S = OPT
O = 736
T = 12.54		 S = OPT
O = 736
T = 12.54
normalized-ii32d1.wcnf S = OPT
O = 285
T = 503.72		 S = OPT
O = 285
T = 503.72
normalized-ii32d2.wcnf S = OPT
O = 372
T = 864.46		 S = OPT
O = 372
T = 864.46
normalized-ii32d3.wcnf S = OPT
O = 802
T = 92.65		 S = OPT
O = 802
T = 92.65
normalized-ii32e5.wcnf S = OPT
O = 503
T = 44.09		 S = OPT
O = 503
T = 44.09
normalized-ii8a2.wcnf S = OPT
O = 139
T = 11.65		 S = OPT
O = 139
T = 11.65
normalized-ii8a3.wcnf S = OPT
O = 191
T = 17.69		 S = OPT
O = 191
T = 17.69
normalized-ii8a4.wcnf S = OPT
O = 283
T = 11.78		 S = OPT
O = 283
T = 11.78
normalized-ii8b2.wcnf S = OPT
O = 379
T = 12.81		 S = OPT
O = 379
T = 12.81
normalized-ii8b3.wcnf S = OPT
O = 507
T = 16.90		 S = OPT
O = 507
T = 16.90
normalized-ii8b4.wcnf S = OPT
O = 654
T = 20.10		 S = OPT
O = 654
T = 20.10
normalized-ii8c2.wcnf S = OPT
O = 525
T = 20.39		 S = OPT
O = 525
T = 20.39
normalized-ii8d1.wcnf S = OPT
O = 343
T = 13.21		 S = OPT
O = 343
T = 13.21
normalized-ii8d2.wcnf S = OPT
O = 540
T = 17.99		 S = OPT
O = 540
T = 17.99
normalized-ii8e1.wcnf S = OPT
O = 343
T = 12.55		 S = OPT
O = 343
T = 12.55
normalized-ii8e2.wcnf S = OPT
O = 494
T = 18.40		 S = OPT
O = 494
T = 18.40
normalized-par32-1-c.wcnf S = OPT
O = 1315
T = 1182.43		 S = OPT
O = 1315
T = 1182.43
normalized-par32-1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-par32-2-c.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-par32-2.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
c1355_F1001gat-1048gat@1.wcnf S = OPT
O = 21
T = 9.81		 S = OPT
O = 21
T = 9.81
c1355_F1001gat@1.wcnf S = OPT
O = 21
T = 9.78		 S = OPT
O = 21
T = 9.78
c1355_F1036gat-1229gat@1.wcnf S = OPT
O = 13
T = 9.98		 S = OPT
O = 13
T = 9.98
c1355_F106gat-409gat@1.wcnf S = OPT
O = 33
T = 9.92		 S = OPT
O = 33
T = 9.92
c1355_F106gat@0.wcnf S = OPT
O = 14
T = 9.97		 S = OPT
O = 14
T = 9.97
c1355_F113gat-1260gat@1.wcnf S = OPT
O = 13
T = 9.83		 S = OPT
O = 13
T = 9.83
c1355_F1150gat@0.wcnf S = OPT
O = 13
T = 9.95		 S = OPT
O = 13
T = 9.95
c1355_F1183gat-1262gat@1.wcnf S = OPT
O = 33
T = 9.81		 S = OPT
O = 33
T = 9.81
c1355_F120gat-414gat@1.wcnf S = OPT
O = 33
T = 9.91		 S = OPT
O = 33
T = 9.91
c1355_F1229gat@1.wcnf S = OPT
O = 33
T = 9.86		 S = OPT
O = 33
T = 9.86
c1355_F127gat-418gat@1.wcnf S = OPT
O = 33
T = 9.82		 S = OPT
O = 33
T = 9.82
c1355_F141gat@0.wcnf S = OPT
O = 14
T = 9.93		 S = OPT
O = 14
T = 9.93
c1355_F155gat@1.wcnf S = OPT
O = 14
T = 9.91		 S = OPT
O = 14
T = 9.91
c1355_F176gat-1278gat@1.wcnf S = OPT
O = 13
T = 9.96		 S = OPT
O = 13
T = 9.96
c1355_F183gat@0.wcnf S = OPT
O = 14
T = 9.94		 S = OPT
O = 14
T = 9.94
c1355_F197gat-308gat@1.wcnf S = OPT
O = 33
T = 9.81		 S = OPT
O = 33
T = 9.81
c1355_F1gat@0.wcnf S = OPT
O = 14
T = 9.90		 S = OPT
O = 14
T = 9.90
c1355_F43gat@1.wcnf S = OPT
O = 14
T = 9.87		 S = OPT
O = 14
T = 9.87
c1355_F50gat@1.wcnf S = OPT
O = 14
T = 9.85		 S = OPT
O = 14
T = 9.85
c1355_F543gat@1.wcnf S = OPT
O = 33
T = 9.95		 S = OPT
O = 33
T = 9.95
c1355_F57gat@1.wcnf S = OPT
O = 14
T = 9.91		 S = OPT
O = 14
T = 9.91
c1355_F71gat@1.wcnf S = OPT
O = 14
T = 9.99		 S = OPT
O = 14
T = 9.99
c3540_F20@1.wcnf S = OPT
O = 6
T = 10.33		 S = OPT
O = 6
T = 10.33
c3540_F41@1.wcnf S = OPT
O = 7
T = 9.95		 S = OPT
O = 7
T = 9.95
c3540_F45@0.wcnf S = OPT
O = 9
T = 10.54		 S = OPT
O = 9
T = 10.54
c3540_F45@1.wcnf S = OPT
O = 9
T = 10.82		 S = OPT
O = 9
T = 10.82
c6288_F137gat@1.wcnf S = OPT
O = 10
T = 10.87		 S = OPT
O = 10
T = 10.87
c6288_F205gat@1.wcnf S = OPT
O = 7
T = 10.93		 S = OPT
O = 7
T = 10.93
c6288_F35gat@1.wcnf S = OPT
O = 4
T = 9.87		 S = OPT
O = 4
T = 9.87
c6288_F69gat@1.wcnf S = OPT
O = 6
T = 9.99		 S = OPT
O = 6
T = 9.99
normalized-C499.a.wcnf S = OPT
O = 64
T = 11.41		 S = OPT
O = 64
T = 11.41
normalized-addm4.r.wcnf S = OPT
O = 165
T = 9.78		 S = OPT
O = 165
T = 9.78
normalized-alu4.b.wcnf S = OPT
O = 50
T = 11.38		 S = OPT
O = 50
T = 11.38
normalized-apex6.b.wcnf S = OPT
O = 136
T = 14.75		 S = OPT
O = 136
T = 14.75
normalized-bench1.r.wcnf S = OPT
O = 121
T = 10.23		 S = OPT
O = 121
T = 10.23
normalized-des.a.wcnf S = OPT
O = 942
T = 10.70		 S = OPT
O = 942
T = 10.70
normalized-duke2.b.wcnf S = OPT
O = 70
T = 11.05		 S = OPT
O = 70
T = 11.05
normalized-ex1010.pi.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
normalized-ex5.r.wcnf S = OPT
O = 37
T = 12.27		 S = OPT
O = 37
T = 12.27
normalized-exam.pi.wcnf S = OPT
O = 63
T = 10.10		 S = OPT
O = 63
T = 10.10
normalized-f51m.b.wcnf S = OPT
O = 18
T = 9.93		 S = OPT
O = 18
T = 9.93
normalized-fout.r.wcnf S = OPT
O = 38
T = 9.80		 S = OPT
O = 38
T = 9.80
normalized-jac3.wcnf S = OPT
O = 15
T = 10.00		 S = OPT
O = 15
T = 10.00
normalized-lin.rom.r.wcnf S = OPT
O = 120
T = 9.84		 S = OPT
O = 120
T = 9.84
normalized-m100_100_10_10.r.wcnf S = OPT
O = 12
T = 14.93		 S = OPT
O = 12
T = 14.93
normalized-m100_100_10_15.r.wcnf S = OPT
O = 10
T = 10.27		 S = OPT
O = 10
T = 10.27
normalized-m100_100_10_30.r.wcnf S = OPT
O = 8
T = 10.39		 S = OPT
O = 8
T = 10.39
normalized-m100_100_30_30.r.wcnf S = OPT
O = 5
T = 12.15		 S = OPT
O = 5
T = 12.15
normalized-m100_300_10_10.r.wcnf S = OPT
O = 21
T = 10.37		 S = OPT
O = 21
T = 10.37
normalized-m100_300_10_14.r.wcnf S = OPT
O = 19
T = 10.24		 S = OPT
O = 19
T = 10.24
normalized-m100_300_10_15.r.wcnf S = OPT
O = 19
T = 14.47		 S = OPT
O = 19
T = 14.47
normalized-m100_300_10_20.r.wcnf S = OPT
O = 17
T = 11.18		 S = OPT
O = 17
T = 11.18
normalized-m200_500_10_10.r.wcnf S = OPT
O = 39
T = 649.28		 S = OPT
O = 39
T = 649.28
normalized-m4.r.wcnf S = OPT
O = 90
T = 10.02		 S = OPT
O = 90
T = 10.02
normalized-maincont.r.wcnf S = OPT
O = 7
T = 9.75		 S = OPT
O = 7
T = 9.75
normalized-max1024.pi.wcnf S = OPT
O = 259
T = 10.98		 S = OPT
O = 259
T = 10.98
normalized-max1024.r.wcnf S = OPT
O = 245
T = 11.58		 S = OPT
O = 245
T = 11.58
normalized-max512.r.wcnf S = OPT
O = 113
T = 9.74		 S = OPT
O = 113
T = 9.74
normalized-mlp4.r.wcnf S = OPT
O = 109
T = 9.79		 S = OPT
O = 109
T = 9.79
normalized-pdc.r.wcnf S = OPT
O = 94
T = 10.19		 S = OPT
O = 94
T = 10.19
normalized-prom2.pi.wcnf S = OPT
O = 287
T = 10.12		 S = OPT
O = 287
T = 10.12
normalized-prom2.r.wcnf S = OPT
O = 278
T = 10.14		 S = OPT
O = 278
T = 10.14
normalized-rd84.b.wcnf S = OPT
O = 5
T = 16.67		 S = OPT
O = 5
T = 16.67
normalized-rot.b.wcnf S = OPT
O = 115
T = 10.21		 S = OPT
O = 115
T = 10.21
normalized-sao2.b.wcnf S = OPT
O = 25
T = 10.18		 S = OPT
O = 25
T = 10.18
normalized-saucier.r.wcnf S = OPT
O = 6
T = 58.92		 S = OPT
O = 6
T = 58.92
normalized-test1.r.wcnf S = OPT
O = 110
T = 9.80		 S = OPT
O = 110
T = 9.80
normalized-test4.pi.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
ctrl.wcnf S = OPT
O = 15
T = 9.95		 S = OPT
O = 15
T = 9.95
mrisc_mem2wire.wcnf S = OPT
O = 5
T = 45.78		 S = OPT
O = 5
T = 45.78
spi.wcnf S = OPT
O = 46
T = 12.35		 S = OPT
O = 46
T = 12.35
sudoku.wcnf S = OPT
O = 13
T = 16.63		 S = OPT
O = 13
T = 16.63
SAT02__industrial__biere__dinphil__dp10s10.shuffled.cnf.wcnf.8.wcnf S = OPT
O = 240
T = 27.53		 S = OPT
O = 240
T = 27.53
SAT02__industrial__goldberg__fpga_routing__vda_gr_rcs_w9.shuffled.cnf.wcnf.5.wcnf S = OPT
O = 6
T = 10.12		 S = OPT
O = 6
T = 10.12
SAT02__industrial__goldberg__fpga_routing__vda_gr_rcs_w9.shuffled.cnf.wcnf.8.wcnf S = OPT
O = 3
T = 10.13		 S = OPT
O = 3
T = 10.13
SAT04__industrial__vangelder__cnf-color__abb313GPIA-9-tr.used-as.sat04-321.cnf.wcnf.3.wcnf S = OPT
O = 80
T = 141.03		 S = OPT
O = 80
T = 141.03
SAT04__industrial__vangelder__cnf-color__abb313GPIA-9-tr.used-as.sat04-321.cnf.wcnf.6.wcnf S = OPT
O = 25
T = 50.09		 S = OPT
O = 25
T = 50.09
SAT04__industrial__velev__pipe-sat-1-1__12pipe_bug4_q0.used-as.sat04-723.cnf.wcnf.1.wcnf S = OPT
O = 179
T = 23.10		 S = OPT
O = 179
T = 23.10
SAT04__industrial__velev__pipe-sat-1-1__12pipe_bug4_q0.used-as.sat04-723.cnf.wcnf.8.wcnf S = OPT
O = 86
T = 20.07		 S = OPT
O = 86
T = 20.07
SAT04__industrial__velev__pipe-sat-1-1__12pipe_bug6_q0.used-as.sat04-725.cnf.wcnf.10.wcnf S = OPT
O = 50
T = 19.79		 S = OPT
O = 50
T = 19.79
SAT04__industrial__velev__pipe-sat-1-1__12pipe_bug6_q0.used-as.sat04-725.cnf.wcnf.5.wcnf S = OPT
O = 53
T = 18.92		 S = OPT
O = 53
T = 18.92
SAT07__industrial__vliw_sat_4.0__9vliw_m_9stages_iq3_C1_bug5.cnf.wcnf.4.wcnf S = OPT
O = 8
T = 34.06		 S = OPT
O = 8
T = 34.06
SAT07__industrial__vliw_sat_4.0__9vliw_m_9stages_iq3_C1_bug6.cnf.wcnf.1.wcnf S = OPT
O = 14
T = 33.27		 S = OPT
O = 14
T = 33.27
SAT07__industrial__vliw_sat_4.0__9vliw_m_9stages_iq3_C1_bug6.cnf.wcnf.4.wcnf S = OPT
O = 24
T = 56.28		 S = OPT
O = 24
T = 56.28
SAT07__industrial__vliw_sat_4.0__9vliw_m_9stages_iq3_C1_bug6.cnf.wcnf.7.wcnf S = OPT
O = 3
T = 33.12		 S = OPT
O = 3
T = 33.12
SAT09__APPLICATIONS__satComp09_BioInstances__rbcl_xits_15_SAT.cnf.wcnf.9.wcnf S = OPT
O = 26
T = 13.77		 S = OPT
O = 26
T = 13.77
SAT09__APPLICATIONS__satComp09_BioInstances__rbcl_xits_18_SAT.cnf.wcnf.2.wcnf S = OPT
O = 7
T = 10.28		 S = OPT
O = 7
T = 10.28
SAT11__application__fuhs__AProVE11__AProVE11-09.cnf.wcnf.10.wcnf S = OPT
O = 208
T = 25.71		 S = OPT
O = 208
T = 25.71
SAT11__application__fuhs__AProVE11__AProVE11-09.cnf.wcnf.4.wcnf S = OPT
O = 1382
T = 149.27		 S = OPT
O = 1382
T = 149.27
SAT11__application__fuhs__AProVE11__AProVE11-09.cnf.wcnf.8.wcnf S = OPT
O = 320
T = 36.01		 S = OPT
O = 320
T = 36.01
SAT11__application__fuhs__AProVE11__AProVE11-10.cnf.wcnf.3.wcnf S = OPT
O = 1028
T = 96.77		 S = OPT
O = 1028
T = 96.77
SAT11__application__fuhs__AProVE11__AProVE11-12.cnf.wcnf.2.wcnf S = OPT
O = 501
T = 25.31		 S = OPT
O = 501
T = 25.31
SAT11__application__fuhs__AProVE11__AProVE11-12.cnf.wcnf.4.wcnf S = OPT
O = 180
T = 17.60		 S = OPT
O = 180
T = 17.60
SAT11__application__fuhs__AProVE11__AProVE11-16.cnf.wcnf.1.wcnf S = OPT
O = 263
T = 20.64		 S = OPT
O = 263
T = 20.64
SAT11__application__jarvisalo__AAAI2010-SATPlanning__aaai10-planning-ipc5-TPP-30-step11.cnf.wcnf.1.wcnf S = OPT
O = 1
T = 52.21		 S = OPT
O = 1
T = 52.21
SAT11__application__jarvisalo__AAAI2010-SATPlanning__aaai10-planning-ipc5-pipesworld-12-step16.cnf.wcnf.2.wcnf S = OPT
O = 1
T = 11.30		 S = OPT
O = 1
T = 11.30
SAT11__application__jarvisalo__AAAI2010-SATPlanning__aaai10-planning-ipc5-pipesworld-12-step16.cnf.wcnf.7.wcnf S = OPT
O = 1
T = 11.28		 S = OPT
O = 1
T = 11.28
SAT11__application__jarvisalo__AAAI2010-SATPlanning__aaai10-planning-ipc5-pipesworld-18-step16.cnf.wcnf.1.wcnf S = OPT
O = 1
T = 13.80		 S = OPT
O = 1
T = 13.80
SAT11__application__jarvisalo__AAAI2010-SATPlanning__aaai10-planning-ipc5-pipesworld-18-step16.cnf.wcnf.4.wcnf S = OPT
O = 1
T = 13.79		 S = OPT
O = 1
T = 13.79
SAT11__application__jarvisalo__smtqfbv-aigs__smtlib-qfbv-aigs-bin_libmsrpc_vc1225336-tseitin.cnf.wcnf.4.wcnf S = OPT
O = 154
T = 16.72		 S = OPT
O = 154
T = 16.72
SAT11__application__jarvisalo__smtqfbv-aigs__smtlib-qfbv-aigs-bin_libsmbsharemodes_vc5759-tseitin.cnf.wcnf.9.wcnf S = OPT
O = 118
T = 28.68		 S = OPT
O = 118
T = 28.68
SAT11__application__jarvisalo__smtqfbv-aigs__smtlib-qfbv-aigs-rfunit_flat-64-tseitin.cnf.wcnf.10.wcnf S = OPT
O = 9
T = 11.78		 S = OPT
O = 9
T = 11.78
SAT11__application__jarvisalo__smtqfbv-aigs__smtlib-qfbv-aigs-rfunit_flat-64-tseitin.cnf.wcnf.2.wcnf S = OPT
O = 73
T = 14.56		 S = OPT
O = 73
T = 14.56
SAT11__application__jarvisalo__smtqfbv-aigs__smtlib-qfbv-aigs-rfunit_flat-64-tseitin.cnf.wcnf.7.wcnf S = OPT
O = 20
T = 12.51		 S = OPT
O = 20
T = 12.51
SAT11__application__leberre__2dimensionalstrippacking__E05F18.cnf.wcnf.7.wcnf S = OPT
O = 61
T = 33.34		 S = OPT
O = 61
T = 33.34
SAT11__application__leberre__2dimensionalstrippacking__E05F18.cnf.wcnf.9.wcnf S = OPT
O = 82
T = 38.54		 S = OPT
O = 82
T = 38.54
SAT11__application__manthey__traffic__traffic_3_uc_sat.cnf.wcnf.8.wcnf S = OPT
O = 77
T = 15.39		 S = OPT
O = 77
T = 15.39
SAT11__application__manthey__traffic__traffic_r_sat.cnf.wcnf.4.wcnf S = OPT
O = 78
T = 30.12		 S = OPT
O = 78
T = 30.12
SAT11__application__manthey__traffic__traffic_r_sat.cnf.wcnf.6.wcnf S = OPT
O = 120
T = 62.13		 S = OPT
O = 120
T = 62.13
SAT11__application__rintanen__SATPlanning__blocks-blocks-36-0.180-SAT.cnf.wcnf.2.wcnf S = OPT
O = 35
T = 87.12		 S = OPT
O = 35
T = 87.12
SAT11__application__rintanen__SATPlanning__openstacks-sequencedstrips-nonadl-nonnegated-os-sequencedstrips-p30_3.085-SAT.cnf.wcnf.4.wcnf S = OPT
O = 6
T = 13.97		 S = OPT
O = 6
T = 13.97
SAT_RACE06__ibm-2002-21r-k95.cnf.wcnf.4.wcnf S = OPT
O = 2
T = 52.89		 S = OPT
O = 2
T = 52.89
SAT_RACE06__velev-pipe-sat-1.0-b9.cnf.wcnf.2.wcnf S = OPT
O = 25
T = 38.52		 S = OPT
O = 25
T = 38.52
SAT_RACE06__velev-pipe-sat-1.0-b9.cnf.wcnf.5.wcnf S = OPT
O = 85
T = 25.58		 S = OPT
O = 85
T = 25.58
SAT_RACE08__cnf__ibm-2004-01-k90.cnf.wcnf.10.wcnf S = OPT
O = 5
T = 10.74		 S = OPT
O = 5
T = 10.74
TEAMS20_l7aa.cnf.wcnf S = OPT
O = 26
T = 24.88		 S = OPT
O = 26
T = 24.88
teams16_l7a.cnf.wcnf S = OPT
O = 18
T = 12.64		 S = OPT
O = 18
T = 12.64
teams20_l2a.cnf.wcnf S = OPT
O = 12
T = 13.32		 S = OPT
O = 12
T = 13.32
teams20_l4a.cnf.wcnf S = OPT
O = 18
T = 16.78		 S = OPT
O = 18
T = 16.78
teams20_l6a.cnf.wcnf S = OPT
O = 18
T = 19.93		 S = OPT
O = 18
T = 19.93
teams20_l8a.cnf.wcnf S = OPT
O = 16
T = 12.17		 S = OPT
O = 16
T = 12.17
teams24_l4a.cnf.wcnf S = OPT
O = 14
T = 20.05		 S = OPT
O = 14
T = 20.05
cnf.10.p.10.wcnf S = OPT
O = 10
T = 47.81		 S = OPT
O = 10
T = 47.81
cnf.10.p.9.wcnf S = OPT
O = 10
T = 31.84		 S = OPT
O = 10
T = 31.84
cnf.11.p.10.wcnf S = OPT
O = 11
T = 32.82		 S = OPT
O = 11
T = 32.82
cnf.11.p.9.wcnf S = OPT
O = 11
T = 80.98		 S = OPT
O = 11
T = 80.98
cnf.12.p.10.wcnf S = OPT
O = 12
T = 87.87		 S = OPT
O = 12
T = 87.87
cnf.12.p.8.wcnf S = OPT
O = 12
T = 43.99		 S = OPT
O = 12
T = 43.99
cnf.12.p.9.wcnf S = OPT
O = 12
T = 52.05		 S = OPT
O = 12
T = 52.05
cnf.12.t.9.wcnf S = OPT
O = 12
T = 19.08		 S = OPT
O = 12
T = 19.08
cnf.13.p.10.wcnf S = OPT
O = 13
T = 54.51		 S = OPT
O = 13
T = 54.51
cnf.13.p.8.wcnf S = OPT
O = 13
T = 87.37		 S = OPT
O = 13
T = 87.37
cnf.13.p.9.wcnf S = OPT
O = 13
T = 52.94		 S = OPT
O = 13
T = 52.94
cnf.14.d.10.wcnf S = OPT
O = 14
T = 26.81		 S = OPT
O = 14
T = 26.81
cnf.14.p.10.wcnf S = OPT
O = 14
T = 99.47		 S = OPT
O = 14
T = 99.47
cnf.14.p.9.wcnf S = OPT
O = 14
T = 76.59		 S = OPT
O = 14
T = 76.59
cnf.14.t.7.wcnf S = OPT
O = 14
T = 20.28		 S = OPT
O = 14
T = 20.28
cnf.14.t.9.wcnf S = OPT
O = 14
T = 22.68		 S = OPT
O = 14
T = 22.68
cnf.15.p.10.wcnf S = OPT
O = 15
T = 215.82		 S = OPT
O = 15
T = 215.82
cnf.15.p.8.wcnf S = OPT
O = 15
T = 104.84		 S = OPT
O = 15
T = 104.84
cnf.15.p.9.wcnf S = OPT
O = 15
T = 134.69		 S = OPT
O = 15
T = 134.69
cnf.15.t.10.wcnf S = OPT
O = 15
T = 28.53		 S = OPT
O = 15
T = 28.53
cnf.16.p.10.wcnf S = OPT
O = 16
T = 203.25		 S = OPT
O = 16
T = 203.25
cnf.16.p.8.wcnf S = OPT
O = 16
T = 189.95		 S = OPT
O = 16
T = 189.95
cnf.16.p.9.wcnf S = OPT
O = 16
T = 501.45		 S = OPT
O = 16
T = 501.45
cnf.16.t.9.wcnf S = OPT
O = 16
T = 25.47		 S = OPT
O = 16
T = 25.47
cnf.17.d.10.wcnf S = OPT
O = 17
T = 26.44		 S = OPT
O = 17
T = 26.44
cnf.17.d.9.wcnf S = OPT
O = 17
T = 19.35		 S = OPT
O = 17
T = 19.35
cnf.17.p.10.wcnf S = OPT
O = 17
T = 314.50		 S = OPT
O = 17
T = 314.50
cnf.17.p.9.wcnf S = OPT
O = 17
T = 110.37		 S = OPT
O = 17
T = 110.37
cnf.17.t.10.wcnf S = OPT
O = 17
T = 28.83		 S = OPT
O = 17
T = 28.83
cnf.17.t.8.wcnf S = OPT
O = 17
T = 18.64		 S = OPT
O = 17
T = 18.64
cnf.18.d.7.wcnf S = OPT
O = 18
T = 22.55		 S = OPT
O = 18
T = 22.55
cnf.18.p.10.wcnf S = OPT
O = 18
T = 561.52		 S = OPT
O = 18
T = 561.52
cnf.18.p.8.wcnf S = OPT
O = 18
T = 117.40		 S = OPT
O = 18
T = 117.40
cnf.18.p.9.wcnf S = OPT
O = 18
T = 605.17		 S = OPT
O = 18
T = 605.17
cnf.18.t.9.wcnf S = OPT
O = 18
T = 29.78		 S = OPT
O = 18
T = 29.78
cnf.19.d.10.wcnf S = OPT
O = 19
T = 23.37		 S = OPT
O = 19
T = 23.37
cnf.19.p.10.wcnf S = OPT
O = 19
T = 220.42		 S = OPT
O = 19
T = 220.42
cnf.19.p.8.wcnf S = OPT
O = 19
T = 111.28		 S = OPT
O = 19
T = 111.28
cnf.19.p.9.wcnf S = OPT
O = 19
T = 161.56		 S = OPT
O = 19
T = 161.56
cnf.19.t.7.wcnf S = OPT
O = 19
T = 28.64		 S = OPT
O = 19
T = 28.64
cnf.20.d.10.wcnf S = OPT
O = 20
T = 23.05		 S = OPT
O = 20
T = 23.05
cnf.20.d.9.wcnf S = OPT
O = 20
T = 19.81		 S = OPT
O = 20
T = 19.81
cnf.20.p.10.wcnf S = OPT
O = 20
T = 808.30		 S = OPT
O = 20
T = 808.30
cnf.20.p.9.wcnf S = OPT
O = 20
T = 659.44		 S = OPT
O = 20
T = 659.44
cnf.20.t.10.wcnf S = OPT
O = 20
T = 52.69		 S = OPT
O = 20
T = 52.69
cnf.20.t.8.wcnf S = OPT
O = 20
T = 31.27		 S = OPT
O = 20
T = 31.27
cnf.8.p.10.wcnf S = OPT
O = 8
T = 25.16		 S = OPT
O = 8
T = 25.16
cnf.8.p.9.wcnf S = OPT
O = 8
T = 20.45		 S = OPT
O = 8
T = 20.45
cnf.9.p.10.wcnf S = OPT
O = 9
T = 26.87		 S = OPT
O = 9
T = 26.87
cnf.9.p.9.wcnf S = OPT
O = 9
T = 31.59		 S = OPT
O = 9
T = 31.59
splitedReads_0.matrix.wcnf S = OPT
O = 1500
T = 328.16		 S = OPT
O = 1500
T = 328.16
splitedReads_137.matrix.wcnf S = OPT
O = 90
T = 10.48		 S = OPT
O = 90
T = 10.48
splitedReads_158.matrix.wcnf S = OPT
O = 173
T = 10.09		 S = OPT
O = 173
T = 10.09
splitedReads_160.matrix.wcnf S = OPT
O = 186
T = 10.09		 S = OPT
O = 186
T = 10.09
splitedReads_18.matrix.wcnf S = OPT
O = 138
T = 10.87		 S = OPT
O = 138
T = 10.87
splitedReads_414.matrix.wcnf S = OPT
O = 171
T = 11.11		 S = OPT
O = 171
T = 11.11
GreeceWesternGreeceUniversityInstance4.xml.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
SouthAfricaWoodlands2009.xml.wcnf S = OPT
O = 0
T = 21.83		 S = OPT
O = 0
T = 21.83
b14_C-mbd14-0209.wcnf S = OPT
O = 25
T = 94.98		 S = OPT
O = 25
T = 94.98
b14_C-mbd14-0213.wcnf S = OPT
O = 27
T = 18.58		 S = OPT
O = 27
T = 18.58
b14_C-mbd14-0218.wcnf S = OPT
O = 25
T = 28.25		 S = OPT
O = 25
T = 28.25
b14_C-mbd14-0225.wcnf S = OPT
O = 24
T = 62.84		 S = OPT
O = 24
T = 62.84
b14_C-mbd14-0231.wcnf S = OPT
O = 22
T = 52.63		 S = OPT
O = 22
T = 52.63
b14_C-mbd14-0248.wcnf S = OPT
O = 25
T = 16.34		 S = OPT
O = 25
T = 16.34
b14_C-mbd14-0256.wcnf S = OPT
O = 22
T = 18.83		 S = OPT
O = 22
T = 18.83
b14_C-mbd14-0259.wcnf S = OPT
O = 21
T = 50.23		 S = OPT
O = 21
T = 50.23
b15_C-mbd14-0240.wcnf S = OPT
O = 21
T = 22.79		 S = OPT
O = 21
T = 22.79
b15_C-mbd14-0256.wcnf S = OPT
O = 24
T = 10.66		 S = OPT
O = 24
T = 10.66
b15_C-mbd14-0259.wcnf S = OPT
O = 22
T = 10.46		 S = OPT
O = 22
T = 10.46
b15_C-mbd14-0288.wcnf S = OPT
O = 26
T = 22.91		 S = OPT
O = 26
T = 22.91
b15_C-mbd14-0305.wcnf S = OPT
O = 23
T = 12.14		 S = OPT
O = 23
T = 12.14
b15_C-mbd14-0330.wcnf S = OPT
O = 20
T = 11.26		 S = OPT
O = 20
T = 11.26
b17_C-mbd14-0205.wcnf S = OPT
O = 22
T = 10.18		 S = OPT
O = 22
T = 10.18
b17_C-mbd14-0206.wcnf S = OPT
O = 27
T = 10.12		 S = OPT
O = 27
T = 10.12
b17_C-mbd14-0217.wcnf S = OPT
O = 24
T = 10.19		 S = OPT
O = 24
T = 10.19
b17_C-mbd14-0218.wcnf S = OPT
O = 27
T = 9.92		 S = OPT
O = 27
T = 9.92
b17_C-mbd14-0220.wcnf S = OPT
O = 24
T = 10.20		 S = OPT
O = 24
T = 10.20
b17_C-mbd14-0224.wcnf S = OPT
O = 23
T = 10.24		 S = OPT
O = 23
T = 10.24
b17_C-mbd14-0229.wcnf S = OPT
O = 19
T = 10.21		 S = OPT
O = 19
T = 10.21
b17_C-mbd14-0230.wcnf S = OPT
O = 24
T = 9.71		 S = OPT
O = 24
T = 9.71
b20_C-mbd14-0202.wcnf S = OPT
O = 21
T = 10.04		 S = OPT
O = 21
T = 10.04
b20_C-mbd14-0211.wcnf S = OPT
O = 23
T = 15.02		 S = OPT
O = 23
T = 15.02
b20_C-mbd14-0213.wcnf S = OPT
O = 22
T = 10.70		 S = OPT
O = 22
T = 10.70
b20_C-mbd14-0214.wcnf S = OPT
O = 17
T = 10.93		 S = OPT
O = 17
T = 10.93
b20_C-mbd14-0216.wcnf S = OPT
O = 26
T = 10.73		 S = OPT
O = 26
T = 10.73
b20_C-mbd14-0217.wcnf S = OPT
O = 21
T = 10.65		 S = OPT
O = 21
T = 10.65
b20_C-mbd14-0221.wcnf S = OPT
O = 22
T = 10.65		 S = OPT
O = 22
T = 10.65
b20_C-mbd14-0222.wcnf S = OPT
O = 28
T = 20.69		 S = OPT
O = 28
T = 20.69
b21_C-mbd14-0203.wcnf S = OPT
O = 27
T = 12.71		 S = OPT
O = 27
T = 12.71
b21_C-mbd14-0204.wcnf S = OPT
O = 22
T = 10.20		 S = OPT
O = 22
T = 10.20
b21_C-mbd14-0205.wcnf S = OPT
O = 21
T = 11.16		 S = OPT
O = 21
T = 11.16
b21_C-mbd14-0217.wcnf S = OPT
O = 21
T = 10.24		 S = OPT
O = 21
T = 10.24
b21_C-mbd14-0218.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
b21_C-mbd14-0221.wcnf S = OPT
O = 19
T = 10.09		 S = OPT
O = 19
T = 10.09
b21_C-mbd14-0224.wcnf S = OPT
O = 16
T = 10.35		 S = OPT
O = 16
T = 10.35
b21_C-mbd14-0227.wcnf S = OPT
O = 24
T = 10.19		 S = OPT
O = 24
T = 10.19
b22_C-mbd14-0204.wcnf S = OPT
O = 23
T = 10.25		 S = OPT
O = 23
T = 10.25
b22_C-mbd14-0205.wcnf S = OPT
O = 28
T = 9.93		 S = OPT
O = 28
T = 9.93
b22_C-mbd14-0207.wcnf S = OPT
O = 25
T = 10.03		 S = OPT
O = 25
T = 10.03
b22_C-mbd14-0208.wcnf S = OPT
O = 23
T = 10.12		 S = OPT
O = 23
T = 10.12
b22_C-mbd14-0210.wcnf S = OPT
O = 26
T = 10.32		 S = OPT
O = 26
T = 10.32
b22_C-mbd14-0211.wcnf S = OPT
O = 22
T = 10.11		 S = OPT
O = 22
T = 10.11
b22_C-mbd14-0213.wcnf S = OPT
O = 26
T = 10.11		 S = OPT
O = 26
T = 10.11
b22_C-mbd14-0215.wcnf S = OPT
O = 22
T = 10.02		 S = OPT
O = 22
T = 10.02
1aabfc32-d491-11df-9a24-00163e3d3b7c_l3.wcnf S = OPT
O = 2236
T = 14.21		 S = OPT
O = 2236
T = 14.21
2c3aece6-c8b2-11df-a040-00163e3d3b7c_l3.wcnf S = OPT
O = 814
T = 17.59		 S = OPT
O = 814
T = 17.59
4ede8d96-c17a-11df-a7c5-00163e3d3b7c_l3.wcnf S = OPT
O = 631
T = 10.08		 S = OPT
O = 631
T = 10.08
7f80e4f0-4fe9-11e0-acd7-00163e1e087d_l3.wcnf S = OPT
O = 404
T = 15.83		 S = OPT
O = 404
T = 15.83
ff4a1d84-d490-11df-9e6c-00163e3d3b7c_l3.wcnf S = OPT
O = 2236
T = 14.21		 S = OPT
O = 2236
T = 14.21
rand118_l2.wcnf S = OPT
O = 447
T = 10.28		 S = OPT
O = 447
T = 10.28
rand172_l2.wcnf S = OPT
O = 670
T = 10.38		 S = OPT
O = 670
T = 10.38
rand179_l2.wcnf S = OPT
O = 1088
T = 10.45		 S = OPT
O = 1088
T = 10.45
rand196_l2.wcnf S = OPT
O = 1298
T = 10.75		 S = OPT
O = 1298
T = 10.75
rand208_l2.wcnf S = OPT
O = 349
T = 10.24		 S = OPT
O = 349
T = 10.24
rand209_l2.wcnf S = OPT
O = 1199
T = 10.44		 S = OPT
O = 1199
T = 10.44
rand21_l2.wcnf S = OPT
O = 1465
T = 10.84		 S = OPT
O = 1465
T = 10.84
rand242_l2.wcnf S = OPT
O = 388
T = 10.40		 S = OPT
O = 388
T = 10.40
rand289_l2.wcnf S = OPT
O = 350
T = 10.45		 S = OPT
O = 350
T = 10.45
rand290_l2.wcnf S = OPT
O = 1017
T = 10.34		 S = OPT
O = 1017
T = 10.34
rand308_l2.wcnf S = OPT
O = 1235
T = 10.25		 S = OPT
O = 1235
T = 10.25
rand30_l2.wcnf S = OPT
O = 512
T = 10.21		 S = OPT
O = 512
T = 10.21
rand313_l2.wcnf S = OPT
O = 1595
T = 10.62		 S = OPT
O = 1595
T = 10.62
rand377_l2.wcnf S = OPT
O = 574
T = 10.10		 S = OPT
O = 574
T = 10.10
rand411_l2.wcnf S = OPT
O = 578
T = 10.19		 S = OPT
O = 578
T = 10.19
rand414_l2.wcnf S = OPT
O = 1259
T = 10.15		 S = OPT
O = 1259
T = 10.15
rand425_l2.wcnf S = OPT
O = 694
T = 10.12		 S = OPT
O = 694
T = 10.12
rand446_l2.wcnf S = OPT
O = 416
T = 10.18		 S = OPT
O = 416
T = 10.18
rand484_l2.wcnf S = OPT
O = 331
T = 10.27		 S = OPT
O = 331
T = 10.27
rand507_l2.wcnf S = OPT
O = 1197
T = 9.99		 S = OPT
O = 1197
T = 9.99
rand695_l2.wcnf S = OPT
O = 974
T = 9.95		 S = OPT
O = 974
T = 9.95
rand717_l2.wcnf S = OPT
O = 1120
T = 10.28		 S = OPT
O = 1120
T = 10.28
rand736_l2.wcnf S = OPT
O = 1232
T = 9.91		 S = OPT
O = 1232
T = 9.91
rand736_l3.wcnf S = OPT
O = 1481
T = 10.32		 S = OPT
O = 1481
T = 10.32
rand794_l2.wcnf S = OPT
O = 472
T = 10.14		 S = OPT
O = 472
T = 10.14
rand7_l2.wcnf S = OPT
O = 971
T = 10.42		 S = OPT
O = 971
T = 10.42
rand813_l2.wcnf S = OPT
O = 1192
T = 10.16		 S = OPT
O = 1192
T = 10.16
rand869_l2.wcnf S = OPT
O = 459
T = 10.64		 S = OPT
O = 459
T = 10.64
rand874_l2.wcnf S = OPT
O = 863
T = 10.42		 S = OPT
O = 863
T = 10.42
rand892_l2.wcnf S = OPT
O = 1119
T = 10.18		 S = OPT
O = 1119
T = 10.18
rand937_l2.wcnf S = OPT
O = 439
T = 10.32		 S = OPT
O = 439
T = 10.32
rand943_l2.wcnf S = OPT
O = 829
T = 10.49		 S = OPT
O = 829
T = 10.49
rand954_l2.wcnf S = OPT
O = 700
T = 10.17		 S = OPT
O = 700
T = 10.17
rand96_l2.wcnf S = OPT
O = 392
T = 10.26		 S = OPT
O = 392
T = 10.26
rand984_l2.wcnf S = OPT
O = 839
T = 10.52		 S = OPT
O = 839
T = 10.52
10tree110p.wcnf S = OPT
O = 20
T = 11.05		 S = OPT
O = 20
T = 11.05
10tree120p.wcnf S = OPT
O = 41
T = 14.42		 S = OPT
O = 41
T = 14.42
10tree130p.wcnf S = OPT
O = 63
T = 37.36		 S = OPT
O = 63
T = 37.36
10tree215p.wcnf S = OPT
O = 31
T = 15.97		 S = OPT
O = 31
T = 15.97
10tree225p.wcnf S = OPT
O = 52
T = 43.37		 S = OPT
O = 52
T = 43.37
10tree305p.wcnf S = OPT
O = 9
T = 10.15		 S = OPT
O = 9
T = 10.15
10tree315p.wcnf S = OPT
O = 30
T = 14.70		 S = OPT
O = 30
T = 14.70
10tree325p.wcnf S = OPT
O = 48
T = 24.17		 S = OPT
O = 48
T = 24.17
10tree405p.wcnf S = OPT
O = 9
T = 10.13		 S = OPT
O = 9
T = 10.13
10tree410p.wcnf S = OPT
O = 21
T = 11.12		 S = OPT
O = 21
T = 11.12
10tree420p.wcnf S = OPT
O = 41
T = 32.08		 S = OPT
O = 41
T = 32.08
10tree430p.wcnf S = OPT
O = 62
T = 36.82		 S = OPT
O = 62
T = 36.82
10tree505posib.wcnf S = OPT
O = 10
T = 10.38		 S = OPT
O = 10
T = 10.38
10tree515p.wcnf S = OPT
O = 29
T = 11.96		 S = OPT
O = 29
T = 11.96
10tree525p.wcnf S = OPT
O = 52
T = 30.99		 S = OPT
O = 52
T = 30.99
15tree1001p.wcnf S = OPT
O = 13
T = 28.88		 S = OPT
O = 13
T = 28.88
15tree101p.wcnf S = OPT
O = 13
T = 26.08		 S = OPT
O = 13
T = 26.08
15tree201p.wcnf S = OPT
O = 13
T = 17.23		 S = OPT
O = 13
T = 17.23
15tree301p.wcnf S = OPT
O = 13
T = 21.89		 S = OPT
O = 13
T = 21.89
15tree401p.wcnf S = OPT
O = 13
T = 18.67		 S = OPT
O = 13
T = 18.67
15tree501p.wcnf S = OPT
O = 13
T = 23.66		 S = OPT
O = 13
T = 23.66
15tree601p.wcnf S = OPT
O = 13
T = 38.67		 S = OPT
O = 13
T = 38.67
15tree701p.wcnf S = OPT
O = 13
T = 28.43		 S = OPT
O = 13
T = 28.43
15tree801p.wcnf S = OPT
O = 13
T = 15.39		 S = OPT
O = 13
T = 15.39
15tree901p.wcnf S = OPT
O = 13
T = 18.94		 S = OPT
O = 13
T = 18.94
10tree115p.wcnf S = OPT
O = 31
T = 11.20		 S = OPT
O = 31
T = 11.20
10tree125p.wcnf S = OPT
O = 52
T = 12.89		 S = OPT
O = 52
T = 12.89
10tree210p.wcnf S = OPT
O = 21
T = 10.77		 S = OPT
O = 21
T = 10.77
10tree220p.wcnf S = OPT
O = 42
T = 12.33		 S = OPT
O = 42
T = 12.33
10tree230p.wcnf S = OPT
O = 63
T = 21.83		 S = OPT
O = 63
T = 21.83
10tree310p.wcnf S = OPT
O = 21
T = 10.90		 S = OPT
O = 21
T = 10.90
10tree320p.wcnf S = OPT
O = 42
T = 12.52		 S = OPT
O = 42
T = 12.52
10tree330p.wcnf S = OPT
O = 63
T = 18.50		 S = OPT
O = 63
T = 18.50
10tree405posib.wcnf S = OPT
O = 10
T = 10.19		 S = OPT
O = 10
T = 10.19
10tree415p.wcnf S = OPT
O = 31
T = 11.36		 S = OPT
O = 31
T = 11.36
10tree425p.wcnf S = OPT
O = 52
T = 14.70		 S = OPT
O = 52
T = 14.70
10tree505p.wcnf S = OPT
O = 10
T = 10.15		 S = OPT
O = 10
T = 10.15
10tree510p.wcnf S = OPT
O = 21
T = 11.22		 S = OPT
O = 21
T = 11.22
10tree520p.wcnf S = OPT
O = 42
T = 13.04		 S = OPT
O = 42
T = 13.04
10tree530p.wcnf S = OPT
O = 63
T = 17.15		 S = OPT
O = 63
T = 17.15
15tree1001posib.wcnf S = OPT
O = 13
T = 11.15		 S = OPT
O = 13
T = 11.15
15tree101posib.wcnf S = OPT
O = 13
T = 12.39		 S = OPT
O = 13
T = 12.39
15tree201posib.wcnf S = OPT
O = 13
T = 11.88		 S = OPT
O = 13
T = 11.88
15tree301posib.wcnf S = OPT
O = 13
T = 13.32		 S = OPT
O = 13
T = 13.32
15tree401posib.wcnf S = OPT
O = 13
T = 11.35		 S = OPT
O = 13
T = 11.35
15tree501posib.wcnf S = OPT
O = 13
T = 11.35		 S = OPT
O = 13
T = 11.35
15tree601posib.wcnf S = OPT
O = 13
T = 11.85		 S = OPT
O = 13
T = 11.85
15tree701posib.wcnf S = OPT
O = 13
T = 11.60		 S = OPT
O = 13
T = 11.60
15tree801posib.wcnf S = OPT
O = 13
T = 11.71		 S = OPT
O = 13
T = 11.71
15tree901posib.wcnf S = OPT
O = 13
T = 11.25		 S = OPT
O = 13
T = 11.25
normalized-s3-3-3-1pb.wcnf S = OPT
O = 36
T = 9.77		 S = OPT
O = 36
T = 9.77
normalized-s3-3-3-2pb.wcnf S = OPT
O = 36
T = 9.88		 S = OPT
O = 36
T = 9.88
normalized-s3-3-3-3pb.wcnf S = OPT
O = 36
T = 10.01		 S = OPT
O = 36
T = 10.01
normalized-s3-3-3-4pb.wcnf S = OPT
O = 36
T = 9.87		 S = OPT
O = 36
T = 9.87
normalized-s3-3-3-5pb.wcnf S = OPT
O = 34
T = 9.83		 S = OPT
O = 34
T = 9.83
normalized-s4-4-3-10pb.wcnf S = OPT
O = 70
T = 10.12		 S = OPT
O = 70
T = 10.12
normalized-s4-4-3-1pb.wcnf S = OPT
O = 62
T = 10.12		 S = OPT
O = 62
T = 10.12
normalized-s4-4-3-2pb.wcnf S = OPT
O = 64
T = 10.23		 S = OPT
O = 64
T = 10.23
normalized-s4-4-3-3pb.wcnf S = OPT
O = 62
T = 11.42		 S = OPT
O = 62
T = 11.42
normalized-s4-4-3-4pb.wcnf S = OPT
O = 60
T = 10.17		 S = OPT
O = 60
T = 10.17
normalized-s4-4-3-5pb.wcnf S = OPT
O = 60
T = 10.12		 S = OPT
O = 60
T = 10.12
normalized-s4-4-3-6pb.wcnf S = OPT
O = 66
T = 10.15		 S = OPT
O = 66
T = 10.15
normalized-s4-4-3-7pb.wcnf S = OPT
O = 64
T = 10.97		 S = OPT
O = 64
T = 10.97
normalized-s4-4-3-8pb.wcnf S = OPT
O = 36
T = 10.07		 S = OPT
O = 36
T = 10.07
normalized-s4-4-3-9pb.wcnf S = OPT
O = 68
T = 10.23		 S = OPT
O = 68
T = 10.23
1bpi_.2knt_.g.wcnf.t.wcnf S = OPT
O = 35
T = 66.12		 S = OPT
O = 35
T = 66.12
1bpi_.5pti_.g.wcnf.t.wcnf S = OPT
O = 29
T = 35.66		 S = OPT
O = 29
T = 35.66
1knt_.1bpi_.g.wcnf.t.wcnf S = OPT
O = 35
T = 69.19		 S = OPT
O = 35
T = 69.19
1knt_.2knt_.g.wcnf.t.wcnf S = OPT
O = 16
T = 13.73		 S = OPT
O = 16
T = 13.73
1knt_.5pti_.g.wcnf.t.wcnf S = OPT
O = 29
T = 50.98		 S = OPT
O = 29
T = 50.98
1vii_.1cph_.g.wcnf.t.wcnf S = OPT
O = 7
T = 9.98		 S = OPT
O = 7
T = 9.98
2knt_.5pti_.g.wcnf.t.wcnf S = OPT
O = 32
T = 63.35		 S = OPT
O = 32
T = 63.35
3ebx_.1era_.g.wcnf.t.wcnf S = OPT
O = 34
T = 93.72		 S = OPT
O = 34
T = 93.72
3ebx_.6ebx_.g.wcnf.t.wcnf S = OPT
O = 23
T = 19.56		 S = OPT
O = 23
T = 19.56
6ebx_.1era_.g.wcnf.t.wcnf S = OPT
O = 30
T = 43.52		 S = OPT
O = 30
T = 43.52
p1.wcnf.t.wcnf S = OPT
O = 35
T = 96.85		 S = OPT
O = 35
T = 96.85
sandiaprotein.g.wcnf.t.wcnf S = OPT
O = 28
T = 39.77		 S = OPT
O = 28
T = 39.77
b18-s_PathRelaxation_Set_FS_1.wcnf S = OPT
O = 148
T = 17.22		 S = OPT
O = 148
T = 17.22
b18-s_PathRelaxation_Set_FS_10.wcnf S = OPT
O = 113
T = 31.71		 S = OPT
O = 113
T = 31.71
b18-s_PathRelaxation_Set_FS_11.wcnf S = OPT
O = 113
T = 29.82		 S = OPT
O = 113
T = 29.82
b18-s_PathRelaxation_Set_FS_12.wcnf S = OPT
O = 113
T = 34.65		 S = OPT
O = 113
T = 34.65
b18-s_PathRelaxation_Set_FS_2.wcnf S = OPT
O = 145
T = 32.84		 S = OPT
O = 145
T = 32.84
b18-s_PathRelaxation_Set_FS_3.wcnf S = OPT
O = 145
T = 40.53		 S = OPT
O = 145
T = 40.53
b18-s_PathRelaxation_Set_FS_4.wcnf S = OPT
O = 145
T = 304.42		 S = OPT
O = 145
T = 304.42
b18-s_PathRelaxation_Set_FS_5.wcnf S = OPT
O = 145
T = 324.56		 S = OPT
O = 145
T = 324.56
b18-s_PathRelaxation_Set_FS_6.wcnf S = OPT
O = 145
T = 150.06		 S = OPT
O = 145
T = 150.06
b18-s_PathRelaxation_Set_FS_7.wcnf S = OPT
O = 145
T = 188.84		 S = OPT
O = 145
T = 188.84
b18-s_PathRelaxation_Set_FS_8.wcnf S = OPT
O = 145
T = 163.19		 S = OPT
O = 145
T = 163.19
b18-s_PathRelaxation_Set_FS_9.wcnf S = OPT
O = 145
T = 128.87		 S = OPT
O = 145
T = 128.87
b20-s_PathRelaxation_Set_FS_1.wcnf S = OPT
O = 84
T = 15.22		 S = OPT
O = 84
T = 15.22
b20-s_PathRelaxation_Set_FS_10.wcnf S = OPT
O = 83
T = 11.86		 S = OPT
O = 83
T = 11.86
b20-s_PathRelaxation_Set_FS_11.wcnf S = OPT
O = 83
T = 12.53		 S = OPT
O = 83
T = 12.53
b20-s_PathRelaxation_Set_FS_12.wcnf S = OPT
O = 83
T = 12.32		 S = OPT
O = 83
T = 12.32
b20-s_PathRelaxation_Set_FS_2.wcnf S = OPT
O = 83
T = 15.39		 S = OPT
O = 83
T = 15.39
b20-s_PathRelaxation_Set_FS_3.wcnf S = OPT
O = 83
T = 11.71		 S = OPT
O = 83
T = 11.71
b20-s_PathRelaxation_Set_FS_4.wcnf S = OPT
O = 83
T = 11.63		 S = OPT
O = 83
T = 11.63
b20-s_PathRelaxation_Set_FS_5.wcnf S = OPT
O = 83
T = 15.90		 S = OPT
O = 83
T = 15.90
b20-s_PathRelaxation_Set_FS_6.wcnf S = OPT
O = 83
T = 16.14		 S = OPT
O = 83
T = 16.14
b20-s_PathRelaxation_Set_FS_7.wcnf S = OPT
O = 83
T = 16.26		 S = OPT
O = 83
T = 16.26
b20-s_PathRelaxation_Set_FS_8.wcnf S = OPT
O = 83
T = 11.98		 S = OPT
O = 83
T = 11.98
b20-s_PathRelaxation_Set_FS_9.wcnf S = OPT
O = 83
T = 12.08		 S = OPT
O = 83
T = 12.08
b21-s_PathRelaxation_Set_FS_1.wcnf S = OPT
O = 89
T = 15.13		 S = OPT
O = 89
T = 15.13
b21-s_PathRelaxation_Set_FS_10.wcnf S = OPT
O = 88
T = 17.23		 S = OPT
O = 88
T = 17.23
b21-s_PathRelaxation_Set_FS_11.wcnf S = OPT
O = 88
T = 17.78		 S = OPT
O = 88
T = 17.78
b21-s_PathRelaxation_Set_FS_12.wcnf S = OPT
O = 88
T = 18.30		 S = OPT
O = 88
T = 18.30
b21-s_PathRelaxation_Set_FS_2.wcnf S = OPT
O = 89
T = 16.96		 S = OPT
O = 89
T = 16.96
b21-s_PathRelaxation_Set_FS_3.wcnf S = OPT
O = 89
T = 17.27		 S = OPT
O = 89
T = 17.27
b21-s_PathRelaxation_Set_FS_4.wcnf S = OPT
O = 89
T = 18.18		 S = OPT
O = 89
T = 18.18
b21-s_PathRelaxation_Set_FS_5.wcnf S = OPT
O = 89
T = 25.85		 S = OPT
O = 89
T = 25.85
b21-s_PathRelaxation_Set_FS_6.wcnf S = OPT
O = 88
T = 20.14		 S = OPT
O = 88
T = 20.14
b21-s_PathRelaxation_Set_FS_7.wcnf S = OPT
O = 88
T = 17.20		 S = OPT
O = 88
T = 17.20
b21-s_PathRelaxation_Set_FS_8.wcnf S = OPT
O = 88
T = 17.34		 S = OPT
O = 88
T = 17.34
b21-s_PathRelaxation_Set_FS_9.wcnf S = OPT
O = 88
T = 17.78		 S = OPT
O = 88
T = 17.78
b21-s_PathRelaxation_FS_1.wcnf S = OPT
O = 89
T = 11.09		 S = OPT
O = 89
T = 11.09
b21-s_PathRelaxation_FS_10.wcnf S = OPT
O = 89
T = 11.11		 S = OPT
O = 89
T = 11.11
b21-s_PathRelaxation_FS_11.wcnf S = OPT
O = 88
T = 10.98		 S = OPT
O = 88
T = 10.98
b21-s_PathRelaxation_FS_12.wcnf S = OPT
O = 88
T = 11.10		 S = OPT
O = 88
T = 11.10
b21-s_PathRelaxation_FS_13.wcnf S = OPT
O = 89
T = 11.14		 S = OPT
O = 89
T = 11.14
b21-s_PathRelaxation_FS_14.wcnf S = OPT
O = 89
T = 11.14		 S = OPT
O = 89
T = 11.14
b21-s_PathRelaxation_FS_15.wcnf S = OPT
O = 89
T = 11.02		 S = OPT
O = 89
T = 11.02
b21-s_PathRelaxation_FS_16.wcnf S = OPT
O = 88
T = 11.44		 S = OPT
O = 88
T = 11.44
b21-s_PathRelaxation_FS_17.wcnf S = OPT
O = 88
T = 11.14		 S = OPT
O = 88
T = 11.14
b21-s_PathRelaxation_FS_18.wcnf S = OPT
O = 88
T = 11.13		 S = OPT
O = 88
T = 11.13
b21-s_PathRelaxation_FS_19.wcnf S = OPT
O = 88
T = 11.17		 S = OPT
O = 88
T = 11.17
b21-s_PathRelaxation_FS_2.wcnf S = OPT
O = 90
T = 11.49		 S = OPT
O = 90
T = 11.49
b21-s_PathRelaxation_FS_20.wcnf S = OPT
O = 88
T = 11.13		 S = OPT
O = 88
T = 11.13
b21-s_PathRelaxation_FS_21.wcnf S = OPT
O = 88
T = 11.38		 S = OPT
O = 88
T = 11.38
b21-s_PathRelaxation_FS_22.wcnf S = OPT
O = 88
T = 11.20		 S = OPT
O = 88
T = 11.20
b21-s_PathRelaxation_FS_23.wcnf S = OPT
O = 88
T = 11.07		 S = OPT
O = 88
T = 11.07
b21-s_PathRelaxation_FS_24.wcnf S = OPT
O = 88
T = 10.97		 S = OPT
O = 88
T = 10.97
b21-s_PathRelaxation_FS_25.wcnf S = OPT
O = 88
T = 10.78		 S = OPT
O = 88
T = 10.78
b21-s_PathRelaxation_FS_3.wcnf S = OPT
O = 90
T = 11.14		 S = OPT
O = 90
T = 11.14
b21-s_PathRelaxation_FS_4.wcnf S = OPT
O = 92
T = 11.00		 S = OPT
O = 92
T = 11.00
b21-s_PathRelaxation_FS_5.wcnf S = OPT
O = 89
T = 11.00		 S = OPT
O = 89
T = 11.00
b21-s_PathRelaxation_FS_6.wcnf S = OPT
O = 88
T = 11.00		 S = OPT
O = 88
T = 11.00
b21-s_PathRelaxation_FS_7.wcnf S = OPT
O = 89
T = 11.02		 S = OPT
O = 89
T = 11.02
b21-s_PathRelaxation_FS_8.wcnf S = OPT
O = 89
T = 10.90		 S = OPT
O = 89
T = 10.90
b21-s_PathRelaxation_FS_9.wcnf S = OPT
O = 88
T = 11.02		 S = OPT
O = 88
T = 11.02
TWComp_1c75_N69.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
TWComp_1dj7_N73.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
TWComp_1dp_N76.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
TWComp_1en2_N69.wcnf S = OPT
O = 16
T = 412.54		 S = OPT
O = 16
T = 412.54
TWComp_alarm_N37.wcnf S = OPT
O = 4
T = 10.18		 S = OPT
O = 4
T = 10.18
TWComp_barle_N48.wcnf S = OPT
O = 7
T = 13.32		 S = OPT
O = 7
T = 13.32
TWComp_barley-pp_N26.wcnf S = OPT
O = 7
T = 10.12		 S = OPT
O = 7
T = 10.12
TWComp_barley2_N48.wcnf S = OPT
O = 7
T = 12.48		 S = OPT
O = 7
T = 12.48
TWComp_celar02_N100.wcnf S = OPT
O = 10
T = 16.30		 S = OPT
O = 10
T = 16.30
TWComp_celar09pp_N67.wcnf S = OPT
O = 7
T = 13.09		 S = OPT
O = 7
T = 13.09
TWComp_david-pp_N29.wcnf S = OPT
O = 13
T = 11.03		 S = OPT
O = 13
T = 11.03
TWComp_david_N87.wcnf S = OPT
O = 13
T = 30.31		 S = OPT
O = 13
T = 30.31
TWComp_eil51.tsp_N51.wcnf S = OPT
O = 8
T = 1127.39		 S = OPT
O = 8
T = 1127.39
TWComp_hailfinder_N56.wcnf S = OPT
O = 4
T = 11.65		 S = OPT
O = 4
T = 11.65
TWComp_hepar2_N70.wcnf S = OPT
O = 6
T = 13.62		 S = OPT
O = 6
T = 13.62
TWComp_huck_N74.wcnf S = OPT
O = 10
T = 15.06		 S = OPT
O = 10
T = 15.06
TWComp_jean_N77.wcnf S = OPT
O = 9
T = 16.03		 S = OPT
O = 9
T = 16.03
TWComp_mainuk_N48.wcnf S = OPT
O = 7
T = 10.90		 S = OPT
O = 7
T = 10.90
TWComp_mildew_35.wcnf S = OPT
O = 4
T = 9.99		 S = OPT
O = 4
T = 9.99
TWComp_miles500_N128.wcnf S = OPT
O = 22
T = 363.68		 S = OPT
O = 22
T = 363.68
TWComp_mulsol.i.5-pp_N119.wcnf S = OPT
O = 31
T = 1182.41		 S = OPT
O = 31
T = 1182.41
TWComp_myciel4_N23.wcnf S = OPT
O = 10
T = 21.52		 S = OPT
O = 10
T = 21.52
TWComp_myciel5_N47.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
TWComp_oesoca+_N67.wcnf S = OPT
O = 11
T = 103.26		 S = OPT
O = 11
T = 103.26
TWComp_oesoca4_N42.wcnf S = OPT
O = 3
T = 10.53		 S = OPT
O = 3
T = 10.53
TWComp_oesoca_N39.wcnf S = OPT
O = 3
T = 10.38		 S = OPT
O = 3
T = 10.38
TWComp_pathfinder_N109.wcnf S = OPT
O = 6
T = 17.10		 S = OPT
O = 6
T = 17.10
TWComp_queen5_5_N25.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
TWComp_queen6_6_N36.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
TWComp_queen7_7_N49.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
TWComp_ship-ship-pp_N30.wcnf S = OPT
O = 8
T = 43.37		 S = OPT
O = 8
T = 43.37
TWComp_water_N32.wcnf S = OPT
O = 9
T = 10.66		 S = OPT
O = 9
T = 10.66
TWComp_win95pts_N76.wcnf S = OPT
O = 8
T = 15.69		 S = OPT
O = 8
T = 15.69