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-fpga35_34_sat_pb.cnf.cr.opb
MD5SUM	f49e527e8d063bcfa5508a2b00211475
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	36
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	9.75752
Number of variables	1785
Total number of constraints	1293
Number of constraints which are clauses	1224
Number of constraints which are cardinality constraints (but not clauses)	69
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	17
Maximum length of a constraint	35

Trace number 34664

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-05-28 10:11:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23976 boxname=wulflinc6 idbench=50 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f49e527e8d063bcfa5508a2b00211475  /oldhome/oroussel/tmp/wulflinc6/normalized-fpga35_34_sat_pb.cnf.cr.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc6/normalized-fpga35_34_sat_pb.cnf.cr.opb
IDLAUNCH: 23976
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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	: 2
cpu MHz		: 451.042
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:        176312 kB
Buffers:         38796 kB
Cached:         794604 kB
SwapCached:        484 kB
Active:          51780 kB
Inactive:       784020 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        176060 kB
SwapTotal:     2097136 kB
SwapFree:      2095980 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5708 kB
Slab:            16856 kB
Committed_AS:    63732 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 10:14:41 (client local time) WITH STATUS 10 IN 200.519 SECONDS
stats: 23976 0 200.519 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...

Decision: 1716/5217	Time: 12.828/86400
Decision: 1716/5217	Time: 14.5508/86400
Decision: 1716/5217	Time: 16.0206/86400
Decision: 1716/5217	Time: 17.8593/86400
Decision: 1716/5217	Time: 19.581/86400
Decision: 1716/5217	Time: 21.5067/86400
Decision: 1716/5217	Time: 23.2955/86400
Decision: 1716/5217	Time: 25.3581/86400
Decision: 1716/5217	Time: 27.2739/86400
Decision: 1716/5217	Time: 29.3755/86400
Decision: 1716/5217	Time: 31.0963/86400
Decision: 1716/5217	Time: 32.794/86400
Decision: 1716/5217	Time: 34.8217/86400
Decision: 1716/5217	Time: 36.8314/86400
Decision: 1716/5217	Time: 38.5071/86400
Decision: 1716/5217	Time: 40.5748/86400
Decision: 1716/5217	Time: 42.4805/86400
Decision: 1716/5217	Time: 44.4162/86400
Decision: 1716/5217	Time: 46.6969/86400
Decision: 1716/5217	Time: 48.9186/86400
Decision: 1716/5217	Time: 51.1702/86400
Decision: 1716/5217	Time: 53.2169/86400
Decision: 1716/5217	Time: 56.0615/86400
Decision: 1716/5217	Time: 57.7482/86400
Decision: 1716/5217	Time: 59.6499/86400
Decision: 1716/5217	Time: 61.4837/86400
Decision: 1716/5217	Time: 63.9053/86400
Decision: 1716/5217	Time: 66.022/86400
Decision: 1716/5217	Time: 68.7585/86400
Decision: 1716/5217	Time: 71.5211/86400
Decision: 1716/5217	Time: 73.9958/86400
Decision: 1716/5217	Time: 76.1884/86400
Decision: 1716/5217	Time: 78.2121/86400
Decision: 1716/5217	Time: 80.4848/86400
Decision: 1716/5217	Time: 83.7793/86400
Decision: 1716/5217	Time: 86.6638/86400
Decision: 1716/5217	Time: 89.0445/86400
Decision: 1716/5217	Time: 91.3501/86400
Decision: 1716/5217	Time: 93.9527/86400
Decision: 1716/5217	Time: 96.8333/86400
Decision: 1716/5217	Time: 99.8838/86400
Decision: 1716/5217	Time: 101.996/86400
Decision: 1716/5217	Time: 105.079/86400
Decision: 1716/5217	Time: 107.452/86400
Decision: 1716/5217	Time: 110.317/86400
Decision: 1716/5217	Time: 113.035/86400
Decision: 1716/5217	Time: 114.848/86400
Decision: 1716/5217	Time: 117.713/86400
Decision: 1716/5217	Time: 119.894/86400
Decision: 1716/5217	Time: 122.193/86400
Decision: 1716/5217	Time: 125.336/86400
Decision: 1716/5217	Time: 128.172/86400
Decision: 1716/5217	Time: 130.833/86400
Decision: 1716/5217	Time: 133.518/86400
Decision: 1716/5217	Time: 136.475/86400
Decision: 1716/5217	Time: 139.17/86400
Decision: 1716/5217	Time: 141.218/86400
Decision: 1716/5217	Time: 143.902/86400
Decision: 1716/5217	Time: 147.291/86400
Decision: 1716/5217	Time: 150.706/86400
Decision: 1716/5217	Time: 153.303/86400
Decision: 1716/5217	Time: 155.763/86400
Decision: 1716/5217	Time: 158.663/86400
Decision: 1716/5217	Time: 161.689/86400
Decision: 1716/5217	Time: 164.646/86400
Decision: 1716/5217	Time: 167.837/86400
Decision: 1716/5217	Time: 170.111/86400
Decision: 1716/5217	Time: 173.17/86400
Decision: 1716/5217	Time: 176.57/86400
Decision: 1716/5217	Time: 180.061/86400
Decision: 1716/5217	Time: 182.217/86400
Decision: 1716/5217	Time: 185.159/86400
Decision: 1716/5217	Time: 187.461/86400
Decision: 1716/5217	Time: 190.479/86400
Decision: 1716/5217	Time: 193.282/86400
Decision: 1716/5217	Time: 196.008/86400
Decision: 1716/5217	Time: 198.47/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 -v1351 -v1352 -v1353 -v1354 -v1355 -v1356 -v1357 -v1358 v1359 v136 -v1360 -v1361 -v1362 -v1363 -v1364 -v1365 -v1366 -v1367 -v1368 -v1369 -v137 -v1370 -v1371 -v1372 -v1373 v1374 -v1375 -v1376 -v1377 -v1378 -v1379 -v138 -v1380 -v1381 -v1382 -v1383 -v1384 v1385 -v1386 -v1387 -v1388 -v1389 -v139 -v1390 -v1391 -v1392 -v1393 -v1394 -v1395 -v1396 v1397 -v1398 -v1399 -v14 -v140 -v1400 -v1401 -v1402 -v1403 -v1404 -v1405 -v1406 -v1407 -v1408 -v1409 -v141 -v1410 -v1411 -v1412 -v1413 -v1414 -v1415 -v1416 -v1417 v1418 -v1419 -v142 -v1420 -v1421 -v1422 -v1423 -v1424 -v1425 -v1426 -v1427 -v1428 -v1429 -v143 -v1430 -v1431 -v1432 -v1433 -v1434 -v1435 -v1436 -v1437 -v1438 v1439 v144 -v1440 -v1441 -v1442 -v1443 -v1444 -v1445 -v1446 -v1447 -v1448 -v1449 -v145 -v1450 -v1451 -v1452 -v1453 -v1454 -v1455 -v1456 -v1457 -v1458 -v1459 -v146 -v1460 -v1461 v1462 -v1463 -v1464 -v1465 -v1466 -v1467 -v1468 -v1469 -v147 -v1470 -v1471 v1472 -v1473 -v1474 -v1475 -v1476 -v1477 -v1478 -v1479 -v148 -v1480 -v1481 -v1482 -v1483 -v1484 -v1485 v1486 -v1487 -v1488 -v1489 -v149 -v1490 -v1491 -v1492 -v1493 -v1494 -v1495 -v1496 -v1497 -v1498 -v1499 v15 -v150 -v1500 -v1501 -v1502 -v1503 -v1504 -v1505 -v1506 -v1507 -v1508 -v1509 -v151 -v1510 -v1511 -v1512 v1513 v1514 -v1515 -v1516 -v1517 -v1518 -v1519 -v152 -v1520 -v1521 -v1522 -v1523 -v1524 -v1525 -v1526 -v1527 -v1528 -v1529 -v153 -v1530 -v1531 -v1532 -v1533 -v1534 -v1535 -v1536 -v1537 -v1538 -v1539 -v154 -v1540 -v1541 -v1542 -v1543 v1544 -v1545 -v1546 -v1547 -v1548 -v1549 -v155 -v1550 -v1551 -v1552 -v1553 -v1554 -v1555 -v1556 -v1557 -v1558 -v1559 -v156 v1560 -v1561 -v1562 -v1563 -v1564 -v1565 -v1566 -v1567 -v1568 v1569 -v157 -v1570 -v1571 -v1572 -v1573 -v1574 -v1575 -v1576 -v1577 -v1578 -v1579 -v158 -v1580 -v1581 -v1582 -v1583 -v1584 -v1585 -v1586 v1587 -v1588 -v1589 -v159 -v1590 -v1591 -v1592 -v1593 -v1594 -v1595 -v1596 -v1597 -v1598 -v1599 -v16 -v160 -v1600 -v1601 -v1602 -v1603 -v1604 -v1605 -v1606 -v1607 -v1608 -v1609 -v161 v1610 -v1611 -v1612 -v1613 -v1614 -v1615 -v1616 v1617 -v1618 -v1619 -v162 -v1620 -v1621 -v1622 -v1623 -v1624 -v1625 -v1626 -v1627 -v1628 -v1629 -v163 -v1630 -v1631 -v1632 -v1633 -v1634 -v1635 -v1636 -v1637 -v1638 -v1639 -v164 -v1640 -v1641 -v1642 -v1643 -v1644 -v1645 -v1646 -v1647 -v1648 -v1649 -v165 -v1650 -v1651 v1652 -v1653 -v1654 -v1655 -v1656 -v1657 -v1658 -v1659 -v166 -v1660 -v1661 -v1662 -v1663 -v1664 -v1665 -v1666 -v1667 -v1668 -v1669 -v167 v1670 -v1671 -v1672 -v1673 -v1674 -v1675 -v1676 -v1677 -v1678 -v1679 -v168 -v1680 -v1681 -v1682 -v1683 -v1684 -v1685 -v1686 -v1687 -v1688 -v1689 -v169 -v1690 v1691 -v1692 -v1693 -v1694 -v1695 -v1696 -v1697 -v1698 -v1699 -v17 -v170 -v1700 -v1701 -v1702 -v1703 -v1704 -v1705 -v1706 -v1707 -v1708 -v1709 -v171 v1710 -v1711 -v1712 -v1713 -v1714 -v1715 -v1716 -v1717 -v1718 -v1719 -v172 -v1720 -v1721 -v1722 -v1723 -v1724 -v1725 -v1726 -v1727 v1728 -v1729 -v173 -v1730 -v1731 -v1732 -v1733 -v1734 -v1735 -v1736 -v1737 -v1738 -v1739 -v174 -v1740 -v1741 -v1742 -v1743 -v1744 -v1745 -v1746 -v1747 -v1748 -v1749 -v175 v1750 -v1751 -v1752 -v1753 -v1754 -v1755 -v1756 -v1757 -v1758 -v1759 -v176 v1760 -v1761 -v1762 -v1763 -v1764 -v1765 -v1766 -v1767 -v1768 -v1769 -v177 -v1770 -v1771 -v1772 -v1773 -v1774 -v1775 -v1776 -v1777 -v1778 -v1779 -v178 -v1780 -v1781 -v1782 v1783 -v1784 -v1785 -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.37 0.13 0.04 2/54 1860
Raw data (stat): 1860 (runsolver) R 1859 25568 25567 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 805759101 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+9.99981 s]
Raw data (loadavg): 0.46 0.15 0.05 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 1397 0 0 0 984 15 0 0 25 0 1 0 805759101 6557696 1124 4294967295 134512640 135726644 3221224576 3221223184 134741266 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1601 1124 300 300 0 1301 0
vsize: 6404
[startup+19.9999 s]
Raw data (loadavg): 0.55 0.18 0.06 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 1834 0 0 0 1968 31 0 0 25 0 1 0 805759101 9302016 1561 4294967295 134512640 135726644 3221224576 3221223072 134744145 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2271 1561 300 300 0 1971 0
vsize: 9084
[startup+30.0005 s]
Raw data (loadavg): 0.61 0.21 0.07 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 1961 0 0 0 2954 46 0 0 25 0 1 0 805759101 9568256 1688 4294967295 134512640 135726644 3221224576 3221223088 134742621 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2336 1688 300 300 0 2036 0
vsize: 9344
[startup+40.0002 s]
Raw data (loadavg): 0.67 0.23 0.08 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2018 0 0 0 3938 61 0 0 25 0 1 0 805759101 9695232 1745 4294967295 134512640 135726644 3221224576 3221223072 134744063 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2367 1745 300 300 0 2067 0
vsize: 9468
[startup+50.0004 s]
Raw data (loadavg): 0.72 0.26 0.09 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2273 0 0 0 4923 77 0 0 25 0 1 0 805759101 10678272 1807 4294967295 134512640 135726644 3221224576 3221223264 134744989 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2607 1807 300 300 0 2307 0
vsize: 10428
[startup+60.001 s]
Raw data (loadavg): 0.77 0.28 0.10 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2313 0 0 0 5912 89 0 0 25 0 1 0 805759101 10788864 1847 4294967295 134512640 135726644 3221224576 3221223072 134743953 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2634 1847 300 300 0 2334 0
vsize: 10536
[startup+70.0017 s]
Raw data (loadavg): 0.80 0.31 0.11 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2390 0 0 0 6897 103 0 0 25 0 1 0 805759101 11030528 1924 4294967295 134512640 135726644 3221224576 3221223184 134741266 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2693 1924 300 300 0 2393 0
vsize: 10772
[startup+80.0018 s]
Raw data (loadavg): 0.83 0.33 0.12 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2431 0 0 0 7885 116 0 0 25 0 1 0 805759101 11124736 1965 4294967295 134512640 135726644 3221224576 3221223072 134743889 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2716 1965 300 300 0 2416 0
vsize: 10864
[startup+90.0024 s]
Raw data (loadavg): 0.86 0.35 0.12 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2470 0 0 0 8871 130 0 0 25 0 1 0 805759101 11223040 2004 4294967295 134512640 135726644 3221224576 3221223184 134741242 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2740 2004 300 300 0 2440 0
vsize: 10960
[startup+100.002 s]
Raw data (loadavg): 0.88 0.37 0.13 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2495 0 0 0 9859 142 0 0 25 0 1 0 805759101 11223040 2029 4294967295 134512640 135726644 3221224576 3221223072 134744048 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2740 2029 300 300 0 2440 0
vsize: 10960
[startup+110.002 s]
Raw data (loadavg): 0.90 0.39 0.14 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2538 0 0 0 10848 154 0 0 25 0 1 0 805759101 11333632 2072 4294967295 134512640 135726644 3221224576 3221223184 134741242 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2767 2072 300 300 0 2467 0
vsize: 11068
[startup+120.003 s]
Raw data (loadavg): 0.91 0.41 0.15 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2576 0 0 0 11839 163 0 0 25 0 1 0 805759101 11464704 2110 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2799 2110 300 300 0 2499 0
vsize: 11196
[startup+130.002 s]
Raw data (loadavg): 0.92 0.43 0.16 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2619 0 0 0 12827 175 0 0 25 0 1 0 805759101 11558912 2153 4294967295 134512640 135726644 3221224576 3221223184 134741242 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2822 2153 300 300 0 2522 0
vsize: 11288
[startup+140.003 s]
Raw data (loadavg): 0.94 0.45 0.17 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2661 0 0 0 13815 188 0 0 25 0 1 0 805759101 11661312 2195 4294967295 134512640 135726644 3221224576 3221223184 134740854 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2847 2195 300 300 0 2547 0
vsize: 11388
[startup+150.003 s]
Raw data (loadavg): 0.95 0.47 0.18 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2696 0 0 0 14805 198 0 0 25 0 1 0 805759101 11767808 2230 4294967295 134512640 135726644 3221224576 3221223072 134743955 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2873 2230 300 300 0 2573 0
vsize: 11492
[startup+160.003 s]
Raw data (loadavg): 0.95 0.48 0.19 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 2736 0 0 0 15793 210 0 0 25 0 1 0 805759101 11874304 2270 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2899 2270 300 300 0 2599 0
vsize: 11596
[startup+170.003 s]
Raw data (loadavg): 0.96 0.50 0.19 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 3144 0 0 0 16781 222 0 0 25 0 1 0 805759101 13447168 2293 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3283 2293 300 300 0 2983 0
vsize: 13132
[startup+180.004 s]
Raw data (loadavg): 0.97 0.52 0.20 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 3181 0 0 0 17770 234 0 0 25 0 1 0 805759101 13557760 2330 4294967295 134512640 135726644 3221224576 3221223184 134740873 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3310 2330 300 300 0 3010 0
vsize: 13240
[startup+190.003 s]
Raw data (loadavg): 0.97 0.53 0.21 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 3214 0 0 0 18760 244 0 0 25 0 1 0 805759101 13656064 2363 4294967295 134512640 135726644 3221224576 3221223072 134744163 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3334 2363 300 300 0 3034 0
vsize: 13336
[startup+200.003 s]
Raw data (loadavg): 0.97 0.55 0.22 2/54 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 3253 0 0 0 19749 256 0 0 25 0 1 0 805759101 13754368 2402 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3358 2402 300 300 0 3058 0
vsize: 13432
[startup+200.47 s]
Raw data (loadavg): 0.97 0.55 0.22 1/53 1860
Raw data (stat): 1860 (pb2sat) R 1859 25568 25567 0 -1 0 3253 0 0 0 19749 256 0 0 25 0 1 0 805759101 13754368 2402 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3358 2402 300 300 0 3058 0
vsize: 0

Child status: 10
Real time (s): 200.469
CPU time (s): 200.519
CPU user time (s): 197.944
CPU system time (s): 2.57461
CPU usage (%): 100.025
Max. virtual memory (Kb): 13432
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	0
#### END VERIFIER DATA ####