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
AES1-30-1.wcnf S = OPT
O = 1
T = 10.79		 S = OPT
O = 1
T = 10.79
AES1-30-2.wcnf S = OPT
O = 1
T = 10.60		 S = OPT
O = 1
T = 10.60
AES1-30-3.wcnf S = OPT
O = 1
T = 10.70		 S = OPT
O = 1
T = 10.70
AES1-30-4.wcnf S = OPT
O = 1
T = 10.66		 S = OPT
O = 1
T = 10.66
AES1-30-5.wcnf S = OPT
O = 1
T = 10.65		 S = OPT
O = 1
T = 10.65
AES1-40-10.wcnf S = OPT
O = 1
T = 10.90		 S = OPT
O = 1
T = 10.90
AES1-40-6.wcnf S = OPT
O = 1
T = 10.65		 S = OPT
O = 1
T = 10.65
AES1-40-7.wcnf S = OPT
O = 1
T = 10.72		 S = OPT
O = 1
T = 10.72
AES1-40-8.wcnf S = OPT
O = 1
T = 10.70		 S = OPT
O = 1
T = 10.70
AES1-40-9.wcnf S = OPT
O = 1
T = 10.66		 S = OPT
O = 1
T = 10.66
AES1-50-11.wcnf S = OPT
O = 1
T = 10.69		 S = OPT
O = 1
T = 10.69
AES1-50-12.wcnf S = OPT
O = 1
T = 10.79		 S = OPT
O = 1
T = 10.79
AES1-50-13.wcnf S = OPT
O = 1
T = 10.69		 S = OPT
O = 1
T = 10.69
AES1-50-14.wcnf S = OPT
O = 1
T = 10.87		 S = OPT
O = 1
T = 10.87
AES1-50-15.wcnf S = OPT
O = 1
T = 10.80		 S = OPT
O = 1
T = 10.80
AES1-60-16.wcnf S = OPT
O = 1
T = 10.72		 S = OPT
O = 1
T = 10.72
AES1-60-17.wcnf S = OPT
O = 1
T = 10.84		 S = OPT
O = 1
T = 10.84
AES1-60-18.wcnf S = OPT
O = 1
T = 10.47		 S = OPT
O = 1
T = 10.47
AES1-60-19.wcnf S = OPT
O = 1
T = 10.73		 S = OPT
O = 1
T = 10.73
AES1-60-20.wcnf S = OPT
O = 1
T = 10.89		 S = OPT
O = 1
T = 10.89
AES1-70-21.wcnf S = OPT
O = 1
T = 10.98		 S = OPT
O = 1
T = 10.98
AES1-70-22.wcnf S = OPT
O = 1
T = 11.38		 S = OPT
O = 1
T = 11.38
AES1-70-23.wcnf S = OPT
O = 1
T = 47.17		 S = OPT
O = 1
T = 47.17
AES1-70-24.wcnf S = OPT
O = 1
T = 15.67		 S = OPT
O = 1
T = 15.67
AES1-70-25.wcnf S = OPT
O = 1
T = 13.34		 S = OPT
O = 1
T = 13.34
AES1-72-26.wcnf S = OPT
O = 1
T = 12.52		 S = OPT
O = 1
T = 12.52
AES1-72-27.wcnf S = OPT
O = 1
T = 20.71		 S = OPT
O = 1
T = 20.71
AES1-72-28.wcnf S = OPT
O = 1
T = 13.00		 S = OPT
O = 1
T = 13.00
AES1-72-29.wcnf S = OPT
O = 1
T = 12.05		 S = OPT
O = 1
T = 12.05
AES1-72-30.wcnf S = OPT
O = 1
T = 26.40		 S = OPT
O = 1
T = 26.40
AES1-74-31.wcnf S = OPT
O = 1
T = 26.63		 S = OPT
O = 1
T = 26.63
AES1-74-32.wcnf S = OPT
O = 1
T = 26.63		 S = OPT
O = 1
T = 26.63
AES1-74-33.wcnf S = OPT
O = 1
T = 26.32		 S = OPT
O = 1
T = 26.32
AES1-74-34.wcnf S = OPT
O = 1
T = 11.61		 S = OPT
O = 1
T = 11.61
AES1-74-35.wcnf S = OPT
O = 1
T = 16.57		 S = OPT
O = 1
T = 16.57
AES1-76-36.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
AES1-76-37.wcnf S = OPT
O = 1
T = 104.25		 S = OPT
O = 1
T = 104.25
AES1-76-38.wcnf S = OPT
O = 1
T = 625.46		 S = OPT
O = 1
T = 625.46
AES1-76-39.wcnf S = OPT
O = 1
T = 19.84		 S = OPT
O = 1
T = 19.84
AES1-76-40.wcnf S = OPT
O = 1
T = 51.39		 S = OPT
O = 1
T = 51.39
AES2-30-41.wcnf S = OPT
O = 2
T = 10.70		 S = OPT
O = 2
T = 10.70
AES2-30-42.wcnf S = OPT
O = 2
T = 10.63		 S = OPT
O = 2
T = 10.63
AES2-30-43.wcnf S = OPT
O = 2
T = 10.65		 S = OPT
O = 2
T = 10.65
AES2-30-44.wcnf S = OPT
O = 2
T = 10.65		 S = OPT
O = 2
T = 10.65
AES2-30-45.wcnf S = OPT
O = 2
T = 10.81		 S = OPT
O = 2
T = 10.81
AES2-40-46.wcnf S = OPT
O = 2
T = 10.70		 S = OPT
O = 2
T = 10.70
AES2-40-47.wcnf S = OPT
O = 2
T = 10.80		 S = OPT
O = 2
T = 10.80
AES2-40-48.wcnf S = OPT
O = 2
T = 10.71		 S = OPT
O = 2
T = 10.71
AES2-40-49.wcnf S = OPT
O = 2
T = 10.67		 S = OPT
O = 2
T = 10.67
AES2-40-50.wcnf S = OPT
O = 2
T = 10.74		 S = OPT
O = 2
T = 10.74
AES2-50-51.wcnf S = OPT
O = 2
T = 11.01		 S = OPT
O = 2
T = 11.01
AES2-50-52.wcnf S = OPT
O = 2
T = 10.94		 S = OPT
O = 2
T = 10.94
AES2-50-53.wcnf S = OPT
O = 2
T = 10.69		 S = OPT
O = 2
T = 10.69
AES2-50-54.wcnf S = OPT
O = 2
T = 10.82		 S = OPT
O = 2
T = 10.82
AES2-50-55.wcnf S = OPT
O = 2
T = 10.97		 S = OPT
O = 2
T = 10.97
AES2-60-56.wcnf S = OPT
O = 2
T = 13.21		 S = OPT
O = 2
T = 13.21
AES2-60-57.wcnf S = OPT
O = 2
T = 12.00		 S = OPT
O = 2
T = 12.00
AES2-60-58.wcnf S = OPT
O = 2
T = 11.73		 S = OPT
O = 2
T = 11.73
AES2-60-59.wcnf S = OPT
O = 2
T = 10.69		 S = OPT
O = 2
T = 10.69
AES2-60-60.wcnf S = OPT
O = 2
T = 11.59		 S = OPT
O = 2
T = 11.59
AES2-70-61.wcnf S = OPT
O = 2
T = 16.86		 S = OPT
O = 2
T = 16.86
AES2-70-62.wcnf S = OPT
O = 2
T = 57.24		 S = OPT
O = 2
T = 57.24
AES2-70-63.wcnf S = OPT
O = 2
T = 15.41		 S = OPT
O = 2
T = 15.41
AES2-70-64.wcnf S = OPT
O = 2
T = 19.15		 S = OPT
O = 2
T = 19.15
AES2-70-65.wcnf S = OPT
O = 2
T = 51.35		 S = OPT
O = 2
T = 51.35
AES2-72-66.wcnf S = OPT
O = 2
T = 77.22		 S = OPT
O = 2
T = 77.22
AES2-72-67.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
AES2-72-68.wcnf S = OPT
O = 2
T = 17.08		 S = OPT
O = 2
T = 17.08
AES2-72-69.wcnf S = OPT
O = 2
T = 24.21		 S = OPT
O = 2
T = 24.21
AES2-72-70.wcnf S = OPT
O = 2
T = 16.23		 S = OPT
O = 2
T = 16.23
AES2-74-11.wcnf S = OPT
O = 2
T = 39.61		 S = OPT
O = 2
T = 39.61
AES2-74-71.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
AES2-74-72.wcnf S = OPT
O = 2
T = 15.91		 S = OPT
O = 2
T = 15.91
AES2-74-73.wcnf S = OPT
O = 2
T = 13.72		 S = OPT
O = 2
T = 13.72
AES2-74-74.wcnf S = OPT
O = 2
T = 100.16		 S = OPT
O = 2
T = 100.16
AES2-74-75.wcnf S = OPT
O = 2
T = 16.20		 S = OPT
O = 2
T = 16.20
causal_n5_i10_N10000_uai13_constant_int.wcnf S = OPT
O = 8
T = 13.66		 S = OPT
O = 8
T = 13.66
causal_n5_i10_N500_uai13_constant_int.wcnf S = OPT
O = 8
T = 12.65		 S = OPT
O = 8
T = 12.65
causal_n5_i2_N500_uai13_harddeps_int.wcnf S = OPT
O = 5
T = 11.67		 S = OPT
O = 5
T = 11.67
causal_n5_i4_N500_uai13_harddeps_int.wcnf S = OPT
O = 4
T = 12.35		 S = OPT
O = 4
T = 12.35
causal_n5_i5_N10000_uai13_constant_int.wcnf S = OPT
O = 5
T = 13.19		 S = OPT
O = 5
T = 13.19
causal_n5_i5_N1000_uai13_constant_int.wcnf S = OPT
O = 5
T = 13.59		 S = OPT
O = 5
T = 13.59
causal_n5_i5_N500_uai13_constant_int.wcnf S = OPT
O = 5
T = 15.57		 S = OPT
O = 5
T = 15.57
causal_n5_i7_N10000_uai13_constant_int.wcnf S = OPT
O = 11
T = 19.41		 S = OPT
O = 11
T = 19.41
causal_n5_i7_N10000_uai13_harddeps_int.wcnf S = OPT
O = 17
T = 19.88		 S = OPT
O = 17
T = 19.88
causal_n5_i7_N1000_uai13_constant_int.wcnf S = OPT
O = 11
T = 17.51		 S = OPT
O = 11
T = 17.51
causal_n5_i7_N1000_uai13_harddeps_int.wcnf S = OPT
O = 17
T = 29.05		 S = OPT
O = 17
T = 29.05
causal_n5_i7_N500_uai13_constant_int.wcnf S = OPT
O = 11
T = 22.18		 S = OPT
O = 11
T = 22.18
causal_n5_i7_N500_uai13_harddeps_int.wcnf S = OPT
O = 17
T = 22.13		 S = OPT
O = 17
T = 22.13
causal_n5_i8_N10000_uai13_harddeps_int.wcnf S = OPT
O = 18
T = 25.12		 S = OPT
O = 18
T = 25.12
causal_n5_i8_N1000_uai13_harddeps_int.wcnf S = OPT
O = 18
T = 23.80		 S = OPT
O = 18
T = 23.80
causal_n5_i8_N500_uai13_harddeps_int.wcnf S = OPT
O = 18
T = 20.90		 S = OPT
O = 18
T = 20.90
causal_n5_i9_N10000_uai13_constant_int.wcnf S = OPT
O = 12
T = 12.46		 S = OPT
O = 12
T = 12.46
causal_n5_i9_N10000_uai13_harddeps_int.wcnf S = OPT
O = 17
T = 18.05		 S = OPT
O = 17
T = 18.05
causal_n5_i9_N1000_uai13_constant_int.wcnf S = OPT
O = 12
T = 12.97		 S = OPT
O = 12
T = 12.97
causal_n5_i9_N1000_uai13_harddeps_int.wcnf S = OPT
O = 17
T = 17.54		 S = OPT
O = 17
T = 17.54
causal_n5_i9_N500_uai13_constant_int.wcnf S = OPT
O = 12
T = 15.46		 S = OPT
O = 12
T = 15.46
causal_n5_i9_N500_uai13_harddeps_int.wcnf S = OPT
O = 17
T = 20.43		 S = OPT
O = 17
T = 20.43
causal_n6_i10_N1000_uai14_constant_int.wcnf S = OPT
O = 28
T = 11.58		 S = OPT
O = 28
T = 11.58
causal_n6_i10_N500_uai14_constant_int.wcnf S = OPT
O = 28
T = 10.87		 S = OPT
O = 28
T = 10.87
causal_n6_i10_N500_uai14_harddeps_int.wcnf S = OPT
O = 33
T = 11.02		 S = OPT
O = 33
T = 11.02
causal_n6_i1_N10000_uai14_constant_int.wcnf S = OPT
O = 19
T = 16.66		 S = OPT
O = 19
T = 16.66
causal_n6_i1_N500_uai13_harddeps_int.wcnf S = OPT
O = 19
T = 245.06		 S = OPT
O = 19
T = 245.06
causal_n6_i2_N10000_uai14_harddeps_int.wcnf S = OPT
O = 48
T = 17.80		 S = OPT
O = 48
T = 17.80
causal_n6_i2_N1000_uai13_constant_int.wcnf S = OPT
O = 15
T = 100.54		 S = OPT
O = 15
T = 100.54
causal_n6_i2_N1000_uai14_harddeps_int.wcnf S = OPT
O = 48
T = 18.28		 S = OPT
O = 48
T = 18.28
causal_n6_i2_N500_uai14_harddeps_int.wcnf S = OPT
O = 48
T = 21.09		 S = OPT
O = 48
T = 21.09
causal_n6_i3_N10000_uai14_constant_int.wcnf S = OPT
O = 22
T = 10.58		 S = OPT
O = 22
T = 10.58
causal_n6_i3_N10000_uai14_harddeps_int.wcnf S = OPT
O = 56
T = 23.40		 S = OPT
O = 56
T = 23.40
causal_n6_i3_N1000_uai14_harddeps_int.wcnf S = OPT
O = 56
T = 20.22		 S = OPT
O = 56
T = 20.22
causal_n6_i3_N500_uai14_harddeps_int.wcnf S = OPT
O = 56
T = 19.96		 S = OPT
O = 56
T = 19.96
causal_n6_i4_N1000_uai14_constant_int.wcnf S = OPT
O = 17
T = 13.25		 S = OPT
O = 17
T = 13.25
causal_n6_i4_N500_uai14_constant_int.wcnf S = OPT
O = 17
T = 14.78		 S = OPT
O = 17
T = 14.78
causal_n6_i5_N10000_uai13_constant_int.wcnf S = OPT
O = 4
T = 17.91		 S = OPT
O = 4
T = 17.91
causal_n6_i5_N10000_uai13_harddeps_int.wcnf S = OPT
O = 4
T = 16.24		 S = OPT
O = 4
T = 16.24
causal_n6_i5_N1000_uai13_constant_int.wcnf S = OPT
O = 4
T = 17.25		 S = OPT
O = 4
T = 17.25
causal_n6_i5_N1000_uai13_harddeps_int.wcnf S = OPT
O = 4
T = 16.68		 S = OPT
O = 4
T = 16.68
causal_n6_i5_N500_uai13_constant_int.wcnf S = OPT
O = 4
T = 21.06		 S = OPT
O = 4
T = 21.06
causal_n6_i5_N500_uai13_harddeps_int.wcnf S = OPT
O = 4
T = 19.45		 S = OPT
O = 4
T = 19.45
causal_n6_i6_N1000_uai14_constant_int.wcnf S = OPT
O = 19
T = 19.37		 S = OPT
O = 19
T = 19.37
causal_n6_i7_N1000_uai14_harddeps_int.wcnf S = OPT
O = 49
T = 15.22		 S = OPT
O = 49
T = 15.22
causal_n6_i8_N10000_uai14_constant_int.wcnf S = OPT
O = 26
T = 14.41		 S = OPT
O = 26
T = 14.41
causal_n6_i8_N1000_uai14_constant_int.wcnf S = OPT
O = 26
T = 13.27		 S = OPT
O = 26
T = 13.27
causal_n6_i9_N10000_uai14_constant_int.wcnf S = OPT
O = 28
T = 13.49		 S = OPT
O = 28
T = 13.49
causal_n6_i9_N10000_uai14_harddeps_int.wcnf S = OPT
O = 34
T = 13.34		 S = OPT
O = 34
T = 13.34
causal_n6_i9_N1000_uai14_constant_int.wcnf S = OPT
O = 28
T = 15.76		 S = OPT
O = 28
T = 15.76
causal_n6_i9_N500_uai14_constant_int.wcnf S = OPT
O = 28
T = 13.45		 S = OPT
O = 28
T = 13.45
causal_n7_i10_N10000_uai14_constant_int.wcnf S = OPT
O = 42
T = 22.51		 S = OPT
O = 42
T = 22.51
causal_n7_i10_N1000_uai14_constant_int.wcnf S = OPT
O = 42
T = 23.44		 S = OPT
O = 42
T = 23.44
causal_n7_i10_N500_uai14_constant_int.wcnf S = OPT
O = 42
T = 29.88		 S = OPT
O = 42
T = 29.88
causal_n7_i2_N10000_uai14_harddeps_int.wcnf S = OPT
O = 63
T = 111.10		 S = OPT
O = 63
T = 111.10
causal_n7_i2_N500_uai14_harddeps_int.wcnf S = OPT
O = 63
T = 80.27		 S = OPT
O = 63
T = 80.27
causal_n7_i4_N10000_uai14_harddeps_int.wcnf S = OPT
O = 101
T = 207.97		 S = OPT
O = 101
T = 207.97
causal_n7_i4_N1000_uai14_constant_int.wcnf S = OPT
O = 63
T = 273.80		 S = OPT
O = 63
T = 273.80
causal_n7_i4_N1000_uai14_harddeps_int.wcnf S = OPT
O = 101
T = 341.69		 S = OPT
O = 101
T = 341.69
causal_n7_i4_N500_uai14_constant_int.wcnf S = OPT
O = 63
T = 161.56		 S = OPT
O = 63
T = 161.56
causal_n7_i4_N500_uai14_harddeps_int.wcnf S = OPT
O = 101
T = 458.90		 S = OPT
O = 101
T = 458.90
causal_n7_i5_N10000_uai14_constant_int.wcnf S = OPT
O = 48
T = 26.72		 S = OPT
O = 48
T = 26.72
causal_n7_i5_N1000_uai14_constant_int.wcnf S = OPT
O = 48
T = 38.88		 S = OPT
O = 48
T = 38.88
causal_n7_i5_N500_uai14_constant_int.wcnf S = OPT
O = 48
T = 33.69		 S = OPT
O = 48
T = 33.69
causal_n7_i6_N10000_uai14_harddeps_int.wcnf S = OPT
O = 116
T = 492.51		 S = OPT
O = 116
T = 492.51
causal_n7_i6_N1000_uai14_harddeps_int.wcnf S = OPT
O = 116
T = 555.18		 S = OPT
O = 116
T = 555.18
causal_n7_i6_N500_uai14_harddeps_int.wcnf S = OPT
O = 116
T = 697.59		 S = OPT
O = 116
T = 697.59
causal_n7_i7_N10000_uai14_harddeps_int.wcnf S = OPT
O = 95
T = 520.78		 S = OPT
O = 95
T = 520.78
causal_n7_i7_N1000_uai14_harddeps_int.wcnf S = OPT
O = 95
T = 588.45		 S = OPT
O = 95
T = 588.45
causal_n7_i8_N10000_uai14_constant_int.wcnf S = OPT
O = 24
T = 15.07		 S = OPT
O = 24
T = 15.07
causal_n7_i8_N10000_uai14_harddeps_int.wcnf S = OPT
O = 94
T = 71.64		 S = OPT
O = 94
T = 71.64
causal_n7_i8_N1000_uai14_constant_int.wcnf S = OPT
O = 24
T = 13.86		 S = OPT
O = 24
T = 13.86
causal_n7_i8_N1000_uai14_harddeps_int.wcnf S = OPT
O = 94
T = 66.10		 S = OPT
O = 94
T = 66.10
causal_n7_i8_N500_uai14_constant_int.wcnf S = OPT
O = 24
T = 13.64		 S = OPT
O = 24
T = 13.64
causal_n7_i8_N500_uai14_harddeps_int.wcnf S = OPT
O = 94
T = 47.67		 S = OPT
O = 94
T = 47.67
causal_n7_i9_N10000_uai14_constant_int.wcnf S = OPT
O = 46
T = 26.54		 S = OPT
O = 46
T = 26.54
causal_n7_i9_N10000_uai14_harddeps_int.wcnf S = OPT
O = 82
T = 81.76		 S = OPT
O = 82
T = 81.76
causal_n7_i9_N1000_uai14_constant_int.wcnf S = OPT
O = 46
T = 20.44		 S = OPT
O = 46
T = 20.44
causal_n7_i9_N1000_uai14_harddeps_int.wcnf S = OPT
O = 82
T = 66.49		 S = OPT
O = 82
T = 66.49
causal_n7_i9_N500_uai14_constant_int.wcnf S = OPT
O = 46
T = 25.42		 S = OPT
O = 46
T = 25.42
causal_n7_i9_N500_uai14_harddeps_int.wcnf S = OPT
O = 82
T = 44.34		 S = OPT
O = 82
T = 44.34
s00641_nan_explicit_0_0.wcnf S = OPT
O = 52
T = 9.94		 S = OPT
O = 52
T = 9.94
s00641_nan_explicit_1_0.wcnf S = OPT
O = 60
T = 9.58		 S = OPT
O = 60
T = 9.58
s00641_nan_explicit_2_0.wcnf S = OPT
O = 60
T = 9.87		 S = OPT
O = 60
T = 9.87
s00641_nan_explicit_3_0.wcnf S = OPT
O = 58
T = 9.93		 S = OPT
O = 58
T = 9.93
s00641_nan_explicit_4_0.wcnf S = OPT
O = 65
T = 9.88		 S = OPT
O = 65
T = 9.88
s00641_nan_explicit_5_0.wcnf S = OPT
O = 67
T = 9.96		 S = OPT
O = 67
T = 9.96
s00641_nan_explicit_6_0.wcnf S = OPT
O = 67
T = 9.90		 S = OPT
O = 67
T = 9.90
s00641_nan_explicit_7_0.wcnf S = OPT
O = 67
T = 9.93		 S = OPT
O = 67
T = 9.93
s00641_nan_explicit_8_0.wcnf S = OPT
O = 69
T = 9.94		 S = OPT
O = 69
T = 9.94
s00641_nan_explicit_9_0.wcnf S = OPT
O = 68
T = 9.96		 S = OPT
O = 68
T = 9.96
s01423_nan_explicit_0_0.wcnf S = OPT
O = 63
T = 10.09		 S = OPT
O = 63
T = 10.09
s01423_nan_explicit_1_0.wcnf S = OPT
O = 63
T = 10.15		 S = OPT
O = 63
T = 10.15
s01423_nan_explicit_2_0.wcnf S = OPT
O = 60
T = 10.15		 S = OPT
O = 60
T = 10.15
s01423_nan_explicit_3_0.wcnf S = OPT
O = 69
T = 10.20		 S = OPT
O = 69
T = 10.20
s01423_nan_explicit_4_0.wcnf S = OPT
O = 56
T = 10.03		 S = OPT
O = 56
T = 10.03
s01423_nan_explicit_5_0.wcnf S = OPT
O = 59
T = 10.02		 S = OPT
O = 59
T = 10.02
s01423_nan_explicit_6_0.wcnf S = OPT
O = 64
T = 10.11		 S = OPT
O = 64
T = 10.11
s01423_nan_explicit_7_0.wcnf S = OPT
O = 65
T = 10.19		 S = OPT
O = 65
T = 10.19
s01423_nan_explicit_8_0.wcnf S = OPT
O = 63
T = 9.99		 S = OPT
O = 63
T = 9.99
s01423_nan_explicit_9_0.wcnf S = OPT
O = 70
T = 10.09		 S = OPT
O = 70
T = 10.09
s38417_nan_explicit_0_0.wcnf S = OPT
O = 60
T = 11.38		 S = OPT
O = 60
T = 11.38
s38417_nan_explicit_10_0.wcnf S = OPT
O = 65
T = 10.42		 S = OPT
O = 65
T = 10.42
s38417_nan_explicit_11_0.wcnf S = OPT
O = 68
T = 10.30		 S = OPT
O = 68
T = 10.30
s38417_nan_explicit_12_0.wcnf S = OPT
O = 70
T = 10.49		 S = OPT
O = 70
T = 10.49
s38417_nan_explicit_13_0.wcnf S = OPT
O = 67
T = 10.61		 S = OPT
O = 67
T = 10.61
s38417_nan_explicit_14_0.wcnf S = OPT
O = 55
T = 10.47		 S = OPT
O = 55
T = 10.47
s38417_nan_explicit_15_0.wcnf S = OPT
O = 65
T = 10.44		 S = OPT
O = 65
T = 10.44
s38417_nan_explicit_16_0.wcnf S = OPT
O = 69
T = 10.29		 S = OPT
O = 69
T = 10.29
s38417_nan_explicit_17_0.wcnf S = OPT
O = 61
T = 10.54		 S = OPT
O = 61
T = 10.54
s38417_nan_explicit_18_0.wcnf S = OPT
O = 63
T = 10.42		 S = OPT
O = 63
T = 10.42
s38417_nan_explicit_19_0.wcnf S = OPT
O = 70
T = 10.38		 S = OPT
O = 70
T = 10.38
s38417_nan_explicit_1_0.wcnf S = OPT
O = 58
T = 11.00		 S = OPT
O = 58
T = 11.00
s38417_nan_explicit_20_0.wcnf S = OPT
O = 64
T = 10.68		 S = OPT
O = 64
T = 10.68
s38417_nan_explicit_21_0.wcnf S = OPT
O = 65
T = 10.32		 S = OPT
O = 65
T = 10.32
s38417_nan_explicit_22_0.wcnf S = OPT
O = 55
T = 10.81		 S = OPT
O = 55
T = 10.81
s38417_nan_explicit_23_0.wcnf S = OPT
O = 68
T = 10.03		 S = OPT
O = 68
T = 10.03
s38417_nan_explicit_24_0.wcnf S = OPT
O = 63
T = 10.00		 S = OPT
O = 63
T = 10.00
s38417_nan_explicit_25_0.wcnf S = OPT
O = 69
T = 10.30		 S = OPT
O = 69
T = 10.30
s38417_nan_explicit_26_0.wcnf S = OPT
O = 64
T = 10.24		 S = OPT
O = 64
T = 10.24
s38417_nan_explicit_27_0.wcnf S = OPT
O = 67
T = 10.31		 S = OPT
O = 67
T = 10.31
s38417_nan_explicit_28_0.wcnf S = OPT
O = 63
T = 10.21		 S = OPT
O = 63
T = 10.21
s38417_nan_explicit_29_0.wcnf S = OPT
O = 69
T = 10.60		 S = OPT
O = 69
T = 10.60
s38417_nan_explicit_2_0.wcnf S = OPT
O = 64
T = 10.90		 S = OPT
O = 64
T = 10.90
s38417_nan_explicit_3_0.wcnf S = OPT
O = 65
T = 10.87		 S = OPT
O = 65
T = 10.87
s38417_nan_explicit_4_0.wcnf S = OPT
O = 58
T = 10.96		 S = OPT
O = 58
T = 10.96
s38417_nan_explicit_5_0.wcnf S = OPT
O = 69
T = 10.44		 S = OPT
O = 69
T = 10.44
s38417_nan_explicit_6_0.wcnf S = OPT
O = 61
T = 10.55		 S = OPT
O = 61
T = 10.55
s38417_nan_explicit_7_0.wcnf S = OPT
O = 72
T = 10.76		 S = OPT
O = 72
T = 10.76
s38417_nan_explicit_8_0.wcnf S = OPT
O = 70
T = 10.30		 S = OPT
O = 70
T = 10.30
s38417_nan_explicit_9_0.wcnf S = OPT
O = 67
T = 10.41		 S = OPT
O = 67
T = 10.41
s38584_nan_explicit_0_0.wcnf S = OPT
O = 121
T = 125.46		 S = OPT
O = 121
T = 125.46
s38584_nan_explicit_10_0.wcnf S = OPT
O = 209
T = 639.28		 S = OPT
O = 209
T = 639.28
s38584_nan_explicit_11_0.wcnf S = OPT
O = 193
T = 179.94		 S = OPT
O = 193
T = 179.94
s38584_nan_explicit_12_0.wcnf S = OPT
O = 191
T = 44.54		 S = OPT
O = 191
T = 44.54
s38584_nan_explicit_13_0.wcnf S = OPT
O = 192
T = 99.16		 S = OPT
O = 192
T = 99.16
s38584_nan_explicit_14_0.wcnf S = OPT
O = 202
T = 296.68		 S = OPT
O = 202
T = 296.68
s38584_nan_explicit_15_0.wcnf S = OPT
O = 208
T = 278.17		 S = OPT
O = 208
T = 278.17
s38584_nan_explicit_16_0.wcnf S = OPT
O = 188
T = 53.08		 S = OPT
O = 188
T = 53.08
s38584_nan_explicit_17_0.wcnf S = OPT
O = 185
T = 37.09		 S = OPT
O = 185
T = 37.09
s38584_nan_explicit_18_0.wcnf S = OPT
O = 186
T = 39.67		 S = OPT
O = 186
T = 39.67
s38584_nan_explicit_19_0.wcnf S = OPT
O = 198
T = 46.78		 S = OPT
O = 198
T = 46.78
s38584_nan_explicit_1_0.wcnf S = OPT
O = 126
T = 251.16		 S = OPT
O = 126
T = 251.16
s38584_nan_explicit_20_0.wcnf S = OPT
O = 194
T = 44.47		 S = OPT
O = 194
T = 44.47
s38584_nan_explicit_21_0.wcnf S = OPT
O = 184
T = 28.63		 S = OPT
O = 184
T = 28.63
s38584_nan_explicit_22_0.wcnf S = OPT
O = 179
T = 36.01		 S = OPT
O = 179
T = 36.01
s38584_nan_explicit_23_0.wcnf S = OPT
O = 179
T = 65.18		 S = OPT
O = 179
T = 65.18
s38584_nan_explicit_24_0.wcnf S = OPT
O = 177
T = 30.05		 S = OPT
O = 177
T = 30.05
s38584_nan_explicit_25_0.wcnf S = OPT
O = 188
T = 28.23		 S = OPT
O = 188
T = 28.23
s38584_nan_explicit_26_0.wcnf S = OPT
O = 169
T = 29.63		 S = OPT
O = 169
T = 29.63
s38584_nan_explicit_27_0.wcnf S = OPT
O = 203
T = 34.39		 S = OPT
O = 203
T = 34.39
s38584_nan_explicit_28_0.wcnf S = OPT
O = 193
T = 43.57		 S = OPT
O = 193
T = 43.57
s38584_nan_explicit_29_0.wcnf S = OPT
O = 200
T = 29.25		 S = OPT
O = 200
T = 29.25
s38584_nan_explicit_2_0.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s38584_nan_explicit_30_0.wcnf S = OPT
O = 200
T = 52.66		 S = OPT
O = 200
T = 52.66
s38584_nan_explicit_31_0.wcnf S = OPT
O = 190
T = 56.88		 S = OPT
O = 190
T = 56.88
s38584_nan_explicit_32_0.wcnf S = OPT
O = 200
T = 73.72		 S = OPT
O = 200
T = 73.72
s38584_nan_explicit_33_0.wcnf S = OPT
O = 189
T = 23.80		 S = OPT
O = 189
T = 23.80
s38584_nan_explicit_34_0.wcnf S = OPT
O = 189
T = 27.77		 S = OPT
O = 189
T = 27.77
s38584_nan_explicit_35_0.wcnf S = OPT
O = 183
T = 26.98		 S = OPT
O = 183
T = 26.98
s38584_nan_explicit_36_0.wcnf S = OPT
O = 183
T = 26.74		 S = OPT
O = 183
T = 26.74
s38584_nan_explicit_37_0.wcnf S = OPT
O = 181
T = 23.57		 S = OPT
O = 181
T = 23.57
s38584_nan_explicit_38_0.wcnf S = OPT
O = 189
T = 25.02		 S = OPT
O = 189
T = 25.02
s38584_nan_explicit_39_0.wcnf S = OPT
O = 198
T = 47.36		 S = OPT
O = 198
T = 47.36
s38584_nan_explicit_3_0.wcnf S = OPT
O = 150
T = 104.95		 S = OPT
O = 150
T = 104.95
s38584_nan_explicit_40_0.wcnf S = OPT
O = 191
T = 28.19		 S = OPT
O = 191
T = 28.19
s38584_nan_explicit_41_0.wcnf S = OPT
O = 163
T = 25.12		 S = OPT
O = 163
T = 25.12
s38584_nan_explicit_42_0.wcnf S = OPT
O = 193
T = 26.52		 S = OPT
O = 193
T = 26.52
s38584_nan_explicit_43_0.wcnf S = OPT
O = 178
T = 24.75		 S = OPT
O = 178
T = 24.75
s38584_nan_explicit_44_0.wcnf S = OPT
O = 168
T = 24.18		 S = OPT
O = 168
T = 24.18
s38584_nan_explicit_45_0.wcnf S = OPT
O = 168
T = 24.22		 S = OPT
O = 168
T = 24.22
s38584_nan_explicit_46_0.wcnf S = OPT
O = 172
T = 25.87		 S = OPT
O = 172
T = 25.87
s38584_nan_explicit_47_0.wcnf S = OPT
O = 154
T = 22.27		 S = OPT
O = 154
T = 22.27
s38584_nan_explicit_48_0.wcnf S = OPT
O = 164
T = 25.68		 S = OPT
O = 164
T = 25.68
s38584_nan_explicit_49_0.wcnf S = OPT
O = 166
T = 14.51		 S = OPT
O = 166
T = 14.51
s38584_nan_explicit_4_0.wcnf S = OPT
O = 146
T = 178.49		 S = OPT
O = 146
T = 178.49
s38584_nan_explicit_5_0.wcnf S = OPT
O = 176
T = 671.82		 S = OPT
O = 176
T = 671.82
s38584_nan_explicit_6_0.wcnf S = OPT
O = 185
T = 208.15		 S = OPT
O = 185
T = 208.15
s38584_nan_explicit_7_0.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s38584_nan_explicit_8_0.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s38584_nan_explicit_9_0.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
frb20-11-1.partial.wcnf S = OPT
O = 200
T = 9.99		 S = OPT
O = 200
T = 9.99
frb20-11-2.partial.wcnf S = OPT
O = 200
T = 9.91		 S = OPT
O = 200
T = 9.91
frb20-11-3.partial.wcnf S = OPT
O = 200
T = 10.06		 S = OPT
O = 200
T = 10.06
frb20-11-4.partial.wcnf S = OPT
O = 200
T = 9.89		 S = OPT
O = 200
T = 9.89
frb20-11-5.partial.wcnf S = OPT
O = 200
T = 10.07		 S = OPT
O = 200
T = 10.07
frb25-13-1.partial.wcnf S = OPT
O = 300
T = 11.09		 S = OPT
O = 300
T = 11.09
frb25-13-2.partial.wcnf S = OPT
O = 300
T = 10.50		 S = OPT
O = 300
T = 10.50
frb25-13-3.partial.wcnf S = OPT
O = 300
T = 10.29		 S = OPT
O = 300
T = 10.29
frb25-13-4.partial.wcnf S = OPT
O = 300
T = 10.42		 S = OPT
O = 300
T = 10.42
frb25-13-5.partial.wcnf S = OPT
O = 300
T = 10.28		 S = OPT
O = 300
T = 10.28
frb30-15-1.partial.wcnf S = OPT
O = 420
T = 13.51		 S = OPT
O = 420
T = 13.51
frb30-15-2.partial.wcnf S = OPT
O = 420
T = 14.67		 S = OPT
O = 420
T = 14.67
frb30-15-3.partial.wcnf S = OPT
O = 420
T = 16.10		 S = OPT
O = 420
T = 16.10
frb30-15-4.partial.wcnf S = OPT
O = 420
T = 12.51		 S = OPT
O = 420
T = 12.51
frb30-15-5.partial.wcnf S = OPT
O = 420
T = 10.98		 S = OPT
O = 420
T = 10.98
frb35-17-1.partial.wcnf S = OPT
O = 560
T = 25.20		 S = OPT
O = 560
T = 25.20
frb35-17-2.partial.wcnf S = OPT
O = 560
T = 43.82		 S = OPT
O = 560
T = 43.82
frb35-17-3.partial.wcnf S = OPT
O = 560
T = 36.67		 S = OPT
O = 560
T = 36.67
frb35-17-4.partial.wcnf S = OPT
O = 560
T = 13.25		 S = OPT
O = 560
T = 13.25
frb35-17-5.partial.wcnf S = OPT
O = 560
T = 48.23		 S = OPT
O = 560
T = 48.23
frb40-19-1.partial.wcnf S = OPT
O = 720
T = 51.33		 S = OPT
O = 720
T = 51.33
frb40-19-2.partial.wcnf S = OPT
O = 720
T = 109.80		 S = OPT
O = 720
T = 109.80
frb40-19-3.partial.wcnf S = OPT
O = 720
T = 93.13		 S = OPT
O = 720
T = 93.13
frb40-19-4.partial.wcnf S = OPT
O = 720
T = 29.54		 S = OPT
O = 720
T = 29.54
frb40-19-5.partial.wcnf S = OPT
O = 720
T = 271.23		 S = OPT
O = 720
T = 271.23
ft10-808-1090.wcnf S = OPT
O = 122
T = 45.19		 S = OPT
O = 122
T = 45.19
la04-567-0696.wcnf S = OPT
O = 23
T = 12.61		 S = OPT
O = 23
T = 12.61
orb08-894-1058.wcnf S = OPT
O = 5
T = 22.67		 S = OPT
O = 5
T = 22.67
max_clq_150-0-447-1.clq.wcnf S = OPT
O = 147
T = 9.82		 S = OPT
O = 147
T = 9.82
max_clq_150-0-447-2.clq.wcnf S = OPT
O = 147
T = 9.79		 S = OPT
O = 147
T = 9.79
max_clq_150-0-447-3.clq.wcnf S = OPT
O = 147
T = 9.80		 S = OPT
O = 147
T = 9.80
max_clq_150-0-447-4.clq.wcnf S = OPT
O = 147
T = 9.77		 S = OPT
O = 147
T = 9.77
max_clq_150-1-894-1.clq.wcnf S = OPT
O = 146
T = 9.85		 S = OPT
O = 146
T = 9.85
max_clq_150-1-894-2.clq.wcnf S = OPT
O = 146
T = 9.85		 S = OPT
O = 146
T = 9.85
max_clq_150-1-894-3.clq.wcnf S = OPT
O = 146
T = 9.92		 S = OPT
O = 146
T = 9.92
max_clq_150-1-894-4.clq.wcnf S = OPT
O = 146
T = 9.50		 S = OPT
O = 146
T = 9.50
max_clq_150-10-4917-1.clq.wcnf S = OPT
O = 141
T = 10.08		 S = OPT
O = 141
T = 10.08
max_clq_150-10-4917-2.clq.wcnf S = OPT
O = 141
T = 10.18		 S = OPT
O = 141
T = 10.18
max_clq_150-10-4917-3.clq.wcnf S = OPT
O = 141
T = 10.04		 S = OPT
O = 141
T = 10.04
max_clq_150-10-4917-4.clq.wcnf S = OPT
O = 141
T = 10.08		 S = OPT
O = 141
T = 10.08
max_clq_150-11-5364-1.clq.wcnf S = OPT
O = 140
T = 10.18		 S = OPT
O = 140
T = 10.18
max_clq_150-11-5364-2.clq.wcnf S = OPT
O = 141
T = 10.22		 S = OPT
O = 141
T = 10.22
max_clq_150-11-5364-3.clq.wcnf S = OPT
O = 140
T = 10.03		 S = OPT
O = 140
T = 10.03
max_clq_150-11-5364-4.clq.wcnf S = OPT
O = 140
T = 10.01		 S = OPT
O = 140
T = 10.01
max_clq_150-12-5811-1.clq.wcnf S = OPT
O = 140
T = 10.30		 S = OPT
O = 140
T = 10.30
max_clq_150-12-5811-2.clq.wcnf S = OPT
O = 140
T = 10.15		 S = OPT
O = 140
T = 10.15
max_clq_150-12-5811-3.clq.wcnf S = OPT
O = 139
T = 10.16		 S = OPT
O = 139
T = 10.16
max_clq_150-12-5811-4.clq.wcnf S = OPT
O = 140
T = 10.27		 S = OPT
O = 140
T = 10.27
max_clq_150-13-6258-1.clq.wcnf S = OPT
O = 138
T = 10.49		 S = OPT
O = 138
T = 10.49
max_clq_150-13-6258-2.clq.wcnf S = OPT
O = 139
T = 10.65		 S = OPT
O = 139
T = 10.65
max_clq_150-13-6258-3.clq.wcnf S = OPT
O = 138
T = 9.88		 S = OPT
O = 138
T = 9.88
max_clq_150-13-6258-4.clq.wcnf S = OPT
O = 138
T = 10.23		 S = OPT
O = 138
T = 10.23
max_clq_150-14-6705-1.clq.wcnf S = OPT
O = 138
T = 11.02		 S = OPT
O = 138
T = 11.02
max_clq_150-14-6705-2.clq.wcnf S = OPT
O = 137
T = 10.80		 S = OPT
O = 137
T = 10.80
max_clq_150-14-6705-3.clq.wcnf S = OPT
O = 137
T = 10.74		 S = OPT
O = 137
T = 10.74
max_clq_150-14-6705-4.clq.wcnf S = OPT
O = 137
T = 10.60		 S = OPT
O = 137
T = 10.60
max_clq_150-15-7152-1.clq.wcnf S = OPT
O = 135
T = 10.49		 S = OPT
O = 135
T = 10.49
max_clq_150-15-7152-2.clq.wcnf S = OPT
O = 136
T = 11.06		 S = OPT
O = 136
T = 11.06
max_clq_150-15-7152-3.clq.wcnf S = OPT
O = 135
T = 11.06		 S = OPT
O = 135
T = 11.06
max_clq_150-15-7152-4.clq.wcnf S = OPT
O = 136
T = 10.86		 S = OPT
O = 136
T = 10.86
max_clq_150-16-7599-1.clq.wcnf S = OPT
O = 134
T = 11.30		 S = OPT
O = 134
T = 11.30
max_clq_150-16-7599-2.clq.wcnf S = OPT
O = 135
T = 11.83		 S = OPT
O = 135
T = 11.83
max_clq_150-16-7599-3.clq.wcnf S = OPT
O = 134
T = 11.01		 S = OPT
O = 134
T = 11.01
max_clq_150-16-7599-4.clq.wcnf S = OPT
O = 135
T = 11.85		 S = OPT
O = 135
T = 11.85
max_clq_150-17-8046-1.clq.wcnf S = OPT
O = 132
T = 12.12		 S = OPT
O = 132
T = 12.12
max_clq_150-17-8046-2.clq.wcnf S = OPT
O = 133
T = 12.15		 S = OPT
O = 133
T = 12.15
max_clq_150-17-8046-3.clq.wcnf S = OPT
O = 132
T = 12.54		 S = OPT
O = 132
T = 12.54
max_clq_150-17-8046-4.clq.wcnf S = OPT
O = 132
T = 11.56		 S = OPT
O = 132
T = 11.56
max_clq_150-18-8493-1.clq.wcnf S = OPT
O = 130
T = 12.96		 S = OPT
O = 130
T = 12.96
max_clq_150-18-8493-2.clq.wcnf S = OPT
O = 130
T = 14.01		 S = OPT
O = 130
T = 14.01
max_clq_150-18-8493-3.clq.wcnf S = OPT
O = 129
T = 11.74		 S = OPT
O = 129
T = 11.74
max_clq_150-18-8493-4.clq.wcnf S = OPT
O = 129
T = 11.84		 S = OPT
O = 129
T = 11.84
max_clq_150-19-8940-1.clq.wcnf S = OPT
O = 127
T = 14.36		 S = OPT
O = 127
T = 14.36
max_clq_150-19-8940-2.clq.wcnf S = OPT
O = 126
T = 12.46		 S = OPT
O = 126
T = 12.46
max_clq_150-19-8940-3.clq.wcnf S = OPT
O = 127
T = 13.96		 S = OPT
O = 127
T = 13.96
max_clq_150-19-8940-4.clq.wcnf S = OPT
O = 127
T = 14.87		 S = OPT
O = 127
T = 14.87
max_clq_150-2-1341-1.clq.wcnf S = OPT
O = 146
T = 9.91		 S = OPT
O = 146
T = 9.91
max_clq_150-2-1341-2.clq.wcnf S = OPT
O = 146
T = 9.89		 S = OPT
O = 146
T = 9.89
max_clq_150-2-1341-3.clq.wcnf S = OPT
O = 146
T = 10.04		 S = OPT
O = 146
T = 10.04
max_clq_150-2-1341-4.clq.wcnf S = OPT
O = 145
T = 10.03		 S = OPT
O = 145
T = 10.03
max_clq_150-20-9387-1.clq.wcnf S = OPT
O = 123
T = 12.93		 S = OPT
O = 123
T = 12.93
max_clq_150-20-9387-2.clq.wcnf S = OPT
O = 124
T = 16.25		 S = OPT
O = 124
T = 16.25
max_clq_150-20-9387-3.clq.wcnf S = OPT
O = 123
T = 13.79		 S = OPT
O = 123
T = 13.79
max_clq_150-20-9387-4.clq.wcnf S = OPT
O = 123
T = 13.52		 S = OPT
O = 123
T = 13.52
max_clq_150-21-9834-1.clq.wcnf S = OPT
O = 117
T = 12.77		 S = OPT
O = 117
T = 12.77
max_clq_150-21-9834-2.clq.wcnf S = OPT
O = 118
T = 14.05		 S = OPT
O = 118
T = 14.05
max_clq_150-21-9834-3.clq.wcnf S = OPT
O = 116
T = 11.71		 S = OPT
O = 116
T = 11.71
max_clq_150-21-9834-4.clq.wcnf S = OPT
O = 118
T = 13.59		 S = OPT
O = 118
T = 13.59
max_clq_150-22-10281-1.clq.wcnf S = OPT
O = 107
T = 10.24		 S = OPT
O = 107
T = 10.24
max_clq_150-22-10281-2.clq.wcnf S = OPT
O = 107
T = 10.26		 S = OPT
O = 107
T = 10.26
max_clq_150-22-10281-3.clq.wcnf S = OPT
O = 108
T = 10.81		 S = OPT
O = 108
T = 10.81
max_clq_150-22-10281-4.clq.wcnf S = OPT
O = 108
T = 10.88		 S = OPT
O = 108
T = 10.88
max_clq_150-23-10728-1.clq.wcnf S = OPT
O = 91
T = 9.89		 S = OPT
O = 91
T = 9.89
max_clq_150-23-10728-2.clq.wcnf S = OPT
O = 89
T = 9.89		 S = OPT
O = 89
T = 9.89
max_clq_150-23-10728-3.clq.wcnf S = OPT
O = 91
T = 9.79		 S = OPT
O = 91
T = 9.79
max_clq_150-23-10728-4.clq.wcnf S = OPT
O = 90
T = 9.83		 S = OPT
O = 90
T = 9.83
max_clq_150-3-1788-1.clq.wcnf S = OPT
O = 145
T = 9.91		 S = OPT
O = 145
T = 9.91
max_clq_150-3-1788-2.clq.wcnf S = OPT
O = 145
T = 9.87		 S = OPT
O = 145
T = 9.87
max_clq_150-3-1788-3.clq.wcnf S = OPT
O = 145
T = 9.80		 S = OPT
O = 145
T = 9.80
max_clq_150-3-1788-4.clq.wcnf S = OPT
O = 145
T = 9.91		 S = OPT
O = 145
T = 9.91
max_clq_150-4-2235-1.clq.wcnf S = OPT
O = 144
T = 10.06		 S = OPT
O = 144
T = 10.06
max_clq_150-4-2235-2.clq.wcnf S = OPT
O = 145
T = 9.94		 S = OPT
O = 145
T = 9.94
max_clq_150-4-2235-3.clq.wcnf S = OPT
O = 144
T = 9.83		 S = OPT
O = 144
T = 9.83
max_clq_150-4-2235-4.clq.wcnf S = OPT
O = 145
T = 9.97		 S = OPT
O = 145
T = 9.97
max_clq_150-5-2682-1.clq.wcnf S = OPT
O = 144
T = 9.90		 S = OPT
O = 144
T = 9.90
max_clq_150-5-2682-2.clq.wcnf S = OPT
O = 144
T = 9.90		 S = OPT
O = 144
T = 9.90
max_clq_150-5-2682-3.clq.wcnf S = OPT
O = 144
T = 10.05		 S = OPT
O = 144
T = 10.05
max_clq_150-5-2682-4.clq.wcnf S = OPT
O = 144
T = 9.86		 S = OPT
O = 144
T = 9.86
max_clq_150-6-3129-1.clq.wcnf S = OPT
O = 144
T = 9.96		 S = OPT
O = 144
T = 9.96
max_clq_150-6-3129-2.clq.wcnf S = OPT
O = 143
T = 9.90		 S = OPT
O = 143
T = 9.90
max_clq_150-6-3129-3.clq.wcnf S = OPT
O = 143
T = 9.91		 S = OPT
O = 143
T = 9.91
max_clq_150-6-3129-4.clq.wcnf S = OPT
O = 144
T = 10.05		 S = OPT
O = 144
T = 10.05
max_clq_150-7-3576-1.clq.wcnf S = OPT
O = 144
T = 10.00		 S = OPT
O = 144
T = 10.00
max_clq_150-7-3576-2.clq.wcnf S = OPT
O = 143
T = 9.51		 S = OPT
O = 143
T = 9.51
max_clq_150-7-3576-3.clq.wcnf S = OPT
O = 143
T = 9.89		 S = OPT
O = 143
T = 9.89
max_clq_150-7-3576-4.clq.wcnf S = OPT
O = 143
T = 9.57		 S = OPT
O = 143
T = 9.57
max_clq_150-8-4023-1.clq.wcnf S = OPT
O = 143
T = 10.00		 S = OPT
O = 143
T = 10.00
max_clq_150-8-4023-2.clq.wcnf S = OPT
O = 142
T = 9.60		 S = OPT
O = 142
T = 9.60
max_clq_150-8-4023-3.clq.wcnf S = OPT
O = 143
T = 9.97		 S = OPT
O = 143
T = 9.97
max_clq_150-8-4023-4.clq.wcnf S = OPT
O = 142
T = 9.62		 S = OPT
O = 142
T = 9.62
max_clq_150-9-4470-1.clq.wcnf S = OPT
O = 142
T = 9.96		 S = OPT
O = 142
T = 9.96
max_clq_150-9-4470-2.clq.wcnf S = OPT
O = 142
T = 9.98		 S = OPT
O = 142
T = 9.98
max_clq_150-9-4470-3.clq.wcnf S = OPT
O = 142
T = 10.02		 S = OPT
O = 142
T = 10.02
max_clq_150-9-4470-4.clq.wcnf S = OPT
O = 142
T = 9.61		 S = OPT
O = 142
T = 9.61
MANN_a27.clq.wcnf S = OPT
O = 252
T = 11.22		 S = OPT
O = 252
T = 11.22
MANN_a45.clq.wcnf S = OPT
O = 690
T = 177.69		 S = OPT
O = 690
T = 177.69
MANN_a81.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
MANN_a9.clq.wcnf S = OPT
O = 29
T = 9.78		 S = OPT
O = 29
T = 9.78
brock200_1.clq.wcnf S = OPT
O = 179
T = 43.01		 S = OPT
O = 179
T = 43.01
brock200_2.clq.wcnf S = OPT
O = 188
T = 11.30		 S = OPT
O = 188
T = 11.30
brock200_3.clq.wcnf S = OPT
O = 185
T = 14.05		 S = OPT
O = 185
T = 14.05
brock200_4.clq.wcnf S = OPT
O = 183
T = 20.10		 S = OPT
O = 183
T = 20.10
brock400_1.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
brock400_2.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
brock400_3.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
brock400_4.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
brock800_1.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
brock800_2.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
brock800_3.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
brock800_4.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
c-fat200-1.clq.wcnf S = OPT
O = 188
T = 9.86		 S = OPT
O = 188
T = 9.86
c-fat200-2.clq.wcnf S = OPT
O = 176
T = 9.87		 S = OPT
O = 176
T = 9.87
c-fat200-5.clq.wcnf S = OPT
O = 142
T = 9.99		 S = OPT
O = 142
T = 9.99
c-fat500-1.clq.wcnf S = OPT
O = 486
T = 10.76		 S = OPT
O = 486
T = 10.76
c-fat500-10.clq.wcnf S = OPT
O = 374
T = 10.11		 S = OPT
O = 374
T = 10.11
c-fat500-2.clq.wcnf S = OPT
O = 474
T = 10.58		 S = OPT
O = 474
T = 10.58
c-fat500-5.clq.wcnf S = OPT
O = 436
T = 10.11		 S = OPT
O = 436
T = 10.11
hamming10-2.clq.wcnf S = OPT
O = 512
T = 9.87		 S = OPT
O = 512
T = 9.87
hamming10-4.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
hamming6-2.clq.wcnf S = OPT
O = 32
T = 9.76		 S = OPT
O = 32
T = 9.76
hamming6-4.clq.wcnf S = OPT
O = 60
T = 9.98		 S = OPT
O = 60
T = 9.98
hamming8-2.clq.wcnf S = OPT
O = 128
T = 9.79		 S = OPT
O = 128
T = 9.79
hamming8-4.clq.wcnf S = OPT
O = 240
T = 10.02		 S = OPT
O = 240
T = 10.02
johnson16-2-4.clq.wcnf S = OPT
O = 112
T = 9.77		 S = OPT
O = 112
T = 9.77
johnson32-2-4.clq.wcnf S = OPT
O = 480
T = 9.85		 S = OPT
O = 480
T = 9.85
johnson8-2-4.clq.wcnf S = OPT
O = 24
T = 9.83		 S = OPT
O = 24
T = 9.83
johnson8-4-4.clq.wcnf S = OPT
O = 56
T = 9.73		 S = OPT
O = 56
T = 9.73
keller4.clq.wcnf S = OPT
O = 160
T = 12.26		 S = OPT
O = 160
T = 12.26
keller5.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
p_hat1000-1.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
p_hat1000-2.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
p_hat1000-3.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
p_hat300-1.clq.wcnf S = OPT
O = 292
T = 44.44		 S = OPT
O = 292
T = 44.44
p_hat300-2.clq.wcnf S = OPT
O = 275
T = 163.73		 S = OPT
O = 275
T = 163.73
p_hat300-3.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
p_hat500-1.clq.wcnf S = OPT
O = 491
T = 141.51		 S = OPT
O = 491
T = 141.51
p_hat500-2.clq.wcnf S = OPT
O = 464
T = 351.92		 S = OPT
O = 464
T = 351.92
p_hat500-3.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
p_hat700-1.clq.wcnf S = OPT
O = 689
T = 1003.56		 S = OPT
O = 689
T = 1003.56
p_hat700-2.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
p_hat700-3.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
san1000.clq.wcnf S = OPT
O = 985
T = 129.71		 S = OPT
O = 985
T = 129.71
san200_0.7_1.clq.wcnf S = OPT
O = 170
T = 9.86		 S = OPT
O = 170
T = 9.86
san200_0.7_2.clq.wcnf S = OPT
O = 182
T = 12.52		 S = OPT
O = 182
T = 12.52
san200_0.9_1.clq.wcnf S = OPT
O = 130
T = 9.79		 S = OPT
O = 130
T = 9.79
san200_0.9_2.clq.wcnf S = OPT
O = 140
T = 9.95		 S = OPT
O = 140
T = 9.95
san200_0.9_3.clq.wcnf S = OPT
O = 156
T = 34.89		 S = OPT
O = 156
T = 34.89
san400_0.5_1.clq.wcnf S = OPT
O = 387
T = 16.46		 S = OPT
O = 387
T = 16.46
san400_0.7_1.clq.wcnf S = OPT
O = 360
T = 10.25		 S = OPT
O = 360
T = 10.25
san400_0.7_2.clq.wcnf S = OPT
O = 370
T = 10.75		 S = OPT
O = 370
T = 10.75
san400_0.7_3.clq.wcnf S = OPT
O = 378
T = 10.81		 S = OPT
O = 378
T = 10.81
san400_0.9_1.clq.wcnf S = OPT
O = 300
T = 10.30		 S = OPT
O = 300
T = 10.30
sanr200_0.7.clq.wcnf S = OPT
O = 182
T = 25.27		 S = OPT
O = 182
T = 25.27
sanr200_0.9.clq.wcnf S = OPT
O = 158
T = 92.75		 S = OPT
O = 158
T = 92.75
sanr400_0.5.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
sanr400_0.7.clq.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
cnf3.150.250.832706.cnf.wcnf S = OPT
O = 15
T = 9.73		 S = OPT
O = 15
T = 9.73
cnf3.150.250.832707.cnf.wcnf S = OPT
O = 18
T = 9.76		 S = OPT
O = 18
T = 9.76
cnf3.150.250.832708.cnf.wcnf S = OPT
O = 20
T = 9.91		 S = OPT
O = 20
T = 9.91
cnf3.150.250.832709.cnf.wcnf S = OPT
O = 24
T = 9.78		 S = OPT
O = 24
T = 9.78
cnf3.150.250.832710.cnf.wcnf S = OPT
O = 24
T = 9.78		 S = OPT
O = 24
T = 9.78
cnf3.150.250.832711.cnf.wcnf S = OPT
O = 20
T = 9.78		 S = OPT
O = 20
T = 9.78
cnf3.150.250.832712.cnf.wcnf S = OPT
O = 23
T = 9.82		 S = OPT
O = 23
T = 9.82
cnf3.150.250.832713.cnf.wcnf S = OPT
O = 16
T = 9.86		 S = OPT
O = 16
T = 9.86
cnf3.150.250.832714.cnf.wcnf S = OPT
O = 23
T = 9.77		 S = OPT
O = 23
T = 9.77
cnf3.150.250.832715.cnf.wcnf S = OPT
O = 24
T = 9.81		 S = OPT
O = 24
T = 9.81
cnf3.150.300.195561.cnf.wcnf S = OPT
O = 22
T = 9.85		 S = OPT
O = 22
T = 9.85
cnf3.150.300.195562.cnf.wcnf S = OPT
O = 22
T = 9.78		 S = OPT
O = 22
T = 9.78
cnf3.150.300.195563.cnf.wcnf S = OPT
O = 20
T = 9.79		 S = OPT
O = 20
T = 9.79
cnf3.150.300.195564.cnf.wcnf S = OPT
O = 26
T = 9.80		 S = OPT
O = 26
T = 9.80
cnf3.150.300.195565.cnf.wcnf S = OPT
O = 27
T = 9.76		 S = OPT
O = 27
T = 9.76
cnf3.150.300.195566.cnf.wcnf S = OPT
O = 21
T = 9.80		 S = OPT
O = 21
T = 9.80
cnf3.150.300.195567.cnf.wcnf S = OPT
O = 26
T = 9.80		 S = OPT
O = 26
T = 9.80
cnf3.150.300.195568.cnf.wcnf S = OPT
O = 25
T = 9.81		 S = OPT
O = 25
T = 9.81
cnf3.150.300.195569.cnf.wcnf S = OPT
O = 27
T = 9.84		 S = OPT
O = 27
T = 9.84
cnf3.150.300.195570.cnf.wcnf S = OPT
O = 20
T = 9.74		 S = OPT
O = 20
T = 9.74
cnf3.150.350.558416.cnf.wcnf S = OPT
O = 32
T = 9.84		 S = OPT
O = 32
T = 9.84
cnf3.150.350.558417.cnf.wcnf S = OPT
O = 30
T = 9.89		 S = OPT
O = 30
T = 9.89
cnf3.150.350.558418.cnf.wcnf S = OPT
O = 29
T = 9.80		 S = OPT
O = 29
T = 9.80
cnf3.150.350.558419.cnf.wcnf S = OPT
O = 29
T = 9.83		 S = OPT
O = 29
T = 9.83
cnf3.150.350.558420.cnf.wcnf S = OPT
O = 32
T = 9.77		 S = OPT
O = 32
T = 9.77
cnf3.150.350.558421.cnf.wcnf S = OPT
O = 30
T = 9.79		 S = OPT
O = 30
T = 9.79
cnf3.150.350.558422.cnf.wcnf S = OPT
O = 30
T = 9.80		 S = OPT
O = 30
T = 9.80
cnf3.150.350.558423.cnf.wcnf S = OPT
O = 26
T = 9.79		 S = OPT
O = 26
T = 9.79
cnf3.150.350.558424.cnf.wcnf S = OPT
O = 24
T = 9.76		 S = OPT
O = 24
T = 9.76
cnf3.150.350.558425.cnf.wcnf S = OPT
O = 27
T = 9.76		 S = OPT
O = 27
T = 9.76
cnf3.150.400.921271.cnf.wcnf S = OPT
O = 38
T = 9.79		 S = OPT
O = 38
T = 9.79
cnf3.150.400.921272.cnf.wcnf S = OPT
O = 33
T = 9.86		 S = OPT
O = 33
T = 9.86
cnf3.150.400.921273.cnf.wcnf S = OPT
O = 31
T = 9.95		 S = OPT
O = 31
T = 9.95
cnf3.150.400.921274.cnf.wcnf S = OPT
O = 34
T = 9.83		 S = OPT
O = 34
T = 9.83
cnf3.150.400.921275.cnf.wcnf S = OPT
O = 37
T = 9.73		 S = OPT
O = 37
T = 9.73
cnf3.150.400.921276.cnf.wcnf S = OPT
O = 34
T = 9.75		 S = OPT
O = 34
T = 9.75
cnf3.150.400.921277.cnf.wcnf S = OPT
O = 33
T = 9.77		 S = OPT
O = 33
T = 9.77
cnf3.150.400.921278.cnf.wcnf S = OPT
O = 31
T = 9.88		 S = OPT
O = 31
T = 9.88
cnf3.150.400.921279.cnf.wcnf S = OPT
O = 28
T = 9.73		 S = OPT
O = 28
T = 9.73
cnf3.150.400.921280.cnf.wcnf S = OPT
O = 30
T = 9.74		 S = OPT
O = 30
T = 9.74
cnf3.150.450.284126.cnf.wcnf S = OPT
O = 43
T = 9.90		 S = OPT
O = 43
T = 9.90
cnf3.150.450.284127.cnf.wcnf S = OPT
O = 34
T = 9.88		 S = OPT
O = 34
T = 9.88
cnf3.150.450.284128.cnf.wcnf S = OPT
O = 34
T = 9.86		 S = OPT
O = 34
T = 9.86
cnf3.150.450.284129.cnf.wcnf S = OPT
O = 33
T = 9.81		 S = OPT
O = 33
T = 9.81
cnf3.150.450.284130.cnf.wcnf S = OPT
O = 36
T = 9.86		 S = OPT
O = 36
T = 9.86
cnf3.150.450.284131.cnf.wcnf S = OPT
O = 31
T = 9.41		 S = OPT
O = 31
T = 9.41
cnf3.150.450.284132.cnf.wcnf S = OPT
O = 31
T = 9.92		 S = OPT
O = 31
T = 9.92
cnf3.150.450.284133.cnf.wcnf S = OPT
O = 39
T = 9.91		 S = OPT
O = 39
T = 9.91
cnf3.150.450.284134.cnf.wcnf S = OPT
O = 39
T = 10.14		 S = OPT
O = 39
T = 10.14
cnf3.150.450.284135.cnf.wcnf S = OPT
O = 35
T = 9.89		 S = OPT
O = 35
T = 9.89
cnf3.150.500.646981.cnf.wcnf S = OPT
O = 47
T = 11.54		 S = OPT
O = 47
T = 11.54
cnf3.150.500.646982.cnf.wcnf S = OPT
O = 46
T = 10.50		 S = OPT
O = 46
T = 10.50
cnf3.150.500.646983.cnf.wcnf S = OPT
O = 47
T = 11.09		 S = OPT
O = 47
T = 11.09
cnf3.150.500.646984.cnf.wcnf S = OPT
O = 42
T = 9.80		 S = OPT
O = 42
T = 9.80
cnf3.150.500.646985.cnf.wcnf S = OPT
O = 53
T = 11.21		 S = OPT
O = 53
T = 11.21
cnf3.150.500.646986.cnf.wcnf S = OPT
O = 47
T = 10.23		 S = OPT
O = 47
T = 10.23
cnf3.150.500.646987.cnf.wcnf S = OPT
O = 43
T = 10.12		 S = OPT
O = 43
T = 10.12
cnf3.150.500.646988.cnf.wcnf S = OPT
O = 41
T = 10.08		 S = OPT
O = 41
T = 10.08
cnf3.150.500.646989.cnf.wcnf S = OPT
O = 49
T = 10.34		 S = OPT
O = 49
T = 10.34
cnf3.150.500.646990.cnf.wcnf S = OPT
O = 44
T = 10.03		 S = OPT
O = 44
T = 10.03
cnf3.150.550.009836.cnf.wcnf S = OPT
O = 54
T = 11.93		 S = OPT
O = 54
T = 11.93
cnf3.150.550.009837.cnf.wcnf S = OPT
O = 52
T = 11.19		 S = OPT
O = 52
T = 11.19
cnf3.150.550.009838.cnf.wcnf S = OPT
O = 45
T = 10.18		 S = OPT
O = 45
T = 10.18
cnf3.150.550.009839.cnf.wcnf S = OPT
O = 39
T = 9.81		 S = OPT
O = 39
T = 9.81
cnf3.150.550.009840.cnf.wcnf S = OPT
O = 52
T = 11.93		 S = OPT
O = 52
T = 11.93
cnf3.150.550.009841.cnf.wcnf S = OPT
O = 57
T = 11.89		 S = OPT
O = 57
T = 11.89
cnf3.150.550.009842.cnf.wcnf S = OPT
O = 45
T = 10.36		 S = OPT
O = 45
T = 10.36
cnf3.150.550.009843.cnf.wcnf S = OPT
O = 40
T = 9.94		 S = OPT
O = 40
T = 9.94
cnf3.150.550.009844.cnf.wcnf S = OPT
O = 47
T = 10.79		 S = OPT
O = 47
T = 10.79
cnf3.150.550.009845.cnf.wcnf S = OPT
O = 50
T = 10.34		 S = OPT
O = 50
T = 10.34
cnf3.150.600.372691.cnf.wcnf S = OPT
O = 63
T = 10.12		 S = OPT
O = 63
T = 10.12
cnf3.150.600.372692.cnf.wcnf S = OPT
O = 49
T = 11.43		 S = OPT
O = 49
T = 11.43
cnf3.150.600.372693.cnf.wcnf S = OPT
O = 69
T = 9.97		 S = OPT
O = 69
T = 9.97
cnf3.150.600.372694.cnf.wcnf S = OPT
O = 62
T = 9.66		 S = OPT
O = 62
T = 9.66
cnf3.150.600.372695.cnf.wcnf S = OPT
O = 53
T = 10.26		 S = OPT
O = 53
T = 10.26
cnf3.150.600.372696.cnf.wcnf S = OPT
O = 53
T = 10.51		 S = OPT
O = 53
T = 10.51
cnf3.150.600.372697.cnf.wcnf S = OPT
O = 46
T = 11.00		 S = OPT
O = 46
T = 11.00
cnf3.150.600.372698.cnf.wcnf S = OPT
O = 57
T = 10.58		 S = OPT
O = 57
T = 10.58
cnf3.150.600.372699.cnf.wcnf S = OPT
O = 65
T = 9.91		 S = OPT
O = 65
T = 9.91
cnf3.150.600.372700.cnf.wcnf S = OPT
O = 60
T = 10.28		 S = OPT
O = 60
T = 10.28
3col100_5_1.shuffled.cnf.wcnf S = OPT
O = 100
T = 9.82		 S = OPT
O = 100
T = 9.82
3col100_5_10.shuffled.cnf.wcnf S = OPT
O = 94
T = 9.93		 S = OPT
O = 94
T = 9.93
3col100_5_2.shuffled.cnf.wcnf S = OPT
O = 104
T = 9.83		 S = OPT
O = 104
T = 9.83
3col100_5_3.shuffled.cnf.wcnf S = OPT
O = 92
T = 9.81		 S = OPT
O = 92
T = 9.81
3col100_5_4.shuffled.cnf.wcnf S = OPT
O = 97
T = 9.89		 S = OPT
O = 97
T = 9.89
3col100_5_5.shuffled.cnf.wcnf S = OPT
O = 86
T = 9.91		 S = OPT
O = 86
T = 9.91
3col100_5_6.shuffled.cnf.wcnf S = OPT
O = 90
T = 9.48		 S = OPT
O = 90
T = 9.48
3col100_5_7.shuffled.cnf.wcnf S = OPT
O = 85
T = 9.81		 S = OPT
O = 85
T = 9.81
3col100_5_8.shuffled.cnf.wcnf S = OPT
O = 94
T = 9.80		 S = OPT
O = 94
T = 9.80
3col100_5_9.shuffled.cnf.wcnf S = OPT
O = 94
T = 9.84		 S = OPT
O = 94
T = 9.84
3col120_5_1.shuffled.cnf.wcnf S = OPT
O = 123
T = 10.96		 S = OPT
O = 123
T = 10.96
3col120_5_10.shuffled.cnf.wcnf S = OPT
O = 125
T = 10.61		 S = OPT
O = 125
T = 10.61
3col120_5_2.shuffled.cnf.wcnf S = OPT
O = 124
T = 10.67		 S = OPT
O = 124
T = 10.67
3col120_5_3.shuffled.cnf.wcnf S = OPT
O = 119
T = 10.54		 S = OPT
O = 119
T = 10.54
3col120_5_4.shuffled.cnf.wcnf S = OPT
O = 122
T = 10.70		 S = OPT
O = 122
T = 10.70
3col120_5_5.shuffled.cnf.wcnf S = OPT
O = 112
T = 10.58		 S = OPT
O = 112
T = 10.58
3col120_5_6.shuffled.cnf.wcnf S = OPT
O = 121
T = 10.54		 S = OPT
O = 121
T = 10.54
3col120_5_7.shuffled.cnf.wcnf S = OPT
O = 120
T = 10.66		 S = OPT
O = 120
T = 10.66
3col120_5_8.shuffled.cnf.wcnf S = OPT
O = 110
T = 11.14		 S = OPT
O = 110
T = 11.14
3col120_5_9.shuffled.cnf.wcnf S = OPT
O = 117
T = 10.57		 S = OPT
O = 117
T = 10.57
3col140_5_1.shuffled.cnf.wcnf S = OPT
O = 121
T = 11.57		 S = OPT
O = 121
T = 11.57
3col140_5_10.shuffled.cnf.wcnf S = OPT
O = 122
T = 11.64		 S = OPT
O = 122
T = 11.64
3col140_5_2.shuffled.cnf.wcnf S = OPT
O = 131
T = 12.03		 S = OPT
O = 131
T = 12.03
3col140_5_3.shuffled.cnf.wcnf S = OPT
O = 128
T = 12.71		 S = OPT
O = 128
T = 12.71
3col140_5_4.shuffled.cnf.wcnf S = OPT
O = 128
T = 12.25		 S = OPT
O = 128
T = 12.25
3col140_5_5.shuffled.cnf.wcnf S = OPT
O = 124
T = 11.66		 S = OPT
O = 124
T = 11.66
3col140_5_6.shuffled.cnf.wcnf S = OPT
O = 120
T = 11.55		 S = OPT
O = 120
T = 11.55
3col140_5_7.shuffled.cnf.wcnf S = OPT
O = 119
T = 11.59		 S = OPT
O = 119
T = 11.59
3col140_5_8.shuffled.cnf.wcnf S = OPT
O = 123
T = 11.33		 S = OPT
O = 123
T = 11.33
3col140_5_9.shuffled.cnf.wcnf S = OPT
O = 134
T = 12.42		 S = OPT
O = 134
T = 12.42
3col80_5_1.shuffled.cnf.wcnf S = OPT
O = 79
T = 9.81		 S = OPT
O = 79
T = 9.81
3col80_5_10.shuffled.cnf.wcnf S = OPT
O = 75
T = 9.74		 S = OPT
O = 75
T = 9.74
3col80_5_2.shuffled.cnf.wcnf S = OPT
O = 71
T = 9.38		 S = OPT
O = 71
T = 9.38
3col80_5_3.shuffled.cnf.wcnf S = OPT
O = 88
T = 9.77		 S = OPT
O = 88
T = 9.77
3col80_5_4.shuffled.cnf.wcnf S = OPT
O = 73
T = 9.76		 S = OPT
O = 73
T = 9.76
3col80_5_5.shuffled.cnf.wcnf S = OPT
O = 78
T = 9.84		 S = OPT
O = 78
T = 9.84
3col80_5_6.shuffled.cnf.wcnf S = OPT
O = 76
T = 9.75		 S = OPT
O = 76
T = 9.75
3col80_5_7.shuffled.cnf.wcnf S = OPT
O = 80
T = 9.80		 S = OPT
O = 80
T = 9.80
3col80_5_8.shuffled.cnf.wcnf S = OPT
O = 82
T = 9.74		 S = OPT
O = 82
T = 9.74
3col80_5_9.shuffled.cnf.wcnf S = OPT
O = 79
T = 9.73		 S = OPT
O = 79
T = 9.73
cnt05.shuffled.cnf.wcnf S = OPT
O = 174
T = 9.79		 S = OPT
O = 174
T = 9.79
cnt06.shuffled.cnf.wcnf S = OPT
O = 365
T = 11.08		 S = OPT
O = 365
T = 11.08
cnt07.shuffled.cnf.wcnf S = OPT
O = 877
T = 10.74		 S = OPT
O = 877
T = 10.74
dp02s02.shuffled.cnf.wcnf S = OPT
O = 100
T = 9.77		 S = OPT
O = 100
T = 9.77
dp03s03.shuffled.cnf.wcnf S = OPT
O = 254
T = 10.71		 S = OPT
O = 254
T = 10.71
dp04s04.shuffled.cnf.wcnf S = OPT
O = 533
T = 9.86		 S = OPT
O = 533
T = 9.86
dp05s05.shuffled.cnf.wcnf S = OPT
O = 765
T = 10.00		 S = OPT
O = 765
T = 10.00
dp06s06.shuffled.cnf.wcnf S = OPT
O = 1164
T = 12.47		 S = OPT
O = 1164
T = 12.47
dp07s07.shuffled.cnf.wcnf S = OPT
O = 1563
T = 24.00		 S = OPT
O = 1563
T = 24.00
ezfact32_1.shuffled.cnf.wcnf S = OPT
O = 400
T = 9.77		 S = OPT
O = 400
T = 9.77
ezfact32_10.shuffled.cnf.wcnf S = OPT
O = 389
T = 9.87		 S = OPT
O = 389
T = 9.87
ezfact32_2.shuffled.cnf.wcnf S = OPT
O = 364
T = 9.72		 S = OPT
O = 364
T = 9.72
ezfact32_3.shuffled.cnf.wcnf S = OPT
O = 397
T = 9.75		 S = OPT
O = 397
T = 9.75
ezfact32_4.shuffled.cnf.wcnf S = OPT
O = 379
T = 9.75		 S = OPT
O = 379
T = 9.75
ezfact32_5.shuffled.cnf.wcnf S = OPT
O = 394
T = 9.84		 S = OPT
O = 394
T = 9.84
ezfact32_6.shuffled.cnf.wcnf S = OPT
O = 382
T = 9.76		 S = OPT
O = 382
T = 9.76
ezfact32_7.shuffled.cnf.wcnf S = OPT
O = 394
T = 10.04		 S = OPT
O = 394
T = 10.04
ezfact32_8.shuffled.cnf.wcnf S = OPT
O = 392
T = 9.78		 S = OPT
O = 392
T = 9.78
ezfact32_9.shuffled.cnf.wcnf S = OPT
O = 382
T = 9.71		 S = OPT
O = 382
T = 9.71
med11.shuffled.cnf.wcnf S = OPT
O = 164
T = 9.83		 S = OPT
O = 164
T = 9.83
kbtree9_7_3_5_30_1.wcsp.wcnf S = OPT
O = 9
T = 18.07		 S = OPT
O = 9
T = 18.07
kbtree9_7_3_5_30_2.wcsp.wcnf S = OPT
O = 7
T = 11.15		 S = OPT
O = 7
T = 11.15
kbtree9_7_3_5_30_3.wcsp.wcnf S = OPT
O = 9
T = 13.46		 S = OPT
O = 9
T = 13.46
kbtree9_7_3_5_30_4.wcsp.wcnf S = OPT
O = 6
T = 11.19		 S = OPT
O = 6
T = 11.19
kbtree9_7_3_5_30_5.wcsp.wcnf S = OPT
O = 6
T = 10.89		 S = OPT
O = 6
T = 10.89
kbtree9_7_3_5_30_6.wcsp.wcnf S = OPT
O = 9
T = 23.87		 S = OPT
O = 9
T = 23.87
kbtree9_7_3_5_40_1.wcsp.wcnf S = OPT
O = 27
T = 46.00		 S = OPT
O = 27
T = 46.00
kbtree9_7_3_5_40_2.wcsp.wcnf S = OPT
O = 26
T = 41.33		 S = OPT
O = 26
T = 41.33
kbtree9_7_3_5_40_3.wcsp.wcnf S = OPT
O = 22
T = 38.44		 S = OPT
O = 22
T = 38.44
kbtree9_7_3_5_40_4.wcsp.wcnf S = OPT
O = 22
T = 29.68		 S = OPT
O = 22
T = 29.68
kbtree9_7_3_5_40_5.wcsp.wcnf S = OPT
O = 23
T = 29.72		 S = OPT
O = 23
T = 29.72
kbtree9_7_3_5_40_6.wcsp.wcnf S = OPT
O = 26
T = 34.64		 S = OPT
O = 26
T = 34.64
kbtree9_7_3_5_50_1.wcsp.wcnf S = OPT
O = 36
T = 62.33		 S = OPT
O = 36
T = 62.33
kbtree9_7_3_5_50_2.wcsp.wcnf S = OPT
O = 37
T = 74.43		 S = OPT
O = 37
T = 74.43
kbtree9_7_3_5_50_3.wcsp.wcnf S = OPT
O = 37
T = 48.05		 S = OPT
O = 37
T = 48.05
kbtree9_7_3_5_50_4.wcsp.wcnf S = OPT
O = 38
T = 49.38		 S = OPT
O = 38
T = 49.38
kbtree9_7_3_5_50_5.wcsp.wcnf S = OPT
O = 37
T = 47.26		 S = OPT
O = 37
T = 47.26
kbtree9_7_3_5_50_6.wcsp.wcnf S = OPT
O = 38
T = 67.11		 S = OPT
O = 38
T = 67.11
kbtree9_7_3_5_60_1.wcsp.wcnf S = OPT
O = 54
T = 24.47		 S = OPT
O = 54
T = 24.47
kbtree9_7_3_5_60_2.wcsp.wcnf S = OPT
O = 59
T = 72.28		 S = OPT
O = 59
T = 72.28
kbtree9_7_3_5_60_3.wcsp.wcnf S = OPT
O = 59
T = 83.26		 S = OPT
O = 59
T = 83.26
kbtree9_7_3_5_60_4.wcsp.wcnf S = OPT
O = 59
T = 69.63		 S = OPT
O = 59
T = 69.63
kbtree9_7_3_5_60_5.wcsp.wcnf S = OPT
O = 56
T = 73.75		 S = OPT
O = 56
T = 73.75
kbtree9_7_3_5_60_6.wcsp.wcnf S = OPT
O = 57
T = 68.63		 S = OPT
O = 57
T = 68.63
kbtree9_7_3_5_70_1.wcsp.wcnf S = OPT
O = 74
T = 24.08		 S = OPT
O = 74
T = 24.08
kbtree9_7_3_5_70_2.wcsp.wcnf S = OPT
O = 72
T = 68.84		 S = OPT
O = 72
T = 68.84
kbtree9_7_3_5_70_3.wcsp.wcnf S = OPT
O = 74
T = 57.06		 S = OPT
O = 74
T = 57.06
kbtree9_7_3_5_70_4.wcsp.wcnf S = OPT
O = 73
T = 51.38		 S = OPT
O = 73
T = 51.38
kbtree9_7_3_5_70_5.wcsp.wcnf S = OPT
O = 72
T = 57.44		 S = OPT
O = 72
T = 57.44
kbtree9_7_3_5_70_6.wcsp.wcnf S = OPT
O = 74
T = 88.37		 S = OPT
O = 74
T = 88.37
kbtree9_7_3_5_80_1.wcsp.wcnf S = OPT
O = 96
T = 24.05		 S = OPT
O = 96
T = 24.05
kbtree9_7_3_5_80_2.wcsp.wcnf S = OPT
O = 103
T = 61.75		 S = OPT
O = 103
T = 61.75
kbtree9_7_3_5_80_3.wcsp.wcnf S = OPT
O = 102
T = 21.34		 S = OPT
O = 102
T = 21.34
kbtree9_7_3_5_80_4.wcsp.wcnf S = OPT
O = 100
T = 20.88		 S = OPT
O = 100
T = 20.88
kbtree9_7_3_5_80_5.wcsp.wcnf S = OPT
O = 104
T = 45.34		 S = OPT
O = 104
T = 45.34
kbtree9_7_3_5_80_6.wcsp.wcnf S = OPT
O = 104
T = 58.12		 S = OPT
O = 104
T = 58.12
kbtree9_7_3_5_90_1.wcsp.wcnf S = OPT
O = 124
T = 18.88		 S = OPT
O = 124
T = 18.88
kbtree9_7_3_5_90_2.wcsp.wcnf S = OPT
O = 125
T = 18.43		 S = OPT
O = 125
T = 18.43
kbtree9_7_3_5_90_3.wcsp.wcnf S = OPT
O = 121
T = 14.07		 S = OPT
O = 121
T = 14.07
kbtree9_7_3_5_90_4.wcsp.wcnf S = OPT
O = 126
T = 17.84		 S = OPT
O = 126
T = 17.84
kbtree9_7_3_5_90_5.wcsp.wcnf S = OPT
O = 124
T = 40.40		 S = OPT
O = 124
T = 40.40
kbtree9_7_3_5_90_6.wcsp.wcnf S = OPT
O = 128
T = 45.02		 S = OPT
O = 128
T = 45.02
normalized-mps-v2-20-10-stein15.opb.msat.wcnf S = OPT
O = 9
T = 9.74		 S = OPT
O = 9
T = 9.74
normalized-mps-v2-20-10-stein27.opb.msat.wcnf S = OPT
O = 18
T = 9.90		 S = OPT
O = 18
T = 9.90
normalized-mps-v2-20-10-stein45.opb.msat.wcnf S = OPT
O = 30
T = 25.37		 S = OPT
O = 30
T = 25.37
normalized-mps-v2-20-10-stein9.opb.msat.wcnf S = OPT
O = 5
T = 9.77		 S = OPT
O = 5
T = 9.77
rev44-10.wcnf S = OPT
O = 5
T = 10.37		 S = OPT
O = 5
T = 10.37
rev44-12.wcnf S = OPT
O = 2
T = 10.45		 S = OPT
O = 2
T = 10.45
rev44-14.wcnf S = OPT
O = 0
T = 9.82		 S = OPT
O = 0
T = 9.82
rev44-16.wcnf S = OPT
O = 0
T = 9.91		 S = OPT
O = 0
T = 9.91
rev44-18.wcnf S = OPT
O = 0
T = 9.83		 S = OPT
O = 0
T = 9.83
rev44-2.wcnf S = OPT
O = 16
T = 9.91		 S = OPT
O = 16
T = 9.91
rev44-20.wcnf S = OPT
O = 0
T = 9.88		 S = OPT
O = 0
T = 9.88
rev44-22.wcnf S = OPT
O = 0
T = 9.92		 S = OPT
O = 0
T = 9.92
rev44-24.wcnf S = OPT
O = 0
T = 9.99		 S = OPT
O = 0
T = 9.99
rev44-4.wcnf S = OPT
O = 14
T = 9.73		 S = OPT
O = 14
T = 9.73
rev44-6.wcnf S = OPT
O = 11
T = 9.83		 S = OPT
O = 11
T = 9.83
rev44-8.wcnf S = OPT
O = 8
T = 10.06		 S = OPT
O = 8
T = 10.06
rev66-10.wcnf S = OPT
O = 23
T = 128.19		 S = OPT
O = 23
T = 128.19
rev66-12.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rev66-14.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rev66-16.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rev66-18.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rev66-2.wcnf S = OPT
O = 36
T = 9.79		 S = OPT
O = 36
T = 9.79
rev66-20.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rev66-22.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rev66-24.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rev66-26.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rev66-28.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rev66-30.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rev66-32.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rev66-34.wcnf S = OPT
O = 0
T = 14.84		 S = OPT
O = 0
T = 14.84
rev66-36.wcnf S = OPT
O = 0
T = 16.14		 S = OPT
O = 0
T = 16.14
rev66-38.wcnf S = OPT
O = 0
T = 12.66		 S = OPT
O = 0
T = 12.66
rev66-4.wcnf S = OPT
O = 34
T = 9.86		 S = OPT
O = 34
T = 9.86
rev66-40.wcnf S = OPT
O = 0
T = 15.14		 S = OPT
O = 0
T = 15.14
rev66-42.wcnf S = OPT
O = 0
T = 11.72		 S = OPT
O = 0
T = 11.72
rev66-44.wcnf S = OPT
O = 0
T = 15.04		 S = OPT
O = 0
T = 15.04
rev66-46.wcnf S = OPT
O = 0
T = 23.73		 S = OPT
O = 0
T = 23.73
rev66-48.wcnf S = OPT
O = 0
T = 18.93		 S = OPT
O = 0
T = 18.93
rev66-50.wcnf S = OPT
O = 0
T = 18.62		 S = OPT
O = 0
T = 18.62
rev66-52.wcnf S = OPT
O = 0
T = 19.13		 S = OPT
O = 0
T = 19.13
rev66-54.wcnf S = OPT
O = 0
T = 17.76		 S = OPT
O = 0
T = 17.76
rev66-56.wcnf S = OPT
O = 0
T = 18.82		 S = OPT
O = 0
T = 18.82
rev66-58.wcnf S = OPT
O = 0
T = 11.37		 S = OPT
O = 0
T = 11.37
rev66-6.wcnf S = OPT
O = 32
T = 10.72		 S = OPT
O = 32
T = 10.72
rev66-60.wcnf S = OPT
O = 0
T = 27.47		 S = OPT
O = 0
T = 27.47
rev66-62.wcnf S = OPT
O = 0
T = 24.30		 S = OPT
O = 0
T = 24.30
rev66-64.wcnf S = OPT
O = 0
T = 27.02		 S = OPT
O = 0
T = 27.02
rev66-8.wcnf S = OPT
O = 30
T = 38.12		 S = OPT
O = 30
T = 38.12
cnf_10.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
cnf_10_center.wcnf S = OPT
O = 159
T = 318.81		 S = OPT
O = 159
T = 318.81
cnf_12.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
cnf_12_center.wcnf S = OPT
O = 237
T = 110.18		 S = OPT
O = 237
T = 110.18
cnf_small.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO