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_33_sat_pb.cnf.cr.opb
MD5SUM	d4fd8917eebbcee2e1b2df9714e1fab8
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	1.59276
Number of variables	1733
Total number of constraints	1256
Number of constraints which are clauses	1188
Number of constraints which are cardinality constraints (but not clauses)	68
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 41931

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-06-15 20:06:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=25147 boxname=wulflinc5 idbench=49 idsolver=18 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d4fd8917eebbcee2e1b2df9714e1fab8  /oldhome/oroussel/tmp/wulflinc5/normalized-fpga35_33_sat_pb.cnf.cr.opb
REAL COMMAND:  pb2sat-v2 /oldhome/oroussel/tmp/wulflinc5/normalized-fpga35_33_sat_pb.cnf.cr.opb
IDLAUNCH: 25147
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        831232 kB
Buffers:         33572 kB
Cached:         147084 kB
SwapCached:        700 kB
Active:          59668 kB
Inactive:       123080 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        830980 kB
SwapTotal:     2097136 kB
SwapFree:      2095508 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5156 kB
Slab:            14968 kB
Committed_AS:    63716 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-15 20:08:01 (client local time) WITH STATUS 10 IN 110.364 SECONDS
stats: 25147 0 110.364 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...

c Decision: 1665/5063	Time: 12.1711/86400
c Decision: 1665/5063	Time: 13.7149/86400
c Decision: 1665/5063	Time: 15.8976/86400
c Decision: 1665/5063	Time: 17.3204/86400
c Decision: 1665/5063	Time: 19.459/86400
c Decision: 1665/5063	Time: 21.3478/86400
c Decision: 1665/5063	Time: 23.8244/86400
c Decision: 1665/5063	Time: 25.4801/86400
c Decision: 1665/5063	Time: 27.9388/86400
c Decision: 1665/5063	Time: 30.4604/86400
c Decision: 1665/5063	Time: 32.885/86400
c Decision: 1665/5063	Time: 35.0407/86400
c Decision: 1665/5063	Time: 37.8312/86400
c Decision: 1665/5063	Time: 40.2489/86400
c Decision: 1665/5063	Time: 42.2486/86400
c Decision: 1665/5063	Time: 44.3972/86400
c Decision: 1665/5063	Time: 46.4059/86400
c Decision: 1665/5063	Time: 49.1675/86400
c Decision: 1665/5063	Time: 51.9261/86400
c Decision: 1665/5063	Time: 54.5187/86400
c Decision: 1665/5063	Time: 57.5972/86400
c Decision: 1665/5063	Time: 60.1759/86400
c Decision: 1665/5063	Time: 62.2275/86400
c Decision: 1665/5063	Time: 64.9991/86400
c Decision: 1665/5063	Time: 67.6837/86400
c Decision: 1665/5063	Time: 70.7452/86400
c Decision: 1665/5063	Time: 73.1199/86400
c Decision: 1665/5063	Time: 75.7125/86400
c Decision: 1665/5063	Time: 78.1861/86400
c Decision: 1665/5063	Time: 80.8197/86400
c Decision: 1665/5063	Time: 83.8453/86400
c Decision: 1665/5063	Time: 86.8738/86400
c Decision: 1665/5063	Time: 89.9573/86400
c Decision: 1665/5063	Time: 93.2848/86400
c Decision: 1665/5063	Time: 95.7424/86400
c Decision: 1665/5063	Time: 99.4109/86400
c Decision: 1665/5063	Time: 102.839/86400
c Decision: 1665/5063	Time: 106.28/86400
c Decision: 1665/5063	Time: 109.432/86400
-800 
-809 
-753 
-1199 
-1097 
-1584 
-1585 
-1586 
-1433 
-1080 
-1421 
-966 
-1513 
-1027 
-1587 
-1359 
-1500 
-1069 
-1588 
-1468 
-1395 
-1074 
-1613 
-1718 
-1028 
-328 
-1512 
-1727 
-883 
-905 
-1005 
-838 
-1083 
-1686 
-1335 
-1029 
1460 
-1690 
-725 
-1693 
-1728 
-1599 
-1533 
-1092 
-1240 
-1192 
-1030 
-1420 
-890 
-1647 
-1474 
-582 
-1540 
-1673 
-1593 
-538 
-214 
-1031 
-1087 
-1465 
-1660 
-1661 
-1646 
-1330 
-1662 
-1432 
-1238 
-1648 
-716 
-1663 
-1664 
-636 
-720 
-1665 
-657 
-749 
-1666 
-1428 
-1522 
-141 
-1667 
-1600 
-1461 
-660 
-918 
-1668 
-1519 
-1595 
1669 
-1411 
-1211 
-754 
-255 
-777 
-1480 
-955 
-1095 
-1155 
-1156 
-1157 
-1158 
-1576 
-915 
-1159 
-1160 
-1161 
-1162 
-1163 
-581 
-1164 
-1165 
-893 
-810 
-1437 
-1166 
-1167 
1168 
-717 
-1169 
-1082 
-1170 
-1171 
-1172 
-1173 
-1713 
-1174 
-1175 
-755 
-380 
-1176 
-1177 
-1122 
-1178 
-1179 
-1180 
-1128 
-1181 
-978 
-979 
-980 
-19 
-580 
-981 
-982 
-983 
-973 
-1107 
-472 
-984 
-985 
-986 
-987 
-988 
-989 
-990 
-751 
-991 
-928 
-992 
993 
-994 
-681 
-866 
-995 
-996 
-997 
-998 
-999 
-885 
-251 
-1000 
-876 
-1001 
-1002 
-1003 
-438 
-439 
-440 
-441 
-974 
-442 
-443 
444 
-445 
-446 
-447 
-448 
-449 
-450 
-451 
-1431 
-452 
-453 
-142 
-143 
-144 
145 
-146 
-147 
-148 
-149 
-844 
-150 
-151 
-152 
-153 
-154 
-155 
-156 
-157 
-364 
-365 
-921 
-366 
-367 
-368 
-369 
-370 
-371 
372 
-373 
-374 
-375 
-653 
-1364 
-376 
-377 
-378 
-379 
-20 
-21 
-22 
-23 
-24 
-25 
-1422 
-26 
-27 
-28 
29 
-30 
-31 
-32 
-33 
-34 
-35 
-1536 
-329 
-330 
331 
-332 
-333 
-334 
-335 
-336 
-337 
-338 
-1075 
-339 
-340 
-341 
-342 
-343 
-344 
-584 
-585 
-586 
-587 
-1703 
588 
-589 
-590 
-591 
-592 
-593 
-594 
-595 
-596 
-597 
-345 
-598 
-599 
-276 
277 
-278 
-279 
-280 
-281 
-282 
-283 
-1714 
-284 
-285 
-286 
-287 
-288 
-289 
-290 
-291 
-125 
-126 
-541 
-127 
-128 
-129 
-130 
-131 
-132 
-133 
-134 
-135 
-136 
-1715 
137 
-138 
-139 
-140 
-160 
-161 
-162 
-163 
-164 
-165 
-1547 
-166 
167 
-168 
-169 
-170 
-171 
-172 
-173 
-174 
-175 
-811 
-1716 
-312 
-313 
-314 
-315 
-316 
317 
-318 
-319 
-320 
-321 
-1405 
-322 
-323 
-324 
-325 
-326 
-327 
-233 
-234 
-235 
-236 
-535 
-237 
-238 
-239 
-240 
-241 
-242 
243 
-244 
-245 
-246 
-1413 
-247 
-248 
-637 
-638 
-639 
-640 
-641 
-642 
-643 
-644 
-1365 
-645 
-646 
-647 
648 
-649 
-650 
-651 
-652 
-55 
-56 
-1592 
-57 
-58 
-59 
-60 
-61 
-62 
-63 
-64 
-65 
-66 
-1336 
-67 
68 
-69 
-70 
-108 
-109 
-110 
-111 
-112 
-113 
-1414 
-114 
-115 
-116 
-117 
-118 
-119 
-120 
-121 
-122 
-123 
-1517 
455 
-456 
-457 
-458 
-459 
-460 
-461 
-462 
-463 
-464 
1473 
-465 
-466 
-467 
-468 
-469 
-470 
-665 
-666 
-667 
-668 
-812 
-1545 
-669 
-670 
-671 
-672 
-673 
-674 
-675 
-676 
-677 
-678 
-1334 
-679 
680 
-72 
-73 
-74 
-75 
-76 
-77 
-78 
-79 
-1515 
-80 
-81 
-82 
-83 
-84 
-85 
86 
-87 
-177 
-178 
-1102 
-179 
-180 
-181 
-182 
183 
-184 
-185 
-186 
-187 
-188 
-1574 
-189 
-190 
-191 
-192 
-193 
-293 
-294 
-295 
-296 
-297 
1429 
-298 
-299 
-300 
-301 
-302 
-303 
-304 
-305 
-306 
-307 
-1638 
308 
-309 
-346 
-347 
-348 
-349 
-350 
-351 
-352 
-353 
-568 
-354 
355 
-356 
-357 
-358 
-359 
-360 
-361 
-362 
-477 
-1639 
-478 
-479 
-480 
-481 
-482 
-483 
-484 
-485 
-486 
-487 
-574 
-488 
-489 
490 
-491 
-492 
-493 
-420 
-421 
-422 
-423 
-813 
-1427 
-424 
-425 
-426 
-427 
-428 
-429 
-430 
-431 
-432 
-433 
-1266 
434 
-435 
-436 
-544 
-545 
-546 
-547 
-548 
-549 
-550 
-1597 
-551 
-552 
-553 
554 
-555 
-556 
-557 
-558 
-559 
-560 
-570 
-728 
-729 
730 
-731 
-732 
-733 
-734 
-735 
-736 
-737 
-663 
-738 
-739 
-740 
-741 
-742 
-743 
-744 
-757 
-758 
-759 
-1598 
-760 
-761 
-762 
-763 
-764 
-765 
-766 
-767 
-768 
-769 
-1121 
-770 
-771 
-772 
-773 
-847 
-848 
-849 
-850 
-851 
-852 
-1112 
-853 
854 
-855 
-856 
-857 
-858 
-859 
-860 
-861 
-862 
-1640 
-863 
-195 
-196 
-197 
-198 
-199 
-200 
-201 
-202 
-203 
-1125 
-204 
-205 
-206 
207 
-208 
-209 
-210 
-211 
-381 
-382 
-814 
-1507 
-383 
-384 
-385 
-386 
-387 
-388 
389 
-390 
-391 
-392 
-1641 
-393 
-394 
-395 
-396 
-397 
-399 
-400 
-401 
-402 
-403 
-471 
404 
-405 
-406 
-407 
-408 
-409 
-410 
-411 
-412 
-413 
-1423 
-414 
-415 
-90 
-91 
-92 
-93 
94 
-95 
-96 
-97 
-1642 
-98 
-99 
-100 
-101 
-102 
-103 
-104 
-105 
-106 
-256 
-1117 
-257 
-258 
-259 
-260 
-261 
-262 
-263 
-264 
-265 
-266 
-846 
267 
-268 
-269 
-270 
-271 
-272 
-778 
-779 
-780 
-781 
-569 
-782 
-783 
-784 
-785 
-786 
-787 
-788 
-789 
-790 
-791 
-1076 
-792 
-793 
794 
2 
-3 
-4 
-5 
-6 
-7 
-8 
-1643 
-9 
-10 
-11 
-12 
-13 
-14 
-15 
-16 
-17 
-18 
-815 
-1091 
-215 
216 
-217 
-218 
-219 
-220 
-221 
-222 
-223 
-224 
-1477 
-225 
-226 
-227 
-228 
-229 
-230 
-231 
-37 
-38 
-39 
-1644 
40 
-41 
-42 
-43 
-44 
-45 
-46 
-47 
-48 
-49 
-1550 
-50 
-51 
-52 
-53 
-1416 
-36 
-1306 
-1307 
1308 
-869 
-816 
-1309 
-1310 
-1311 
-1312 
-1313 
-1314 
-1073 
-1315 
-1110 
-1316 
-817 
-1317 
-1233 
-1318 
-1274 
-1319 
-1320 
-968 
-1321 
-903 
-911 
-801 
-818 
-1322 
-888 
-910 
-1323 
-1004 
-253 
-1324 
-1325 
-1326 
-1106 
-819 
-1327 
-1685 
-1732 
-1729 
-1730 
-1733 
-1425 
-1270 
-124 
-310 
-820 
-1654 
-1525 
-1511 
-1502 
-1271 
-1108 
-1530 
-1184 
-1552 
-292 
-821 
-1624 
-1206 
-909 
-1622 
-1721 
-1531 
1652 
-1402 
-1277 
-1649 
-822 
-89 
-1099 
-1470 
-1398 
-1626 
-1196 
-1368 
-1369 
-1370 
-273 
-823 
-1337 
-1371 
-1372 
-897 
-1373 
-1189 
-576 
-1374 
-1194 
-1375 
-824 
-1376 
-1377 
-1378 
723 
-1379 
-1380 
-1381 
-419 
-1382 
-1383 
-825 
-956 
-1384 
-748 
-726 
-1385 
-1386 
-1387 
-1113 
-912 
-718 
-826 
-1237 
-501 
-502 
-503 
-504 
-505 
-506 
507 
-508 
-509 
-827 
-510 
-511 
-512 
-513 
-514 
-515 
-516 
-517 
-518 
-519 
-802 
-828 
-520 
-521 
-522 
-523 
-524 
-525 
-526 
-527 
-528 
-529 
-829 
-530 
-531 
-532 
-88 
-533 
-534 
-930 
-931 
-601 
-919 
-830 
-889 
-932 
-933 
-934 
-935 
-936 
-937 
-938 
-939 
-940 
-831 
-473 
-941 
-942 
-176 
-943 
-944 
-476 
-945 
-946 
-927 
-832 
-947 
-948 
-949 
-950 
-398 
891 
-654 
-951 
-952 
-953 
-833 
-954 
-1554 
-1555 
-573 
-1556 
-1557 
-1558 
-1559 
-1560 
-1067 
-1129 
-1561 
-1360 
-1272 
-1562 
-1563 
-454 
-1564 
-1542 
-1407 
-1565 
-566 
-1566 
-1236 
-1535 
-875 
-1185 
-1567 
-878 
-1568 
-1569 
-877 
-868 
-1532 
1543 
-1534 
-1570 
-658 
-252 
-1674 
-1424 
-1467 
-562 
-540 
-1675 
-1676 
-842 
-1671 
-1418 
-1036 
-1677 
-722 
-870 
-1678 
803 
-1130 
-1209 
-1538 
-1516 
-1651 
-536 
-1123 
-1679 
-1390 
-1553 
-1409 
-1131 
-1680 
-1601 
1681 
-1659 
-1625 
-1682 
-496 
-1683 
-1684 
-1366 
-1033 
-957 
-1602 
-416 
-1367 
-879 
-1603 
-1201 
-1546 
-1604 
-159 
-1132 
-1463 
-975 
-1397 
-1605 
-1606 
-1607 
-1528 
-1408 
-1591 
-1608 
-1068 
-923 
-1609 
-578 
543 
-1035 
-1610 
-917 
-1207 
-840 
-1393 
-1133 
-1611 
-575 
-881 
-1612 
-1471 
-1484 
-750 
-1119 
-1265 
-898 
-1134 
-746 
-1520 
-1689 
-1203 
-1518 
-1182 
-1331 
-1656 
-1544 
-1504 
-1135 
-1706 
-664 
-1707 
-494 
-1708 
-884 
-1709 
-1235 
-1510 
1200 
-54 
-864 
-1645 
-1670 
-835 
-1412 
-1551 
-1358 
-1539 
-1691 
-1361 
-1136 
-914 
-567 
-1338 
-719 
-213 
-1339 
-1195 
-1340 
-158 
-1341 
-804 
-1137 
-311 
-834 
-1342 
-1343 
-1344 
-1345 
-1346 
-71 
-1347 
-1348 
-1138 
-1349 
-926 
1350 
-1351 
-727 
-1352 
-1353 
-1354 
-1098 
-1355 
-1139 
-965 
-1356 
-922 
-1 
-1085 
-1357 
-1616 
-894 
-537 
-1617 
-1090 
-565 
-1618 
-1094 
-1388 
-1394 
-843 
-925 
-1391 
-500 
-107 
-1140 
-1619 
-1614 
-1620 
-212 
-839 
474 
-1400 
-1549 
-892 
-1594 
-1141 
-1088 
-1529 
-961 
-1078 
-1508 
-656 
-1621 
-1105 
-1037 
-896 
-1142 
-836 
-1485 
-901 
-775 
-1486 
-1487 
-895 
-659 
-1476 
-661 
-1143 
-1488 
-1489 
-1197 
-900 
-1415 
-1490 
-1118 
-662 
-1491 
1032 
-1144 
-916 
-1492 
-1493 
-1494 
-1495 
-1072 
-1208 
-1109 
-1193 
-796 
-1145 
-571 
-1496 
-1188 
-1497 
-1498 
-1499 
-1241 
-1242 
-1243 
-1244 
-805 
-1146 
-882 
1245 
-1246 
-908 
-958 
-1247 
-1248 
-1249 
-887 
-1250 
-1147 
-499 
-1251 
-960 
-1104 
-1210 
-495 
-845 
-1252 
-1253 
-1254 
-874 
-1255 
-1256 
-1257 
-1258 
-1259 
-1260 
-1261 
-1262 
-577 
-1263 
-1148 
-1100 
-1658 
-1704 
-1575 
-1481 
-1710 
-1722 
-1514 
-1695 
579 
798 
-1720 
-1280 
-1333 
-752 
-1482 
-1406 
-1723 
-1127 
-561 
-724 
-1149 
-1392 
-1724 
-1034 
-1472 
-1650 
-1589 
-1653 
-1572 
-797 
-1717 
-1101 
-1524 
-498 
-1725 
-1401 
-1278 
-880 
-682 
-683 
-684 
-685 
-1150 
-686 
-687 
-688 
-689 
-690 
-691 
692 
-693 
-694 
-695 
-1151 
-696 
-697 
-274 
-698 
-699 
-700 
-701 
-702 
-703 
-704 
-1152 
-705 
-706 
-707 
-708 
-709 
-710 
-711 
-712 
-713 
-714 
-806 
-1153 
-715 
-1623 
-1615 
-1627 
-1628 
-1526 
-1629 
-1070 
-1202 
-1630 
-1006 
-1239 
-1631 
-1066 
-906 
-250 
-1506 
-1205 
-1399 
-1632 
-1434 
-417 
-1527 
-1120 
-1633 
-1634 
-902 
-1275 
-1635 
-1571 
-1279 
-1081 
-655 
-1396 
-1389 
-871 
1537 
-1636 
-1590 
-603 
604 
-605 
-606 
-1007 
-607 
-608 
-275 
-609 
-610 
-611 
-612 
-613 
-614 
-615 
-1008 
-616 
-617 
-618 
-619 
-620 
-621 
-622 
-623 
-624 
-625 
-1009 
-626 
-627 
-628 
-629 
-630 
-631 
-632 
-633 
-634 
-635 
-1010 
-249 
-1281 
-1282 
-1283 
-1284 
-1285 
-1286 
-1089 
-1287 
-1204 
-721 
-1288 
-963 
-1267 
-1289 
-1290 
-1291 
-1292 
-1079 
-1038 
-1183 
-1011 
-1293 
-1114 
-1294 
-886 
-1295 
-1296 
-1297 
-1298 
-1299 
-1300 
-807 
-1012 
-1301 
-1302 
1303 
-907 
-1276 
-1304 
962 
-1501 
-1719 
-1523 
-1013 
-1672 
-1731 
-1712 
-1086 
-1509 
-967 
-1404 
-873 
-977 
-795 
-1014 
-1198 
-1103 
-1462 
-1478 
-1637 
-1694 
-1305 
-1234 
-969 
-1726 
1015 
-1269 
-1711 
-1479 
-1687 
-1503 
-747 
-972 
-1264 
-1469 
-1541 
-1016 
-1705 
-1696 
-542 
-1697 
-1521 
-1655 
-1698 
-1548 
-1115 
-1435 
-1017 
-1464 
-232 
-976 
-1466 
-1111 
-1699 
-1688 
-1700 
-1483 
-1186 
-1018 
-1692 
-1701 
-1426 
-1573 
-1126 
-799 
-1596 
-194 
-1096 
-1657 
-1019 
-745 
-1273 
-1702 
-1419 
-1328 
1362 
-1040 
-904 
-1041 
-1042 
-1020 
-913 
-583 
-497 
-1043 
-1044 
-1045 
-1046 
1047 
-475 
-1048 
-1021 
-1049 
-1050 
-602 
-563 
-1051 
-872 
-1052 
-1053 
-1054 
-1055 
-808 
-1022 
-1056 
-1057 
-1058 
-1059 
-1060 
-1061 
-1062 
-971 
-1063 
-1064 
-776 
-1065 
-437 
-1212 
-1213 
-1214 
-1215 
-1216 
-1217 
1218 
-1219 
-1023 
-1220 
-1221 
-924 
-1222 
-1223 
-774 
-970 
-1224 
-1225 
-1226 
-1024 
-1227 
-920 
-1154 
-1228 
-1187 
-1229 
-1230 
-1231 
-1232 
-1190 
-1025 
-1039 
-1093 
-959 
-1071 
-1084 
-1116 
-1438 
-1439 
-1440 
-1441 
-756 
-1442 
-1443 
-1444 
-1403 
-1191 
-1077 
-1445 
-1124 
-1446 
-929 
-1026 
-899 
1447 
-1448 
-865 
-572 
-1449 
-1450 
-1410 
-1451 
-1452 
-564 
-1453 
-1454 
-1455 
-1456 
-418 
-600 
-1457 
-1458 
-1459 
-1329 
-837 
-1268 
-1577 
-1578 
-363 
-1579 
-1580 
-1505 
-1581 
-867 
-1436 
-841 
1582 
-1332 
-1583 
-1417 
-1363 
-1430 
-1475 
-964 
-254 
-539 
s 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 -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.61 0.88 0.88 2/54 2132
Raw data (stat): 2132 (runsolver) R 2131 7266 7265 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 964870299 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.0008 s]
Raw data (loadavg): 0.67 0.88 0.88 2/54 2132
Raw data (stat): 2132 (pb2sat-v2) R 2131 7266 7265 0 -1 0 1415 0 0 0 983 16 0 0 25 0 1 0 964870299 6553600 1143 4294967295 134512640 135730672 3221224576 3221223184 134744655 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1600 1143 301 301 0 1299 0
vsize: 6400
[startup+20.0016 s]
Raw data (loadavg): 0.72 0.89 0.88 2/54 2132
Raw data (stat): 2132 (pb2sat-v2) R 2131 7266 7265 0 -1 0 1632 0 0 0 1968 31 0 0 25 0 1 0 964870299 6930432 1360 4294967295 134512640 135730672 3221224576 3221223184 134744646 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1692 1360 301 301 0 1391 0
vsize: 6768
[startup+30.0019 s]
Raw data (loadavg): 0.76 0.89 0.88 2/54 2132
Raw data (stat): 2132 (pb2sat-v2) R 2131 7266 7265 0 -1 0 1694 0 0 0 2953 46 0 0 25 0 1 0 964870299 7151616 1422 4294967295 134512640 135730672 3221224576 3221223072 134747489 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1746 1422 301 301 0 1445 0
vsize: 6984
[startup+40.002 s]
Raw data (loadavg): 0.80 0.89 0.89 2/54 2132
Raw data (stat): 2132 (pb2sat-v2) R 2131 7266 7265 0 -1 0 1748 0 0 0 3937 62 0 0 25 0 1 0 964870299 7245824 1476 4294967295 134512640 135730672 3221224576 3221223072 134747587 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1769 1476 301 301 0 1468 0
vsize: 7076
[startup+50.0028 s]
Raw data (loadavg): 0.83 0.89 0.89 2/54 2132
Raw data (stat): 2132 (pb2sat-v2) R 2131 7266 7265 0 -1 0 1811 0 0 0 4925 74 0 0 25 0 1 0 964870299 7483392 1539 4294967295 134512640 135730672 3221224576 3221223184 134744794 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1827 1539 301 301 0 1526 0
vsize: 7308
[startup+60.0031 s]
Raw data (loadavg): 0.85 0.90 0.89 2/54 2132
Raw data (stat): 2132 (pb2sat-v2) R 2131 7266 7265 0 -1 0 2031 0 0 0 5913 87 0 0 25 0 1 0 964870299 8269824 1566 4294967295 134512640 135730672 3221224576 3221223184 134744655 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2019 1566 301 301 0 1718 0
vsize: 8076
[startup+70.0033 s]
Raw data (loadavg): 0.88 0.90 0.89 2/54 2132
Raw data (stat): 2132 (pb2sat-v2) R 2131 7266 7265 0 -1 0 2083 0 0 0 6899 100 0 0 25 0 1 0 964870299 8388608 1618 4294967295 134512640 135730672 3221224576 3221223072 134747568 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2048 1618 301 301 0 1747 0
vsize: 8192
[startup+80.004 s]
Raw data (loadavg): 0.89 0.90 0.89 2/54 2132
Raw data (stat): 2132 (pb2sat-v2) R 2131 7266 7265 0 -1 0 2136 0 0 0 7890 109 0 0 25 0 1 0 964870299 8495104 1671 4294967295 134512640 135730672 3221224576 3221223184 134744655 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2074 1671 301 301 0 1773 0
vsize: 8296
[startup+90.0033 s]
Raw data (loadavg): 0.91 0.91 0.89 2/54 2132
Raw data (stat): 2132 (pb2sat-v2) R 2131 7266 7265 0 -1 0 2210 0 0 0 8877 123 0 0 25 0 1 0 964870299 10698752 1745 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2612 1745 301 301 0 2311 0
vsize: 10448
[startup+100.004 s]
Raw data (loadavg): 0.92 0.91 0.89 2/54 2132
Raw data (stat): 2132 (pb2sat-v2) R 2131 7266 7265 0 -1 0 2278 0 0 0 9866 134 0 0 25 0 1 0 964870299 10698752 1813 4294967295 134512640 135730672 3221224576 3221223072 134747657 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2612 1813 301 301 0 2311 0
vsize: 10448
[startup+110.005 s]
Raw data (loadavg): 0.93 0.91 0.89 2/54 2132
Raw data (stat): 2132 (pb2sat-v2) R 2131 7266 7265 0 -1 0 2316 0 0 0 10853 147 0 0 25 0 1 0 964870299 10813440 1851 4294967295 134512640 135730672 3221224576 3221223072 134747543 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2640 1851 301 301 0 2339 0
vsize: 10560
[startup+110.365 s]
Raw data (loadavg): 0.94 0.91 0.89 1/53 2132
Raw data (stat): 2132 (pb2sat-v2) R 2131 7266 7265 0 -1 0 2316 0 0 0 10853 147 0 0 25 0 1 0 964870299 10813440 1851 4294967295 134512640 135730672 3221224576 3221223072 134747543 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2640 1851 301 301 0 2339 0
vsize: 0

Child status: 10
Real time (s): 110.364
CPU time (s): 110.364
CPU user time (s): 108.869
CPU system time (s): 1.49477
CPU usage (%): 99.9998
Max. virtual memory (Kb): 10560
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	0
#### END VERIFIER DATA ####