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
clq1-cv160c800l2g1.wcnf S = OPT
O = 61
T = 107.34		 S = OPT
O = 61
T = 107.34
clq1-cv160c800l2g10.wcnf S = OPT
O = 53
T = 59.22		 S = OPT
O = 53
T = 59.22
clq1-cv160c800l2g11.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
clq1-cv160c800l2g12.wcnf S = OPT
O = 59
T = 110.91		 S = OPT
O = 59
T = 110.91
clq1-cv160c800l2g13.wcnf S = OPT
O = 51
T = 15.87		 S = OPT
O = 51
T = 15.87
clq1-cv160c800l2g14.wcnf S = OPT
O = 45
T = 11.51		 S = OPT
O = 45
T = 11.51
clq1-cv160c800l2g15.wcnf S = OPT
O = 62
T = 238.36		 S = OPT
O = 62
T = 238.36
clq1-cv160c800l2g16.wcnf S = OPT
O = 56
T = 39.99		 S = OPT
O = 56
T = 39.99
clq1-cv160c800l2g17.wcnf S = OPT
O = 59
T = 130.75		 S = OPT
O = 59
T = 130.75
clq1-cv160c800l2g18.wcnf S = OPT
O = 55
T = 37.98		 S = OPT
O = 55
T = 37.98
clq1-cv160c800l2g19.wcnf S = OPT
O = 68
T = 499.33		 S = OPT
O = 68
T = 499.33
clq1-cv160c800l2g2.wcnf S = OPT
O = 48
T = 12.33		 S = OPT
O = 48
T = 12.33
clq1-cv160c800l2g20.wcnf S = OPT
O = 46
T = 12.51		 S = OPT
O = 46
T = 12.51
clq1-cv160c800l2g21.wcnf S = OPT
O = 56
T = 45.29		 S = OPT
O = 56
T = 45.29
clq1-cv160c800l2g22.wcnf S = OPT
O = 56
T = 46.52		 S = OPT
O = 56
T = 46.52
clq1-cv160c800l2g23.wcnf S = OPT
O = 51
T = 12.91		 S = OPT
O = 51
T = 12.91
clq1-cv160c800l2g24.wcnf S = OPT
O = 49
T = 13.15		 S = OPT
O = 49
T = 13.15
clq1-cv160c800l2g25.wcnf S = OPT
O = 55
T = 75.91		 S = OPT
O = 55
T = 75.91
clq1-cv160c800l2g26.wcnf S = OPT
O = 53
T = 73.75		 S = OPT
O = 53
T = 73.75
clq1-cv160c800l2g27.wcnf S = OPT
O = 56
T = 72.15		 S = OPT
O = 56
T = 72.15
clq1-cv160c800l2g28.wcnf S = OPT
O = 50
T = 24.06		 S = OPT
O = 50
T = 24.06
clq1-cv160c800l2g29.wcnf S = OPT
O = 42
T = 11.43		 S = OPT
O = 42
T = 11.43
clq1-cv160c800l2g3.wcnf S = OPT
O = 60
T = 124.29		 S = OPT
O = 60
T = 124.29
clq1-cv160c800l2g30.wcnf S = OPT
O = 60
T = 24.86		 S = OPT
O = 60
T = 24.86
clq1-cv160c800l2g4.wcnf S = OPT
O = 49
T = 28.00		 S = OPT
O = 49
T = 28.00
clq1-cv160c800l2g5.wcnf S = OPT
O = 49
T = 21.25		 S = OPT
O = 49
T = 21.25
clq1-cv160c800l2g6.wcnf S = OPT
O = 62
T = 103.45		 S = OPT
O = 62
T = 103.45
clq1-cv160c800l2g7.wcnf S = OPT
O = 61
T = 302.03		 S = OPT
O = 61
T = 302.03
clq1-cv160c800l2g8.wcnf S = OPT
O = 49
T = 15.86		 S = OPT
O = 49
T = 15.86
clq1-cv160c800l2g9.wcnf S = OPT
O = 57
T = 118.04		 S = OPT
O = 57
T = 118.04
clq1-cv260c1040l2g1.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
clq1-cv260c1040l2g10.wcnf S = OPT
O = 61
T = 1359.42		 S = OPT
O = 61
T = 1359.42
clq1-cv260c1040l2g11.wcnf S = OPT
O = 40
T = 15.97		 S = OPT
O = 40
T = 15.97
clq1-cv260c1040l2g12.wcnf S = OPT
O = 58
T = 304.10		 S = OPT
O = 58
T = 304.10
clq1-cv260c1040l2g13.wcnf S = OPT
O = 38
T = 14.39		 S = OPT
O = 38
T = 14.39
clq1-cv260c1040l2g14.wcnf S = OPT
O = 57
T = 117.32		 S = OPT
O = 57
T = 117.32
clq1-cv260c1040l2g15.wcnf S = OPT
O = 46
T = 49.68		 S = OPT
O = 46
T = 49.68
clq1-cv260c1040l2g16.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = 59
T = TO
clq1-cv260c1040l2g17.wcnf S = OPT
O = 51
T = 207.06		 S = OPT
O = 51
T = 207.06
clq1-cv260c1040l2g18.wcnf S = OPT
O = 52
T = 28.28		 S = OPT
O = 52
T = 28.28
clq1-cv260c1040l2g19.wcnf S = OPT
O = 57
T = 99.47		 S = OPT
O = 57
T = 99.47
clq1-cv260c1040l2g2.wcnf S = OPT
O = 54
T = 23.18		 S = OPT
O = 54
T = 23.18
clq1-cv260c1040l2g20.wcnf S = OPT
O = 63
T = 1119.53		 S = OPT
O = 63
T = 1119.53
clq1-cv260c1040l2g21.wcnf S = OPT
O = 55
T = 54.64		 S = OPT
O = 55
T = 54.64
clq1-cv260c1040l2g22.wcnf S = OPT
O = 58
T = 204.68		 S = OPT
O = 58
T = 204.68
clq1-cv260c1040l2g23.wcnf S = OPT
O = 52
T = 30.32		 S = OPT
O = 52
T = 30.32
clq1-cv260c1040l2g24.wcnf S = OPT
O = 42
T = 12.46		 S = OPT
O = 42
T = 12.46
clq1-cv260c1040l2g25.wcnf S = OPT
O = 46
T = 16.92		 S = OPT
O = 46
T = 16.92
clq1-cv260c1040l2g26.wcnf S = OPT
O = 50
T = 141.20		 S = OPT
O = 50
T = 141.20
clq1-cv260c1040l2g27.wcnf S = OPT
O = 69
T = 1111.51		 S = OPT
O = 69
T = 1111.51
clq1-cv260c1040l2g28.wcnf S = OPT
O = 58
T = 203.29		 S = OPT
O = 58
T = 203.29
clq1-cv260c1040l2g29.wcnf S = OPT
O = 54
T = 106.85		 S = OPT
O = 54
T = 106.85
clq1-cv260c1040l2g3.wcnf S = OPT
O = 52
T = 34.76		 S = OPT
O = 52
T = 34.76
clq1-cv260c1040l2g30.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
clq1-cv260c1040l2g4.wcnf S = OPT
O = 45
T = 30.11		 S = OPT
O = 45
T = 30.11
clq1-cv260c1040l2g5.wcnf S = OPT
O = 58
T = 540.31		 S = OPT
O = 58
T = 540.31
clq1-cv260c1040l2g6.wcnf S = OPT
O = 49
T = 21.12		 S = OPT
O = 49
T = 21.12
clq1-cv260c1040l2g7.wcnf S = OPT
O = 46
T = 14.47		 S = OPT
O = 46
T = 14.47
clq1-cv260c1040l2g8.wcnf S = OPT
O = 48
T = 21.55		 S = OPT
O = 48
T = 21.55
clq1-cv260c1040l2g9.wcnf S = OPT
O = 50
T = 147.98		 S = OPT
O = 50
T = 147.98
clq1-c2mv70c350l3g1.wcnf S = OPT
O = 54
T = 137.27		 S = OPT
O = 54
T = 137.27
clq1-c2mv70c350l3g10.wcnf S = OPT
O = 43
T = 28.48		 S = OPT
O = 43
T = 28.48
clq1-c2mv70c350l3g11.wcnf S = OPT
O = 48
T = 46.52		 S = OPT
O = 48
T = 46.52
clq1-c2mv70c350l3g12.wcnf S = OPT
O = 51
T = 22.69		 S = OPT
O = 51
T = 22.69
clq1-c2mv70c350l3g13.wcnf S = OPT
O = 46
T = 31.28		 S = OPT
O = 46
T = 31.28
clq1-c2mv70c350l3g14.wcnf S = OPT
O = 50
T = 79.02		 S = OPT
O = 50
T = 79.02
clq1-c2mv70c350l3g15.wcnf S = OPT
O = 51
T = 53.13		 S = OPT
O = 51
T = 53.13
clq1-c2mv70c350l3g16.wcnf S = OPT
O = 51
T = 58.76		 S = OPT
O = 51
T = 58.76
clq1-c2mv70c350l3g17.wcnf S = OPT
O = 45
T = 40.22		 S = OPT
O = 45
T = 40.22
clq1-c2mv70c350l3g18.wcnf S = OPT
O = 51
T = 304.55		 S = OPT
O = 51
T = 304.55
clq1-c2mv70c350l3g19.wcnf S = OPT
O = 55
T = 186.95		 S = OPT
O = 55
T = 186.95
clq1-c2mv70c350l3g2.wcnf S = OPT
O = 48
T = 27.82		 S = OPT
O = 48
T = 27.82
clq1-c2mv70c350l3g20.wcnf S = OPT
O = 50
T = 64.17		 S = OPT
O = 50
T = 64.17
clq1-c2mv70c350l3g21.wcnf S = OPT
O = 40
T = 27.30		 S = OPT
O = 40
T = 27.30
clq1-c2mv70c350l3g22.wcnf S = OPT
O = 50
T = 87.16		 S = OPT
O = 50
T = 87.16
clq1-c2mv70c350l3g23.wcnf S = OPT
O = 52
T = 49.96		 S = OPT
O = 52
T = 49.96
clq1-c2mv70c350l3g24.wcnf S = OPT
O = 50
T = 84.58		 S = OPT
O = 50
T = 84.58
clq1-c2mv70c350l3g25.wcnf S = OPT
O = 45
T = 44.99		 S = OPT
O = 45
T = 44.99
clq1-c2mv70c350l3g26.wcnf S = OPT
O = 50
T = 28.79		 S = OPT
O = 50
T = 28.79
clq1-c2mv70c350l3g27.wcnf S = OPT
O = 56
T = 369.83		 S = OPT
O = 56
T = 369.83
clq1-c2mv70c350l3g28.wcnf S = OPT
O = 51
T = 68.96		 S = OPT
O = 51
T = 68.96
clq1-c2mv70c350l3g29.wcnf S = OPT
O = 55
T = 96.92		 S = OPT
O = 55
T = 96.92
clq1-c2mv70c350l3g3.wcnf S = OPT
O = 49
T = 197.65		 S = OPT
O = 49
T = 197.65
clq1-c2mv70c350l3g30.wcnf S = OPT
O = 53
T = 167.01		 S = OPT
O = 53
T = 167.01
clq1-c2mv70c350l3g4.wcnf S = OPT
O = 47
T = 34.68		 S = OPT
O = 47
T = 34.68
clq1-c2mv70c350l3g5.wcnf S = OPT
O = 46
T = 28.50		 S = OPT
O = 46
T = 28.50
clq1-c2mv70c350l3g6.wcnf S = OPT
O = 49
T = 25.96		 S = OPT
O = 49
T = 25.96
clq1-c2mv70c350l3g7.wcnf S = OPT
O = 54
T = 167.50		 S = OPT
O = 54
T = 167.50
clq1-c2mv70c350l3g8.wcnf S = OPT
O = 48
T = 148.85		 S = OPT
O = 48
T = 148.85
clq1-c2mv70c350l3g9.wcnf S = OPT
O = 50
T = 127.33		 S = OPT
O = 50
T = 127.33
clq1-c2mv80c400l3g1.wcnf S = OPT
O = 56
T = 101.15		 S = OPT
O = 56
T = 101.15
clq1-c2mv80c400l3g10.wcnf S = OPT
O = 55
T = 85.46		 S = OPT
O = 55
T = 85.46
clq1-c2mv80c400l3g11.wcnf S = OPT
O = 57
T = 240.86		 S = OPT
O = 57
T = 240.86
clq1-c2mv80c400l3g12.wcnf S = OPT
O = 65
T = 925.91		 S = OPT
O = 65
T = 925.91
clq1-c2mv80c400l3g13.wcnf S = OPT
O = 60
T = 741.82		 S = OPT
O = 60
T = 741.82
clq1-c2mv80c400l3g14.wcnf S = OPT
O = 59
T = 341.08		 S = OPT
O = 59
T = 341.08
clq1-c2mv80c400l3g15.wcnf S = OPT
O = 59
T = 219.64		 S = OPT
O = 59
T = 219.64
clq1-c2mv80c400l3g16.wcnf S = OPT
O = 61
T = 596.95		 S = OPT
O = 61
T = 596.95
clq1-c2mv80c400l3g17.wcnf S = OPT
O = 66
T = 1105.39		 S = OPT
O = 66
T = 1105.39
clq1-c2mv80c400l3g18.wcnf S = OPT
O = 58
T = 204.45		 S = OPT
O = 58
T = 204.45
clq1-c2mv80c400l3g19.wcnf S = OPT
O = 55
T = 278.20		 S = OPT
O = 55
T = 278.20
clq1-c2mv80c400l3g2.wcnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
clq1-c2mv80c400l3g20.wcnf S = OPT
O = 56
T = 185.73		 S = OPT
O = 56
T = 185.73
clq1-c2mv80c400l3g21.wcnf S = OPT
O = 65
T = 670.18		 S = OPT
O = 65
T = 670.18
clq1-c2mv80c400l3g22.wcnf S = OPT
O = 64
T = 739.11		 S = OPT
O = 64
T = 739.11
clq1-c2mv80c400l3g23.wcnf S = OPT
O = 56
T = 186.65		 S = OPT
O = 56
T = 186.65
clq1-c2mv80c400l3g24.wcnf S = OPT
O = 51
T = 51.96		 S = OPT
O = 51
T = 51.96
clq1-c2mv80c400l3g25.wcnf S = OPT
O = 55
T = 171.84		 S = OPT
O = 55
T = 171.84
clq1-c2mv80c400l3g26.wcnf S = OPT
O = 59
T = 670.12		 S = OPT
O = 59
T = 670.12
clq1-c2mv80c400l3g27.wcnf S = OPT
O = 59
T = 406.98		 S = OPT
O = 59
T = 406.98
clq1-c2mv80c400l3g28.wcnf S = OPT
O = 57
T = 108.13		 S = OPT
O = 57
T = 108.13
clq1-c2mv80c400l3g29.wcnf S = OPT
O = 63
T = 270.24		 S = OPT
O = 63
T = 270.24
clq1-c2mv80c400l3g3.wcnf S = OPT
O = 63
T = 822.61		 S = OPT
O = 63
T = 822.61
clq1-c2mv80c400l3g30.wcnf S = OPT
O = 59
T = 225.62		 S = OPT
O = 59
T = 225.62
clq1-c2mv80c400l3g4.wcnf S = OPT
O = 61
T = 295.89		 S = OPT
O = 61
T = 295.89
clq1-c2mv80c400l3g5.wcnf S = OPT
O = 62
T = 377.35		 S = OPT
O = 62
T = 377.35
clq1-c2mv80c400l3g6.wcnf S = OPT
O = 59
T = 161.22		 S = OPT
O = 59
T = 161.22
clq1-c2mv80c400l3g7.wcnf S = OPT
O = 64
T = 1226.16		 S = OPT
O = 64
T = 1226.16
clq1-c2mv80c400l3g8.wcnf S = OPT
O = 65
T = 755.37		 S = OPT
O = 65
T = 755.37
clq1-c2mv80c400l3g9.wcnf S = OPT
O = 59
T = 324.53		 S = OPT
O = 59
T = 324.53
file_rpms_wcnf_L2_V150_C4000_H150_0.wcnf S = OPT
O = 802
T = 10.17		 S = OPT
O = 802
T = 10.17
file_rpms_wcnf_L2_V150_C4000_H150_1.wcnf S = UNSAT
O = N/A
T = 9.88		 S = UNSAT
O = N/A
T = 9.88
file_rpms_wcnf_L2_V150_C4000_H150_2.wcnf S = OPT
O = 805
T = 10.20		 S = OPT
O = 805
T = 10.20
file_rpms_wcnf_L2_V150_C4000_H150_3.wcnf S = OPT
O = 752
T = 10.82		 S = OPT
O = 752
T = 10.82
file_rpms_wcnf_L2_V150_C4000_H150_4.wcnf S = OPT
O = 750
T = 11.14		 S = OPT
O = 750
T = 11.14
file_rpms_wcnf_L2_V150_C4000_H150_5.wcnf S = OPT
O = 756
T = 15.20		 S = OPT
O = 756
T = 15.20
file_rpms_wcnf_L2_V150_C4000_H150_6.wcnf S = OPT
O = 782
T = 17.82		 S = OPT
O = 782
T = 17.82
file_rpms_wcnf_L2_V150_C4000_H150_7.wcnf S = OPT
O = 755
T = 13.84		 S = OPT
O = 755
T = 13.84
file_rpms_wcnf_L2_V150_C4000_H150_8.wcnf S = OPT
O = 764
T = 26.52		 S = OPT
O = 764
T = 26.52
file_rpms_wcnf_L2_V150_C4000_H150_9.wcnf S = OPT
O = 792
T = 12.15		 S = OPT
O = 792
T = 12.15
file_rpms_wcnf_L2_V150_C4500_H150_0.wcnf S = OPT
O = 867
T = 17.42		 S = OPT
O = 867
T = 17.42
file_rpms_wcnf_L2_V150_C4500_H150_1.wcnf S = OPT
O = 905
T = 15.78		 S = OPT
O = 905
T = 15.78
file_rpms_wcnf_L2_V150_C4500_H150_2.wcnf S = OPT
O = 912
T = 12.10		 S = OPT
O = 912
T = 12.10
file_rpms_wcnf_L2_V150_C4500_H150_3.wcnf S = OPT
O = 878
T = 10.83		 S = OPT
O = 878
T = 10.83
file_rpms_wcnf_L2_V150_C4500_H150_4.wcnf S = OPT
O = 890
T = 16.71		 S = OPT
O = 890
T = 16.71
file_rpms_wcnf_L2_V150_C4500_H150_5.wcnf S = OPT
O = 881
T = 13.59		 S = OPT
O = 881
T = 13.59
file_rpms_wcnf_L2_V150_C4500_H150_6.wcnf S = OPT
O = 856
T = 13.87		 S = OPT
O = 856
T = 13.87
file_rpms_wcnf_L2_V150_C4500_H150_7.wcnf S = OPT
O = 875
T = 14.45		 S = OPT
O = 875
T = 14.45
file_rpms_wcnf_L2_V150_C4500_H150_8.wcnf S = OPT
O = 908
T = 10.66		 S = OPT
O = 908
T = 10.66
file_rpms_wcnf_L2_V150_C4500_H150_9.wcnf S = OPT
O = 898
T = 11.01		 S = OPT
O = 898
T = 11.01
file_rpms_wcnf_L2_V150_C5000_H150_0.wcnf S = OPT
O = 1018
T = 11.77		 S = OPT
O = 1018
T = 11.77
file_rpms_wcnf_L2_V150_C5000_H150_1.wcnf S = OPT
O = 1015
T = 18.42		 S = OPT
O = 1015
T = 18.42
file_rpms_wcnf_L2_V150_C5000_H150_2.wcnf S = OPT
O = 979
T = 14.88		 S = OPT
O = 979
T = 14.88
file_rpms_wcnf_L2_V150_C5000_H150_3.wcnf S = OPT
O = 1032
T = 13.03		 S = OPT
O = 1032
T = 13.03
file_rpms_wcnf_L2_V150_C5000_H150_4.wcnf S = OPT
O = 1018
T = 30.13		 S = OPT
O = 1018
T = 30.13
file_rpms_wcnf_L2_V150_C5000_H150_5.wcnf S = OPT
O = 991
T = 11.77		 S = OPT
O = 991
T = 11.77
file_rpms_wcnf_L2_V150_C5000_H150_6.wcnf S = OPT
O = 1005
T = 11.65		 S = OPT
O = 1005
T = 11.65
file_rpms_wcnf_L2_V150_C5000_H150_7.wcnf S = OPT
O = 991
T = 12.73		 S = OPT
O = 991
T = 12.73
file_rpms_wcnf_L2_V150_C5000_H150_8.wcnf S = OPT
O = 999
T = 10.79		 S = OPT
O = 999
T = 10.79
file_rpms_wcnf_L2_V150_C5000_H150_9.wcnf S = OPT
O = 993
T = 10.85		 S = OPT
O = 993
T = 10.85
file_rpms_wcnf_L2_V150_C2500_H150_0.wcnf S = OPT
O = 464
T = 10.04		 S = OPT
O = 464
T = 10.04
file_rpms_wcnf_L2_V150_C2500_H150_1.wcnf S = OPT
O = 454
T = 10.33		 S = OPT
O = 454
T = 10.33
file_rpms_wcnf_L2_V150_C2500_H150_2.wcnf S = OPT
O = 423
T = 10.99		 S = OPT
O = 423
T = 10.99
file_rpms_wcnf_L2_V150_C2500_H150_3.wcnf S = OPT
O = 442
T = 10.65		 S = OPT
O = 442
T = 10.65
file_rpms_wcnf_L2_V150_C2500_H150_4.wcnf S = OPT
O = 447
T = 9.97		 S = OPT
O = 447
T = 9.97
file_rpms_wcnf_L2_V150_C2500_H150_5.wcnf S = OPT
O = 433
T = 10.11		 S = OPT
O = 433
T = 10.11
file_rpms_wcnf_L2_V150_C2500_H150_6.wcnf S = OPT
O = 461
T = 10.31		 S = OPT
O = 461
T = 10.31
file_rpms_wcnf_L2_V150_C2500_H150_7.wcnf S = OPT
O = 434
T = 11.50		 S = OPT
O = 434
T = 11.50
file_rpms_wcnf_L2_V150_C2500_H150_8.wcnf S = OPT
O = 456
T = 10.62		 S = OPT
O = 456
T = 10.62
file_rpms_wcnf_L2_V150_C2500_H150_9.wcnf S = OPT
O = 470
T = 9.90		 S = OPT
O = 470
T = 9.90
file_rpms_wcnf_L2_V150_C3000_H150_0.wcnf S = OPT
O = 539
T = 11.66		 S = OPT
O = 539
T = 11.66
file_rpms_wcnf_L2_V150_C3000_H150_1.wcnf S = OPT
O = 560
T = 13.39		 S = OPT
O = 560
T = 13.39
file_rpms_wcnf_L2_V150_C3000_H150_2.wcnf S = OPT
O = 531
T = 10.97		 S = OPT
O = 531
T = 10.97
file_rpms_wcnf_L2_V150_C3000_H150_3.wcnf S = OPT
O = 555
T = 13.63		 S = OPT
O = 555
T = 13.63
file_rpms_wcnf_L2_V150_C3000_H150_4.wcnf S = OPT
O = 556
T = 10.14		 S = OPT
O = 556
T = 10.14
file_rpms_wcnf_L2_V150_C3000_H150_5.wcnf S = OPT
O = 538
T = 15.53		 S = OPT
O = 538
T = 15.53
file_rpms_wcnf_L2_V150_C3000_H150_6.wcnf S = OPT
O = 537
T = 14.30		 S = OPT
O = 537
T = 14.30
file_rpms_wcnf_L2_V150_C3000_H150_7.wcnf S = OPT
O = 527
T = 10.97		 S = OPT
O = 527
T = 10.97
file_rpms_wcnf_L2_V150_C3000_H150_8.wcnf S = OPT
O = 564
T = 15.58		 S = OPT
O = 564
T = 15.58
file_rpms_wcnf_L2_V150_C3000_H150_9.wcnf S = OPT
O = 552
T = 10.61		 S = OPT
O = 552
T = 10.61
file_rpms_wcnf_L2_V150_C3500_H150_0.wcnf S = OPT
O = 680
T = 16.07		 S = OPT
O = 680
T = 16.07
file_rpms_wcnf_L2_V150_C3500_H150_1.wcnf S = OPT
O = 679
T = 10.97		 S = OPT
O = 679
T = 10.97
file_rpms_wcnf_L2_V150_C3500_H150_2.wcnf S = OPT
O = 716
T = 10.58		 S = OPT
O = 716
T = 10.58
file_rpms_wcnf_L2_V150_C3500_H150_3.wcnf S = OPT
O = 669
T = 11.29		 S = OPT
O = 669
T = 11.29
file_rpms_wcnf_L2_V150_C3500_H150_4.wcnf S = OPT
O = 627
T = 11.19		 S = OPT
O = 627
T = 11.19
file_rpms_wcnf_L2_V150_C3500_H150_5.wcnf S = OPT
O = 667
T = 16.27		 S = OPT
O = 667
T = 16.27
file_rpms_wcnf_L2_V150_C3500_H150_6.wcnf S = OPT
O = 688
T = 10.09		 S = OPT
O = 688
T = 10.09
file_rpms_wcnf_L2_V150_C3500_H150_7.wcnf S = OPT
O = 675
T = 10.46		 S = OPT
O = 675
T = 10.46
file_rpms_wcnf_L2_V150_C3500_H150_8.wcnf S = OPT
O = 675
T = 10.75		 S = OPT
O = 675
T = 10.75
file_rpms_wcnf_L2_V150_C3500_H150_9.wcnf S = OPT
O = 638
T = 11.43		 S = OPT
O = 638
T = 11.43
file_rpms_wcnf_L3_V100_C600_H100_0.wcnf S = OPT
O = 8
T = 18.54		 S = OPT
O = 8
T = 18.54
file_rpms_wcnf_L3_V100_C600_H100_1.wcnf S = OPT
O = 8
T = 16.49		 S = OPT
O = 8
T = 16.49
file_rpms_wcnf_L3_V100_C600_H100_2.wcnf S = OPT
O = 8
T = 18.43		 S = OPT
O = 8
T = 18.43
file_rpms_wcnf_L3_V100_C600_H100_3.wcnf S = OPT
O = 9
T = 18.80		 S = OPT
O = 9
T = 18.80
file_rpms_wcnf_L3_V100_C600_H100_4.wcnf S = OPT
O = 7
T = 11.76		 S = OPT
O = 7
T = 11.76
file_rpms_wcnf_L3_V100_C600_H100_5.wcnf S = OPT
O = 8
T = 13.99		 S = OPT
O = 8
T = 13.99
file_rpms_wcnf_L3_V100_C600_H100_6.wcnf S = OPT
O = 7
T = 15.85		 S = OPT
O = 7
T = 15.85
file_rpms_wcnf_L3_V100_C600_H100_7.wcnf S = OPT
O = 8
T = 17.05		 S = OPT
O = 8
T = 17.05
file_rpms_wcnf_L3_V100_C600_H100_8.wcnf S = OPT
O = 5
T = 12.49		 S = OPT
O = 5
T = 12.49
file_rpms_wcnf_L3_V100_C600_H100_9.wcnf S = OPT
O = 9
T = 14.46		 S = OPT
O = 9
T = 14.46
file_rpms_wcnf_L3_V100_C700_H100_0.wcnf S = OPT
O = 18
T = 56.13		 S = OPT
O = 18
T = 56.13
file_rpms_wcnf_L3_V100_C700_H100_1.wcnf S = OPT
O = 14
T = 84.30		 S = OPT
O = 14
T = 84.30
file_rpms_wcnf_L3_V100_C700_H100_2.wcnf S = OPT
O = 15
T = 35.45		 S = OPT
O = 15
T = 35.45
file_rpms_wcnf_L3_V100_C700_H100_3.wcnf S = OPT
O = 12
T = 29.84		 S = OPT
O = 12
T = 29.84
file_rpms_wcnf_L3_V100_C700_H100_4.wcnf S = OPT
O = 11
T = 35.03		 S = OPT
O = 11
T = 35.03
file_rpms_wcnf_L3_V100_C700_H100_5.wcnf S = OPT
O = 14
T = 87.10		 S = OPT
O = 14
T = 87.10
file_rpms_wcnf_L3_V100_C700_H100_6.wcnf S = OPT
O = 12
T = 39.70		 S = OPT
O = 12
T = 39.70
file_rpms_wcnf_L3_V100_C700_H100_7.wcnf S = OPT
O = 17
T = 69.76		 S = OPT
O = 17
T = 69.76
file_rpms_wcnf_L3_V100_C700_H100_8.wcnf S = OPT
O = 16
T = 111.61		 S = OPT
O = 16
T = 111.61
file_rpms_wcnf_L3_V100_C700_H100_9.wcnf S = OPT
O = 12
T = 30.59		 S = OPT
O = 12
T = 30.59
file_rpms_wcnf_L3_V100_C800_H100_0.wcnf S = OPT
O = 21
T = 111.03		 S = OPT
O = 21
T = 111.03
file_rpms_wcnf_L3_V100_C800_H100_1.wcnf S = OPT
O = 21
T = 186.61		 S = OPT
O = 21
T = 186.61
file_rpms_wcnf_L3_V100_C800_H100_2.wcnf S = OPT
O = 20
T = 140.66		 S = OPT
O = 20
T = 140.66
file_rpms_wcnf_L3_V100_C800_H100_3.wcnf S = OPT
O = 22
T = 68.31		 S = OPT
O = 22
T = 68.31
file_rpms_wcnf_L3_V100_C800_H100_4.wcnf S = OPT
O = 18
T = 76.67		 S = OPT
O = 18
T = 76.67
file_rpms_wcnf_L3_V100_C800_H100_5.wcnf S = OPT
O = 20
T = 85.19		 S = OPT
O = 20
T = 85.19
file_rpms_wcnf_L3_V100_C800_H100_6.wcnf S = OPT
O = 17
T = 82.52		 S = OPT
O = 17
T = 82.52
file_rpms_wcnf_L3_V100_C800_H100_7.wcnf S = OPT
O = 23
T = 116.18		 S = OPT
O = 23
T = 116.18
file_rpms_wcnf_L3_V100_C800_H100_8.wcnf S = OPT
O = 25
T = 410.46		 S = OPT
O = 25
T = 410.46
file_rpms_wcnf_L3_V100_C800_H100_9.wcnf S = OPT
O = 20
T = 98.83		 S = OPT
O = 20
T = 98.83