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 Sat4j-i ubcsat-irots
clq1-cv160c800l2g1.wcnf O = 75
T = 46.93
O = 112
T = 4.99
(out)(err)
O = 75
T = 46.93
(out)(err)
clq1-cv160c800l2g10.wcnf O = 68
T = 190.03
O = 86
T = 25.77
(out)(err)
O = 68
T = 190.03
(out)(err)
clq1-cv160c800l2g11.wcnf O = 83
T = 202.24
O = 111
T = 117.11
(out)(err)
O = 83
T = 202.24
(out)(err)
clq1-cv160c800l2g12.wcnf O = 75
T = 30.86
O = 101
T = 4.52
(out)(err)
O = 75
T = 30.86
(out)(err)
clq1-cv160c800l2g13.wcnf O = 67
T = 89.85
O = 90
T = 1.95
(out)(err)
O = 67
T = 89.85
(out)(err)
clq1-cv160c800l2g14.wcnf O = 55
T = 30.84
O = 85
T = 4.55
(out)(err)
O = 55
T = 30.84
(out)(err)
clq1-cv160c800l2g15.wcnf O = 80
T = 134.13
O = 95
T = 5.45
(out)(err)
O = 80
T = 134.13
(out)(err)
clq1-cv160c800l2g16.wcnf O = 68
T = 32.72
O = 104
T = 5.32
(out)(err)
O = 68
T = 32.72
(out)(err)
clq1-cv160c800l2g17.wcnf O = 72
T = 203.21
O = 97
T = 1.91
(out)(err)
O = 72
T = 203.21
(out)(err)
clq1-cv160c800l2g18.wcnf O = 67
T = 30.49
O = 99
T = 85.83
(out)(err)
O = 67
T = 30.49
(out)(err)
clq1-cv160c800l2g19.wcnf O = 87
T = 44.23
O = 119
T = 5.34
(out)(err)
O = 87
T = 44.23
(out)(err)
clq1-cv160c800l2g2.wcnf O = 67
T = 29.33
O = 87
T = 54.64
(out)(err)
O = 67
T = 29.33
(out)(err)
clq1-cv160c800l2g20.wcnf O = 61
T = 36.40
O = 91
T = 2.73
(out)(err)
O = 61
T = 36.40
(out)(err)
clq1-cv160c800l2g21.wcnf O = 73
T = 58.02
O = 90
T = 2.12
(out)(err)
O = 73
T = 58.02
(out)(err)
clq1-cv160c800l2g22.wcnf O = 70
T = 155.45
O = 111
T = 5.46
(out)(err)
O = 70
T = 155.45
(out)(err)
clq1-cv160c800l2g23.wcnf O = 63
T = 191.73
O = 99
T = 2.24
(out)(err)
O = 63
T = 191.73
(out)(err)
clq1-cv160c800l2g24.wcnf O = 70
T = 31.85
O = 81
T = 147.58
(out)(err)
O = 70
T = 31.85
(out)(err)
clq1-cv160c800l2g25.wcnf O = 68
T = 29.78
O = 106
T = 3.75
(out)(err)
O = 68
T = 29.78
(out)(err)
clq1-cv160c800l2g26.wcnf O = 67
T = 114.27
O = 90
T = 5.12
(out)(err)
O = 67
T = 114.27
(out)(err)
clq1-cv160c800l2g27.wcnf O = 73
T = 252.69
O = 108
T = 1.09
(out)(err)
O = 73
T = 252.69
(out)(err)
clq1-cv160c800l2g28.wcnf O = 63
T = 45.30
O = 98
T = 4.97
(out)(err)
O = 63
T = 45.30
(out)(err)
clq1-cv160c800l2g29.wcnf O = 58
T = 32.33
O = 82
T = 5.13
(out)(err)
O = 58
T = 32.33
(out)(err)
clq1-cv160c800l2g3.wcnf O = 75
T = 189.11
O = 107
T = 3.67
(out)(err)
O = 75
T = 189.11
(out)(err)
clq1-cv160c800l2g30.wcnf O = 78
T = 103.45
O = 122
T = 3.67
(out)(err)
O = 78
T = 103.45
(out)(err)
clq1-cv160c800l2g4.wcnf O = 68
T = 130.27
O = 99
T = 4.45
(out)(err)
O = 68
T = 130.27
(out)(err)
clq1-cv160c800l2g5.wcnf O = 62
T = 100.47
O = 87
T = 3.81
(out)(err)
O = 62
T = 100.47
(out)(err)
clq1-cv160c800l2g6.wcnf O = 79
T = 93.31
O = 102
T = 4.75
(out)(err)
O = 79
T = 93.31
(out)(err)
clq1-cv160c800l2g7.wcnf O = 83
T = 127.25
O = 94
T = 2.98
(out)(err)
O = 83
T = 127.25
(out)(err)
clq1-cv160c800l2g8.wcnf O = 65
T = 80.32
O = 79
T = 29.96
(out)(err)
O = 65
T = 80.32
(out)(err)
clq1-cv160c800l2g9.wcnf O = 70
T = 106.15
O = 87
T = 151.98
(out)(err)
O = 70
T = 106.15
(out)(err)
clq1-cv260c1040l2g1.wcnf O = 96
T = 42.62
O = 100
T = 1.72
(out)(err)
O = 96
T = 42.62
(out)(err)
clq1-cv260c1040l2g10.wcnf O = 93
T = 37.70
O = 94
T = 4.59
(out)(err)
O = 93
T = 37.70
(out)(err)
clq1-cv260c1040l2g11.wcnf O = 50
T = 2.33
O = 50
T = 2.33
(out)(err)
O = 71
T = 67.27
(out)(err)
clq1-cv260c1040l2g12.wcnf O = 84
T = 184.39
O = 88
T = 3.22
(out)(err)
O = 84
T = 184.39
(out)(err)
clq1-cv260c1040l2g13.wcnf O = 56
T = 3.57
O = 56
T = 3.57
(out)(err)
O = 70
T = 16.20
(out)(err)
clq1-cv260c1040l2g14.wcnf O = 84
T = 37.59
O = 104
T = 5.22
(out)(err)
O = 84
T = 37.59
(out)(err)
clq1-cv260c1040l2g15.wcnf O = 64
T = 1.83
O = 64
T = 1.83
(out)(err)
O = 80
T = 176.11
(out)(err)
clq1-cv260c1040l2g16.wcnf O = 82
T = 4.36
O = 82
T = 4.36
(out)(err)
O = 82
T = 39.31
(out)(err)
clq1-cv260c1040l2g17.wcnf O = 78
T = 36.66
O = 80
T = 3.88
(out)(err)
O = 78
T = 36.66
(out)(err)
clq1-cv260c1040l2g18.wcnf O = 66
T = 39.62
O = 70
T = 5.66
(out)(err)
O = 66
T = 39.62
(out)(err)
clq1-cv260c1040l2g19.wcnf O = 91
T = 3.78
O = 91
T = 3.78
(out)(err)
O = 95
T = 121.16
(out)(err)
clq1-cv260c1040l2g2.wcnf O = 86
T = 11.29
O = 86
T = 176.45
(out)(err)
O = 86
T = 11.29
(out)(err)
clq1-cv260c1040l2g20.wcnf O = 82
T = 3.01
O = 82
T = 3.01
(out)(err)
O = 84
T = 43.56
(out)(err)
clq1-cv260c1040l2g21.wcnf O = 83
T = 42.17
O = 90
T = 1.37
(out)(err)
O = 83
T = 42.17
(out)(err)
clq1-cv260c1040l2g22.wcnf O = 91
T = 40.30
O = 115
T = 3.57
(out)(err)
O = 91
T = 40.30
(out)(err)
clq1-cv260c1040l2g23.wcnf O = 82
T = 37.78
O = 98
T = 4.89
(out)(err)
O = 82
T = 37.78
(out)(err)
clq1-cv260c1040l2g24.wcnf O = 62
T = 2.02
O = 62
T = 2.02
(out)(err)
O = 77
T = 30.75
(out)(err)
clq1-cv260c1040l2g25.wcnf O = 66
T = 155.53
O = 91
T = 1.71
(out)(err)
O = 66
T = 155.53
(out)(err)
clq1-cv260c1040l2g26.wcnf O = 73
T = 41.21
O = 82
T = 4.36
(out)(err)
O = 73
T = 41.21
(out)(err)
clq1-cv260c1040l2g27.wcnf O = 99
T = 38.06
O = 130
T = 3.87
(out)(err)
O = 99
T = 38.06
(out)(err)
clq1-cv260c1040l2g28.wcnf O = 94
T = 252.99
O = 100
T = 4.02
(out)(err)
O = 94
T = 252.99
(out)(err)
clq1-cv260c1040l2g29.wcnf O = 81
T = 20.13
O = 105
T = 2.50
(out)(err)
O = 81
T = 20.13
(out)(err)
clq1-cv260c1040l2g3.wcnf O = 75
T = 76.40
O = 89
T = 2.55
(out)(err)
O = 75
T = 76.40
(out)(err)
clq1-cv260c1040l2g30.wcnf O = 86
T = 37.19
O = 101
T = 4.00
(out)(err)
O = 86
T = 37.19
(out)(err)
clq1-cv260c1040l2g4.wcnf O = 75
T = 193.94
O = 79
T = 1.31
(out)(err)
O = 75
T = 193.94
(out)(err)
clq1-cv260c1040l2g5.wcnf O = 89
T = 2.70
O = 89
T = 2.70
(out)(err)
O = 90
T = 173.03
(out)(err)
clq1-cv260c1040l2g6.wcnf O = 86
T = 26.97
O = 90
T = 2.90
(out)(err)
O = 86
T = 26.97
(out)(err)
clq1-cv260c1040l2g7.wcnf O = 76
T = 42.44
O = 82
T = 3.55
(out)(err)
O = 76
T = 42.44
(out)(err)
clq1-cv260c1040l2g8.wcnf O = 74
T = 262.74
O = 82
T = 3.35
(out)(err)
O = 74
T = 262.74
(out)(err)
clq1-cv260c1040l2g9.wcnf O = 64
T = 4.01
O = 64
T = 4.01
(out)(err)
O = 80
T = 110.47
(out)(err)
clq1-c2mv70c350l3g1.wcnf O = 57
T = 28.31
O = 72
T = 3.96
(out)(err)
O = 57
T = 28.31
(out)(err)
clq1-c2mv70c350l3g10.wcnf O = 43
T = 80.61
O = 59
T = 2.05
(out)(err)
O = 43
T = 80.61
(out)(err)
clq1-c2mv70c350l3g11.wcnf O = 50
T = 11.98
O = 67
T = 67.64
(out)(err)
O = 50
T = 11.98
(out)(err)
clq1-c2mv70c350l3g12.wcnf O = 52
T = 13.62
O = 66
T = 1.99
(out)(err)
O = 52
T = 13.62
(out)(err)
clq1-c2mv70c350l3g13.wcnf O = 47
T = 198.87
O = 69
T = 8.18
(out)(err)
O = 47
T = 198.87
(out)(err)
clq1-c2mv70c350l3g14.wcnf O = 51
T = 131.40
O = 73
T = 2.76
(out)(err)
O = 51
T = 131.40
(out)(err)
clq1-c2mv70c350l3g15.wcnf O = 53
T = 229.61
O = 81
T = 4.66
(out)(err)
O = 53
T = 229.61
(out)(err)
clq1-c2mv70c350l3g16.wcnf O = 52
T = 193.45
O = 70
T = 4.80
(out)(err)
O = 52
T = 193.45
(out)(err)
clq1-c2mv70c350l3g17.wcnf O = 47
T = 11.66
O = 62
T = 5.03
(out)(err)
O = 47
T = 11.66
(out)(err)
clq1-c2mv70c350l3g18.wcnf O = 52
T = 83.02
O = 67
T = 4.10
(out)(err)
O = 52
T = 83.02
(out)(err)
clq1-c2mv70c350l3g19.wcnf O = 56
T = 41.68
O = 75
T = 4.75
(out)(err)
O = 56
T = 41.68
(out)(err)
clq1-c2mv70c350l3g2.wcnf O = 48
T = 181.84
O = 70
T = 1.60
(out)(err)
O = 48
T = 181.84
(out)(err)
clq1-c2mv70c350l3g20.wcnf O = 52
T = 16.38
O = 69
T = 65.61
(out)(err)
O = 52
T = 16.38
(out)(err)
clq1-c2mv70c350l3g21.wcnf O = 40
T = 184.87
O = 62
T = 4.60
(out)(err)
O = 40
T = 184.87
(out)(err)
clq1-c2mv70c350l3g22.wcnf O = 51
T = 100.08
O = 71
T = 1.72
(out)(err)
O = 51
T = 100.08
(out)(err)
clq1-c2mv70c350l3g23.wcnf O = 53
T = 65.54
O = 69
T = 3.03
(out)(err)
O = 53
T = 65.54
(out)(err)
clq1-c2mv70c350l3g24.wcnf O = 53
T = 150.62
O = 69
T = 20.93
(out)(err)
O = 53
T = 150.62
(out)(err)
clq1-c2mv70c350l3g25.wcnf O = 45
T = 29.20
O = 70
T = 2.88
(out)(err)
O = 45
T = 29.20
(out)(err)
clq1-c2mv70c350l3g26.wcnf O = 51
T = 35.24
O = 74
T = 2.07
(out)(err)
O = 51
T = 35.24
(out)(err)
clq1-c2mv70c350l3g27.wcnf O = 58
T = 132.35
O = 71
T = 4.29
(out)(err)
O = 58
T = 132.35
(out)(err)
clq1-c2mv70c350l3g28.wcnf O = 54
T = 12.41
O = 71
T = 3.93
(out)(err)
O = 54
T = 12.41
(out)(err)
clq1-c2mv70c350l3g29.wcnf O = 55
T = 161.92
O = 80
T = 8.59
(out)(err)
O = 55
T = 161.92
(out)(err)
clq1-c2mv70c350l3g3.wcnf O = 51
T = 52.76
O = 76
T = 3.32
(out)(err)
O = 51
T = 52.76
(out)(err)
clq1-c2mv70c350l3g30.wcnf O = 55
T = 14.67
O = 72
T = 2.28
(out)(err)
O = 55
T = 14.67
(out)(err)
clq1-c2mv70c350l3g4.wcnf O = 50
T = 220.85
O = 61
T = 4.19
(out)(err)
O = 50
T = 220.85
(out)(err)
clq1-c2mv70c350l3g5.wcnf O = 48
T = 13.57
O = 66
T = 3.25
(out)(err)
O = 48
T = 13.57
(out)(err)
clq1-c2mv70c350l3g6.wcnf O = 51
T = 26.45
O = 72
T = 2.56
(out)(err)
O = 51
T = 26.45
(out)(err)
clq1-c2mv70c350l3g7.wcnf O = 55
T = 218.49
O = 72
T = 3.72
(out)(err)
O = 55
T = 218.49
(out)(err)
clq1-c2mv70c350l3g8.wcnf O = 50
T = 162.76
O = 58
T = 5.03
(out)(err)
O = 50
T = 162.76
(out)(err)
clq1-c2mv70c350l3g9.wcnf O = 52
T = 129.06
O = 68
T = 4.84
(out)(err)
O = 52
T = 129.06
(out)(err)
clq1-c2mv80c400l3g1.wcnf O = 59
T = 152.79
O = 95
T = 2.39
(out)(err)
O = 59
T = 152.79
(out)(err)
clq1-c2mv80c400l3g10.wcnf O = 60
T = 11.55
O = 85
T = 8.91
(out)(err)
O = 60
T = 11.55
(out)(err)
clq1-c2mv80c400l3g11.wcnf O = 59
T = 16.85
O = 84
T = 3.94
(out)(err)
O = 59
T = 16.85
(out)(err)
clq1-c2mv80c400l3g12.wcnf O = 66
T = 61.03
O = 86
T = 6.82
(out)(err)
O = 66
T = 61.03
(out)(err)
clq1-c2mv80c400l3g13.wcnf O = 62
T = 31.45
O = 88
T = 3.74
(out)(err)
O = 62
T = 31.45
(out)(err)
clq1-c2mv80c400l3g14.wcnf O = 61
T = 152.29
O = 83
T = 4.55
(out)(err)
O = 61
T = 152.29
(out)(err)
clq1-c2mv80c400l3g15.wcnf O = 62
T = 15.25
O = 92
T = 5.44
(out)(err)
O = 62
T = 15.25
(out)(err)
clq1-c2mv80c400l3g16.wcnf O = 65
T = 14.98
O = 89
T = 5.03
(out)(err)
O = 65
T = 14.98
(out)(err)
clq1-c2mv80c400l3g17.wcnf O = 68
T = 79.46
O = 83
T = 6.01
(out)(err)
O = 68
T = 79.46
(out)(err)
clq1-c2mv80c400l3g18.wcnf O = 59
T = 15.50
O = 89
T = 4.96
(out)(err)
O = 59
T = 15.50
(out)(err)
clq1-c2mv80c400l3g19.wcnf O = 57
T = 212.64
O = 82
T = 4.25
(out)(err)
O = 57
T = 212.64
(out)(err)
clq1-c2mv80c400l3g2.wcnf O = 68
T = 207.69
O = 94
T = 3.98
(out)(err)
O = 68
T = 207.69
(out)(err)
clq1-c2mv80c400l3g20.wcnf O = 58
T = 202.68
O = 95
T = 6.51
(out)(err)
O = 58
T = 202.68
(out)(err)
clq1-c2mv80c400l3g21.wcnf O = 67
T = 188.58
O = 91
T = 6.11
(out)(err)
O = 67
T = 188.58
(out)(err)
clq1-c2mv80c400l3g22.wcnf O = 68
T = 30.31
O = 97
T = 3.45
(out)(err)
O = 68
T = 30.31
(out)(err)
clq1-c2mv80c400l3g23.wcnf O = 58
T = 52.38
O = 92
T = 4.85
(out)(err)
O = 58
T = 52.38
(out)(err)
clq1-c2mv80c400l3g24.wcnf O = 54
T = 16.67
O = 90
T = 4.64
(out)(err)
O = 54
T = 16.67
(out)(err)
clq1-c2mv80c400l3g25.wcnf O = 58
T = 15.01
O = 98
T = 4.70
(out)(err)
O = 58
T = 15.01
(out)(err)
clq1-c2mv80c400l3g26.wcnf O = 59
T = 113.07
O = 97
T = 2.38
(out)(err)
O = 59
T = 113.07
(out)(err)
clq1-c2mv80c400l3g27.wcnf O = 62
T = 17.23
O = 88
T = 1.72
(out)(err)
O = 62
T = 17.23
(out)(err)
clq1-c2mv80c400l3g28.wcnf O = 60
T = 162.71
O = 89
T = 5.16
(out)(err)
O = 60
T = 162.71
(out)(err)
clq1-c2mv80c400l3g29.wcnf O = 66
T = 10.27
O = 90
T = 5.00
(out)(err)
O = 66
T = 10.27
(out)(err)
clq1-c2mv80c400l3g3.wcnf O = 64
T = 44.87
O = 96
T = 3.02
(out)(err)
O = 64
T = 44.87
(out)(err)
clq1-c2mv80c400l3g30.wcnf O = 60
T = 181.55
O = 93
T = 3.91
(out)(err)
O = 60
T = 181.55
(out)(err)
clq1-c2mv80c400l3g4.wcnf O = 63
T = 16.15
O = 95
T = 3.92
(out)(err)
O = 63
T = 16.15
(out)(err)
clq1-c2mv80c400l3g5.wcnf O = 67
T = 15.45
O = 87
T = 2.56
(out)(err)
O = 67
T = 15.45
(out)(err)
clq1-c2mv80c400l3g6.wcnf O = 63
T = 35.36
O = 91
T = 5.96
(out)(err)
O = 63
T = 35.36
(out)(err)
clq1-c2mv80c400l3g7.wcnf O = 66
T = 43.71
O = 92
T = 3.64
(out)(err)
O = 66
T = 43.71
(out)(err)
clq1-c2mv80c400l3g8.wcnf O = 68
T = 13.35
O = 86
T = 5.17
(out)(err)
O = 68
T = 13.35
(out)(err)
clq1-c2mv80c400l3g9.wcnf O = 63
T = 31.04
O = 86
T = 4.42
(out)(err)
O = 63
T = 31.04
(out)(err)
file_rpms_wcnf_L2_V150_C4000_H150_0.wcnf O = 802
T = 9.28
O = 930
T = 5.60
(out)(err)
O = 802
T = 9.28
(out)(err)
file_rpms_wcnf_L2_V150_C4000_H150_1.wcnf O = 4802
T = 7.75
O = N/A
T = TO
(out)(err)
O = 4802
T = 7.75
(out)(err)
file_rpms_wcnf_L2_V150_C4000_H150_2.wcnf O = 805
T = 10.03
O = 934
T = 6.06
(out)(err)
O = 805
T = 10.03
(out)(err)
file_rpms_wcnf_L2_V150_C4000_H150_3.wcnf O = 752
T = 8.69
O = 909
T = 7.65
(out)(err)
O = 752
T = 8.69
(out)(err)
file_rpms_wcnf_L2_V150_C4000_H150_4.wcnf O = 750
T = 10.32
O = 896
T = 4.62
(out)(err)
O = 750
T = 10.32
(out)(err)
file_rpms_wcnf_L2_V150_C4000_H150_5.wcnf O = 756
T = 3.95
O = 879
T = 4.36
(out)(err)
O = 756
T = 3.95
(out)(err)
file_rpms_wcnf_L2_V150_C4000_H150_6.wcnf O = 782
T = 7.26
O = 880
T = 5.50
(out)(err)
O = 782
T = 7.26
(out)(err)
file_rpms_wcnf_L2_V150_C4000_H150_7.wcnf O = 755
T = 7.09
O = 920
T = 5.74
(out)(err)
O = 755
T = 7.09
(out)(err)
file_rpms_wcnf_L2_V150_C4000_H150_8.wcnf O = 764
T = 12.31
O = 909
T = 4.98
(out)(err)
O = 764
T = 12.31
(out)(err)
file_rpms_wcnf_L2_V150_C4000_H150_9.wcnf O = 792
T = 9.07
O = 948
T = 3.24
(out)(err)
O = 792
T = 9.07
(out)(err)
file_rpms_wcnf_L2_V150_C4500_H150_0.wcnf O = 867
T = 10.10
O = 1047
T = 5.27
(out)(err)
O = 867
T = 10.10
(out)(err)
file_rpms_wcnf_L2_V150_C4500_H150_1.wcnf O = 905
T = 8.34
O = 1021
T = 4.71
(out)(err)
O = 905
T = 8.34
(out)(err)
file_rpms_wcnf_L2_V150_C4500_H150_2.wcnf O = 912
T = 7.52
O = 1007
T = 7.09
(out)(err)
O = 912
T = 7.52
(out)(err)
file_rpms_wcnf_L2_V150_C4500_H150_3.wcnf O = 878
T = 8.03
O = 1053
T = 8.87
(out)(err)
O = 878
T = 8.03
(out)(err)
file_rpms_wcnf_L2_V150_C4500_H150_4.wcnf O = 890
T = 10.47
O = 1066
T = 6.19
(out)(err)
O = 890
T = 10.47
(out)(err)
file_rpms_wcnf_L2_V150_C4500_H150_5.wcnf O = 881
T = 9.41
O = 1099
T = 4.44
(out)(err)
O = 881
T = 9.41
(out)(err)
file_rpms_wcnf_L2_V150_C4500_H150_6.wcnf O = 856
T = 8.25
O = 985
T = 4.40
(out)(err)
O = 856
T = 8.25
(out)(err)
file_rpms_wcnf_L2_V150_C4500_H150_7.wcnf O = 875
T = 9.79
O = 1034
T = 3.93
(out)(err)
O = 875
T = 9.79
(out)(err)
file_rpms_wcnf_L2_V150_C4500_H150_8.wcnf O = 908
T = 8.18
O = 1048
T = 5.26
(out)(err)
O = 908
T = 8.18
(out)(err)
file_rpms_wcnf_L2_V150_C4500_H150_9.wcnf O = 898
T = 11.06
O = 1048
T = 3.48
(out)(err)
O = 898
T = 11.06
(out)(err)
file_rpms_wcnf_L2_V150_C5000_H150_0.wcnf O = 1018
T = 11.80
O = 1178
T = 7.03
(out)(err)
O = 1018
T = 11.80
(out)(err)
file_rpms_wcnf_L2_V150_C5000_H150_1.wcnf O = 1015
T = 9.85
O = 1198
T = 5.41
(out)(err)
O = 1015
T = 9.85
(out)(err)
file_rpms_wcnf_L2_V150_C5000_H150_2.wcnf O = 979
T = 9.59
O = 1120
T = 4.52
(out)(err)
O = 979
T = 9.59
(out)(err)
file_rpms_wcnf_L2_V150_C5000_H150_3.wcnf O = 1032
T = 9.89
O = 1164
T = 4.25
(out)(err)
O = 1032
T = 9.89
(out)(err)
file_rpms_wcnf_L2_V150_C5000_H150_4.wcnf O = 1018
T = 7.36
O = 1155
T = 5.73
(out)(err)
O = 1018
T = 7.36
(out)(err)
file_rpms_wcnf_L2_V150_C5000_H150_5.wcnf O = 991
T = 7.27
O = 1130
T = 3.17
(out)(err)
O = 991
T = 7.27
(out)(err)
file_rpms_wcnf_L2_V150_C5000_H150_6.wcnf O = 1005
T = 7.93
O = 1129
T = 5.29
(out)(err)
O = 1005
T = 7.93
(out)(err)
file_rpms_wcnf_L2_V150_C5000_H150_7.wcnf O = 991
T = 9.46
O = 1132
T = 5.54
(out)(err)
O = 991
T = 9.46
(out)(err)
file_rpms_wcnf_L2_V150_C5000_H150_8.wcnf O = 999
T = 10.81
O = 1151
T = 3.80
(out)(err)
O = 999
T = 10.81
(out)(err)
file_rpms_wcnf_L2_V150_C5000_H150_9.wcnf O = 993
T = 5.40
O = 1140
T = 4.17
(out)(err)
O = 993
T = 5.40
(out)(err)
file_rpms_wcnf_L2_V150_C2500_H150_0.wcnf O = 464
T = 9.29
O = 536
T = 5.17
(out)(err)
O = 464
T = 9.29
(out)(err)
file_rpms_wcnf_L2_V150_C2500_H150_1.wcnf O = 454
T = 9.63
O = 575
T = 2.80
(out)(err)
O = 454
T = 9.63
(out)(err)
file_rpms_wcnf_L2_V150_C2500_H150_2.wcnf O = 423
T = 5.91
O = 543
T = 4.99
(out)(err)
O = 423
T = 5.91
(out)(err)
file_rpms_wcnf_L2_V150_C2500_H150_3.wcnf O = 442
T = 7.42
O = 551
T = 2.38
(out)(err)
O = 442
T = 7.42
(out)(err)
file_rpms_wcnf_L2_V150_C2500_H150_4.wcnf O = 447
T = 8.18
O = 535
T = 5.45
(out)(err)
O = 447
T = 8.18
(out)(err)
file_rpms_wcnf_L2_V150_C2500_H150_5.wcnf O = 433
T = 7.28
O = 521
T = 4.34
(out)(err)
O = 433
T = 7.28
(out)(err)
file_rpms_wcnf_L2_V150_C2500_H150_6.wcnf O = 461
T = 8.47
O = 523
T = 3.65
(out)(err)
O = 461
T = 8.47
(out)(err)
file_rpms_wcnf_L2_V150_C2500_H150_7.wcnf O = 434
T = 8.58
O = 549
T = 5.45
(out)(err)
O = 434
T = 8.58
(out)(err)
file_rpms_wcnf_L2_V150_C2500_H150_8.wcnf O = 456
T = 0.87
O = 531
T = 3.51
(out)(err)
O = 456
T = 0.87
(out)(err)
file_rpms_wcnf_L2_V150_C2500_H150_9.wcnf O = 470
T = 7.77
O = 566
T = 2.18
(out)(err)
O = 470
T = 7.77
(out)(err)
file_rpms_wcnf_L2_V150_C3000_H150_0.wcnf O = 539
T = 8.72
O = 694
T = 3.10
(out)(err)
O = 539
T = 8.72
(out)(err)
file_rpms_wcnf_L2_V150_C3000_H150_1.wcnf O = 560
T = 7.14
O = 699
T = 5.55
(out)(err)
O = 560
T = 7.14
(out)(err)
file_rpms_wcnf_L2_V150_C3000_H150_2.wcnf O = 531
T = 1.17
O = 662
T = 5.26
(out)(err)
O = 531
T = 1.17
(out)(err)
file_rpms_wcnf_L2_V150_C3000_H150_3.wcnf O = 555
T = 9.76
O = 652
T = 3.00
(out)(err)
O = 555
T = 9.76
(out)(err)
file_rpms_wcnf_L2_V150_C3000_H150_4.wcnf O = 556
T = 9.52
O = 626
T = 1.98
(out)(err)
O = 556
T = 9.52
(out)(err)
file_rpms_wcnf_L2_V150_C3000_H150_5.wcnf O = 538
T = 6.90
O = 679
T = 3.01
(out)(err)
O = 538
T = 6.90
(out)(err)
file_rpms_wcnf_L2_V150_C3000_H150_6.wcnf O = 537
T = 7.81
O = 663
T = 1.22
(out)(err)
O = 537
T = 7.81
(out)(err)
file_rpms_wcnf_L2_V150_C3000_H150_7.wcnf O = 527
T = 8.10
O = 648
T = 3.27
(out)(err)
O = 527
T = 8.10
(out)(err)
file_rpms_wcnf_L2_V150_C3000_H150_8.wcnf O = 564
T = 3.53
O = 649
T = 2.34
(out)(err)
O = 564
T = 3.53
(out)(err)
file_rpms_wcnf_L2_V150_C3000_H150_9.wcnf O = 552
T = 9.08
O = 652
T = 5.02
(out)(err)
O = 552
T = 9.08
(out)(err)
file_rpms_wcnf_L2_V150_C3500_H150_0.wcnf O = 680
T = 8.12
O = 790
T = 5.60
(out)(err)
O = 680
T = 8.12
(out)(err)
file_rpms_wcnf_L2_V150_C3500_H150_1.wcnf O = 679
T = 8.12
O = 802
T = 5.99
(out)(err)
O = 679
T = 8.12
(out)(err)
file_rpms_wcnf_L2_V150_C3500_H150_2.wcnf O = 716
T = 7.52
O = 796
T = 2.89
(out)(err)
O = 716
T = 7.52
(out)(err)
file_rpms_wcnf_L2_V150_C3500_H150_3.wcnf O = 669
T = 7.33
O = 776
T = 5.11
(out)(err)
O = 669
T = 7.33
(out)(err)
file_rpms_wcnf_L2_V150_C3500_H150_4.wcnf O = 627
T = 6.98
O = 754
T = 3.70
(out)(err)
O = 627
T = 6.98
(out)(err)
file_rpms_wcnf_L2_V150_C3500_H150_5.wcnf O = 667
T = 6.04
O = 809
T = 5.79
(out)(err)
O = 667
T = 6.04
(out)(err)
file_rpms_wcnf_L2_V150_C3500_H150_6.wcnf O = 688
T = 9.18
O = 819
T = 1.99
(out)(err)
O = 688
T = 9.18
(out)(err)
file_rpms_wcnf_L2_V150_C3500_H150_7.wcnf O = 675
T = 7.71
O = 808
T = 3.74
(out)(err)
O = 675
T = 7.71
(out)(err)
file_rpms_wcnf_L2_V150_C3500_H150_8.wcnf O = 675
T = 10.68
O = 823
T = 5.59
(out)(err)
O = 675
T = 10.68
(out)(err)
file_rpms_wcnf_L2_V150_C3500_H150_9.wcnf O = 638
T = 8.71
O = 794
T = 3.57
(out)(err)
O = 638
T = 8.71
(out)(err)
file_rpms_wcnf_L3_V100_C600_H100_0.wcnf O = 8
T = 3.51
O = 15
T = 21.39
(out)(err)
O = 8
T = 3.51
(out)(err)
file_rpms_wcnf_L3_V100_C600_H100_1.wcnf O = 8
T = 3.36
O = 21
T = 4.81
(out)(err)
O = 8
T = 3.36
(out)(err)
file_rpms_wcnf_L3_V100_C600_H100_2.wcnf O = 8
T = 3.03
O = 36
T = 5.14
(out)(err)
O = 8
T = 3.03
(out)(err)
file_rpms_wcnf_L3_V100_C600_H100_3.wcnf O = 9
T = 2.60
O = 35
T = 3.92
(out)(err)
O = 9
T = 2.60
(out)(err)
file_rpms_wcnf_L3_V100_C600_H100_4.wcnf O = 7
T = 3.16
O = 28
T = 4.82
(out)(err)
O = 7
T = 3.16
(out)(err)
file_rpms_wcnf_L3_V100_C600_H100_5.wcnf O = 8
T = 3.99
O = 34
T = 4.32
(out)(err)
O = 8
T = 3.99
(out)(err)
file_rpms_wcnf_L3_V100_C600_H100_6.wcnf O = 7
T = 3.22
O = 15
T = 5.09
(out)(err)
O = 7
T = 3.22
(out)(err)
file_rpms_wcnf_L3_V100_C600_H100_7.wcnf O = 8
T = 3.36
O = 26
T = 2.62
(out)(err)
O = 8
T = 3.36
(out)(err)
file_rpms_wcnf_L3_V100_C600_H100_8.wcnf O = 5
T = 2.23
O = 23
T = 3.75
(out)(err)
O = 5
T = 2.23
(out)(err)
file_rpms_wcnf_L3_V100_C600_H100_9.wcnf O = 9
T = 2.87
O = 41
T = 1.04
(out)(err)
O = 9
T = 2.87
(out)(err)
file_rpms_wcnf_L3_V100_C700_H100_0.wcnf O = 18
T = 2.61
O = 48
T = 2.82
(out)(err)
O = 18
T = 2.61
(out)(err)
file_rpms_wcnf_L3_V100_C700_H100_1.wcnf O = 14
T = 3.23
O = 47
T = 4.43
(out)(err)
O = 14
T = 3.23
(out)(err)
file_rpms_wcnf_L3_V100_C700_H100_2.wcnf O = 15
T = 3.78
O = 42
T = 4.98
(out)(err)
O = 15
T = 3.78
(out)(err)
file_rpms_wcnf_L3_V100_C700_H100_3.wcnf O = 12
T = 3.10
O = 46
T = 5.28
(out)(err)
O = 12
T = 3.10
(out)(err)
file_rpms_wcnf_L3_V100_C700_H100_4.wcnf O = 11
T = 3.98
O = 44
T = 6.46
(out)(err)
O = 11
T = 3.98
(out)(err)
file_rpms_wcnf_L3_V100_C700_H100_5.wcnf O = 14
T = 4.58
O = 50
T = 5.20
(out)(err)
O = 14
T = 4.58
(out)(err)
file_rpms_wcnf_L3_V100_C700_H100_6.wcnf O = 12
T = 3.46
O = 37
T = 3.68
(out)(err)
O = 12
T = 3.46
(out)(err)
file_rpms_wcnf_L3_V100_C700_H100_7.wcnf O = 17
T = 3.45
O = 47
T = 4.56
(out)(err)
O = 17
T = 3.45
(out)(err)
file_rpms_wcnf_L3_V100_C700_H100_8.wcnf O = 16
T = 2.97
O = 48
T = 5.76
(out)(err)
O = 16
T = 2.97
(out)(err)
file_rpms_wcnf_L3_V100_C700_H100_9.wcnf O = 12
T = 3.51
O = 50
T = 5.31
(out)(err)
O = 12
T = 3.51
(out)(err)
file_rpms_wcnf_L3_V100_C800_H100_0.wcnf O = 21
T = 4.22
O = 58
T = 3.57
(out)(err)
O = 21
T = 4.22
(out)(err)
file_rpms_wcnf_L3_V100_C800_H100_1.wcnf O = 21
T = 3.97
O = 62
T = 3.82
(out)(err)
O = 21
T = 3.97
(out)(err)
file_rpms_wcnf_L3_V100_C800_H100_2.wcnf O = 20
T = 0.48
O = 53
T = 2.44
(out)(err)
O = 20
T = 0.48
(out)(err)
file_rpms_wcnf_L3_V100_C800_H100_3.wcnf O = 22
T = 4.13
O = 44
T = 4.53
(out)(err)
O = 22
T = 4.13
(out)(err)
file_rpms_wcnf_L3_V100_C800_H100_4.wcnf O = 18
T = 0.42
O = 61
T = 5.46
(out)(err)
O = 18
T = 0.42
(out)(err)
file_rpms_wcnf_L3_V100_C800_H100_5.wcnf O = 20
T = 3.33
O = 41
T = 8.57
(out)(err)
O = 20
T = 3.33
(out)(err)
file_rpms_wcnf_L3_V100_C800_H100_6.wcnf O = 17
T = 3.48
O = 60
T = 4.78
(out)(err)
O = 17
T = 3.48
(out)(err)
file_rpms_wcnf_L3_V100_C800_H100_7.wcnf O = 23
T = 4.03
O = 50
T = 2.21
(out)(err)
O = 23
T = 4.03
(out)(err)
file_rpms_wcnf_L3_V100_C800_H100_8.wcnf O = 25
T = 3.41
O = 56
T = 1.94
(out)(err)
O = 25
T = 3.41
(out)(err)
file_rpms_wcnf_L3_V100_C800_H100_9.wcnf O = 20
T = 3.72
O = 40
T = 4.97
(out)(err)
O = 20
T = 3.72
(out)(err)