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 41935

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-06-15 20:06:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=25148 boxname=wulflinc2 idbench=50 idsolver=18 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f49e527e8d063bcfa5508a2b00211475  /oldhome/oroussel/tmp/wulflinc2/normalized-fpga35_34_sat_pb.cnf.cr.opb
REAL COMMAND:  pb2sat-v2 /oldhome/oroussel/tmp/wulflinc2/normalized-fpga35_34_sat_pb.cnf.cr.opb
IDLAUNCH: 25148
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        864088 kB
Buffers:         33484 kB
Cached:         111736 kB
SwapCached:       4448 kB
Active:          60792 kB
Inactive:        89504 kB
HighTotal:      131008 kB
HighFree:        31248 kB
LowTotal:       903652 kB
LowFree:        832840 kB
SwapTotal:     2097136 kB
SwapFree:      2091696 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5052 kB
Slab:            14592 kB
Committed_AS:    71904 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-15 20:18:32 (client local time) WITH STATUS 10 IN 739.202 SECONDS
stats: 25148 0 739.202 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...

c Decision: 1716/5217	Time: 12.7711/86400
c Decision: 1716/5217	Time: 14.5448/86400
c Decision: 1716/5217	Time: 16.0346/86400
c Decision: 1716/5217	Time: 17.7603/86400
c Decision: 1716/5217	Time: 19.3201/86400
c Decision: 1716/5217	Time: 20.9758/86400
c Decision: 1716/5217	Time: 22.6656/86400
c Decision: 1716/5217	Time: 24.9122/86400
c Decision: 1716/5217	Time: 27.3718/86400
c Decision: 1716/5217	Time: 29.4955/86400
c Decision: 1716/5217	Time: 31.2243/86400
c Decision: 1716/5217	Time: 33.4199/86400
c Decision: 1716/5217	Time: 35.4976/86400
c Decision: 1716/5217	Time: 38.1782/86400
c Decision: 1716/5217	Time: 40.9628/86400
c Decision: 1716/5217	Time: 43.9943/86400
c Decision: 1716/5217	Time: 46.097/86400
c Decision: 1716/5217	Time: 48.0827/86400
c Decision: 1716/5217	Time: 50.5953/86400
c Decision: 1716/5217	Time: 53.3979/86400
c Decision: 1716/5217	Time: 55.3526/86400
c Decision: 1716/5217	Time: 57.4163/86400
c Decision: 1716/5217	Time: 60.0279/86400
c Decision: 1716/5217	Time: 62.5005/86400
c Decision: 1716/5217	Time: 65.2921/86400
c Decision: 1716/5217	Time: 67.7287/86400
c Decision: 1716/5217	Time: 70.7912/86400
c Decision: 1716/5217	Time: 73.0079/86400
c Decision: 1716/5217	Time: 75.3016/86400
c Decision: 1716/5217	Time: 77.6102/86400
c Decision: 1716/5217	Time: 80.7987/86400
c Decision: 1716/5217	Time: 82.8974/86400
c Decision: 1716/5217	Time: 85.604/86400
c Decision: 1716/5217	Time: 88.8585/86400
c Decision: 1716/5217	Time: 91.6101/86400
c Decision: 1716/5217	Time: 95.1395/86400
c Decision: 1716/5217	Time: 98.737/86400
c Decision: 1716/5217	Time: 101.941/86400
c Decision: 1716/5217	Time: 105.325/86400
c Decision: 1716/5217	Time: 108.56/86400
c Decision: 1716/5217	Time: 110.995/86400
c Decision: 1716/5217	Time: 113.937/86400
c Decision: 1716/5217	Time: 116.601/86400
c Decision: 1716/5217	Time: 119.491/86400
c Decision: 1716/5217	Time: 122.966/86400
c Decision: 1716/5217	Time: 125.83/86400
c Decision: 1716/5217	Time: 128.858/86400
c Decision: 1716/5217	Time: 132.22/86400
c Decision: 1716/5217	Time: 135.183/86400
c Decision: 1716/5217	Time: 138.612/86400
c Decision: 1716/5217	Time: 142.173/86400
c Decision: 1716/5217	Time: 145.431/86400
c Decision: 1716/5217	Time: 148.222/86400
c Decision: 1716/5217	Time: 151.803/86400
c Decision: 1716/5217	Time: 155.639/86400
c Decision: 1716/5217	Time: 158.422/86400
c Decision: 1716/5217	Time: 161.315/86400
c Decision: 1716/5217	Time: 164.506/86400
c Decision: 1716/5217	Time: 167.654/86400
c Decision: 1716/5217	Time: 170.878/86400
c Decision: 1716/5217	Time: 175.049/86400
c Decision: 1716/5217	Time: 179.305/86400
c Decision: 1716/5217	Time: 183.239/86400
c Decision: 1716/5217	Time: 187.107/86400
c Decision: 1716/5217	Time: 190.391/86400
c Decision: 1716/5217	Time: 193.552/86400
c Decision: 1716/5217	Time: 196.718/86400
c Decision: 1716/5217	Time: 200.994/86400
c Decision: 1716/5217	Time: 204.24/86400
c Decision: 1716/5217	Time: 207.4/86400
c Decision: 1716/5217	Time: 210.844/86400
c Decision: 1716/5217	Time: 213.958/86400
c Decision: 1716/5217	Time: 216.802/86400
c Decision: 1716/5217	Time: 220.956/86400
c Decision: 1716/5217	Time: 224.227/86400
c Decision: 1716/5217	Time: 228.132/86400
c Decision: 1716/5217	Time: 231.042/86400
c Decision: 1716/5217	Time: 234.644/86400
c Decision: 1716/5217	Time: 238.298/86400
c Decision: 1716/5217	Time: 240.528/86400
c Decision: 1716/5217	Time: 244.493/86400
c Decision: 1716/5217	Time: 248.046/86400
c Decision: 1716/5217	Time: 251.415/86400
c Decision: 1716/5217	Time: 254.634/86400
c Decision: 1716/5217	Time: 258.95/86400
c Decision: 1716/5217	Time: 262.355/86400
c Decision: 1716/5217	Time: 266.219/86400
c Decision: 1716/5217	Time: 269.582/86400
c Decision: 1716/5217	Time: 272.578/86400
c Decision: 1716/5217	Time: 276.327/86400
c Decision: 1716/5217	Time: 281.222/86400
c Decision: 1716/5217	Time: 285.745/86400
c Decision: 1716/5217	Time: 290.361/86400
c Decision: 1716/5217	Time: 293.869/86400
c Decision: 1716/5217	Time: 297.447/86400
c Decision: 1716/5217	Time: 301.886/86400
c Decision: 1716/5217	Time: 305.413/86400
c Decision: 1716/5217	Time: 309.436/86400
c Decision: 1716/5217	Time: 313.051/86400
c Decision: 1716/5217	Time: 316.287/86400
c Decision: 1716/5217	Time: 320.347/86400
c Decision: 1716/5217	Time: 324.22/86400
c Decision: 1716/5217	Time: 327.941/86400
c Decision: 1716/5217	Time: 331.985/86400
c Decision: 1716/5217	Time: 336.259/86400
c Decision: 1716/5217	Time: 340.756/86400
c Decision: 1716/5217	Time: 344.472/86400
c Decision: 1716/5217	Time: 347.881/86400
c Decision: 1716/5217	Time: 350.91/86400
c Decision: 1716/5217	Time: 354.535/86400
c Decision: 1716/5217	Time: 359.412/86400
c Decision: 1716/5217	Time: 363.612/86400
c Decision: 1716/5217	Time: 366.623/86400
c Decision: 1716/5217	Time: 370.054/86400
c Decision: 1716/5217	Time: 374.94/86400
c Decision: 1716/5217	Time: 379.438/86400
c Decision: 1716/5217	Time: 384.043/86400
c Decision: 1716/5217	Time: 388.363/86400
c Decision: 1716/5217	Time: 393.145/86400
c Decision: 1716/5217	Time: 396.935/86400
c Decision: 1716/5217	Time: 401.069/86400
c Decision: 1716/5217	Time: 405.581/86400
c Decision: 1716/5217	Time: 409.202/86400
c Decision: 1716/5217	Time: 413.018/86400
c Decision: 1716/5217	Time: 416.931/86400
c Decision: 1716/5217	Time: 420.664/86400
c Decision: 1716/5217	Time: 424.028/86400
c Decision: 1716/5217	Time: 428.717/86400
c Decision: 1716/5217	Time: 433.383/86400
c Decision: 1716/5217	Time: 437.318/86400
c Decision: 1716/5217	Time: 440.896/86400
c Decision: 1716/5217	Time: 443.667/86400
c Decision: 1716/5217	Time: 448.284/86400
c Decision: 1716/5217	Time: 452.103/86400
c Decision: 1716/5217	Time: 456.01/86400
c Decision: 1716/5217	Time: 460.941/86400
c Decision: 1716/5217	Time: 465.348/86400
c Decision: 1716/5217	Time: 469.304/86400
c Decision: 1716/5217	Time: 474.696/86400
c Decision: 1716/5217	Time: 479.32/86400
c Decision: 1716/5217	Time: 484.999/86400
c Decision: 1716/5217	Time: 489.397/86400
c Decision: 1716/5217	Time: 494.541/86400
c Decision: 1716/5217	Time: 499.351/86400
c Decision: 1716/5217	Time: 504.763/86400
c Decision: 1716/5217	Time: 510.487/86400
c Decision: 1716/5217	Time: 513.869/86400
c Decision: 1716/5217	Time: 519.23/86400
c Decision: 1716/5217	Time: 524.417/86400
c Decision: 1716/5217	Time: 529.905/86400
c Decision: 1716/5217	Time: 534.779/86400
c Decision: 1716/5217	Time: 538.584/86400
c Decision: 1716/5217	Time: 543.238/86400
c Decision: 1716/5217	Time: 547.447/86400
c Decision: 1716/5217	Time: 550.525/86400
c Decision: 1716/5217	Time: 554.746/86400
c Decision: 1716/5217	Time: 558.789/86400
c Decision: 1716/5217	Time: 562.921/86400
c Decision: 1716/5217	Time: 567.092/86400
c Decision: 1716/5217	Time: 571.024/86400
c Decision: 1716/5217	Time: 574.583/86400
c Decision: 1716/5217	Time: 578.739/86400
c Decision: 1716/5217	Time: 583.367/86400
c Decision: 1716/5217	Time: 587.625/86400
c Decision: 1716/5217	Time: 591.49/86400
c Decision: 1716/5217	Time: 595.36/86400
c Decision: 1716/5217	Time: 600.954/86400
c Decision: 1716/5217	Time: 605.499/86400
c Decision: 1716/5217	Time: 611.346/86400
c Decision: 1716/5217	Time: 615.947/86400
c Decision: 1716/5217	Time: 620.154/86400
c Decision: 1716/5217	Time: 625.559/86400
c Decision: 1716/5217	Time: 630.733/86400
c Decision: 1716/5217	Time: 634.488/86400
c Decision: 1716/5217	Time: 639.248/86400
c Decision: 1716/5217	Time: 644.251/86400
c Decision: 1716/5217	Time: 650.206/86400
c Decision: 1716/5217	Time: 654.952/86400
c Decision: 1716/5217	Time: 658.931/86400
c Decision: 1716/5217	Time: 664.024/86400
c Decision: 1716/5217	Time: 668.746/86400
c Decision: 1716/5217	Time: 674.436/86400
c Decision: 1716/5217	Time: 677.728/86400
c Decision: 1716/5217	Time: 681.16/86400
c Decision: 1716/5217	Time: 684.323/86400
c Decision: 1716/5217	Time: 689.114/86400
c Decision: 1716/5217	Time: 692.645/86400
c Decision: 1716/5217	Time: 695.738/86400
c Decision: 1716/5217	Time: 701.719/86400
c Decision: 1716/5217	Time: 708.103/86400
c Decision: 1716/5217	Time: 714.21/86400
c Decision: 1716/5217	Time: 718.402/86400
c Decision: 1716/5217	Time: 722.788/86400
c Decision: 1716/5217	Time: 727.095/86400
c Decision: 1716/5217	Time: 731.38/86400
c Decision: 1716/5217	Time: 735.65/86400
-109 
-118 
-1196 
-607 
-608 
-609 
-610 
-611 
-612 
-613 
-614 
-615 
-616 
-1197 
-617 
-618 
-619 
-620 
-621 
-622 
-1212 
-1213 
-1214 
-1215 
-1198 
-1216 
-1217 
-964 
-1218 
-1219 
-1220 
-1221 
-1222 
-848 
-1223 
-1199 
-1224 
1225 
-1226 
-887 
-1227 
-1228 
-1229 
-1230 
-1231 
-1232 
-919 
-1233 
-1077 
-1234 
-1235 
-1236 
-1237 
-1238 
-1239 
-1240 
-1241 
-1200 
-1242 
-1483 
-1108 
-1282 
-1460 
-771 
-1484 
-1485 
-1409 
-1475 
-1057 
-1486 
1487 
-1245 
-1471 
-1488 
-1403 
-1489 
-1490 
-1277 
-1491 
-1283 
-1366 
-308 
-1492 
-1493 
-1494 
-1495 
-1496 
-1359 
-1279 
-1497 
-1284 
-1498 
-1398 
-1499 
-1500 
-1501 
-1502 
-710 
1520 
-1521 
-1404 
-1285 
-1461 
-1522 
-1523 
-1093 
-1524 
-1525 
-1400 
-1526 
-1527 
-1528 
-119 
-1286 
-1529 
-1530 
-1531 
-1532 
-918 
-1346 
-1207 
-1533 
-1356 
-1392 
-1015 
-1534 
-1535 
-587 
-1085 
-1347 
-1362 
-1536 
-1537 
-1065 
-1456 
1287 
-1538 
-1413 
-1641 
-1642 
-849 
-1336 
-1643 
-1508 
-1644 
-1645 
-1288 
-1646 
-1506 
-1601 
-1507 
-967 
-1348 
-1647 
-1648 
-1466 
1649 
-1289 
-1650 
-669 
-884 
-1396 
-1470 
-1423 
-1607 
-1367 
-1312 
-1651 
-1290 
-1477 
-1652 
-1653 
-962 
-1047 
-1654 
-924 
-925 
-926 
-927 
-1291 
-928 
-929 
-930 
-931 
-932 
-933 
-934 
-935 
-936 
-326 
-1292 
-937 
-938 
-939 
-940 
-941 
-942 
-943 
944 
-945 
-946 
-1293 
-947 
-948 
-949 
-950 
-951 
-952 
-953 
-886 
-954 
-955 
-144 
-956 
-253 
-254 
-255 
-256 
-257 
-258 
-259 
-260 
-261 
-120 
-648 
-262 
-263 
-264 
-265 
-266 
-267 
-268 
269 
-483 
-484 
-1049 
-485 
-486 
-487 
-488 
-489 
-490 
-491 
-492 
-493 
-494 
-1294 
-495 
-496 
497 
-498 
-499 
-442 
-443 
-444 
-445 
-446 
-1295 
-447 
-448 
-449 
-450 
-451 
-452 
-453 
454 
-455 
-456 
-1201 
-457 
-458 
-92 
-93 
-94 
-95 
-96 
-97 
-98 
-99 
-1296 
-100 
-101 
-102 
-103 
-104 
-105 
-106 
107 
-108 
-712 
-1297 
-713 
-714 
-715 
-716 
-717 
-718 
-719 
-720 
-721 
-722 
-1298 
723 
-724 
-725 
-726 
-727 
-728 
791 
-792 
-793 
-794 
-1299 
-795 
-796 
-797 
-798 
-799 
-800 
-801 
-802 
-803 
-804 
-1075 
-805 
-806 
-807 
-504 
-505 
-506 
-507 
-508 
-509 
-510 
-121 
-1300 
-511 
-512 
513 
-514 
-515 
-516 
-517 
-518 
-519 
-520 
-1301 
-752 
-753 
-754 
-755 
-756 
-757 
758 
-759 
-760 
-761 
-1302 
-762 
-763 
-764 
-765 
-766 
-767 
-768 
-671 
-672 
-673 
-1303 
-674 
-675 
676 
-677 
-678 
-679 
-680 
-681 
-682 
-683 
-328 
-684 
-685 
-686 
-687 
-2 
-3 
-4 
-5 
-6 
-7 
-847 
-8 
9 
-10 
-11 
-12 
-13 
-14 
-15 
-16 
-17 
-1304 
-18 
-217 
-218 
-219 
-220 
-221 
-222 
-223 
-224 
-225 
-1305 
-226 
-227 
-228 
-229 
230 
-231 
-232 
-233 
-350 
351 
-1306 
-352 
-353 
-354 
-355 
-356 
-357 
-358 
-359 
-360 
-361 
-1307 
-362 
-363 
-364 
-365 
-366 
-388 
-389 
390 
-391 
-392 
-122 
-1308 
-393 
-394 
-395 
-396 
-397 
-398 
-399 
-400 
-401 
-402 
-973 
-403 
-404 
-145 
-146 
-147 
-148 
-149 
-150 
-151 
-152 
-974 
153 
-154 
-155 
-156 
-157 
-158 
-159 
-160 
-161 
-74 
-975 
-75 
-76 
77 
-78 
-79 
-80 
-81 
-82 
-83 
-84 
-976 
-85 
-86 
-87 
-88 
-89 
-90 
-38 
-39 
-40 
-41 
-977 
42 
-43 
-44 
-45 
-46 
-47 
-48 
-49 
-50 
-51 
-978 
-52 
-53 
-54 
-774 
-775 
-776 
-777 
-778 
-779 
-780 
-979 
-781 
-782 
-783 
784 
-785 
-786 
-787 
-788 
-789 
-790 
-980 
-406 
-407 
-408 
-409 
-410 
-411 
-412 
-413 
414 
-415 
-981 
-416 
-417 
-418 
-419 
-420 
-421 
-422 
-271 
-272 
-273 
123 
-982 
-274 
-275 
-276 
-277 
-278 
-279 
-280 
-281 
282 
-283 
-983 
-284 
-285 
-286 
-287 
-424 
-425 
-426 
-427 
-428 
-429 
-984 
-430 
-431 
-432 
-433 
-434 
-435 
-436 
-437 
438 
-439 
-985 
-440 
309 
-310 
-311 
-312 
-313 
-314 
-315 
-316 
-317 
-986 
-318 
-319 
-320 
-321 
-322 
-323 
-324 
-325 
-732 
-733 
-987 
-734 
-735 
-736 
-737 
-738 
-739 
-740 
-741 
-742 
-743 
-988 
-744 
-745 
-746 
-747 
748 
-56 
-57 
-58 
-59 
-60 
989 
-61 
62 
-63 
-64 
-65 
-66 
-67 
-68 
-69 
-70 
-990 
-71 
-72 
-650 
-651 
-652 
-653 
-654 
-655 
-656 
-657 
-991 
-658 
-659 
-660 
-661 
-662 
-663 
-664 
665 
-666 
-163 
-124 
-992 
-164 
165 
-166 
-167 
-168 
-169 
-170 
-171 
-172 
-173 
-993 
-174 
-175 
-176 
-177 
-178 
-179 
-236 
-237 
-238 
-239 
-994 
-240 
-241 
-242 
-243 
-244 
-245 
-246 
-247 
-248 
249 
-995 
-250 
-251 
-252 
-181 
-182 
-183 
-184 
-185 
-186 
-187 
-996 
-188 
-189 
-190 
191 
-192 
-193 
-194 
-195 
-196 
-197 
-997 
-692 
-693 
-694 
-695 
696 
-697 
-698 
-699 
-700 
-701 
-998 
-702 
-703 
-704 
-705 
-706 
-707 
-708 
-199 
200 
-201 
-999 
-202 
-203 
-204 
-205 
-206 
-207 
-208 
-209 
-210 
-211 
-1000 
-212 
-213 
-214 
-215 
-20 
-21 
-22 
23 
-24 
-25 
-1001 
-26 
-27 
-28 
-29 
-30 
-31 
-32 
-33 
-34 
-35 
-125 
-1002 
-36 
-332 
-333 
-334 
-335 
-336 
-337 
-338 
339 
-340 
-1003 
-341 
-342 
-343 
-344 
-345 
-346 
-347 
-348 
-368 
-369 
-1004 
-370 
-371 
-372 
-373 
-374 
-375 
-376 
-377 
-378 
-379 
-1005 
-380 
-381 
-382 
-383 
-384 
-462 
-463 
-464 
-465 
-466 
-1006 
467 
-468 
-469 
-470 
-471 
-472 
-473 
-474 
-475 
-476 
-1007 
-477 
-478 
-291 
-292 
-293 
-294 
-295 
-296 
-297 
-298 
-1467 
-299 
300 
-301 
-302 
-303 
-304 
-305 
-306 
-307 
-624 
-1325 
-625 
-626 
-627 
-628 
-629 
-630 
-631 
-632 
-633 
-634 
-1451 
-635 
636 
-637 
-638 
-639 
-640 
-1331 
-126 
-1636 
-881 
-1748 
-1402 
-670 
-1581 
-1624 
-1749 
-1699 
-1078 
-127 
-1079 
-1679 
-1446 
-1605 
-1341 
-1680 
-1705 
-731 
-1447 
885 
-110 
-128 
-1734 
-1750 
-1505 
-1087 
-1610 
-1681 
-1751 
-1539 
-1244 
-1618 
-129 
-1395 
-1140 
-1141 
-1142 
-1143 
-1144 
-1081 
-503 
-1145 
-1060 
-130 
-1146 
-1147 
-1148 
-1149 
-1150 
-1151 
-1152 
-969 
-1153 
-769 
-131 
-1154 
-1155 
-1156 
-1157 
-1158 
-1159 
1160 
-1161 
-1162 
-1163 
-132 
-1164 
-1165 
-1166 
-1167 
-844 
-1168 
-1109 
-1110 
-441 
-1111 
-133 
-1112 
-1113 
-1114 
-1115 
-1116 
-1074 
-1117 
-1118 
-1119 
-1072 
-134 
-1120 
-1121 
-1084 
-968 
-1064 
-1122 
1123 
-1124 
-1125 
-1126 
-135 
-1127 
-1128 
-1129 
-1083 
-1130 
-1131 
-1132 
-1133 
-1134 
-1135 
-136 
-1136 
-554 
-555 
-556 
-557 
-558 
-559 
-560 
-561 
-562 
-137 
-563 
-564 
-565 
-566 
-567 
-568 
-37 
-569 
-570 
-571 
-111 
-138 
-572 
-573 
-574 
-575 
-576 
-577 
-235 
-578 
-579 
-580 
-139 
-581 
-582 
-583 
-584 
585 
-586 
-1626 
-482 
-1352 
-1399 
-140 
-1203 
-1391 
-1627 
-882 
-1105 
-1628 
-216 
1629 
-1059 
-1054 
-141 
-1630 
-1611 
-1631 
-1139 
-270 
-1632 
-1633 
-1138 
-1355 
-1615 
-142 
-1480 
-1548 
-1583 
-1634 
-1635 
-1509 
-841 
-642 
-1280 
-1360 
-143 
-623 
-963 
-1518 
-1622 
-1321 
-923 
-1736 
-1243 
-1706 
-1765 
-521 
1600 
-1603 
-1100 
-1313 
-1327 
-1351 
-1401 
-1776 
-1464 
-1103 
-522 
-1052 
-1323 
-1698 
-1010 
-1542 
-1707 
-1764 
-1616 
-1278 
-588 
-523 
-1657 
-1726 
-1725 
-461 
-1476 
-1317 
-589 
-1369 
1370 
-1371 
-524 
-770 
-1281 
-1372 
-1373 
-1374 
-1339 
-1066 
-1375 
-1376 
-1332 
-112 
-525 
-1377 
-1378 
-1048 
-688 
-750 
-808 
-1137 
-1379 
-1380 
-1381 
-526 
-1382 
-1383 
-1384 
-1385 
-1386 
-1337 
-1387 
-1388 
-1389 
-921 
-527 
-1329 
-1247 
-1248 
-1249 
-1250 
-1251 
-1252 
-1253 
-1008 
-1254 
-528 
-1255 
-1256 
-1257 
-1258 
-1259 
-1092 
-1260 
-1202 
-1261 
-1262 
-529 
-1263 
-690 
-1264 
-1265 
-1266 
-1267 
-1056 
-1268 
-1269 
-1270 
-530 
-1097 
331 
-1271 
-1272 
-1273 
-966 
-1754 
-1458 
-1755 
-1756 
-531 
-1326 
-1757 
-1606 
-751 
-1700 
-1577 
-1735 
-1731 
-643 
-1473 
-532 
-1701 
-845 
-1729 
-1727 
-1450 
-1364 
-1517 
-1758 
958 
-1625 
-533 
-289 
-1759 
-1503 
-1319 
-1107 
-329 
-846 
-1104 
-1760 
-1421 
-534 
-1761 
-1710 
-1582 
-1510 
-1711 
-711 
-1712 
-1309 
-1713 
-1697 
-113 
-535 
-1448 
-1578 
-349 
-1457 
-1609 
-1637 
-1053 
-1514 
1349 
-1714 
-536 
-1715 
-1716 
-1462 
-1717 
-1204 
-1459 
-1357 
-1088 
-1614 
-1086 
-537 
-1718 
-1638 
-667 
-1416 
-1333 
-1719 
-1661 
-1310 
-1662 
-1663 
-538 
-970 
-1089 
-1664 
-1080 
-730 
-1017 
-1511 
-1612 
-1665 
-1608 
-539 
-1666 
-922 
-1463 
-1338 
-1667 
1668 
-1350 
-1095 
-1090 
-1098 
-540 
-1660 
-1669 
-1670 
-1671 
-1672 
-330 
-1673 
-1573 
-1465 
-1674 
-541 
-1014 
-1426 
-1210 
-1427 
-1428 
-1170 
-1410 
-1429 
-1430 
-1328 
-542 
-1431 
-1062 
-1432 
-1433 
-459 
-1434 
-1407 
-1435 
-1436 
-1437 
-481 
-1438 
-1069 
-1439 
-1440 
-1335 
1424 
-1441 
-689 
-1442 
-1443 
-543 
-1418 
-644 
-1444 
-1445 
-1205 
-1408 
850 
-851 
-852 
-853 
-114 
-544 
-854 
-855 
-856 
-857 
-858 
-709 
-859 
-860 
-861 
-862 
-545 
-863 
-864 
-865 
-843 
-385 
-866 
-867 
-868 
-869 
-870 
-546 
-871 
-872 
-873 
-874 
-842 
-875 
-876 
-877 
-646 
-878 
-547 
-879 
-1781 
-1469 
-880 
-920 
-1678 
-1549 
-1752 
-1774 
-1708 
-198 
-1733 
-1363 
-1782 
-387 
-1340 
-1722 
-1076 
-1621 
-1546 
-1780 
-548 
-423 
-1417 
-1572 
-1390 
-1516 
-1720 
-1779 
-180 
-1368 
-1703 
-549 
-1682 
-1211 
-1613 
-1316 
-1639 
1604 
-888 
-889 
-890 
-91 
-550 
891 
-892 
-893 
-894 
-895 
-896 
-897 
-898 
-480 
-899 
551 
-900 
-901 
-902 
-903 
-729 
-904 
-905 
-906 
-907 
-908 
-552 
-909 
-910 
-911 
-912 
-913 
-19 
-914 
-367 
-915 
-916 
-115 
-553 
-668 
-1768 
-1209 
-1274 
-1769 
-1324 
-1675 
-1730 
1016 
-1619 
-1171 
-1099 
-1770 
-1721 
-959 
-1704 
-1050 
-1753 
-1070 
-1584 
-288 
-1172 
-1012 
-1541 
-1732 
-1551 
-1659 
-749 
-1504 
-1762 
-1771 
-960 
-641 
-479 
-1772 
-1482 
-1550 
-1773 
-1415 
-1073 
-1425 
-1552 
-1453 
1173 
-1420 
-1553 
-1554 
-1555 
-1556 
-1557 
-1558 
-1559 
-1560 
-1101 
-1174 
-1561 
-1276 
-1544 
-1562 
-1563 
-1543 
-1564 
-1091 
-1067 
-1082 
-1175 
-1565 
-1566 
-1567 
-1322 
-1568 
1545 
-1569 
-1570 
-1206 
-1246 
-1176 
-1571 
-1585 
-1472 
-1586 
-1587 
-1106 
-1588 
-1589 
-1513 
-1096 
-1177 
-1574 
-1397 
-1540 
-647 
1590 
-73 
-1405 
-1419 
-1591 
-1592 
-1013 
-883 
-1593 
-1594 
-1595 
-649 
-1354 
-1596 
-965 
-691 
-1394 
-116 
-1178 
-1580 
-1411 
-1597 
-1598 
-386 
-1314 
-1344 
-1579 
-1724 
-1775 
-1179 
-1783 
-1061 
-1515 
-1102 
-1318 
-1051 
-1784 
-1655 
-1763 
-234 
-1180 
-1656 
-1778 
-1785 
-1677 
-1449 
-1575 
-1723 
-972 
-1767 
-1422 
-1181 
-162 
-1393 
-1055 
1334 
-1071 
-1414 
-1353 
-1094 
-1777 
-1766 
-1182 
-1343 
-1018 
-1019 
-1020 
-327 
-1021 
-1022 
-1023 
-1024 
-1025 
-1183 
-502 
-1026 
-1027 
1028 
-1029 
-957 
-1030 
-773 
-405 
-1031 
-1184 
-1032 
-1033 
-1034 
-1035 
-1036 
-1037 
-1038 
-1039 
-1040 
-1041 
-1185 
-500 
-1042 
-1043 
-1044 
-1045 
-1046 
-1737 
-1009 
-1709 
-1412 
-1169 
-1452 
-1738 
-1739 
-1342 
-1740 
-1741 
-1742 
-1512 
-1728 
-1330 
-1186 
-1208 
-1275 
-1676 
-1620 
-1743 
-1599 
-1315 
-1519 
-1744 
-1745 
-117 
-1187 
-772 
-1481 
-961 
-1058 
1640 
-1746 
-1747 
-1702 
-1358 
-290 
-1188 
-1696 
-1320 
-1068 
-917 
-1474 
-1683 
1684 
-1685 
-1617 
-1406 
-1189 
-1011 
-1658 
-1311 
-1686 
-1687 
-1361 
-1688 
-1478 
-1455 
-1689 
-1190 
-1365 
-1547 
-1690 
-1479 
-1691 
-1602 
-1692 
-1454 
-1693 
-1623 
-1191 
-1468 
-1694 
-1345 
-1695 
-971 
-1576 
-809 
-810 
-811 
-812 
-1192 
-813 
-814 
-815 
-816 
-817 
-818 
-819 
-820 
-821 
-822 
-1193 
-645 
-823 
-824 
-825 
-826 
-827 
-828 
-829 
-55 
-830 
-1194 
-831 
-832 
833 
-834 
-835 
-836 
-837 
-838 
-501 
-839 
-1063 
-840 
-590 
-591 
-460 
-592 
-593 
-594 
-595 
-596 
597 
-1195 
-1 
-598 
-599 
-600 
-601 
-602 
-603 
-604 
-605 
-606 
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 -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.62 0.86 0.87 1/54 29315
Raw data (stat): 29315 (runsolver) R 29314 31399 31398 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 964874430 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 s]
Raw data (loadavg): 0.68 0.86 0.87 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 1475 0 0 0 982 17 0 0 25 0 1 0 964874430 6692864 1203 4294967295 134512640 135730672 3221224576 3221223072 134747735 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1634 1203 301 301 0 1333 0
vsize: 6536
[startup+19.9997 s]
Raw data (loadavg): 0.73 0.86 0.88 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 1691 0 0 0 1968 31 0 0 25 0 1 0 964874430 7073792 1419 4294967295 134512640 135730672 3221224576 3221223072 134747811 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1727 1419 301 301 0 1426 0
vsize: 6908
[startup+30.0009 s]
Raw data (loadavg): 0.77 0.87 0.88 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 1753 0 0 0 2953 45 0 0 25 0 1 0 964874430 7290880 1481 4294967295 134512640 135730672 3221224576 3221223072 134747489 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1780 1481 301 301 0 1479 0
vsize: 7120
[startup+40.0011 s]
Raw data (loadavg): 0.80 0.87 0.88 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 1818 0 0 0 3942 56 0 0 25 0 1 0 964874430 7487488 1546 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1828 1546 301 301 0 1527 0
vsize: 7312
[startup+50.0008 s]
Raw data (loadavg): 0.83 0.88 0.88 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 1859 0 0 0 4931 66 0 0 25 0 1 0 964874430 7581696 1587 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1851 1587 301 301 0 1550 0
vsize: 7404
[startup+60.0008 s]
Raw data (loadavg): 0.86 0.88 0.88 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2118 0 0 0 5920 77 0 0 25 0 1 0 964874430 8470528 1653 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2068 1653 301 301 0 1767 0
vsize: 8272
[startup+70.0012 s]
Raw data (loadavg): 0.88 0.88 0.88 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2168 0 0 0 6906 91 0 0 25 0 1 0 964874430 8593408 1703 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2098 1703 301 301 0 1797 0
vsize: 8392
[startup+80.0019 s]
Raw data (loadavg): 0.90 0.89 0.88 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2209 0 0 0 7895 103 0 0 25 0 1 0 964874430 8708096 1744 4294967295 134512640 135730672 3221224576 3221223232 134748661 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2126 1744 301 301 0 1825 0
vsize: 8504
[startup+90.0019 s]
Raw data (loadavg): 0.91 0.89 0.88 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2254 0 0 0 8883 115 0 0 25 0 1 0 964874430 8806400 1789 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2150 1789 301 301 0 1849 0
vsize: 8600
[startup+100.001 s]
Raw data (loadavg): 0.93 0.89 0.88 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2289 0 0 0 9871 127 0 0 25 0 1 0 964874430 11010048 1824 4294967295 134512640 135730672 3221224576 3221223184 134744850 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2688 1824 301 301 0 2387 0
vsize: 10752
[startup+110.002 s]
Raw data (loadavg): 0.94 0.89 0.88 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2381 0 0 0 10857 141 0 0 25 0 1 0 964874430 11108352 1916 4294967295 134512640 135730672 3221224576 3221223072 134747584 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2712 1916 301 301 0 2411 0
vsize: 10848
[startup+120.002 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2450 0 0 0 11844 154 0 0 25 0 1 0 964874430 11227136 1985 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2741 1985 301 301 0 2440 0
vsize: 10964
[startup+130.002 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2487 0 0 0 12833 165 0 0 25 0 1 0 964874430 11325440 2022 4294967295 134512640 135730672 3221224576 3221223184 134744732 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2765 2022 301 301 0 2464 0
vsize: 11060
[startup+140.002 s]
Raw data (loadavg): 0.96 0.90 0.89 3/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2515 0 0 0 13822 176 0 0 25 0 1 0 964874430 11325440 2050 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2765 2050 301 301 0 2464 0
vsize: 11060
[startup+150.002 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2562 0 0 0 14811 188 0 0 25 0 1 0 964874430 11460608 2097 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2798 2097 301 301 0 2497 0
vsize: 11192
[startup+160.003 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2633 0 0 0 15802 197 0 0 25 0 1 0 964874430 11554816 2168 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2821 2168 301 301 0 2520 0
vsize: 11284
[startup+170.002 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2662 0 0 0 16791 208 0 0 25 0 1 0 964874430 11673600 2197 4294967295 134512640 135730672 3221224576 3221223184 134744732 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2850 2197 301 301 0 2549 0
vsize: 11400
[startup+180.003 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2677 0 0 0 17783 216 0 0 25 0 1 0 964874430 11673600 2212 4294967295 134512640 135730672 3221224576 3221223088 134746168 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2850 2212 301 301 0 2549 0
vsize: 11400
[startup+190.004 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 2700 0 0 0 18775 224 0 0 25 0 1 0 964874430 11767808 2235 4294967295 134512640 135730672 3221224576 3221223184 134744432 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2873 2235 301 301 0 2572 0
vsize: 11492
[startup+200.003 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3119 0 0 0 19766 233 0 0 25 0 1 0 964874430 13340672 2269 4294967295 134512640 135730672 3221224576 3221223184 134744826 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3257 2269 301 301 0 2956 0
vsize: 13028
[startup+210.003 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3143 0 0 0 20756 243 0 0 25 0 1 0 964874430 13455360 2293 4294967295 134512640 135730672 3221224576 3221223184 134744850 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3285 2293 301 301 0 2984 0
vsize: 13140
[startup+220.004 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3205 0 0 0 21747 253 0 0 25 0 1 0 964874430 13684736 2355 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3341 2355 301 301 0 3040 0
vsize: 13364
[startup+230.004 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3276 0 0 0 22735 265 0 0 25 0 1 0 964874430 13684736 2426 4294967295 134512640 135730672 3221224576 3221223184 134744836 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3341 2426 301 301 0 3040 0
vsize: 13364
[startup+240.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3305 0 0 0 23725 275 0 0 25 0 1 0 964874430 13783040 2455 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3365 2455 301 301 0 3064 0
vsize: 13460
[startup+250.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3334 0 0 0 24716 285 0 0 25 0 1 0 964874430 13893632 2484 4294967295 134512640 135730672 3221224576 3221223184 134744655 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3392 2484 301 301 0 3091 0
vsize: 13568
[startup+260.005 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3363 0 0 0 25706 295 0 0 25 0 1 0 964874430 13893632 2513 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3392 2513 301 301 0 3091 0
vsize: 13568
[startup+270.005 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3380 0 0 0 26696 305 0 0 25 0 1 0 964874430 14000128 2530 4294967295 134512640 135730672 3221224576 3221223184 134744826 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3418 2530 301 301 0 3117 0
vsize: 13672
[startup+280.005 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3402 0 0 0 27688 313 0 0 25 0 1 0 964874430 14000128 2552 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3418 2552 301 301 0 3117 0
vsize: 13672
[startup+290.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3426 0 0 0 28679 322 0 0 25 0 1 0 964874430 14106624 2576 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3444 2576 301 301 0 3143 0
vsize: 13776
[startup+300.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3447 0 0 0 29671 331 0 0 25 0 1 0 964874430 14106624 2597 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3444 2597 301 301 0 3143 0
vsize: 13776
[startup+310.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3467 0 0 0 30662 340 0 0 25 0 1 0 964874430 14106624 2617 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3444 2617 301 301 0 3143 0
vsize: 13776
[startup+320.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3492 0 0 0 31655 347 0 0 25 0 1 0 964874430 14217216 2642 4294967295 134512640 135730672 3221224576 3221223184 134744826 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3471 2642 301 301 0 3170 0
vsize: 13884
[startup+330.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3530 0 0 0 32644 358 0 0 25 0 1 0 964874430 14352384 2680 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3504 2680 301 301 0 3203 0
vsize: 14016
[startup+340.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3547 0 0 0 33637 366 0 0 25 0 1 0 964874430 14352384 2697 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3504 2697 301 301 0 3203 0
vsize: 14016
[startup+350.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3566 0 0 0 34630 373 0 0 25 0 1 0 964874430 14352384 2716 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3504 2716 301 301 0 3203 0
vsize: 14016
[startup+360.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3588 0 0 0 35622 381 0 0 25 0 1 0 964874430 14458880 2738 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3530 2738 301 301 0 3229 0
vsize: 14120
[startup+370.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3617 0 0 0 36612 391 0 0 25 0 1 0 964874430 14458880 2767 4294967295 134512640 135730672 3221224576 3221223184 134744649 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3530 2767 301 301 0 3229 0
vsize: 14120
[startup+380.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3636 0 0 0 37604 399 0 0 25 0 1 0 964874430 14573568 2786 4294967295 134512640 135730672 3221224576 3221223184 134744826 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3558 2786 301 301 0 3257 0
vsize: 14232
[startup+390.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3653 0 0 0 38594 409 0 0 25 0 1 0 964874430 14573568 2803 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3558 2803 301 301 0 3257 0
vsize: 14232
[startup+400.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3672 0 0 0 39586 417 0 0 25 0 1 0 964874430 14573568 2822 4294967295 134512640 135730672 3221224576 3221223184 134744826 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3558 2822 301 301 0 3257 0
vsize: 14232
[startup+410.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3703 0 0 0 40580 424 0 0 25 0 1 0 964874430 14708736 2853 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3591 2853 301 301 0 3290 0
vsize: 14364
[startup+420.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3716 0 0 0 41574 430 0 0 25 0 1 0 964874430 14708736 2866 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3591 2866 301 301 0 3290 0
vsize: 14364
[startup+430.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3743 0 0 0 42566 438 0 0 25 0 1 0 964874430 14811136 2893 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3616 2893 301 301 0 3315 0
vsize: 14464
[startup+440.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3758 0 0 0 43558 446 0 0 25 0 1 0 964874430 14811136 2908 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3616 2908 301 301 0 3315 0
vsize: 14464
[startup+450.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3795 0 0 0 44550 454 0 0 25 0 1 0 964874430 14917632 2945 4294967295 134512640 135730672 3221224576 3221223184 134744826 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3642 2945 301 301 0 3341 0
vsize: 14568
[startup+460.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3835 0 0 0 45543 461 0 0 25 0 1 0 964874430 14917632 2985 4294967295 134512640 135730672 3221224576 3221223184 134744868 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3642 2985 301 301 0 3341 0
vsize: 14568
[startup+470.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3865 0 0 0 46538 467 0 0 25 0 1 0 964874430 14917632 3015 4294967295 134512640 135730672 3221224576 3221223184 134744850 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3642 3015 301 301 0 3341 0
vsize: 14568
[startup+480.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3896 0 0 0 47530 475 0 0 25 0 1 0 964874430 15024128 3046 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3668 3046 301 301 0 3367 0
vsize: 14672
[startup+490.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3906 0 0 0 48522 483 0 0 25 0 1 0 964874430 15024128 3056 4294967295 134512640 135730672 3221224576 3221223184 134744459 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3668 3056 301 301 0 3367 0
vsize: 14672
[startup+500.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3927 0 0 0 49513 492 0 0 25 0 1 0 964874430 15118336 3077 4294967295 134512640 135730672 3221224576 3221223088 134746168 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3691 3077 301 301 0 3390 0
vsize: 14764
[startup+510.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3935 0 0 0 50506 499 0 0 25 0 1 0 964874430 15118336 3085 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3691 3085 301 301 0 3390 0
vsize: 14764
[startup+520.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3960 0 0 0 51499 507 0 0 25 0 1 0 964874430 15216640 3110 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3715 3110 301 301 0 3414 0
vsize: 14860
[startup+530.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3969 0 0 0 52491 515 0 0 25 0 1 0 964874430 15216640 3119 4294967295 134512640 135730672 3221224576 3221223184 134744826 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3715 3119 301 301 0 3414 0
vsize: 14860
[startup+540.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 3997 0 0 0 53481 525 0 0 25 0 1 0 964874430 15216640 3147 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3715 3147 301 301 0 3414 0
vsize: 14860
[startup+550.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 4009 0 0 0 54472 534 0 0 25 0 1 0 964874430 15216640 3159 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3715 3159 301 301 0 3414 0
vsize: 14860
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 4061 0 0 0 55464 543 0 0 25 0 1 0 964874430 15478784 3211 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3779 3211 301 301 0 3478 0
vsize: 15116
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 4842 0 0 0 56456 551 0 0 25 0 1 0 964874430 18624512 3223 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4547 3223 301 301 0 4246 0
vsize: 18188
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 4873 0 0 0 57450 557 0 0 25 0 1 0 964874430 18624512 3254 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4547 3254 301 301 0 4246 0
vsize: 18188
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 4884 0 0 0 58442 565 0 0 25 0 1 0 964874430 18718720 3265 4294967295 134512640 135730672 3221224576 3221223184 134744459 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4570 3265 301 301 0 4269 0
vsize: 18280
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 4946 0 0 0 59435 572 0 0 25 0 1 0 964874430 18821120 3327 4294967295 134512640 135730672 3221224576 3221223184 134744826 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4595 3327 301 301 0 4294 0
vsize: 18380
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 4964 0 0 0 60425 583 0 0 25 0 1 0 964874430 18821120 3345 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4595 3345 301 301 0 4294 0
vsize: 18380
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 4975 0 0 0 61416 591 0 0 25 0 1 0 964874430 18821120 3356 4294967295 134512640 135730672 3221224576 3221223184 134744826 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4595 3356 301 301 0 4294 0
vsize: 18380
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 5000 0 0 0 62410 597 0 0 25 0 1 0 964874430 18944000 3381 4294967295 134512640 135730672 3221224576 3221223184 134744826 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4625 3381 301 301 0 4324 0
vsize: 18500
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 5019 0 0 0 63404 604 0 0 25 0 1 0 964874430 18944000 3400 4294967295 134512640 135730672 3221224576 3221223184 134744850 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4625 3400 301 301 0 4324 0
vsize: 18500
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 5037 0 0 0 64398 610 0 0 25 0 1 0 964874430 18944000 3418 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4625 3418 301 301 0 4324 0
vsize: 18500
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 5056 0 0 0 65393 616 0 0 25 0 1 0 964874430 19054592 3437 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4652 3437 301 301 0 4351 0
vsize: 18608
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 5078 0 0 0 66387 621 0 0 25 0 1 0 964874430 19054592 3459 4294967295 134512640 135730672 3221224576 3221223184 134744441 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4652 3459 301 301 0 4351 0
vsize: 18608
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 5090 0 0 0 67382 627 0 0 25 0 1 0 964874430 19054592 3471 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4652 3471 301 301 0 4351 0
vsize: 18608
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 5139 0 0 0 68374 635 0 0 25 0 1 0 964874430 19279872 3520 4294967295 134512640 135730672 3221224576 3221223196 135341601 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4707 3520 301 301 0 4406 0
vsize: 18828
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 5165 0 0 0 69366 643 0 0 25 0 1 0 964874430 19279872 3546 4294967295 134512640 135730672 3221224576 3221223184 134744826 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4707 3546 301 301 0 4406 0
vsize: 18828
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 5187 0 0 0 70359 650 0 0 25 0 1 0 964874430 19415040 3568 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4740 3568 301 301 0 4439 0
vsize: 18960
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 5197 0 0 0 71352 657 0 0 25 0 1 0 964874430 19415040 3578 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4740 3578 301 301 0 4439 0
vsize: 18960
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 5216 0 0 0 72345 664 0 0 25 0 1 0 964874430 19415040 3597 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4740 3597 301 301 0 4439 0
vsize: 18960
[startup+739.113 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 29317
Raw data (stat): 29315 (pb2sat-v2) R 29314 31399 31398 0 -1 0 5216 0 0 0 72345 664 0 0 25 0 1 0 964874430 19415040 3597 4294967295 134512640 135730672 3221224576 3221223184 134744457 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4740 3597 301 301 0 4439 0
vsize: 0

Child status: 10
Real time (s): 739.113
CPU time (s): 739.202
CPU user time (s): 732.483
CPU system time (s): 6.71898
CPU usage (%): 100.012
Max. virtual memory (Kb): 18960
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	0
#### END VERIFIER DATA ####