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
s2v100c1200_1.wcnf O = 865
T = 3.36
O = 1246
T = 1.64
(out)(err)
O = 865
T = 3.36
(out)(err)
s2v100c1200_2.wcnf O = 774
T = 1.99
O = 1100
T = 4.57
(out)(err)
O = 774
T = 1.99
(out)(err)
s2v100c1200_3.wcnf O = 933
T = 2.72
O = 1160
T = 4.18
(out)(err)
O = 933
T = 2.72
(out)(err)
s2v100c1200_4.wcnf O = 798
T = 3.37
O = 1214
T = 4.75
(out)(err)
O = 798
T = 3.37
(out)(err)
s2v100c1200_5.wcnf O = 876
T = 0.62
O = 1160
T = 4.81
(out)(err)
O = 876
T = 0.62
(out)(err)
s2v100c1200_6.wcnf O = 734
T = 1.83
O = 1011
T = 4.35
(out)(err)
O = 734
T = 1.83
(out)(err)
s2v100c1200_7.wcnf O = 800
T = 1.09
O = 1120
T = 3.74
(out)(err)
O = 800
T = 1.09
(out)(err)
s2v100c1200_8.wcnf O = 962
T = 0.67
O = 1292
T = 3.31
(out)(err)
O = 962
T = 0.67
(out)(err)
s2v100c1300_1.wcnf O = 971
T = 1.80
O = 1314
T = 5.61
(out)(err)
O = 971
T = 1.80
(out)(err)
s2v100c1300_2.wcnf O = 930
T = 0.93
O = 1313
T = 4.85
(out)(err)
O = 930
T = 0.93
(out)(err)
s2v100c1300_3.wcnf O = 925
T = 0.55
O = 1178
T = 6.79
(out)(err)
O = 925
T = 0.55
(out)(err)
s2v100c1300_4.wcnf O = 970
T = 2.93
O = 1390
T = 4.13
(out)(err)
O = 970
T = 2.93
(out)(err)
s2v100c1300_5.wcnf O = 962
T = 0.67
O = 1258
T = 7.26
(out)(err)
O = 962
T = 0.67
(out)(err)
s2v100c1300_6.wcnf O = 933
T = 1.35
O = 1328
T = 3.77
(out)(err)
O = 933
T = 1.35
(out)(err)
s2v100c1300_7.wcnf O = 877
T = 1.24
O = 1184
T = 6.01
(out)(err)
O = 877
T = 1.24
(out)(err)
s2v100c1300_8.wcnf O = 941
T = 1.13
O = 1250
T = 2.82
(out)(err)
O = 941
T = 1.13
(out)(err)
s2v100c1400_1.wcnf O = 1019
T = 0.46
O = 1346
T = 3.29
(out)(err)
O = 1019
T = 0.46
(out)(err)
s2v100c1400_2.wcnf O = 1002
T = 5.18
O = 1289
T = 4.57
(out)(err)
O = 1002
T = 5.18
(out)(err)
s2v100c1400_3.wcnf O = 1020
T = 5.63
O = 1288
T = 5.72
(out)(err)
O = 1020
T = 5.63
(out)(err)
s2v100c1400_4.wcnf O = 1094
T = 1.06
O = 1409
T = 4.05
(out)(err)
O = 1094
T = 1.06
(out)(err)
s2v100c1400_5.wcnf O = 1018
T = 6.03
O = 1340
T = 3.58
(out)(err)
O = 1018
T = 6.03
(out)(err)
s2v100c1400_6.wcnf O = 997
T = 1.64
O = 1390
T = 5.63
(out)(err)
O = 997
T = 1.64
(out)(err)
s2v100c1400_7.wcnf O = 1001
T = 4.60
O = 1329
T = 4.12
(out)(err)
O = 1001
T = 4.60
(out)(err)
s2v100c1400_8.wcnf O = 1084
T = 5.51
O = 1334
T = 3.52
(out)(err)
O = 1084
T = 5.51
(out)(err)
s2v100c1500_1.wcnf O = 1077
T = 4.79
O = 1409
T = 6.52
(out)(err)
O = 1077
T = 4.79
(out)(err)
s2v100c1500_2.wcnf O = 1125
T = 5.65
O = 1456
T = 3.01
(out)(err)
O = 1125
T = 5.65
(out)(err)
s2v100c1500_3.wcnf O = 1151
T = 1.04
O = 1378
T = 5.39
(out)(err)
O = 1151
T = 1.04
(out)(err)
s2v100c1500_4.wcnf O = 1072
T = 0.41
O = 1430
T = 3.88
(out)(err)
O = 1072
T = 0.41
(out)(err)
s2v100c1500_5.wcnf O = 1151
T = 1.53
O = 1434
T = 4.56
(out)(err)
O = 1151
T = 1.53
(out)(err)
s2v100c1500_6.wcnf O = 1225
T = 4.79
O = 1624
T = 1.67
(out)(err)
O = 1225
T = 4.79
(out)(err)
s2v100c1500_7.wcnf O = 1186
T = 4.96
O = 1577
T = 4.55
(out)(err)
O = 1186
T = 4.96
(out)(err)
s2v100c1500_8.wcnf O = 1217
T = 0.58
O = 1512
T = 2.42
(out)(err)
O = 1217
T = 0.58
(out)(err)
s2v100c1600_1.wcnf O = 1230
T = 1.14
O = 1612
T = 3.92
(out)(err)
O = 1230
T = 1.14
(out)(err)
s2v100c1600_2.wcnf O = 1265
T = 0.95
O = 1534
T = 2.14
(out)(err)
O = 1265
T = 0.95
(out)(err)
s2v100c1600_3.wcnf O = 1309
T = 0.79
O = 1657
T = 5.48
(out)(err)
O = 1309
T = 0.79
(out)(err)
s2v100c1600_4.wcnf O = 1267
T = 1.08
O = 1693
T = 4.49
(out)(err)
O = 1267
T = 1.08
(out)(err)
s2v100c1600_5.wcnf O = 1298
T = 0.52
O = 1711
T = 4.62
(out)(err)
O = 1298
T = 0.52
(out)(err)
s2v100c1600_6.wcnf O = 1190
T = 0.72
O = 1751
T = 3.27
(out)(err)
O = 1190
T = 0.72
(out)(err)
s2v100c1600_7.wcnf O = 1243
T = 1.35
O = 1584
T = 3.81
(out)(err)
O = 1243
T = 1.35
(out)(err)
s2v100c1600_8.wcnf O = 1184
T = 1.04
O = 1648
T = 4.51
(out)(err)
O = 1184
T = 1.04
(out)(err)
s2v120c1200_1.wcnf O = 840
T = 5.00
O = 1067
T = 4.40
(out)(err)
O = 840
T = 5.00
(out)(err)
s2v120c1200_2.wcnf O = 803
T = 5.60
O = 1067
T = 1.70
(out)(err)
O = 803
T = 5.60
(out)(err)
s2v120c1200_3.wcnf O = 834
T = 6.70
O = 1186
T = 6.48
(out)(err)
O = 834
T = 6.70
(out)(err)
s2v120c1200_4.wcnf O = 811
T = 4.24
O = 1207
T = 2.33
(out)(err)
O = 811
T = 4.24
(out)(err)
s2v120c1200_5.wcnf O = 850
T = 1.52
O = 1074
T = 5.58
(out)(err)
O = 850
T = 1.52
(out)(err)
s2v120c1200_6.wcnf O = 784
T = 5.25
O = 1047
T = 3.39
(out)(err)
O = 784
T = 5.25
(out)(err)
s2v120c1200_7.wcnf O = 747
T = 4.77
O = 1055
T = 5.48
(out)(err)
O = 747
T = 4.77
(out)(err)
s2v120c1200_8.wcnf O = 813
T = 5.23
O = 1230
T = 5.59
(out)(err)
O = 813
T = 5.23
(out)(err)
s2v120c1300_1.wcnf O = 890
T = 4.59
O = 1096
T = 3.68
(out)(err)
O = 890
T = 4.59
(out)(err)
s2v120c1300_2.wcnf O = 847
T = 3.94
O = 1099
T = 4.11
(out)(err)
O = 847
T = 3.94
(out)(err)
s2v120c1300_3.wcnf O = 941
T = 5.53
O = 1338
T = 8.19
(out)(err)
O = 941
T = 5.53
(out)(err)
s2v120c1300_4.wcnf O = 939
T = 4.87
O = 1256
T = 2.31
(out)(err)
O = 939
T = 4.87
(out)(err)
s2v120c1300_5.wcnf O = 949
T = 5.37
O = 1475
T = 2.85
(out)(err)
O = 949
T = 5.37
(out)(err)
s2v120c1300_6.wcnf O = 865
T = 5.58
O = 1192
T = 6.26
(out)(err)
O = 865
T = 5.58
(out)(err)
s2v120c1300_7.wcnf O = 879
T = 5.06
O = 1155
T = 1.42
(out)(err)
O = 879
T = 5.06
(out)(err)
s2v120c1300_8.wcnf O = 868
T = 6.11
O = 1188
T = 2.31
(out)(err)
O = 868
T = 6.11
(out)(err)
s2v120c1400_1.wcnf O = 1028
T = 6.60
O = 1283
T = 6.11
(out)(err)
O = 1028
T = 6.60
(out)(err)
s2v120c1400_2.wcnf O = 1008
T = 5.61
O = 1395
T = 2.42
(out)(err)
O = 1008
T = 5.61
(out)(err)
s2v120c1400_3.wcnf O = 983
T = 5.30
O = 1339
T = 4.83
(out)(err)
O = 983
T = 5.30
(out)(err)
s2v120c1400_4.wcnf O = 1007
T = 6.18
O = 1234
T = 2.40
(out)(err)
O = 1007
T = 6.18
(out)(err)
s2v120c1400_5.wcnf O = 1108
T = 6.44
O = 1494
T = 5.90
(out)(err)
O = 1108
T = 6.44
(out)(err)
s2v120c1400_6.wcnf O = 959
T = 2.06
O = 1359
T = 4.45
(out)(err)
O = 959
T = 2.06
(out)(err)
s2v120c1400_7.wcnf O = 1040
T = 2.21
O = 1404
T = 1.78
(out)(err)
O = 1040
T = 2.21
(out)(err)
s2v120c1400_8.wcnf O = 1025
T = 5.20
O = 1418
T = 4.02
(out)(err)
O = 1025
T = 5.20
(out)(err)
s2v120c1500_1.wcnf O = 1119
T = 1.16
O = 1512
T = 4.97
(out)(err)
O = 1119
T = 1.16
(out)(err)
s2v120c1500_2.wcnf O = 1136
T = 0.82
O = 1527
T = 5.15
(out)(err)
O = 1136
T = 0.82
(out)(err)
s2v120c1500_3.wcnf O = 1062
T = 5.59
O = 1329
T = 1.76
(out)(err)
O = 1062
T = 5.59
(out)(err)
s2v120c1500_4.wcnf O = 1041
T = 4.79
O = 1418
T = 2.42
(out)(err)
O = 1041
T = 4.79
(out)(err)
s2v120c1500_5.wcnf O = 1125
T = 0.96
O = 1557
T = 0.70
(out)(err)
O = 1125
T = 0.96
(out)(err)
s2v120c1500_6.wcnf O = 1113
T = 6.33
O = 1500
T = 5.12
(out)(err)
O = 1113
T = 6.33
(out)(err)
s2v120c1500_7.wcnf O = 1163
T = 6.37
O = 1501
T = 4.88
(out)(err)
O = 1163
T = 6.37
(out)(err)
s2v120c1500_8.wcnf O = 1097
T = 4.68
O = 1649
T = 3.87
(out)(err)
O = 1097
T = 4.68
(out)(err)
s2v120c1600_1.wcnf O = 1190
T = 5.34
O = 1544
T = 3.78
(out)(err)
O = 1190
T = 5.34
(out)(err)
s2v120c1600_2.wcnf O = 1227
T = 5.91
O = 1672
T = 1.20
(out)(err)
O = 1227
T = 5.91
(out)(err)
s2v120c1600_3.wcnf O = 1224
T = 1.19
O = 1672
T = 4.29
(out)(err)
O = 1224
T = 1.19
(out)(err)
s2v120c1600_4.wcnf O = 1264
T = 5.62
O = 1782
T = 2.99
(out)(err)
O = 1264
T = 5.62
(out)(err)
s2v120c1600_5.wcnf O = 1252
T = 3.86
O = 1597
T = 2.72
(out)(err)
O = 1252
T = 3.86
(out)(err)
s2v120c1600_6.wcnf O = 1246
T = 4.82
O = 1592
T = 8.60
(out)(err)
O = 1246
T = 4.82
(out)(err)
s2v120c1600_7.wcnf O = 1159
T = 4.21
O = 1588
T = 3.73
(out)(err)
O = 1159
T = 4.21
(out)(err)
s2v120c1600_8.wcnf O = 1150
T = 6.58
O = 1592
T = 4.96
(out)(err)
O = 1150
T = 6.58
(out)(err)
s2v140c1200_1.wcnf O = 780
T = 5.74
O = 1052
T = 4.65
(out)(err)
O = 780
T = 5.74
(out)(err)
s2v140c1200_2.wcnf O = 733
T = 0.83
O = 1188
T = 6.68
(out)(err)
O = 733
T = 0.83
(out)(err)
s2v140c1200_3.wcnf O = 741
T = 6.09
O = 1014
T = 5.29
(out)(err)
O = 741
T = 6.09
(out)(err)
s2v140c1200_4.wcnf O = 667
T = 5.55
O = 1113
T = 6.68
(out)(err)
O = 667
T = 5.55
(out)(err)
s2v140c1200_5.wcnf O = 714
T = 4.79
O = 995
T = 4.83
(out)(err)
O = 714
T = 4.79
(out)(err)
s2v140c1200_6.wcnf O = 803
T = 0.94
O = 1199
T = 3.55
(out)(err)
O = 803
T = 0.94
(out)(err)
s2v140c1200_7.wcnf O = 774
T = 8.06
O = 1000
T = 4.25
(out)(err)
O = 774
T = 8.06
(out)(err)
s2v140c1200_8.wcnf O = 745
T = 1.57
O = 1006
T = 5.04
(out)(err)
O = 745
T = 1.57
(out)(err)
s2v140c1300_1.wcnf O = 846
T = 5.43
O = 1131
T = 4.62
(out)(err)
O = 846
T = 5.43
(out)(err)
s2v140c1300_2.wcnf O = 774
T = 6.51
O = 1096
T = 3.14
(out)(err)
O = 774
T = 6.51
(out)(err)
s2v140c1300_3.wcnf O = 832
T = 5.38
O = 1029
T = 1.82
(out)(err)
O = 832
T = 5.38
(out)(err)
s2v140c1300_4.wcnf O = 871
T = 0.92
O = 1132
T = 2.08
(out)(err)
O = 871
T = 0.92
(out)(err)
s2v140c1300_5.wcnf O = 844
T = 7.31
O = 1224
T = 8.59
(out)(err)
O = 844
T = 7.31
(out)(err)
s2v140c1300_6.wcnf O = 884
T = 6.36
O = 1232
T = 5.79
(out)(err)
O = 884
T = 6.36
(out)(err)
s2v140c1300_7.wcnf O = 874
T = 5.73
O = 1099
T = 3.23
(out)(err)
O = 874
T = 5.73
(out)(err)
s2v140c1300_8.wcnf O = 812
T = 0.77
O = 1035
T = 3.69
(out)(err)
O = 812
T = 0.77
(out)(err)
s2v140c1400_1.wcnf O = 926
T = 5.62
O = 1297
T = 3.16
(out)(err)
O = 926
T = 5.62
(out)(err)
s2v140c1400_2.wcnf O = 879
T = 7.91
O = 1190
T = 1.71
(out)(err)
O = 879
T = 7.91
(out)(err)
s2v140c1400_3.wcnf O = 936
T = 5.22
O = 1236
T = 2.20
(out)(err)
O = 936
T = 5.22
(out)(err)
s2v140c1400_4.wcnf O = 932
T = 6.38
O = 1286
T = 4.20
(out)(err)
O = 932
T = 6.38
(out)(err)
s2v140c1400_5.wcnf O = 968
T = 5.88
O = 1537
T = 7.84
(out)(err)
O = 968
T = 5.88
(out)(err)
s2v140c1400_6.wcnf O = 967
T = 5.62
O = 1330
T = 5.36
(out)(err)
O = 967
T = 5.62
(out)(err)
s2v140c1400_7.wcnf O = 923
T = 0.40
O = 1221
T = 1.94
(out)(err)
O = 923
T = 0.40
(out)(err)
s2v140c1400_8.wcnf O = 957
T = 6.06
O = 1224
T = 5.96
(out)(err)
O = 957
T = 6.06
(out)(err)
s2v140c1500_1.wcnf O = 986
T = 6.13
O = 1332
T = 2.47
(out)(err)
O = 986
T = 6.13
(out)(err)
s2v140c1500_2.wcnf O = 998
T = 6.75
O = 1384
T = 2.19
(out)(err)
O = 998
T = 6.75
(out)(err)
s2v140c1500_3.wcnf O = 1073
T = 5.61
O = 1380
T = 2.94
(out)(err)
O = 1073
T = 5.61
(out)(err)
s2v140c1500_4.wcnf O = 1047
T = 6.26
O = 1374
T = 4.73
(out)(err)
O = 1047
T = 6.26
(out)(err)
s2v140c1500_5.wcnf O = 1058
T = 6.29
O = 1356
T = 2.97
(out)(err)
O = 1058
T = 6.29
(out)(err)
s2v140c1500_6.wcnf O = 1102
T = 6.26
O = 1427
T = 5.68
(out)(err)
O = 1102
T = 6.26
(out)(err)
s2v140c1500_7.wcnf O = 1010
T = 6.54
O = 1334
T = 4.22
(out)(err)
O = 1010
T = 6.54
(out)(err)
s2v140c1500_8.wcnf O = 1045
T = 7.05
O = 1472
T = 4.56
(out)(err)
O = 1045
T = 7.05
(out)(err)
s2v140c1600_1.wcnf O = 1143
T = 6.27
O = 1622
T = 5.92
(out)(err)
O = 1143
T = 6.27
(out)(err)
s2v140c1600_2.wcnf O = 1140
T = 1.18
O = 1439
T = 1.51
(out)(err)
O = 1140
T = 1.18
(out)(err)
s2v140c1600_3.wcnf O = 1079
T = 5.99
O = 1395
T = 3.90
(out)(err)
O = 1079
T = 5.99
(out)(err)
s2v140c1600_4.wcnf O = 1157
T = 4.70
O = 1606
T = 6.62
(out)(err)
O = 1157
T = 4.70
(out)(err)
s2v140c1600_5.wcnf O = 1119
T = 6.32
O = 1563
T = 6.00
(out)(err)
O = 1119
T = 6.32
(out)(err)
s2v140c1600_6.wcnf O = 1212
T = 7.42
O = 1628
T = 4.82
(out)(err)
O = 1212
T = 7.42
(out)(err)
s2v140c1600_7.wcnf O = 1150
T = 7.50
O = 1698
T = 4.08
(out)(err)
O = 1150
T = 7.50
(out)(err)
s2v140c1600_8.wcnf O = 1180
T = 5.30
O = 1526
T = 4.03
(out)(err)
O = 1180
T = 5.30
(out)(err)
file_rwms_wcnf_L3_V70_C1000_0.wcnf O = 198
T = 3.75
O = 331
T = 3.24
(out)(err)
O = 198
T = 3.75
(out)(err)
file_rwms_wcnf_L3_V70_C1000_1.wcnf O = 212
T = 5.12
O = 356
T = 3.99
(out)(err)
O = 212
T = 5.12
(out)(err)
file_rwms_wcnf_L3_V70_C1000_2.wcnf O = 211
T = 4.31
O = 334
T = 4.76
(out)(err)
O = 211
T = 4.31
(out)(err)
file_rwms_wcnf_L3_V70_C1000_3.wcnf O = 229
T = 4.42
O = 338
T = 7.66
(out)(err)
O = 229
T = 4.42
(out)(err)
file_rwms_wcnf_L3_V70_C1000_4.wcnf O = 202
T = 3.58
O = 557
T = 5.40
(out)(err)
O = 202
T = 3.58
(out)(err)
file_rwms_wcnf_L3_V70_C1000_5.wcnf O = 214
T = 4.38
O = 371
T = 5.96
(out)(err)
O = 214
T = 4.38
(out)(err)
file_rwms_wcnf_L3_V70_C1000_6.wcnf O = 203
T = 4.47
O = 402
T = 4.66
(out)(err)
O = 203
T = 4.47
(out)(err)
file_rwms_wcnf_L3_V70_C1000_7.wcnf O = 200
T = 4.43
O = 221
T = 5.64
(out)(err)
O = 200
T = 4.43
(out)(err)
file_rwms_wcnf_L3_V70_C1000_8.wcnf O = 188
T = 4.16
O = 386
T = 1.71
(out)(err)
O = 188
T = 4.16
(out)(err)
file_rwms_wcnf_L3_V70_C1000_9.wcnf O = 226
T = 3.02
O = 369
T = 5.72
(out)(err)
O = 226
T = 3.02
(out)(err)
file_rwms_wcnf_L3_V70_C700_0.wcnf O = 103
T = 2.13
O = 301
T = 5.96
(out)(err)
O = 103
T = 2.13
(out)(err)
file_rwms_wcnf_L3_V70_C700_1.wcnf O = 107
T = 3.30
O = 169
T = 3.52
(out)(err)
O = 107
T = 3.30
(out)(err)
file_rwms_wcnf_L3_V70_C700_2.wcnf O = 110
T = 4.01
O = 159
T = 3.41
(out)(err)
O = 110
T = 4.01
(out)(err)
file_rwms_wcnf_L3_V70_C700_3.wcnf O = 102
T = 3.81
O = 211
T = 3.93
(out)(err)
O = 102
T = 3.81
(out)(err)
file_rwms_wcnf_L3_V70_C700_4.wcnf O = 110
T = 3.80
O = 152
T = 7.55
(out)(err)
O = 110
T = 3.80
(out)(err)
file_rwms_wcnf_L3_V70_C700_5.wcnf O = 103
T = 2.97
O = 221
T = 4.42
(out)(err)
O = 103
T = 2.97
(out)(err)
file_rwms_wcnf_L3_V70_C700_6.wcnf O = 102
T = 3.91
O = 137
T = 5.27
(out)(err)
O = 102
T = 3.91
(out)(err)
file_rwms_wcnf_L3_V70_C700_7.wcnf O = 104
T = 3.49
O = 258
T = 3.33
(out)(err)
O = 104
T = 3.49
(out)(err)
file_rwms_wcnf_L3_V70_C700_8.wcnf O = 82
T = 4.03
O = 300
T = 4.07
(out)(err)
O = 82
T = 4.03
(out)(err)
file_rwms_wcnf_L3_V70_C700_9.wcnf O = 104
T = 3.19
O = 243
T = 5.26
(out)(err)
O = 104
T = 3.19
(out)(err)
file_rwms_wcnf_L3_V70_C800_0.wcnf O = 132
T = 3.72
O = 381
T = 5.40
(out)(err)
O = 132
T = 3.72
(out)(err)
file_rwms_wcnf_L3_V70_C800_1.wcnf O = 138
T = 3.30
O = 183
T = 3.97
(out)(err)
O = 138
T = 3.30
(out)(err)
file_rwms_wcnf_L3_V70_C800_2.wcnf O = 127
T = 2.55
O = 372
T = 3.34
(out)(err)
O = 127
T = 2.55
(out)(err)
file_rwms_wcnf_L3_V70_C800_3.wcnf O = 134
T = 3.47
O = 290
T = 7.08
(out)(err)
O = 134
T = 3.47
(out)(err)
file_rwms_wcnf_L3_V70_C800_4.wcnf O = 143
T = 0.40
O = 380
T = 4.02
(out)(err)
O = 143
T = 0.40
(out)(err)
file_rwms_wcnf_L3_V70_C800_5.wcnf O = 144
T = 2.50
O = 252
T = 3.79
(out)(err)
O = 144
T = 2.50
(out)(err)
file_rwms_wcnf_L3_V70_C800_6.wcnf O = 135
T = 3.62
O = 350
T = 3.82
(out)(err)
O = 135
T = 3.62
(out)(err)
file_rwms_wcnf_L3_V70_C800_7.wcnf O = 147
T = 2.49
O = 232
T = 6.16
(out)(err)
O = 147
T = 2.49
(out)(err)
file_rwms_wcnf_L3_V70_C800_8.wcnf O = 126
T = 2.70
O = 373
T = 1.61
(out)(err)
O = 126
T = 2.70
(out)(err)
file_rwms_wcnf_L3_V70_C800_9.wcnf O = 138
T = 4.35
O = 363
T = 4.37
(out)(err)
O = 138
T = 4.35
(out)(err)
file_rwms_wcnf_L3_V70_C900_0.wcnf O = 157
T = 3.15
O = 293
T = 7.53
(out)(err)
O = 157
T = 3.15
(out)(err)
file_rwms_wcnf_L3_V70_C900_1.wcnf O = 192
T = 4.32
O = 243
T = 9.15
(out)(err)
O = 192
T = 4.32
(out)(err)
file_rwms_wcnf_L3_V70_C900_2.wcnf O = 177
T = 2.85
O = 211
T = 5.84
(out)(err)
O = 177
T = 2.85
(out)(err)
file_rwms_wcnf_L3_V70_C900_3.wcnf O = 163
T = 1.45
O = 242
T = 5.55
(out)(err)
O = 163
T = 1.45
(out)(err)
file_rwms_wcnf_L3_V70_C900_4.wcnf O = 171
T = 1.88
O = 385
T = 5.35
(out)(err)
O = 171
T = 1.88
(out)(err)
file_rwms_wcnf_L3_V70_C900_5.wcnf O = 175
T = 3.37
O = 377
T = 5.45
(out)(err)
O = 175
T = 3.37
(out)(err)
file_rwms_wcnf_L3_V70_C900_6.wcnf O = 174
T = 3.81
O = 412
T = 4.05
(out)(err)
O = 174
T = 3.81
(out)(err)
file_rwms_wcnf_L3_V70_C900_7.wcnf O = 194
T = 3.87
O = 271
T = 10.84
(out)(err)
O = 194
T = 3.87
(out)(err)
file_rwms_wcnf_L3_V70_C900_8.wcnf O = 179
T = 1.85
O = 244
T = 5.63
(out)(err)
O = 179
T = 1.85
(out)(err)
file_rwms_wcnf_L3_V70_C900_9.wcnf O = 181
T = 2.87
O = 415
T = 4.32
(out)(err)
O = 181
T = 2.87
(out)(err)