PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga30_30_sat_pb.cnf.cr.opb
MD5SUM	511f20f1868f397c99d8a26ca62146c0
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	31
Number of bits of the biggest sum of numbers	5
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04984
Number of variables	1350
Total number of constraints	990
Number of constraints which are clauses	930
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	15
Maximum length of a constraint	30
Trace number 34665

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-05-28 10:11:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23974 boxname=wulflinc18 idbench=48 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  511f20f1868f397c99d8a26ca62146c0  /oldhome/oroussel/tmp/wulflinc18/normalized-fpga30_30_sat_pb.cnf.cr.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc18/normalized-fpga30_30_sat_pb.cnf.cr.opb
IDLAUNCH: 23974
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        365072 kB
Buffers:         31916 kB
Cached:         603880 kB
SwapCached:        820 kB
Active:          37992 kB
Inactive:       599944 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        364820 kB
SwapTotal:     2097892 kB
SwapFree:      2096212 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            25748 kB
Committed_AS:    63568 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-28 10:16:12 (client local time) WITH STATUS 10 IN 299.16 SECONDS
stats: 23974 0 299.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...

Decision: 1290/3930	Time: 6.51001/86400
Decision: 1290/3930	Time: 7.15591/86400
Decision: 1290/3930	Time: 8.23175/86400
Decision: 1290/3930	Time: 9.15161/86400
Decision: 1290/3930	Time: 10.0005/86400
Decision: 1290/3930	Time: 10.9663/86400
Decision: 1290/3930	Time: 11.4563/86400
Decision: 1290/3930	Time: 12.4771/86400
Decision: 1290/3930	Time: 13.8969/86400
Decision: 1290/3930	Time: 14.5658/86400
Decision: 1290/3930	Time: 15.2567/86400
Decision: 1290/3930	Time: 16.0726/86400
Decision: 1290/3930	Time: 17.1384/86400
Decision: 1290/3930	Time: 18.2402/86400
Decision: 1290/3930	Time: 19.1581/86400
Decision: 1290/3930	Time: 19.956/86400
Decision: 1290/3930	Time: 21.0098/86400
Decision: 1290/3930	Time: 21.8467/86400
Decision: 1290/3930	Time: 22.8705/86400
Decision: 1290/3930	Time: 23.7154/86400
Decision: 1290/3930	Time: 24.5993/86400
Decision: 1290/3930	Time: 25.5071/86400
Decision: 1290/3930	Time: 26.9689/86400
Decision: 1290/3930	Time: 28.4497/86400
Decision: 1290/3930	Time: 30.1134/86400
Decision: 1290/3930	Time: 31.5452/86400
Decision: 1290/3930	Time: 32.759/86400
Decision: 1290/3930	Time: 34.3638/86400
Decision: 1290/3930	Time: 36.0125/86400
Decision: 1290/3930	Time: 37.3493/86400
Decision: 1290/3930	Time: 38.3512/86400
Decision: 1290/3930	Time: 39.545/86400
Decision: 1290/3930	Time: 41.0928/86400
Decision: 1290/3930	Time: 41.7517/86400
Decision: 1290/3930	Time: 42.5615/86400
Decision: 1290/3930	Time: 43.3984/86400
Decision: 1290/3930	Time: 44.3943/86400
Decision: 1290/3930	Time: 45.917/86400
Decision: 1290/3930	Time: 46.6199/86400
Decision: 1290/3930	Time: 48.0857/86400
Decision: 1290/3930	Time: 49.0605/86400
Decision: 1290/3930	Time: 50.1834/86400
Decision: 1290/3930	Time: 51.3882/86400
Decision: 1290/3930	Time: 52.438/86400
Decision: 1290/3930	Time: 53.7298/86400
Decision: 1290/3930	Time: 54.7887/86400
Decision: 1290/3930	Time: 55.5965/86400
Decision: 1290/3930	Time: 56.5114/86400
Decision: 1290/3930	Time: 57.5642/86400
Decision: 1290/3930	Time: 58.7401/86400
Decision: 1290/3930	Time: 60.0019/86400
Decision: 1290/3930	Time: 61.2727/86400
Decision: 1290/3930	Time: 62.8005/86400
Decision: 1290/3930	Time: 64.3282/86400
Decision: 1290/3930	Time: 65.518/86400
Decision: 1290/3930	Time: 66.6199/86400
Decision: 1290/3930	Time: 67.4357/86400
Decision: 1290/3930	Time: 68.0617/86400
Decision: 1290/3930	Time: 69.0835/86400
Decision: 1290/3930	Time: 69.9524/86400
Decision: 1290/3930	Time: 70.9622/86400
Decision: 1290/3930	Time: 71.4771/86400
Decision: 1290/3930	Time: 72.178/86400
Decision: 1290/3930	Time: 73.3718/86400
Decision: 1290/3930	Time: 74.3967/86400
Decision: 1290/3930	Time: 75.0676/86400
Decision: 1290/3930	Time: 75.9365/86400
Decision: 1290/3930	Time: 76.5544/86400
Decision: 1290/3930	Time: 77.8742/86400
Decision: 1290/3930	Time: 78.3171/86400
Decision: 1290/3930	Time: 79.2899/86400
Decision: 1290/3930	Time: 80.1158/86400
Decision: 1290/3930	Time: 81.6076/86400
Decision: 1290/3930	Time: 82.9824/86400
Decision: 1290/3930	Time: 84.8641/86400
Decision: 1290/3930	Time: 85.596/86400
Decision: 1290/3930	Time: 86.4539/86400
Decision: 1290/3930	Time: 87.9036/86400
Decision: 1290/3930	Time: 88.8445/86400
Decision: 1290/3930	Time: 89.8133/86400
Decision: 1290/3930	Time: 91.0362/86400
Decision: 1290/3930	Time: 92.277/86400
Decision: 1290/3930	Time: 93.6748/86400
Decision: 1290/3930	Time: 95.6315/86400
Decision: 1290/3930	Time: 96.6423/86400
Decision: 1290/3930	Time: 97.9971/86400
Decision: 1290/3930	Time: 98.889/86400
Decision: 1290/3930	Time: 99.7018/86400
Decision: 1290/3930	Time: 100.525/86400
Decision: 1290/3930	Time: 101.71/86400
Decision: 1290/3930	Time: 103.057/86400
Decision: 1290/3930	Time: 105.357/86400
Decision: 1290/3930	Time: 107.591/86400
Decision: 1290/3930	Time: 109.933/86400
Decision: 1290/3930	Time: 111.897/86400
Decision: 1290/3930	Time: 114.136/86400
Decision: 1290/3930	Time: 115.884/86400
Decision: 1290/3930	Time: 118.616/86400
Decision: 1290/3930	Time: 121.247/86400
Decision: 1290/3930	Time: 123.146/86400
Decision: 1290/3930	Time: 124.906/86400
Decision: 1290/3930	Time: 126.538/86400
Decision: 1290/3930	Time: 128.104/86400
Decision: 1290/3930	Time: 129.428/86400
Decision: 1290/3930	Time: 130.948/86400
Decision: 1290/3930	Time: 133.275/86400
Decision: 1290/3930	Time: 135.311/86400
Decision: 1290/3930	Time: 137.577/86400
Decision: 1290/3930	Time: 139.098/86400
Decision: 1290/3930	Time: 141.024/86400
Decision: 1290/3930	Time: 143.229/86400
Decision: 1290/3930	Time: 145.059/86400
Decision: 1290/3930	Time: 147.424/86400
Decision: 1290/3930	Time: 150.342/86400
Decision: 1290/3930	Time: 152.98/86400
Decision: 1290/3930	Time: 154.562/86400
Decision: 1290/3930	Time: 156.09/86400
Decision: 1290/3930	Time: 157.863/86400
Decision: 1290/3930	Time: 159.483/86400
Decision: 1290/3930	Time: 160.862/86400
Decision: 1290/3930	Time: 162.596/86400
Decision: 1290/3930	Time: 164.047/86400
Decision: 1290/3930	Time: 165.495/86400
Decision: 1290/3930	Time: 166.132/86400
Decision: 1290/3930	Time: 167.385/86400
Decision: 1290/3930	Time: 168.676/86400
Decision: 1290/3930	Time: 170.815/86400
Decision: 1290/3930	Time: 173.456/86400
Decision: 1290/3930	Time: 174.43/86400
Decision: 1290/3930	Time: 176.077/86400
Decision: 1290/3930	Time: 177.63/86400
Decision: 1290/3930	Time: 179.276/86400
Decision: 1290/3930	Time: 182.274/86400
Decision: 1290/3930	Time: 186.103/86400
Decision: 1290/3930	Time: 190.233/86400
Decision: 1290/3930	Time: 193.575/86400
Decision: 1290/3930	Time: 197.084/86400
Decision: 1290/3930	Time: 198.917/86400
Decision: 1290/3930	Time: 201.848/86400
Decision: 1290/3930	Time: 204.296/86400
Decision: 1290/3930	Time: 206.727/86400
Decision: 1290/3930	Time: 208.058/86400
Decision: 1290/3930	Time: 209.519/86400
Decision: 1290/3930	Time: 210.607/86400
Decision: 1290/3930	Time: 211.715/86400
Decision: 1290/3930	Time: 212.702/86400
Decision: 1290/3930	Time: 214.087/86400
Decision: 1290/3930	Time: 214.965/86400
Decision: 1290/3930	Time: 216.55/86400
Decision: 1290/3930	Time: 217.925/86400
Decision: 1290/3930	Time: 220.726/86400
Decision: 1290/3930	Time: 224.308/86400
Decision: 1290/3930	Time: 226.694/86400
Decision: 1290/3930	Time: 228.945/86400
Decision: 1290/3930	Time: 229.945/86400
Decision: 1290/3930	Time: 232.769/86400
Decision: 1290/3930	Time: 234.853/86400
Decision: 1290/3930	Time: 236.392/86400
Decision: 1290/3930	Time: 238.029/86400
Decision: 1290/3930	Time: 239.184/86400
Decision: 1290/3930	Time: 240.939/86400
Decision: 1290/3930	Time: 241.626/86400
Decision: 1290/3930	Time: 242.912/86400
Decision: 1290/3930	Time: 244.076/86400
Decision: 1290/3930	Time: 244.915/86400
Decision: 1290/3930	Time: 246.244/86400
Decision: 1290/3930	Time: 247.85/86400
Decision: 1290/3930	Time: 248.998/86400
Decision: 1290/3930	Time: 250.899/86400
Decision: 1290/3930	Time: 252.873/86400
Decision: 1290/3930	Time: 255.039/86400
Decision: 1290/3930	Time: 257.42/86400
Decision: 1290/3930	Time: 260.455/86400
Decision: 1290/3930	Time: 263.386/86400
Decision: 1290/3930	Time: 267.085/86400
Decision: 1290/3930	Time: 270.323/86400
Decision: 1290/3930	Time: 274.002/86400
Decision: 1290/3930	Time: 276.51/86400
Decision: 1290/3930	Time: 279.506/86400
Decision: 1290/3930	Time: 283.892/86400
Decision: 1290/3930	Time: 287.638/86400
Decision: 1290/3930	Time: 291.223/86400
Decision: 1290/3930	Time: 294.44/86400
Decision: 1290/3930	Time: 297.273/86400s SATISFIABLE
v -v1 -v10 -v100 -v1000 -v1001 -v1002 -v1003 -v1004 -v1005 -v1006 v1007 -v1008 -v1009 -v101 -v1010 -v1011 -v1012 -v1013 -v1014 -v1015 -v1016 -v1017 -v1018 -v1019 -v102 -v1020 -v1021 -v1022 -v1023 -v1024 -v1025 -v1026 -v1027 -v1028 -v1029 -v103 -v1030 v1031 -v1032 -v1033 -v1034 -v1035 -v1036 -v1037 -v1038 -v1039 -v104 -v1040 -v1041 -v1042 -v1043 v1044 -v1045 -v1046 -v1047 -v1048 -v1049 -v105 -v1050 -v1051 -v1052 -v1053 -v1054 v1055 -v1056 -v1057 -v1058 -v1059 -v106 -v1060 -v1061 -v1062 -v1063 -v1064 -v1065 -v1066 -v1067 -v1068 -v1069 -v107 -v1070 -v1071 -v1072 -v1073 -v1074 -v1075 -v1076 -v1077 v1078 -v1079 -v108 -v1080 -v1081 -v1082 -v1083 -v1084 -v1085 -v1086 -v1087 -v1088 -v1089 -v109 -v1090 -v1091 v1092 -v1093 -v1094 -v1095 -v1096 -v1097 -v1098 -v1099 -v11 -v110 -v1100 -v1101 -v1102 -v1103 -v1104 -v1105 -v1106 -v1107 -v1108 v1109 -v111 -v1110 -v1111 -v1112 v1113 -v1114 -v1115 -v1116 -v1117 -v1118 -v1119 -v112 -v1120 -v1121 -v1122 -v1123 -v1124 -v1125 -v1126 -v1127 -v1128 -v1129 v113 v1130 -v1131 -v1132 -v1133 -v1134 -v1135 -v1136 -v1137 -v1138 -v1139 -v114 -v1140 v1141 -v1142 -v1143 -v1144 -v1145 -v1146 -v1147 -v1148 -v1149 -v115 -v1150 -v1151 -v1152 -v1153 -v1154 -v1155 -v1156 -v1157 -v1158 -v1159 -v116 -v1160 -v1161 -v1162 -v1163 v1164 -v1165 -v1166 -v1167 -v1168 -v1169 -v117 -v1170 -v1171 -v1172 v1173 -v1174 -v1175 -v1176 -v1177 -v1178 -v1179 -v118 -v1180 -v1181 -v1182 -v1183 -v1184 -v1185 -v1186 -v1187 -v1188 -v1189 -v119 -v1190 -v1191 -v1192 -v1193 -v1194 -v1195 -v1196 -v1197 v1198 -v1199 -v12 -v120 -v1200 -v1201 v1202 -v1203 -v1204 -v1205 -v1206 -v1207 -v1208 -v1209 -v121 -v1210 -v1211 -v1212 -v1213 -v1214 -v1215 -v1216 -v1217 -v1218 -v1219 -v122 -v1220 -v1221 v1222 -v1223 -v1224 -v1225 -v1226 -v1227 -v1228 -v1229 -v123 -v1230 -v1231 -v1232 -v1233 -v1234 -v1235 -v1236 -v1237 -v1238 -v1239 -v124 -v1240 -v1241 -v1242 -v1243 v1244 -v1245 -v1246 -v1247 -v1248 v1249 -v125 -v1250 -v1251 -v1252 -v1253 -v1254 -v1255 -v1256 -v1257 -v1258 -v1259 -v126 -v1260 -v1261 -v1262 -v1263 -v1264 -v1265 v1266 -v1267 -v1268 -v1269 -v127 -v1270 -v1271 -v1272 -v1273 -v1274 -v1275 -v1276 -v1277 -v1278 -v1279 -v128 -v1280 -v1281 -v1282 -v1283 -v1284 -v1285 -v1286 v1287 -v1288 -v1289 -v129 -v1290 -v1291 -v1292 -v1293 -v1294 -v1295 -v1296 -v1297 -v1298 -v1299 -v13 -v130 -v1300 -v1301 -v1302 -v1303 -v1304 v1305 -v1306 -v1307 -v1308 -v1309 -v131 -v1310 -v1311 -v1312 -v1313 -v1314 v1315 -v1316 -v1317 -v1318 -v1319 -v132 -v1320 -v1321 -v1322 -v1323 -v1324 -v1325 -v1326 -v1327 v1328 -v1329 -v133 -v1330 -v1331 -v1332 -v1333 -v1334 -v1335 -v1336 -v1337 -v1338 -v1339 -v134 -v1340 -v1341 -v1342 -v1343 -v1344 -v1345 v1346 -v1347 -v1348 -v1349 -v135 -v1350 -v136 -v137 -v138 -v139 -v14 -v140 -v141 v142 -v143 -v144 -v145 -v146 -v147 -v148 -v149 -v15 -v150 -v151 -v152 -v153 -v154 -v155 -v156 -v157 -v158 -v159 -v16 v160 -v161 -v162 -v163 -v164 -v165 -v166 -v167 -v168 -v169 -v17 -v170 -v171 -v172 -v173 -v174 -v175 -v176 -v177 -v178 -v179 -v18 -v180 -v181 -v182 -v183 -v184 -v185 -v186 -v187 -v188 -v189 -v19 -v190 -v191 -v192 -v193 -v194 -v195 v196 -v197 -v198 -v199 -v2 -v20 -v200 -v201 -v202 -v203 -v204 -v205 -v206 -v207 -v208 -v209 -v21 -v210 -v211 -v212 -v213 -v214 -v215 -v216 -v217 -v218 -v219 -v22 -v220 -v221 -v222 -v223 -v224 -v225 -v226 -v227 -v228 -v229 -v23 -v230 -v231 -v232 -v233 -v234 -v235 -v236 v237 -v238 -v239 -v24 -v240 -v241 -v242 -v243 -v244 -v245 -v246 -v247 -v248 -v249 v25 -v250 v251 -v252 -v253 -v254 -v255 -v256 -v257 -v258 -v259 -v26 -v260 -v261 -v262 -v263 -v264 -v265 -v266 -v267 -v268 -v269 -v27 -v270 -v271 -v272 -v273 -v274 -v275 -v276 -v277 -v278 -v279 -v28 -v280 -v281 -v282 -v283 -v284 v285 -v286 -v287 -v288 -v289 -v29 -v290 -v291 -v292 -v293 -v294 -v295 -v296 -v297 -v298 -v299 -v3 -v30 -v300 -v301 -v302 -v303 -v304 -v305 -v306 v307 -v308 -v309 -v31 -v310 -v311 -v312 -v313 -v314 -v315 -v316 -v317 -v318 -v319 -v32 -v320 -v321 -v322 -v323 -v324 -v325 -v326 -v327 -v328 -v329 -v33 -v330 -v331 v332 -v333 -v334 -v335 -v336 -v337 -v338 -v339 -v34 -v340 -v341 -v342 -v343 -v344 -v345 -v346 -v347 -v348 -v349 -v35 -v350 -v351 -v352 -v353 -v354 -v355 -v356 -v357 -v358 -v359 -v36 -v360 -v361 -v362 -v363 -v364 v365 -v366 -v367 -v368 -v369 -v37 -v370 -v371 -v372 -v373 -v374 -v375 -v376 -v377 -v378 -v379 -v38 -v380 -v381 -v382 -v383 -v384 -v385 -v386 -v387 -v388 -v389 -v39 -v390 -v391 -v392 -v393 -v394 -v395 -v396 -v397 -v398 -v399 -v4 -v40 -v400 -v401 -v402 -v403 v404 -v405 -v406 -v407 -v408 -v409 -v41 -v410 -v411 -v412 -v413 -v414 -v415 -v416 -v417 -v418 -v419 -v42 -v420 -v421 -v422 -v423 -v424 -v425 -v426 -v427 v428 -v429 v43 -v430 -v431 -v432 -v433 -v434 -v435 -v436 -v437 -v438 -v439 -v44 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 -v449 -v45 -v450 -v451 -v452 -v453 -v454 -v455 -v456 -v457 -v458 -v459 -v46 -v460 -v461 v462 -v463 -v464 -v465 -v466 -v467 -v468 -v469 -v47 -v470 -v471 -v472 -v473 -v474 -v475 -v476 -v477 -v478 -v479 -v48 -v480 -v481 -v482 -v483 -v484 -v485 -v486 -v487 -v488 -v489 -v49 -v490 -v491 -v492 -v493 -v494 -v495 -v496 -v497 -v498 -v499 -v5 -v50 -v500 -v501 -v502 -v503 -v504 -v505 -v506 -v507 -v508 -v509 -v51 v510 -v511 -v512 -v513 -v514 -v515 -v516 -v517 -v518 -v519 -v52 -v520 -v521 -v522 -v523 -v524 -v525 -v526 -v527 -v528 -v529 -v53 -v530 -v531 -v532 -v533 v534 -v535 -v536 -v537 -v538 -v539 -v54 -v540 -v541 -v542 -v543 -v544 -v545 -v546 -v547 -v548 -v549 -v55 -v550 -v551 -v552 -v553 -v554 -v555 -v556 -v557 -v558 -v559 -v56 -v560 -v561 -v562 -v563 -v564 -v565 v566 -v567 -v568 -v569 -v57 -v570 -v571 -v572 -v573 -v574 -v575 -v576 -v577 -v578 v579 -v58 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587 -v588 -v589 -v59 -v590 -v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v6 -v60 -v600 -v601 -v602 -v603 v604 -v605 -v606 -v607 -v608 -v609 -v61 -v610 -v611 -v612 -v613 -v614 -v615 -v616 -v617 -v618 -v619 -v62 -v620 -v621 -v622 -v623 -v624 -v625 -v626 -v627 -v628 -v629 v63 -v630 -v631 -v632 -v633 -v634 -v635 -v636 -v637 -v638 -v639 -v64 -v640 -v641 -v642 -v643 -v644 -v645 -v646 -v647 v648 -v649 -v65 -v650 -v651 -v652 -v653 -v654 -v655 -v656 -v657 -v658 -v659 -v66 -v660 -v661 -v662 -v663 -v664 -v665 -v666 -v667 -v668 -v669 -v67 -v670 -v671 -v672 -v673 -v674 -v675 -v676 -v677 -v678 -v679 -v68 -v680 v681 -v682 -v683 -v684 -v685 -v686 -v687 -v688 -v689 -v69 -v690 -v691 -v692 -v693 -v694 -v695 -v696 -v697 -v698 -v699 -v7 -v70 -v700 -v701 -v702 -v703 -v704 -v705 -v706 -v707 -v708 -v709 -v71 -v710 -v711 -v712 -v713 -v714 -v715 -v716 -v717 v718 -v719 -v72 -v720 -v721 -v722 -v723 -v724 -v725 -v726 -v727 -v728 -v729 -v73 -v730 -v731 -v732 -v733 -v734 -v735 -v736 -v737 -v738 -v739 -v74 v740 -v741 -v742 -v743 -v744 -v745 -v746 -v747 -v748 -v749 -v75 -v750 -v751 -v752 -v753 -v754 -v755 v756 -v757 -v758 -v759 -v76 -v760 -v761 -v762 -v763 -v764 -v765 -v766 -v767 -v768 -v769 -v77 -v770 -v771 -v772 -v773 -v774 -v775 -v776 -v777 -v778 -v779 -v78 -v780 -v781 -v782 -v783 -v784 -v785 -v786 -v787 -v788 -v789 -v79 -v790 -v791 -v792 -v793 -v794 -v795 -v796 v797 -v798 -v799 -v8 -v80 -v800 -v801 -v802 -v803 -v804 -v805 -v806 -v807 -v808 -v809 -v81 -v810 v811 -v812 -v813 -v814 -v815 -v816 -v817 -v818 -v819 -v82 -v820 -v821 -v822 -v823 -v824 -v825 -v826 -v827 -v828 -v829 -v83 -v830 -v831 -v832 -v833 -v834 -v835 -v836 -v837 -v838 -v839 -v84 -v840 -v841 -v842 -v843 -v844 -v845 -v846 -v847 -v848 -v849 -v85 -v850 -v851 -v852 -v853 -v854 -v855 -v856 -v857 -v858 v859 -v86 -v860 -v861 -v862 -v863 -v864 -v865 -v866 -v867 -v868 -v869 -v87 -v870 -v871 -v872 -v873 -v874 -v875 -v876 -v877 -v878 -v879 -v88 -v880 -v881 -v882 -v883 -v884 -v885 -v886 -v887 -v888 -v889 -v89 -v890 -v891 -v892 -v893 -v894 -v895 -v896 -v897 -v898 v899 -v9 -v90 -v900 -v901 -v902 -v903 -v904 -v905 -v906 v907 -v908 -v909 -v91 -v910 -v911 -v912 -v913 -v914 -v915 -v916 -v917 -v918 v919 -v92 -v920 -v921 -v922 -v923 -v924 -v925 -v926 -v927 -v928 -v929 -v93 -v930 -v931 -v932 -v933 -v934 -v935 -v936 -v937 -v938 -v939 -v94 -v940 -v941 -v942 -v943 -v944 v945 v946 -v947 -v948 -v949 -v95 -v950 -v951 -v952 -v953 -v954 -v955 -v956 -v957 -v958 -v959 -v96 -v960 -v961 -v962 -v963 -v964 -v965 -v966 -v967 -v968 -v969 -v97 v970 -v971 -v972 -v973 -v974 -v975 -v976 -v977 -v978 -v979 -v98 -v980 -v981 -v982 v983 -v984 -v985 -v986 -v987 -v988 -v989 -v99 -v990 -v991 -v992 -v993 -v994 -v995 v996 -v997 -v998 -v999 
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.28 0.10 0.03 2/54 31613
Raw data (stat): 31613 (runsolver) R 31612 24172 24171 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 863966009 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0011 s]
Raw data (loadavg): 0.39 0.13 0.04 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 1448 0 0 0 980 18 0 0 25 0 1 0 863966009 6225920 1250 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1520 1250 300 300 0 1220 0
vsize: 6080
[startup+20.002 s]
Raw data (loadavg): 0.48 0.15 0.05 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 1609 0 0 0 1967 31 0 0 25 0 1 0 863966009 6619136 1411 4294967295 134512640 135726644 3221224576 3221223184 134741150 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1616 1411 300 300 0 1316 0
vsize: 6464
[startup+30.0028 s]
Raw data (loadavg): 0.56 0.18 0.06 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 1902 0 0 0 2953 45 0 0 25 0 1 0 863966009 7659520 1511 4294967295 134512640 135726644 3221224576 3221223072 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1870 1511 300 300 0 1570 0
vsize: 7480
[startup+40.0028 s]
Raw data (loadavg): 0.63 0.21 0.07 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 1980 0 0 0 3939 59 0 0 25 0 1 0 863966009 7872512 1589 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1922 1589 300 300 0 1622 0
vsize: 7688
[startup+50.0026 s]
Raw data (loadavg): 0.69 0.23 0.08 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 2065 0 0 0 4925 73 0 0 25 0 1 0 863966009 8122368 1674 4294967295 134512640 135726644 3221224576 3221223120 134736661 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1983 1674 300 300 0 1683 0
vsize: 7932
[startup+60.0029 s]
Raw data (loadavg): 0.73 0.26 0.09 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 2145 0 0 0 5914 83 0 0 25 0 1 0 863966009 8232960 1754 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2010 1754 300 300 0 1710 0
vsize: 8040
[startup+70.0034 s]
Raw data (loadavg): 0.77 0.28 0.10 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 2236 0 0 0 6901 96 0 0 25 0 1 0 863966009 8495104 1845 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2074 1845 300 300 0 1774 0
vsize: 8296
[startup+80.0034 s]
Raw data (loadavg): 0.81 0.31 0.11 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 2732 0 0 0 7889 109 0 0 25 0 1 0 863966009 10289152 1956 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2512 1956 300 300 0 2212 0
vsize: 10048
[startup+90.0035 s]
Raw data (loadavg): 0.84 0.33 0.11 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 2798 0 0 0 8878 120 0 0 25 0 1 0 863966009 10403840 2022 4294967295 134512640 135726644 3221224576 3221223072 134744053 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2540 2022 300 300 0 2240 0
vsize: 10160
[startup+100.003 s]
Raw data (loadavg): 0.86 0.35 0.12 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 2875 0 0 0 9868 130 0 0 25 0 1 0 863966009 10641408 2099 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2598 2099 300 300 0 2298 0
vsize: 10392
[startup+110.004 s]
Raw data (loadavg): 0.88 0.37 0.13 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 2933 0 0 0 10858 140 0 0 25 0 1 0 863966009 10752000 2157 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2625 2157 300 300 0 2325 0
vsize: 10500
[startup+120.004 s]
Raw data (loadavg): 0.90 0.39 0.14 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 2992 0 0 0 11849 150 0 0 25 0 1 0 863966009 10878976 2216 4294967295 134512640 135726644 3221224576 3221223184 134740873 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2656 2216 300 300 0 2356 0
vsize: 10624
[startup+130.004 s]
Raw data (loadavg): 0.91 0.41 0.15 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 3044 0 0 0 12837 162 0 0 25 0 1 0 863966009 10985472 2268 4294967295 134512640 135726644 3221224576 3221223184 134740873 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2682 2268 300 300 0 2382 0
vsize: 10728
[startup+140.005 s]
Raw data (loadavg): 0.93 0.43 0.16 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 3089 0 0 0 13827 172 0 0 25 0 1 0 863966009 11120640 2313 4294967295 134512640 135726644 3221224576 3221223232 134731175 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2715 2313 300 300 0 2415 0
vsize: 10860
[startup+150.005 s]
Raw data (loadavg): 0.94 0.45 0.17 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 3140 0 0 0 14816 183 0 0 25 0 1 0 863966009 11227136 2364 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2741 2364 300 300 0 2441 0
vsize: 10964
[startup+160.006 s]
Raw data (loadavg): 0.95 0.47 0.18 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 3182 0 0 0 15807 192 0 0 25 0 1 0 863966009 11329536 2406 4294967295 134512640 135726644 3221224576 3221223184 134740873 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2766 2406 300 300 0 2466 0
vsize: 11064
[startup+170.006 s]
Raw data (loadavg): 0.95 0.48 0.18 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 3250 0 0 0 16797 202 0 0 25 0 1 0 863966009 11452416 2474 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2796 2474 300 300 0 2496 0
vsize: 11184
[startup+180.007 s]
Raw data (loadavg): 0.96 0.50 0.19 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 3299 0 0 0 17788 212 0 0 25 0 1 0 863966009 11571200 2523 4294967295 134512640 135726644 3221224576 3221223184 134740863 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2825 2523 300 300 0 2525 0
vsize: 11300
[startup+190.007 s]
Raw data (loadavg): 0.97 0.52 0.20 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 3323 0 0 0 18779 221 0 0 25 0 1 0 863966009 11694080 2547 4294967295 134512640 135726644 3221224576 3221223184 134741242 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2855 2547 300 300 0 2555 0
vsize: 11420
[startup+200.007 s]
Raw data (loadavg): 0.97 0.53 0.21 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 3356 0 0 0 19771 230 0 0 25 0 1 0 863966009 11694080 2580 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2855 2580 300 300 0 2555 0
vsize: 11420
[startup+210.007 s]
Raw data (loadavg): 0.98 0.55 0.22 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 3400 0 0 0 20760 240 0 0 25 0 1 0 863966009 11821056 2624 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2886 2624 300 300 0 2586 0
vsize: 11544
[startup+220.007 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 3473 0 0 0 21751 250 0 0 25 0 1 0 863966009 12058624 2697 4294967295 134512640 135726644 3221224576 3221223184 134740873 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2944 2697 300 300 0 2644 0
vsize: 11776
[startup+230.007 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 3503 0 0 0 22742 259 0 0 25 0 1 0 863966009 12058624 2727 4294967295 134512640 135726644 3221224576 3221223184 134740875 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2944 2727 300 300 0 2644 0
vsize: 11776
[startup+240.008 s]
Raw data (loadavg): 0.98 0.59 0.24 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 3550 0 0 0 23730 271 0 0 25 0 1 0 863966009 12161024 2774 4294967295 134512640 135726644 3221224576 3221223184 134740873 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2969 2774 300 300 0 2669 0
vsize: 11876
[startup+250.009 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 4396 0 0 0 24721 280 0 0 25 0 1 0 863966009 15437824 2851 4294967295 134512640 135726644 3221224576 3221223184 134740875 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3769 2851 300 300 0 3469 0
vsize: 15076
[startup+260.009 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 4432 0 0 0 25714 287 0 0 25 0 1 0 863966009 15548416 2887 4294967295 134512640 135726644 3221224576 3221223184 134740873 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3796 2887 300 300 0 3496 0
vsize: 15184
[startup+270.011 s]
Raw data (loadavg): 0.99 0.63 0.26 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 4456 0 0 0 26706 295 0 0 25 0 1 0 863966009 15659008 2911 4294967295 134512640 135726644 3221224576 3221223184 134740873 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3823 2911 300 300 0 3523 0
vsize: 15292
[startup+280.01 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 4492 0 0 0 27695 306 0 0 25 0 1 0 863966009 15659008 2947 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3823 2947 300 300 0 3523 0
vsize: 15292
[startup+290.01 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 4514 0 0 0 28689 313 0 0 25 0 1 0 863966009 15781888 2969 4294967295 134512640 135726644 3221224576 3221223184 134740848 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3853 2969 300 300 0 3553 0
vsize: 15412
[startup+299.144 s]
Raw data (loadavg): 0.99 0.66 0.29 1/53 31613
Raw data (stat): 31613 (pb2sat) R 31612 24172 24171 0 -1 0 4514 0 0 0 28689 313 0 0 25 0 1 0 863966009 15781888 2969 4294967295 134512640 135726644 3221224576 3221223184 134740848 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3853 2969 300 300 0 3553 0
vsize: 0

Child status: 10
Real time (s): 299.144
CPU time (s): 299.16
CPU user time (s): 295.966
CPU system time (s): 3.19351
CPU usage (%): 100.005
Max. virtual memory (Kb): 15412
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	0
#### END VERIFIER DATA ####