Benchmark

Label	Meaning
S	Solution {OPTIMUM FOUND or OPT \| UNSATISFIABLE or UNSAT \| UNKNOWN \| Not available or N/A}
O	Best solution found
T	CPU time (TO for Time Out)
(out)(err)	Standard output and standard error for each solver

Color	Meaning for Complete Solvers	Meaning for Incomplete Solvers
Text	Best solver column	Best solver column
Text	Optimal solution with the best CPU time	Best solution with the best CPU time
Text	Optimal solution and finished within the Time Out	Best solution without the best CPU time
Text	Optimal solution and did not finish within the Time Out	Solution found but not the best
Text	Time Out	Time Out
Text	Buggy solution	Buggy solution

Instance file name	Best solver	ISAC+-2016-co
s2v120c1200_1.wcnf	S = OPT O = 840 T = 21.62	S = OPT O = 840 T = 21.62
s2v120c1200_2.wcnf	S = OPT O = 803 T = 10.06	S = OPT O = 803 T = 10.06
s2v120c1200_3.wcnf	S = OPT O = 834 T = 14.17	S = OPT O = 834 T = 14.17
s2v120c1200_4.wcnf	S = OPT O = 811 T = 12.54	S = OPT O = 811 T = 12.54
s2v120c1200_5.wcnf	S = OPT O = 850 T = 28.58	S = OPT O = 850 T = 28.58
s2v120c1200_6.wcnf	S = OPT O = 784 T = 15.56	S = OPT O = 784 T = 15.56
s2v120c1200_7.wcnf	S = OPT O = 747 T = 8.45	S = OPT O = 747 T = 8.45
s2v120c1200_8.wcnf	S = OPT O = 813 T = 12.87	S = OPT O = 813 T = 12.87
s2v120c1300_1.wcnf	S = OPT O = 890 T = 10.99	S = OPT O = 890 T = 10.99
s2v120c1300_2.wcnf	S = OPT O = 847 T = 9.04	S = OPT O = 847 T = 9.04
s2v120c1300_3.wcnf	S = OPT O = 941 T = 11.99	S = OPT O = 941 T = 11.99
s2v120c1300_4.wcnf	S = OPT O = 939 T = 16.68	S = OPT O = 939 T = 16.68
s2v120c1300_5.wcnf	S = OPT O = 949 T = 30.57	S = OPT O = 949 T = 30.57
s2v120c1300_6.wcnf	S = OPT O = 865 T = 9.69	S = OPT O = 865 T = 9.69
s2v120c1300_7.wcnf	S = OPT O = 879 T = 9.49	S = OPT O = 879 T = 9.49
s2v120c1300_8.wcnf	S = OPT O = 868 T = 12.60	S = OPT O = 868 T = 12.60
s2v120c1400_1.wcnf	S = OPT O = 1028 T = 20.00	S = OPT O = 1028 T = 20.00
s2v120c1400_2.wcnf	S = OPT O = 1008 T = 24.32	S = OPT O = 1008 T = 24.32
s2v120c1400_3.wcnf	S = OPT O = 983 T = 10.56	S = OPT O = 983 T = 10.56
s2v120c1400_4.wcnf	S = OPT O = 1007 T = 31.64	S = OPT O = 1007 T = 31.64
s2v120c1400_5.wcnf	S = OPT O = 1108 T = 155.38	S = OPT O = 1108 T = 155.38
s2v120c1400_6.wcnf	S = OPT O = 959 T = 12.40	S = OPT O = 959 T = 12.40
s2v120c1400_7.wcnf	S = OPT O = 1040 T = 35.14	S = OPT O = 1040 T = 35.14
s2v120c1400_8.wcnf	S = OPT O = 1025 T = 28.80	S = OPT O = 1025 T = 28.80
s2v120c1500_1.wcnf	S = OPT O = 1119 T = 29.16	S = OPT O = 1119 T = 29.16
s2v120c1500_2.wcnf	S = OPT O = 1136 T = 36.86	S = OPT O = 1136 T = 36.86
s2v120c1500_3.wcnf	S = OPT O = 1062 T = 12.96	S = OPT O = 1062 T = 12.96
s2v120c1500_4.wcnf	S = OPT O = 1041 T = 10.06	S = OPT O = 1041 T = 10.06
s2v120c1500_5.wcnf	S = OPT O = 1125 T = 11.48	S = OPT O = 1125 T = 11.48
s2v120c1500_6.wcnf	S = OPT O = 1113 T = 27.52	S = OPT O = 1113 T = 27.52
s2v120c1500_7.wcnf	S = OPT O = 1163 T = 64.63	S = OPT O = 1163 T = 64.63
s2v120c1500_8.wcnf	S = OPT O = 1097 T = 10.65	S = OPT O = 1097 T = 10.65
s2v120c1600_1.wcnf	S = OPT O = 1190 T = 13.85	S = OPT O = 1190 T = 13.85
s2v120c1600_2.wcnf	S = OPT O = 1227 T = 53.22	S = OPT O = 1227 T = 53.22
s2v120c1600_3.wcnf	S = OPT O = 1224 T = 44.09	S = OPT O = 1224 T = 44.09
s2v120c1600_4.wcnf	S = OPT O = 1264 T = 101.57	S = OPT O = 1264 T = 101.57
s2v120c1600_5.wcnf	S = OPT O = 1252 T = 47.01	S = OPT O = 1252 T = 47.01
s2v120c1600_6.wcnf	S = OPT O = 1246 T = 23.30	S = OPT O = 1246 T = 23.30
s2v120c1600_7.wcnf	S = OPT O = 1159 T = 13.19	S = OPT O = 1159 T = 13.19
s2v120c1600_8.wcnf	S = OPT O = 1150 T = 9.64	S = OPT O = 1150 T = 9.64
s2v120c1700-1.wcnf	S = OPT O = 1261 T = 11.89	S = OPT O = 1261 T = 11.89
s2v120c1800-1.wcnf	S = OPT O = 1428 T = 95.63	S = OPT O = 1428 T = 95.63
s2v120c1900-1.wcnf	S = OPT O = 1544 T = 183.42	S = OPT O = 1544 T = 183.42
s2v120c2000-1.wcnf	S = OPT O = 1552 T = 21.71	S = OPT O = 1552 T = 21.71
s2v120c2100-1.wcnf	S = OPT O = 1726 T = 38.96	S = OPT O = 1726 T = 38.96
s2v120c2200-1.wcnf	S = OPT O = 1827 T = 111.56	S = OPT O = 1827 T = 111.56
s2v120c2300-1.wcnf	S = OPT O = 1967 T = 175.91	S = OPT O = 1967 T = 175.91
s2v120c2400-1.wcnf	S = OPT O = 2014 T = 254.93	S = OPT O = 2014 T = 254.93
s2v120c2500-1.wcnf	S = OPT O = 2211 T = 260.99	S = OPT O = 2211 T = 260.99
s2v120c2600-1.wcnf	S = OPT O = 2209 T = 45.00	S = OPT O = 2209 T = 45.00
s2v140c1200_1.wcnf	S = OPT O = 780 T = 37.88	S = OPT O = 780 T = 37.88
s2v140c1200_2.wcnf	S = OPT O = 733 T = 20.98	S = OPT O = 733 T = 20.98
s2v140c1200_3.wcnf	S = OPT O = 741 T = 22.18	S = OPT O = 741 T = 22.18
s2v140c1200_4.wcnf	S = OPT O = 667 T = 7.55	S = OPT O = 667 T = 7.55
s2v140c1200_5.wcnf	S = OPT O = 714 T = 13.82	S = OPT O = 714 T = 13.82
s2v140c1200_6.wcnf	S = OPT O = 803 T = 73.16	S = OPT O = 803 T = 73.16
s2v140c1200_7.wcnf	S = OPT O = 774 T = 83.56	S = OPT O = 774 T = 83.56
s2v140c1200_8.wcnf	S = OPT O = 745 T = 34.06	S = OPT O = 745 T = 34.06
s2v140c1300_1.wcnf	S = OPT O = 846 T = 29.99	S = OPT O = 846 T = 29.99
s2v140c1300_2.wcnf	S = OPT O = 774 T = 8.98	S = OPT O = 774 T = 8.98
s2v140c1300_3.wcnf	S = OPT O = 832 T = 22.81	S = OPT O = 832 T = 22.81
s2v140c1300_4.wcnf	S = OPT O = 871 T = 110.50	S = OPT O = 871 T = 110.50
s2v140c1300_5.wcnf	S = OPT O = 844 T = 36.35	S = OPT O = 844 T = 36.35
s2v140c1300_6.wcnf	S = OPT O = 884 T = 181.81	S = OPT O = 884 T = 181.81
s2v140c1300_7.wcnf	S = OPT O = 874 T = 55.19	S = OPT O = 874 T = 55.19
s2v140c1300_8.wcnf	S = OPT O = 812 T = 50.06	S = OPT O = 812 T = 50.06
s2v140c1400_1.wcnf	S = OPT O = 926 T = 56.77	S = OPT O = 926 T = 56.77
s2v140c1400_2.wcnf	S = OPT O = 879 T = 24.15	S = OPT O = 879 T = 24.15
s2v140c1400_3.wcnf	S = OPT O = 936 T = 51.82	S = OPT O = 936 T = 51.82
s2v140c1400_4.wcnf	S = OPT O = 932 T = 28.10	S = OPT O = 932 T = 28.10
s2v140c1400_5.wcnf	S = OPT O = 968 T = 64.82	S = OPT O = 968 T = 64.82
s2v140c1400_6.wcnf	S = OPT O = 967 T = 178.71	S = OPT O = 967 T = 178.71
s2v140c1400_7.wcnf	S = OPT O = 923 T = 23.05	S = OPT O = 923 T = 23.05
s2v140c1400_8.wcnf	S = OPT O = 957 T = 83.11	S = OPT O = 957 T = 83.11
s2v140c1500_1.wcnf	S = OPT O = 986 T = 33.42	S = OPT O = 986 T = 33.42
s2v140c1500_2.wcnf	S = OPT O = 998 T = 43.43	S = OPT O = 998 T = 43.43
s2v140c1500_3.wcnf	S = OPT O = 1073 T = 187.88	S = OPT O = 1073 T = 187.88
s2v140c1500_4.wcnf	S = OPT O = 1047 T = 173.72	S = OPT O = 1047 T = 173.72
s2v140c1500_5.wcnf	S = OPT O = 1058 T = 107.99	S = OPT O = 1058 T = 107.99
s2v140c1500_6.wcnf	S = OPT O = 1102 T = 342.77	S = OPT O = 1102 T = 342.77
s2v140c1500_7.wcnf	S = OPT O = 1010 T = 26.72	S = OPT O = 1010 T = 26.72
s2v140c1500_8.wcnf	S = OPT O = 1045 T = 63.12	S = OPT O = 1045 T = 63.12
s2v140c1600_1.wcnf	S = OPT O = 1143 T = 40.82	S = OPT O = 1143 T = 40.82
s2v140c1600_2.wcnf	S = OPT O = 1140 T = 37.38	S = OPT O = 1140 T = 37.38
s2v140c1600_3.wcnf	S = OPT O = 1079 T = 39.77	S = OPT O = 1079 T = 39.77
s2v140c1600_4.wcnf	S = OPT O = 1157 T = 104.59	S = OPT O = 1157 T = 104.59
s2v140c1600_5.wcnf	S = OPT O = 1119 T = 92.77	S = OPT O = 1119 T = 92.77
s2v140c1600_6.wcnf	S = OPT O = 1212 T = 219.29	S = OPT O = 1212 T = 219.29
s2v140c1600_7.wcnf	S = OPT O = 1150 T = 91.84	S = OPT O = 1150 T = 91.84
s2v140c1600_8.wcnf	S = OPT O = 1180 T = 82.21	S = OPT O = 1180 T = 82.21
s2v140c1700-1.wcnf	S = OPT O = 1188 T = 103.33	S = OPT O = 1188 T = 103.33
s2v140c1800-1.wcnf	S = OPT O = 1282 T = 62.10	S = OPT O = 1282 T = 62.10
s2v140c1900-1.wcnf	S = OPT O = 1312 T = 20.78	S = OPT O = 1312 T = 20.78
s2v140c2000-1.wcnf	S = OPT O = 1574 T = 402.45	S = OPT O = 1574 T = 402.45
s2v140c2100-1.wcnf	S = OPT O = 1674 T = 666.89	S = OPT O = 1674 T = 666.89
s2v140c2200-1.wcnf	S = OPT O = 1771 T = 741.91	S = OPT O = 1771 T = 741.91
s2v140c2300-1.wcnf	S = OPT O = 1833 T = 193.18	S = OPT O = 1833 T = 193.18
s2v140c2400-1.wcnf	S = OPT O = 1942 T = 952.09	S = OPT O = 1942 T = 952.09
s2v140c2500-1.wcnf	S = OPT O = 2044 T = 1269.19	S = OPT O = 2044 T = 1269.19
s2v140c2600-1.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v160c1200-1.wcnf	S = OPT O = 653 T = 10.78	S = OPT O = 653 T = 10.78
s2v160c1200-2.wcnf	S = OPT O = 669 T = 15.41	S = OPT O = 669 T = 15.41
s2v160c1200-3.wcnf	S = OPT O = 666 T = 37.09	S = OPT O = 666 T = 37.09
s2v160c1300-1.wcnf	S = OPT O = 759 T = 37.60	S = OPT O = 759 T = 37.60
s2v160c1300-2.wcnf	S = OPT O = 753 T = 24.48	S = OPT O = 753 T = 24.48
s2v160c1300-3.wcnf	S = OPT O = 783 T = 66.40	S = OPT O = 783 T = 66.40
s2v160c1400-1.wcnf	S = OPT O = 808 T = 16.59	S = OPT O = 808 T = 16.59
s2v160c1400-2.wcnf	S = OPT O = 811 T = 53.74	S = OPT O = 811 T = 53.74
s2v160c1400-3.wcnf	S = OPT O = 888 T = 243.37	S = OPT O = 888 T = 243.37
s2v160c1500-1.wcnf	S = OPT O = 929 T = 22.50	S = OPT O = 929 T = 22.50
s2v160c1500-2.wcnf	S = OPT O = 896 T = 27.18	S = OPT O = 896 T = 27.18
s2v160c1500-3.wcnf	S = OPT O = 961 T = 436.29	S = OPT O = 961 T = 436.29
s2v160c1600-1.wcnf	S = OPT O = 1096 T = 343.16	S = OPT O = 1096 T = 343.16
s2v160c1600-2.wcnf	S = OPT O = 1069 T = 122.55	S = OPT O = 1069 T = 122.55
s2v160c1600-3.wcnf	S = OPT O = 1074 T = 145.87	S = OPT O = 1074 T = 145.87
s2v160c1700-1.wcnf	S = OPT O = 1182 T = 964.50	S = OPT O = 1182 T = 964.50
s2v160c1700-2.wcnf	S = OPT O = 1094 T = 50.48	S = OPT O = 1094 T = 50.48
s2v160c1700-3.wcnf	S = OPT O = 1110 T = 120.13	S = OPT O = 1110 T = 120.13
s2v160c1800-1.wcnf	S = OPT O = 1247 T = 115.56	S = OPT O = 1247 T = 115.56
s2v160c1800-2.wcnf	S = OPT O = 1258 T = 945.32	S = OPT O = 1258 T = 945.32
s2v160c1800-3.wcnf	S = OPT O = 1297 T = 487.27	S = OPT O = 1297 T = 487.27
s2v160c1900-1.wcnf	S = OPT O = 1377 T = 133.88	S = OPT O = 1377 T = 133.88
s2v160c1900-2.wcnf	S = OPT O = 1381 T = 709.92	S = OPT O = 1381 T = 709.92
s2v160c1900-3.wcnf	S = OPT O = 1332 T = 283.00	S = OPT O = 1332 T = 283.00
s2v160c2000-1.wcnf	S = OPT O = 1377 T = 302.58	S = OPT O = 1377 T = 302.58
s2v160c2000-2.wcnf	S = OPT O = 1456 T = 1517.19	S = OPT O = 1456 T = 1517.19
s2v160c2000-3.wcnf	S = OPT O = 1444 T = 601.33	S = OPT O = 1444 T = 601.33
s2v160c2100-1.wcnf	S = OPT O = 1449 T = 201.58	S = OPT O = 1449 T = 201.58
s2v160c2100-2.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v160c2100-3.wcnf	S = OPT O = 1557 T = 706.54	S = OPT O = 1557 T = 706.54
s2v160c2200-1.wcnf	S = OPT O = 1707 T = 1246.59	S = OPT O = 1707 T = 1246.59
s2v160c2200-2.wcnf	S = OPT O = 1743 T = 1758.29	S = OPT O = 1743 T = 1758.29
s2v160c2200-3.wcnf	S = OPT O = 1562 T = 522.99	S = OPT O = 1562 T = 522.99
s2v160c2300-1.wcnf	S = OPT O = 1710 T = 1013.13	S = OPT O = 1710 T = 1013.13
s2v160c2300-2.wcnf	S = N/A O = N/A T = TO	S = N/A O = 1753 T = TO
s2v160c2300-3.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v160c2400-1.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v160c2400-2.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v160c2400-3.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v160c2500-1.wcnf	S = OPT O = 1875 T = 793.83	S = OPT O = 1875 T = 793.83
s2v160c2500-2.wcnf	S = OPT O = 1929 T = 973.52	S = OPT O = 1929 T = 973.52
s2v160c2500-3.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v160c2600-1.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v160c2600-2.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v160c2600-3.wcnf	S = OPT O = 2047 T = 1245.70	S = OPT O = 2047 T = 1245.70
s2v180c1200-1.wcnf	S = OPT O = 598 T = 23.01	S = OPT O = 598 T = 23.01
s2v180c1200-2.wcnf	S = OPT O = 669 T = 55.17	S = OPT O = 669 T = 55.17
s2v180c1200-3.wcnf	S = OPT O = 588 T = 20.64	S = OPT O = 588 T = 20.64
s2v180c1200-4.wcnf	S = OPT O = 565 T = 26.58	S = OPT O = 565 T = 26.58
s2v180c1300-1.wcnf	S = OPT O = 675 T = 82.61	S = OPT O = 675 T = 82.61
s2v180c1300-2.wcnf	S = OPT O = 712 T = 27.93	S = OPT O = 712 T = 27.93
s2v180c1300-3.wcnf	S = OPT O = 652 T = 17.93	S = OPT O = 652 T = 17.93
s2v180c1300-4.wcnf	S = OPT O = 690 T = 18.34	S = OPT O = 690 T = 18.34
s2v180c1400-1.wcnf	S = OPT O = 746 T = 34.88	S = OPT O = 746 T = 34.88
s2v180c1400-2.wcnf	S = OPT O = 765 T = 122.58	S = OPT O = 765 T = 122.58
s2v180c1400-3.wcnf	S = OPT O = 791 T = 78.38	S = OPT O = 791 T = 78.38
s2v180c1400-4.wcnf	S = OPT O = 805 T = 73.77	S = OPT O = 805 T = 73.77
s2v180c1500-1.wcnf	S = OPT O = 819 T = 17.18	S = OPT O = 819 T = 17.18
s2v180c1500-2.wcnf	S = OPT O = 871 T = 108.27	S = OPT O = 871 T = 108.27
s2v180c1500-3.wcnf	S = OPT O = 864 T = 35.50	S = OPT O = 864 T = 35.50
s2v180c1500-4.wcnf	S = OPT O = 879 T = 729.69	S = OPT O = 879 T = 729.69
s2v180c1600-1.wcnf	S = OPT O = 954 T = 203.06	S = OPT O = 954 T = 203.06
s2v180c1600-2.wcnf	S = OPT O = 1024 T = 1092.29	S = OPT O = 1024 T = 1092.29
s2v180c1600-3.wcnf	S = N/A O = N/A T = TO	S = N/A O = 1052 T = TO
s2v180c1600-4.wcnf	S = OPT O = 921 T = 45.56	S = OPT O = 921 T = 45.56
s2v180c1700-1.wcnf	S = OPT O = 1042 T = 200.40	S = OPT O = 1042 T = 200.40
s2v180c1700-2.wcnf	S = OPT O = 1061 T = 326.72	S = OPT O = 1061 T = 326.72
s2v180c1700-3.wcnf	S = OPT O = 1050 T = 662.67	S = OPT O = 1050 T = 662.67
s2v180c1700-4.wcnf	S = OPT O = 1024 T = 245.17	S = OPT O = 1024 T = 245.17
s2v180c1800-1.wcnf	S = OPT O = 1202 T = 1198.94	S = OPT O = 1202 T = 1198.94
s2v180c1800-2.wcnf	S = N/A O = N/A T = TO	S = N/A O = 1252 T = TO
s2v180c1800-3.wcnf	S = OPT O = 1129 T = 260.62	S = OPT O = 1129 T = 260.62
s2v180c1800-4.wcnf	S = OPT O = 1118 T = 179.33	S = OPT O = 1118 T = 179.33
s2v180c1900-1.wcnf	S = OPT O = 1228 T = 789.61	S = OPT O = 1228 T = 789.61
s2v180c1900-2.wcnf	S = OPT O = 1275 T = 588.94	S = OPT O = 1275 T = 588.94
s2v180c1900-3.wcnf	S = OPT O = 1221 T = 825.02	S = OPT O = 1221 T = 825.02
s2v180c1900-4.wcnf	S = OPT O = 1227 T = 373.76	S = OPT O = 1227 T = 373.76
s2v180c2000-1.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v180c2000-2.wcnf	S = OPT O = 1328 T = 590.23	S = OPT O = 1328 T = 590.23
s2v180c2000-3.wcnf	S = OPT O = 1374 T = 1761.25	S = OPT O = 1374 T = 1761.25
s2v180c2000-4.wcnf	S = OPT O = 1372 T = 1524.28	S = OPT O = 1372 T = 1524.28
s2v180c2100-1.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v180c2100-2.wcnf	S = N/A O = N/A T = TO	S = N/A O = 1500 T = TO
s2v180c2100-3.wcnf	S = OPT O = 1406 T = 1472.68	S = OPT O = 1406 T = 1472.68
s2v180c2100-4.wcnf	S = OPT O = 1484 T = 950.47	S = OPT O = 1484 T = 950.47
s2v180c2200-1.wcnf	S = OPT O = 1480 T = 660.32	S = OPT O = 1480 T = 660.32
s2v180c2200-2.wcnf	S = OPT O = 1553 T = 698.15	S = OPT O = 1553 T = 698.15
s2v180c2200-3.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v180c2200-4.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v200c1200-1.wcnf	S = OPT O = 558 T = 26.18	S = OPT O = 558 T = 26.18
s2v200c1200-2.wcnf	S = OPT O = 570 T = 56.52	S = OPT O = 570 T = 56.52
s2v200c1200-3.wcnf	S = OPT O = 575 T = 70.46	S = OPT O = 575 T = 70.46
s2v200c1200-4.wcnf	S = OPT O = 514 T = 12.72	S = OPT O = 514 T = 12.72
s2v200c1200-5.wcnf	S = OPT O = 523 T = 10.42	S = OPT O = 523 T = 10.42
s2v200c1200-6.wcnf	S = OPT O = 527 T = 19.13	S = OPT O = 527 T = 19.13
s2v200c1200-7.wcnf	S = OPT O = 525 T = 9.45	S = OPT O = 525 T = 9.45
s2v200c1300-1.wcnf	S = OPT O = 641 T = 110.18	S = OPT O = 641 T = 110.18
s2v200c1300-2.wcnf	S = OPT O = 701 T = 39.28	S = OPT O = 701 T = 39.28
s2v200c1300-3.wcnf	S = OPT O = 647 T = 54.00	S = OPT O = 647 T = 54.00
s2v200c1300-4.wcnf	S = OPT O = 666 T = 92.02	S = OPT O = 666 T = 92.02
s2v200c1300-5.wcnf	S = OPT O = 596 T = 26.62	S = OPT O = 596 T = 26.62
s2v200c1300-6.wcnf	S = OPT O = 642 T = 92.18	S = OPT O = 642 T = 92.18
s2v200c1300-7.wcnf	S = OPT O = 652 T = 27.27	S = OPT O = 652 T = 27.27
s2v200c1400-1.wcnf	S = OPT O = 756 T = 264.78	S = OPT O = 756 T = 264.78
s2v200c1400-2.wcnf	S = OPT O = 728 T = 86.93	S = OPT O = 728 T = 86.93
s2v200c1400-3.wcnf	S = OPT O = 693 T = 37.10	S = OPT O = 693 T = 37.10
s2v200c1400-4.wcnf	S = OPT O = 781 T = 609.15	S = OPT O = 781 T = 609.15
s2v200c1400-5.wcnf	S = OPT O = 723 T = 324.07	S = OPT O = 723 T = 324.07
s2v200c1400-6.wcnf	S = OPT O = 732 T = 67.99	S = OPT O = 732 T = 67.99
s2v200c1400-7.wcnf	S = OPT O = 673 T = 64.25	S = OPT O = 673 T = 64.25
s2v200c1500-1.wcnf	S = OPT O = 845 T = 333.47	S = OPT O = 845 T = 333.47
s2v200c1500-2.wcnf	S = OPT O = 841 T = 532.15	S = OPT O = 841 T = 532.15
s2v200c1500-3.wcnf	S = OPT O = 840 T = 159.31	S = OPT O = 840 T = 159.31
s2v200c1500-4.wcnf	S = OPT O = 785 T = 139.88	S = OPT O = 785 T = 139.88
s2v200c1500-5.wcnf	S = OPT O = 833 T = 236.21	S = OPT O = 833 T = 236.21
s2v200c1500-6.wcnf	S = OPT O = 808 T = 179.56	S = OPT O = 808 T = 179.56
s2v200c1500-7.wcnf	S = OPT O = 838 T = 155.98	S = OPT O = 838 T = 155.98
s2v200c1600-1.wcnf	S = OPT O = 960 T = 888.14	S = OPT O = 960 T = 888.14
s2v200c1600-2.wcnf	S = OPT O = 901 T = 362.43	S = OPT O = 901 T = 362.43
s2v200c1600-3.wcnf	S = OPT O = 900 T = 505.33	S = OPT O = 900 T = 505.33
s2v200c1600-4.wcnf	S = OPT O = 909 T = 839.35	S = OPT O = 909 T = 839.35
s2v200c1600-5.wcnf	S = OPT O = 920 T = 214.92	S = OPT O = 920 T = 214.92
s2v200c1600-6.wcnf	S = OPT O = 918 T = 510.99	S = OPT O = 918 T = 510.99
s2v200c1600-7.wcnf	S = OPT O = 894 T = 819.89	S = OPT O = 894 T = 819.89
s2v200c1700-1.wcnf	S = OPT O = 1007 T = 841.73	S = OPT O = 1007 T = 841.73
s2v200c1700-2.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v200c1700-3.wcnf	S = OPT O = 1061 T = 852.38	S = OPT O = 1061 T = 852.38
s2v200c1700-4.wcnf	S = OPT O = 973 T = 378.40	S = OPT O = 973 T = 378.40
s2v200c1700-5.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v200c1700-6.wcnf	S = OPT O = 983 T = 544.12	S = OPT O = 983 T = 544.12
s2v200c1700-7.wcnf	S = OPT O = 1043 T = 1696.33	S = OPT O = 1043 T = 1696.33
s2v200c1800-1.wcnf	S = OPT O = 1066 T = 573.25	S = OPT O = 1066 T = 573.25
s2v200c1800-2.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v200c1800-3.wcnf	S = OPT O = 1104 T = 761.39	S = OPT O = 1104 T = 761.39
s2v200c1800-4.wcnf	S = OPT O = 1107 T = 1638.12	S = OPT O = 1107 T = 1638.12
s2v200c1800-5.wcnf	S = OPT O = 1097 T = 1489.24	S = OPT O = 1097 T = 1489.24
s2v200c1800-6.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s2v200c1800-7.wcnf	S = OPT O = 1060 T = 992.33	S = OPT O = 1060 T = 992.33
s3v110c1000-1.wcnf	S = OPT O = 115 T = 862.84	S = OPT O = 115 T = 862.84
s3v110c1000-10.wcnf	S = OPT O = 115 T = 1602.38	S = OPT O = 115 T = 1602.38
s3v110c1000-2.wcnf	S = OPT O = 108 T = 426.42	S = OPT O = 108 T = 426.42
s3v110c1000-3.wcnf	S = OPT O = 108 T = 413.39	S = OPT O = 108 T = 413.39
s3v110c1000-4.wcnf	S = OPT O = 90 T = 182.03	S = OPT O = 90 T = 182.03
s3v110c1000-5.wcnf	S = OPT O = 131 T = 1630.17	S = OPT O = 131 T = 1630.17
s3v110c1000-6.wcnf	S = OPT O = 116 T = 1138.20	S = OPT O = 116 T = 1138.20
s3v110c1000-7.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v110c1000-8.wcnf	S = OPT O = 125 T = 945.85	S = OPT O = 125 T = 945.85
s3v110c1000-9.wcnf	S = OPT O = 118 T = 975.73	S = OPT O = 118 T = 975.73
s3v110c1100-1.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v110c1100-10.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v110c1100-2.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v110c1100-3.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v110c1100-4.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v110c1100-5.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v110c1100-6.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v110c1100-7.wcnf	S = OPT O = 132 T = 1232.34	S = OPT O = 132 T = 1232.34
s3v110c1100-8.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v110c1100-9.wcnf	S = N/A O = N/A T = TO	S = N/A O = 147 T = TO
s3v110c700-1.wcnf	S = OPT O = 36 T = 16.36	S = OPT O = 36 T = 16.36
s3v110c700-10.wcnf	S = OPT O = 40 T = 19.87	S = OPT O = 40 T = 19.87
s3v110c700-2.wcnf	S = OPT O = 29 T = 13.24	S = OPT O = 29 T = 13.24
s3v110c700-3.wcnf	S = OPT O = 42 T = 29.06	S = OPT O = 42 T = 29.06
s3v110c700-4.wcnf	S = OPT O = 27 T = 10.54	S = OPT O = 27 T = 10.54
s3v110c700-5.wcnf	S = OPT O = 35 T = 22.17	S = OPT O = 35 T = 22.17
s3v110c700-6.wcnf	S = OPT O = 50 T = 46.98	S = OPT O = 50 T = 46.98
s3v110c700-7.wcnf	S = OPT O = 37 T = 21.85	S = OPT O = 37 T = 21.85
s3v110c700-8.wcnf	S = OPT O = 37 T = 27.95	S = OPT O = 37 T = 27.95
s3v110c700-9.wcnf	S = OPT O = 38 T = 22.23	S = OPT O = 38 T = 22.23
s3v110c800-1.wcnf	S = OPT O = 51 T = 45.32	S = OPT O = 51 T = 45.32
s3v110c800-10.wcnf	S = OPT O = 49 T = 20.85	S = OPT O = 49 T = 20.85
s3v110c800-2.wcnf	S = OPT O = 50 T = 28.41	S = OPT O = 50 T = 28.41
s3v110c800-3.wcnf	S = OPT O = 55 T = 92.97	S = OPT O = 55 T = 92.97
s3v110c800-4.wcnf	S = OPT O = 53 T = 47.92	S = OPT O = 53 T = 47.92
s3v110c800-5.wcnf	S = OPT O = 77 T = 238.56	S = OPT O = 77 T = 238.56
s3v110c800-6.wcnf	S = OPT O = 51 T = 56.53	S = OPT O = 51 T = 56.53
s3v110c800-7.wcnf	S = OPT O = 69 T = 162.61	S = OPT O = 69 T = 162.61
s3v110c800-8.wcnf	S = OPT O = 53 T = 67.92	S = OPT O = 53 T = 67.92
s3v110c800-9.wcnf	S = OPT O = 56 T = 55.10	S = OPT O = 56 T = 55.10
s3v110c900-1.wcnf	S = OPT O = 107 T = 1489.08	S = OPT O = 107 T = 1489.08
s3v110c900-10.wcnf	S = OPT O = 70 T = 132.18	S = OPT O = 70 T = 132.18
s3v110c900-2.wcnf	S = OPT O = 66 T = 42.53	S = OPT O = 66 T = 42.53
s3v110c900-3.wcnf	S = OPT O = 85 T = 303.82	S = OPT O = 85 T = 303.82
s3v110c900-4.wcnf	S = OPT O = 106 T = 1705.92	S = OPT O = 106 T = 1705.92
s3v110c900-5.wcnf	S = OPT O = 81 T = 173.83	S = OPT O = 81 T = 173.83
s3v110c900-6.wcnf	S = OPT O = 92 T = 665.78	S = OPT O = 92 T = 665.78
s3v110c900-7.wcnf	S = OPT O = 90 T = 743.98	S = OPT O = 90 T = 743.98
s3v110c900-8.wcnf	S = OPT O = 108 T = 1640.57	S = OPT O = 108 T = 1640.57
s3v110c900-9.wcnf	S = OPT O = 102 T = 762.33	S = OPT O = 102 T = 762.33
s3v70c1000-1.wcnf	S = OPT O = 208 T = 74.17	S = OPT O = 208 T = 74.17
s3v70c1000-2.wcnf	S = OPT O = 224 T = 175.03	S = OPT O = 224 T = 175.03
s3v70c1000-3.wcnf	S = OPT O = 222 T = 183.87	S = OPT O = 222 T = 183.87
s3v70c1000-4.wcnf	S = OPT O = 252 T = 422.94	S = OPT O = 252 T = 422.94
s3v70c1000-5.wcnf	S = OPT O = 218 T = 116.68	S = OPT O = 218 T = 116.68
s3v70c1100-1.wcnf	S = OPT O = 261 T = 241.49	S = OPT O = 261 T = 241.49
s3v70c1100-2.wcnf	S = OPT O = 267 T = 322.93	S = OPT O = 267 T = 322.93
s3v70c1100-3.wcnf	S = OPT O = 272 T = 345.05	S = OPT O = 272 T = 345.05
s3v70c1100-4.wcnf	S = OPT O = 251 T = 156.24	S = OPT O = 251 T = 156.24
s3v70c1100-5.wcnf	S = OPT O = 246 T = 199.84	S = OPT O = 246 T = 199.84
s3v70c1200-1.wcnf	S = OPT O = 312 T = 730.79	S = OPT O = 312 T = 730.79
s3v70c1200-2.wcnf	S = OPT O = 281 T = 175.13	S = OPT O = 281 T = 175.13
s3v70c1200-3.wcnf	S = OPT O = 323 T = 1136.53	S = OPT O = 323 T = 1136.53
s3v70c1200-4.wcnf	S = OPT O = 329 T = 879.68	S = OPT O = 329 T = 879.68
s3v70c1200-5.wcnf	S = OPT O = 289 T = 234.30	S = OPT O = 289 T = 234.30
s3v70c1300-1.wcnf	S = OPT O = 342 T = 1115.61	S = OPT O = 342 T = 1115.61
s3v70c1300-2.wcnf	S = OPT O = 343 T = 934.70	S = OPT O = 343 T = 934.70
s3v70c1300-3.wcnf	S = OPT O = 357 T = 838.32	S = OPT O = 357 T = 838.32
s3v70c1300-4.wcnf	S = OPT O = 368 T = 1624.60	S = OPT O = 368 T = 1624.60
s3v70c1300-5.wcnf	S = OPT O = 331 T = 431.61	S = OPT O = 331 T = 431.61
s3v70c1400-1.wcnf	S = OPT O = 376 T = 664.72	S = OPT O = 376 T = 664.72
s3v70c1400-2.wcnf	S = OPT O = 376 T = 553.90	S = OPT O = 376 T = 553.90
s3v70c1400-3.wcnf	S = OPT O = 404 T = 1528.56	S = OPT O = 404 T = 1528.56
s3v70c1400-4.wcnf	S = OPT O = 386 T = 1193.31	S = OPT O = 386 T = 1193.31
s3v70c1400-5.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v70c1500-1.wcnf	S = N/A O = N/A T = TO	S = N/A O = 447 T = TO
s3v70c1500-2.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v70c1500-3.wcnf	S = OPT O = 399 T = 617.66	S = OPT O = 399 T = 617.66
s3v70c1500-4.wcnf	S = OPT O = 423 T = 1614.06	S = OPT O = 423 T = 1614.06
s3v70c1500-5.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v70c700-1.wcnf	S = OPT O = 101 T = 16.17	S = OPT O = 101 T = 16.17
s3v70c700-2.wcnf	S = OPT O = 93 T = 11.58	S = OPT O = 93 T = 11.58
s3v70c700-3.wcnf	S = OPT O = 110 T = 21.18	S = OPT O = 110 T = 21.18
s3v70c700-4.wcnf	S = OPT O = 94 T = 11.91	S = OPT O = 94 T = 11.91
s3v70c700-5.wcnf	S = OPT O = 83 T = 8.23	S = OPT O = 83 T = 8.23
s3v70c800-1.wcnf	S = OPT O = 126 T = 23.79	S = OPT O = 126 T = 23.79
s3v70c800-2.wcnf	S = OPT O = 129 T = 19.44	S = OPT O = 129 T = 19.44
s3v70c800-3.wcnf	S = OPT O = 152 T = 36.96	S = OPT O = 152 T = 36.96
s3v70c800-4.wcnf	S = OPT O = 133 T = 38.92	S = OPT O = 133 T = 38.92
s3v70c800-5.wcnf	S = OPT O = 136 T = 31.50	S = OPT O = 136 T = 31.50
s3v70c900-1.wcnf	S = OPT O = 176 T = 64.85	S = OPT O = 176 T = 64.85
s3v70c900-2.wcnf	S = OPT O = 151 T = 20.66	S = OPT O = 151 T = 20.66
s3v70c900-3.wcnf	S = OPT O = 147 T = 20.76	S = OPT O = 147 T = 20.76
s3v70c900-4.wcnf	S = OPT O = 187 T = 120.58	S = OPT O = 187 T = 120.58
s3v70c900-5.wcnf	S = OPT O = 130 T = 10.83	S = OPT O = 130 T = 10.83
s3v90c1000-1.wcnf	S = OPT O = 178 T = 839.69	S = OPT O = 178 T = 839.69
s3v90c1000-2.wcnf	S = OPT O = 155 T = 228.62	S = OPT O = 155 T = 228.62
s3v90c1000-3.wcnf	S = OPT O = 157 T = 543.57	S = OPT O = 157 T = 543.57
s3v90c1000-4.wcnf	S = OPT O = 177 T = 731.70	S = OPT O = 177 T = 731.70
s3v90c1000-5.wcnf	S = OPT O = 170 T = 989.07	S = OPT O = 170 T = 989.07
s3v90c1000-6.wcnf	S = OPT O = 163 T = 396.56	S = OPT O = 163 T = 396.56
s3v90c1000-7.wcnf	S = OPT O = 186 T = 1402.02	S = OPT O = 186 T = 1402.02
s3v90c1100-1.wcnf	S = OPT O = 192 T = 1011.38	S = OPT O = 192 T = 1011.38
s3v90c1100-2.wcnf	S = N/A O = N/A T = TO	S = N/A O = 210 T = TO
s3v90c1100-3.wcnf	S = OPT O = 203 T = 1163.82	S = OPT O = 203 T = 1163.82
s3v90c1100-4.wcnf	S = OPT O = 209 T = 1167.40	S = OPT O = 209 T = 1167.40
s3v90c1100-5.wcnf	S = N/A O = N/A T = TO	S = N/A O = 211 T = TO
s3v90c1100-6.wcnf	S = N/A O = N/A T = TO	S = N/A O = 200 T = TO
s3v90c1100-7.wcnf	S = OPT O = 194 T = 967.50	S = OPT O = 194 T = 967.50
s3v90c1200-1.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v90c1200-2.wcnf	S = OPT O = 215 T = 1173.88	S = OPT O = 215 T = 1173.88
s3v90c1200-3.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v90c1200-4.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v90c1200-5.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v90c1200-6.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v90c1200-7.wcnf	S = OPT O = 225 T = 1333.78	S = OPT O = 225 T = 1333.78
s3v90c1300-1.wcnf	S = OPT O = 244 T = 1403.61	S = OPT O = 244 T = 1403.61
s3v90c1300-2.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v90c1300-3.wcnf	S = N/A O = N/A T = TO	S = N/A O = 267 T = TO
s3v90c1300-4.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v90c1300-5.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v90c1300-6.wcnf	S = N/A O = N/A T = TO	S = N/A O = N/A T = TO
s3v90c1300-7.wcnf	S = N/A O = N/A T = TO	S = N/A O = 257 T = TO
s3v90c700-1.wcnf	S = OPT O = 61 T = 18.98	S = OPT O = 61 T = 18.98
s3v90c700-2.wcnf	S = OPT O = 52 T = 10.82	S = OPT O = 52 T = 10.82
s3v90c700-3.wcnf	S = OPT O = 63 T = 17.77	S = OPT O = 63 T = 17.77
s3v90c700-4.wcnf	S = OPT O = 65 T = 26.98	S = OPT O = 65 T = 26.98
s3v90c700-5.wcnf	S = OPT O = 61 T = 17.66	S = OPT O = 61 T = 17.66
s3v90c700-6.wcnf	S = OPT O = 66 T = 27.97	S = OPT O = 66 T = 27.97
s3v90c700-7.wcnf	S = OPT O = 54 T = 16.12	S = OPT O = 54 T = 16.12
s3v90c800-1.wcnf	S = OPT O = 97 T = 116.25	S = OPT O = 97 T = 116.25
s3v90c800-2.wcnf	S = OPT O = 95 T = 58.06	S = OPT O = 95 T = 58.06
s3v90c800-3.wcnf	S = OPT O = 83 T = 26.07	S = OPT O = 83 T = 26.07
s3v90c800-4.wcnf	S = OPT O = 82 T = 19.15	S = OPT O = 82 T = 19.15
s3v90c800-5.wcnf	S = OPT O = 103 T = 45.96	S = OPT O = 103 T = 45.96
s3v90c800-6.wcnf	S = OPT O = 82 T = 26.42	S = OPT O = 82 T = 26.42
s3v90c800-7.wcnf	S = OPT O = 102 T = 101.25	S = OPT O = 102 T = 101.25
s3v90c900-1.wcnf	S = OPT O = 122 T = 139.44	S = OPT O = 122 T = 139.44
s3v90c900-2.wcnf	S = OPT O = 124 T = 205.70	S = OPT O = 124 T = 205.70
s3v90c900-3.wcnf	S = OPT O = 135 T = 410.99	S = OPT O = 135 T = 410.99
s3v90c900-4.wcnf	S = OPT O = 132 T = 366.84	S = OPT O = 132 T = 366.84
s3v90c900-5.wcnf	S = OPT O = 120 T = 154.85	S = OPT O = 120 T = 154.85
s3v90c900-6.wcnf	S = OPT O = 117 T = 131.19	S = OPT O = 117 T = 131.19
s3v90c900-7.wcnf	S = OPT O = 145 T = 434.37	S = OPT O = 145 T = 434.37
file_rwpms_wcnf_L2_V150_C4000_H150_0.wcnf	S = OPT O = 4231 T = 7.05	S = OPT O = 4231 T = 7.05
file_rwpms_wcnf_L2_V150_C4000_H150_1.wcnf	S = UNSAT O = N/A T = 6.56	S = UNSAT O = N/A T = 6.56
file_rwpms_wcnf_L2_V150_C4000_H150_2.wcnf	S = OPT O = 4235 T = 7.37	S = OPT O = 4235 T = 7.37
file_rwpms_wcnf_L2_V150_C4000_H150_3.wcnf	S = OPT O = 4037 T = 8.30	S = OPT O = 4037 T = 8.30
file_rwpms_wcnf_L2_V150_C4000_H150_4.wcnf	S = OPT O = 4031 T = 11.48	S = OPT O = 4031 T = 11.48
file_rwpms_wcnf_L2_V150_C4000_H150_5.wcnf	S = OPT O = 4144 T = 18.17	S = OPT O = 4144 T = 18.17
file_rwpms_wcnf_L2_V150_C4000_H150_6.wcnf	S = OPT O = 4149 T = 17.02	S = OPT O = 4149 T = 17.02
file_rwpms_wcnf_L2_V150_C4000_H150_7.wcnf	S = OPT O = 4043 T = 12.61	S = OPT O = 4043 T = 12.61
file_rwpms_wcnf_L2_V150_C4000_H150_8.wcnf	S = OPT O = 4078 T = 19.30	S = OPT O = 4078 T = 19.30
file_rwpms_wcnf_L2_V150_C4000_H150_9.wcnf	S = OPT O = 4328 T = 11.14	S = OPT O = 4328 T = 11.14
file_rwpms_wcnf_L2_V150_C4500_H150_0.wcnf	S = OPT O = 4572 T = 19.27	S = OPT O = 4572 T = 19.27
file_rwpms_wcnf_L2_V150_C4500_H150_1.wcnf	S = OPT O = 4967 T = 22.58	S = OPT O = 4967 T = 22.58
file_rwpms_wcnf_L2_V150_C4500_H150_2.wcnf	S = OPT O = 4961 T = 12.19	S = OPT O = 4961 T = 12.19
file_rwpms_wcnf_L2_V150_C4500_H150_3.wcnf	S = OPT O = 4614 T = 8.66	S = OPT O = 4614 T = 8.66
file_rwpms_wcnf_L2_V150_C4500_H150_4.wcnf	S = OPT O = 4794 T = 26.44	S = OPT O = 4794 T = 26.44
file_rwpms_wcnf_L2_V150_C4500_H150_5.wcnf	S = OPT O = 4687 T = 13.00	S = OPT O = 4687 T = 13.00
file_rwpms_wcnf_L2_V150_C4500_H150_6.wcnf	S = OPT O = 4605 T = 12.12	S = OPT O = 4605 T = 12.12
file_rwpms_wcnf_L2_V150_C4500_H150_7.wcnf	S = OPT O = 4710 T = 16.77	S = OPT O = 4710 T = 16.77
file_rwpms_wcnf_L2_V150_C4500_H150_8.wcnf	S = OPT O = 4945 T = 12.95	S = OPT O = 4945 T = 12.95
file_rwpms_wcnf_L2_V150_C4500_H150_9.wcnf	S = OPT O = 5023 T = 12.12	S = OPT O = 5023 T = 12.12
file_rwpms_wcnf_L2_V150_C5000_H150_0.wcnf	S = OPT O = 5362 T = 8.73	S = OPT O = 5362 T = 8.73
file_rwpms_wcnf_L2_V150_C5000_H150_1.wcnf	S = OPT O = 5338 T = 7.51	S = OPT O = 5338 T = 7.51
file_rwpms_wcnf_L2_V150_C5000_H150_2.wcnf	S = OPT O = 5312 T = 10.19	S = OPT O = 5312 T = 10.19
file_rwpms_wcnf_L2_V150_C5000_H150_3.wcnf	S = OPT O = 5507 T = 11.27	S = OPT O = 5507 T = 11.27
file_rwpms_wcnf_L2_V150_C5000_H150_4.wcnf	S = OPT O = 5451 T = 26.31	S = OPT O = 5451 T = 26.31
file_rwpms_wcnf_L2_V150_C5000_H150_5.wcnf	S = OPT O = 5308 T = 9.03	S = OPT O = 5308 T = 9.03
file_rwpms_wcnf_L2_V150_C5000_H150_6.wcnf	S = OPT O = 5428 T = 9.68	S = OPT O = 5428 T = 9.68
file_rwpms_wcnf_L2_V150_C5000_H150_7.wcnf	S = OPT O = 5468 T = 20.51	S = OPT O = 5468 T = 20.51
file_rwpms_wcnf_L2_V150_C5000_H150_8.wcnf	S = OPT O = 5339 T = 8.29	S = OPT O = 5339 T = 8.29
file_rwpms_wcnf_L2_V150_C5000_H150_9.wcnf	S = OPT O = 5376 T = 10.91	S = OPT O = 5376 T = 10.91
file_rwpms_wcnf_L2_V150_C1000_H150_0.wcnf	S = OPT O = 626 T = 6.54	S = OPT O = 626 T = 6.54
file_rwpms_wcnf_L2_V150_C1000_H150_1.wcnf	S = OPT O = 745 T = 6.78	S = OPT O = 745 T = 6.78
file_rwpms_wcnf_L2_V150_C1000_H150_2.wcnf	S = OPT O = 629 T = 6.40	S = OPT O = 629 T = 6.40
file_rwpms_wcnf_L2_V150_C1000_H150_3.wcnf	S = OPT O = 723 T = 6.58	S = OPT O = 723 T = 6.58
file_rwpms_wcnf_L2_V150_C1000_H150_4.wcnf	S = OPT O = 737 T = 6.54	S = OPT O = 737 T = 6.54
file_rwpms_wcnf_L2_V150_C1000_H150_5.wcnf	S = OPT O = 668 T = 6.50	S = OPT O = 668 T = 6.50
file_rwpms_wcnf_L2_V150_C1000_H150_6.wcnf	S = OPT O = 641 T = 6.48	S = OPT O = 641 T = 6.48
file_rwpms_wcnf_L2_V150_C1000_H150_7.wcnf	S = OPT O = 688 T = 6.64	S = OPT O = 688 T = 6.64
file_rwpms_wcnf_L2_V150_C1000_H150_8.wcnf	S = OPT O = 577 T = 6.63	S = OPT O = 577 T = 6.63
file_rwpms_wcnf_L2_V150_C1000_H150_9.wcnf	S = OPT O = 714 T = 6.55	S = OPT O = 714 T = 6.55
file_rwpms_wcnf_L2_V150_C1500_H150_0.wcnf	S = OPT O = 1121 T = 7.20	S = OPT O = 1121 T = 7.20
file_rwpms_wcnf_L2_V150_C1500_H150_1.wcnf	S = OPT O = 1142 T = 6.86	S = OPT O = 1142 T = 6.86
file_rwpms_wcnf_L2_V150_C1500_H150_2.wcnf	S = OPT O = 1252 T = 7.14	S = OPT O = 1252 T = 7.14
file_rwpms_wcnf_L2_V150_C1500_H150_3.wcnf	S = OPT O = 1295 T = 6.84	S = OPT O = 1295 T = 6.84
file_rwpms_wcnf_L2_V150_C1500_H150_4.wcnf	S = OPT O = 1261 T = 7.15	S = OPT O = 1261 T = 7.15
file_rwpms_wcnf_L2_V150_C1500_H150_5.wcnf	S = OPT O = 1047 T = 6.65	S = OPT O = 1047 T = 6.65
file_rwpms_wcnf_L2_V150_C1500_H150_6.wcnf	S = OPT O = 1175 T = 6.47	S = OPT O = 1175 T = 6.47
file_rwpms_wcnf_L2_V150_C1500_H150_7.wcnf	S = OPT O = 1145 T = 7.37	S = OPT O = 1145 T = 7.37
file_rwpms_wcnf_L2_V150_C1500_H150_8.wcnf	S = OPT O = 1135 T = 7.14	S = OPT O = 1135 T = 7.14
file_rwpms_wcnf_L2_V150_C1500_H150_9.wcnf	S = OPT O = 1232 T = 7.54	S = OPT O = 1232 T = 7.54
file_rwpms_wcnf_L2_V150_C2000_H150_0.wcnf	S = OPT O = 1842 T = 7.63	S = OPT O = 1842 T = 7.63
file_rwpms_wcnf_L2_V150_C2000_H150_1.wcnf	S = OPT O = 1699 T = 7.21	S = OPT O = 1699 T = 7.21
file_rwpms_wcnf_L2_V150_C2000_H150_2.wcnf	S = OPT O = 1730 T = 7.24	S = OPT O = 1730 T = 7.24
file_rwpms_wcnf_L2_V150_C2000_H150_3.wcnf	S = OPT O = 1885 T = 8.30	S = OPT O = 1885 T = 8.30
file_rwpms_wcnf_L2_V150_C2000_H150_4.wcnf	S = OPT O = 2043 T = 7.05	S = OPT O = 2043 T = 7.05
file_rwpms_wcnf_L2_V150_C2000_H150_5.wcnf	S = OPT O = 1818 T = 8.57	S = OPT O = 1818 T = 8.57
file_rwpms_wcnf_L2_V150_C2000_H150_6.wcnf	S = OPT O = 1832 T = 6.77	S = OPT O = 1832 T = 6.77
file_rwpms_wcnf_L2_V150_C2000_H150_7.wcnf	S = OPT O = 1780 T = 7.46	S = OPT O = 1780 T = 7.46
file_rwpms_wcnf_L2_V150_C2000_H150_8.wcnf	S = OPT O = 1726 T = 6.81	S = OPT O = 1726 T = 6.81
file_rwpms_wcnf_L2_V150_C2000_H150_9.wcnf	S = OPT O = 1807 T = 10.27	S = OPT O = 1807 T = 10.27
file_rwpms_wcnf_L2_V150_C2500_H150_0.wcnf	S = OPT O = 2414 T = 7.22	S = OPT O = 2414 T = 7.22
file_rwpms_wcnf_L2_V150_C2500_H150_1.wcnf	S = OPT O = 2398 T = 8.10	S = OPT O = 2398 T = 8.10
file_rwpms_wcnf_L2_V150_C2500_H150_2.wcnf	S = OPT O = 2113 T = 7.11	S = OPT O = 2113 T = 7.11
file_rwpms_wcnf_L2_V150_C2500_H150_3.wcnf	S = OPT O = 2339 T = 8.87	S = OPT O = 2339 T = 8.87
file_rwpms_wcnf_L2_V150_C2500_H150_4.wcnf	S = OPT O = 2390 T = 7.28	S = OPT O = 2390 T = 7.28
file_rwpms_wcnf_L2_V150_C2500_H150_5.wcnf	S = OPT O = 2332 T = 7.04	S = OPT O = 2332 T = 7.04
file_rwpms_wcnf_L2_V150_C2500_H150_6.wcnf	S = OPT O = 2488 T = 7.74	S = OPT O = 2488 T = 7.74
file_rwpms_wcnf_L2_V150_C2500_H150_7.wcnf	S = OPT O = 2241 T = 9.40	S = OPT O = 2241 T = 9.40
file_rwpms_wcnf_L2_V150_C2500_H150_8.wcnf	S = OPT O = 2353 T = 7.83	S = OPT O = 2353 T = 7.83
file_rwpms_wcnf_L2_V150_C2500_H150_9.wcnf	S = OPT O = 2560 T = 7.02	S = OPT O = 2560 T = 7.02
file_rwpms_wcnf_L2_V150_C3000_H150_0.wcnf	S = OPT O = 2885 T = 15.50	S = OPT O = 2885 T = 15.50
file_rwpms_wcnf_L2_V150_C3000_H150_1.wcnf	S = OPT O = 2918 T = 11.97	S = OPT O = 2918 T = 11.97
file_rwpms_wcnf_L2_V150_C3000_H150_2.wcnf	S = OPT O = 2878 T = 8.34	S = OPT O = 2878 T = 8.34
file_rwpms_wcnf_L2_V150_C3000_H150_3.wcnf	S = OPT O = 3045 T = 11.23	S = OPT O = 3045 T = 11.23
file_rwpms_wcnf_L2_V150_C3000_H150_4.wcnf	S = OPT O = 3021 T = 7.41	S = OPT O = 3021 T = 7.41
file_rwpms_wcnf_L2_V150_C3000_H150_5.wcnf	S = OPT O = 2812 T = 12.14	S = OPT O = 2812 T = 12.14
file_rwpms_wcnf_L2_V150_C3000_H150_6.wcnf	S = OPT O = 2838 T = 14.14	S = OPT O = 2838 T = 14.14
file_rwpms_wcnf_L2_V150_C3000_H150_7.wcnf	S = OPT O = 2815 T = 7.87	S = OPT O = 2815 T = 7.87
file_rwpms_wcnf_L2_V150_C3000_H150_8.wcnf	S = OPT O = 3025 T = 12.67	S = OPT O = 3025 T = 12.67
file_rwpms_wcnf_L2_V150_C3000_H150_9.wcnf	S = OPT O = 2952 T = 9.47	S = OPT O = 2952 T = 9.47
file_rwpms_wcnf_L2_V150_C3500_H150_0.wcnf	S = OPT O = 3634 T = 16.13	S = OPT O = 3634 T = 16.13
file_rwpms_wcnf_L2_V150_C3500_H150_1.wcnf	S = OPT O = 3662 T = 8.74	S = OPT O = 3662 T = 8.74
file_rwpms_wcnf_L2_V150_C3500_H150_2.wcnf	S = OPT O = 3827 T = 13.33	S = OPT O = 3827 T = 13.33
file_rwpms_wcnf_L2_V150_C3500_H150_3.wcnf	S = OPT O = 3512 T = 7.57	S = OPT O = 3512 T = 7.57
file_rwpms_wcnf_L2_V150_C3500_H150_4.wcnf	S = OPT O = 3355 T = 9.82	S = OPT O = 3355 T = 9.82
file_rwpms_wcnf_L2_V150_C3500_H150_5.wcnf	S = OPT O = 3450 T = 16.45	S = OPT O = 3450 T = 16.45
file_rwpms_wcnf_L2_V150_C3500_H150_6.wcnf	S = OPT O = 3654 T = 7.24	S = OPT O = 3654 T = 7.24
file_rwpms_wcnf_L2_V150_C3500_H150_7.wcnf	S = OPT O = 3617 T = 8.29	S = OPT O = 3617 T = 8.29
file_rwpms_wcnf_L2_V150_C3500_H150_8.wcnf	S = OPT O = 3525 T = 8.73	S = OPT O = 3525 T = 8.73
file_rwpms_wcnf_L2_V150_C3500_H150_9.wcnf	S = OPT O = 3240 T = 9.90	S = OPT O = 3240 T = 9.90
file_rwpms_wcnf_L3_V100_C600_H100_0.wcnf	S = OPT O = 28 T = 9.55	S = OPT O = 28 T = 9.55
file_rwpms_wcnf_L3_V100_C600_H100_1.wcnf	S = OPT O = 15 T = 7.37	S = OPT O = 15 T = 7.37
file_rwpms_wcnf_L3_V100_C600_H100_2.wcnf	S = OPT O = 25 T = 8.34	S = OPT O = 25 T = 8.34
file_rwpms_wcnf_L3_V100_C600_H100_3.wcnf	S = OPT O = 25 T = 8.57	S = OPT O = 25 T = 8.57
file_rwpms_wcnf_L3_V100_C600_H100_4.wcnf	S = OPT O = 30 T = 9.66	S = OPT O = 30 T = 9.66
file_rwpms_wcnf_L3_V100_C600_H100_5.wcnf	S = OPT O = 27 T = 8.35	S = OPT O = 27 T = 8.35
file_rwpms_wcnf_L3_V100_C600_H100_6.wcnf	S = OPT O = 26 T = 8.85	S = OPT O = 26 T = 8.85
file_rwpms_wcnf_L3_V100_C600_H100_7.wcnf	S = OPT O = 29 T = 14.48	S = OPT O = 29 T = 14.48
file_rwpms_wcnf_L3_V100_C600_H100_8.wcnf	S = OPT O = 19 T = 9.00	S = OPT O = 19 T = 9.00
file_rwpms_wcnf_L3_V100_C600_H100_9.wcnf	S = OPT O = 30 T = 10.88	S = OPT O = 30 T = 10.88
file_rwpms_wcnf_L3_V100_C700_H100_0.wcnf	S = OPT O = 54 T = 17.73	S = OPT O = 54 T = 17.73
file_rwpms_wcnf_L3_V100_C700_H100_1.wcnf	S = OPT O = 58 T = 44.12	S = OPT O = 58 T = 44.12
file_rwpms_wcnf_L3_V100_C700_H100_2.wcnf	S = OPT O = 59 T = 30.37	S = OPT O = 59 T = 30.37
file_rwpms_wcnf_L3_V100_C700_H100_3.wcnf	S = OPT O = 48 T = 24.95	S = OPT O = 48 T = 24.95
file_rwpms_wcnf_L3_V100_C700_H100_4.wcnf	S = OPT O = 42 T = 13.34	S = OPT O = 42 T = 13.34
file_rwpms_wcnf_L3_V100_C700_H100_5.wcnf	S = OPT O = 46 T = 15.90	S = OPT O = 46 T = 15.90
file_rwpms_wcnf_L3_V100_C700_H100_6.wcnf	S = OPT O = 51 T = 34.55	S = OPT O = 51 T = 34.55
file_rwpms_wcnf_L3_V100_C700_H100_7.wcnf	S = OPT O = 63 T = 60.50	S = OPT O = 63 T = 60.50
file_rwpms_wcnf_L3_V100_C700_H100_8.wcnf	S = OPT O = 64 T = 107.44	S = OPT O = 64 T = 107.44
file_rwpms_wcnf_L3_V100_C700_H100_9.wcnf	S = OPT O = 45 T = 13.79	S = OPT O = 45 T = 13.79
file_rwpms_wcnf_L3_V100_C800_H100_0.wcnf	S = OPT O = 95 T = 134.46	S = OPT O = 95 T = 134.46
file_rwpms_wcnf_L3_V100_C800_H100_1.wcnf	S = OPT O = 81 T = 89.41	S = OPT O = 81 T = 89.41
file_rwpms_wcnf_L3_V100_C800_H100_2.wcnf	S = OPT O = 77 T = 95.23	S = OPT O = 77 T = 95.23
file_rwpms_wcnf_L3_V100_C800_H100_3.wcnf	S = OPT O = 81 T = 43.40	S = OPT O = 81 T = 43.40
file_rwpms_wcnf_L3_V100_C800_H100_4.wcnf	S = OPT O = 75 T = 99.72	S = OPT O = 75 T = 99.72
file_rwpms_wcnf_L3_V100_C800_H100_5.wcnf	S = OPT O = 80 T = 59.55	S = OPT O = 80 T = 59.55
file_rwpms_wcnf_L3_V100_C800_H100_6.wcnf	S = OPT O = 74 T = 55.70	S = OPT O = 74 T = 55.70
file_rwpms_wcnf_L3_V100_C800_H100_7.wcnf	S = OPT O = 99 T = 120.23	S = OPT O = 99 T = 120.23
file_rwpms_wcnf_L3_V100_C800_H100_8.wcnf	S = OPT O = 90 T = 206.77	S = OPT O = 90 T = 206.77
file_rwpms_wcnf_L3_V100_C800_H100_9.wcnf	S = OPT O = 95 T = 209.02	S = OPT O = 95 T = 209.02