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/manquinho/primes-dimacs-cnf/normalized-ii32e5.opb
MD5SUM	6caf33eeba2c45b0896a04cb80501c4f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	503
Optimality of the best value was proved	NO
Number of terms in the objective function	1044
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1044
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1044
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	312.97
Number of variables	1044
Total number of constraints	12158
Number of constraints which are clauses	12158
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Trace number 6212

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-14 03:59:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4674 boxname=wulflinc24 idbench=162 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6caf33eeba2c45b0896a04cb80501c4f  /oldhome/oroussel/tmp/wulflinc24/normalized-ii32e5.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc24/normalized-ii32e5.opb /oldhome/oroussel/tmp/wulflinc24/normalized-ii32e5.opb
IDLAUNCH: 4674
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        831768 kB
Buffers:         35292 kB
Cached:         125100 kB
SwapCached:       3828 kB
Active:          55652 kB
Inactive:       111400 kB
HighTotal:      131008 kB
HighFree:         3696 kB
LowTotal:       903652 kB
LowFree:        828072 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30424 kB
Committed_AS:    63436 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:08:55 (client local time) WITH STATUS 30 IN 563.176 SECONDS
stats: 4674 0 563.176 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 12158 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12158    50526 |    4052       0        0     nan |  0.000 % |
c |       103 |   12158    50526 |    4457     103     4062    39.4 |  0.010 % |
c |       253 |   12158    50526 |    4902     253    10374    41.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 505[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:57176     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       368 |  147482   366919 |   49160     368    14856    40.4 |  0.000 % |
c |       468 |  147482   366919 |   54076     468    19898    42.5 |  0.002 % |
c |       619 |  147482   366919 |   59483     619    26046    42.1 |  0.002 % |
c |       846 |  147443   366832 |   65431     845    37134    43.9 |  0.024 % |
c |      1184 |  147443   366832 |   71975    1183    52835    44.7 |  0.024 % |
c |      1691 |  147376   366677 |   79172    1689    84709    50.2 |  0.059 % |
c ==============================================================================
c [1mFound solution: 504[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2130 |  147279   366454 |   49093    2128   112212    52.7 |  0.059 % |
c |      2230 |  147118   366093 |   54002    2225   115613    52.0 |  0.203 % |
c |      2383 |  147118   366093 |   59402    2378   122701    51.6 |  0.203 % |
c |      2611 |  147118   366093 |   65342    2606   136350    52.3 |  0.203 % |
c |      2951 |  147118   366093 |   71877    2946   154670    52.5 |  0.203 % |
c |      3460 |  146952   365714 |   79064    3453   184269    53.4 |  0.297 % |
c |      4220 |  146952   365714 |   86971    4213   222391    52.8 |  0.297 % |
c |      5359 |  146415   364494 |   95668    5345   324545    60.7 |  0.613 % |
c |      7068 |  145750   362960 |  105235    7047   438165    62.2 |  0.999 % |
c |      9630 |  144169   359330 |  115758    9592   679664    70.9 |  2.016 % |
c |     13477 |  143310   357371 |  127334   13429   873154    65.0 |  2.563 % |
c ==============================================================================
c [1mFound solution: 503[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17144 |  141766   353869 |   47255   17078  1362712    79.8 |  2.563 % |
c |     17244 |  141663   353631 |   51980   17177  1373821    80.0 |  3.691 % |
c |     17396 |  141471   353189 |   57178   17327  1388492    80.1 |  3.822 % |
c |     17621 |  141045   352216 |   62896   17548  1407710    80.2 |  4.095 % |
c |     17960 |  140687   351397 |   69186   17883  1468939    82.1 |  4.328 % |
c |     18468 |  140465   350888 |   76104   18389  1531921    83.3 |  4.470 % |
c |     19227 |  140091   350033 |   83715   19142  1683940    88.0 |  4.708 % |
c |     20366 |  139806   349383 |   92086   20274  1743625    86.0 |  4.888 % |
c |     22076 |  138569   346541 |  101295   21973  1932062    87.9 |  5.706 % |
c |     24638 |  137507   344103 |  111424   24512  2301353    93.9 |  6.410 % |
c |     28482 |  136615   342061 |  122567   28334  3007610   106.1 |  6.990 % |
c |     34248 |  134649   337548 |  134824   34073  3651961   107.2 |  8.292 % |
c |     42901 |  126151   318027 |  148306   42445  5032086   118.6 | 13.937 % |
c |     55877 |  120765   305597 |  163137   55340  7324402   132.4 | 17.622 % |
c ==============================================================================
c [1mOptimal solution: 503[0m
s OPTIMUM FOUND
v x1 -x2 x3 -x4 -x5 x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 -x15 -x16 x17 -x18 -x19 -x20 -x21 -x22 x23 -x24 x25 -x26 -x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 -x41 -x42 x43 -x44 x45 -x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 -x59 -x60 -x61 x62 x63 -x64 -x65 -x66 x67 -x68 x69 -x70 -x71 x72 -x73 -x74 x75 -x76 x77 -x78 x79 -x80 -x81 -x82 x83 -x84 x85 -x86 -x87 x88 x89 -x90 -x91 -x92 x93 -x94 -x95 -x96 -x97 -x98 x99 -x100 x101 -x102 -x103 -x104 x105 -x106 -x107 x108 x109 -x110 x111 -x112 x113 -x114 -x115 -x116 x117 -x118 x119 -x120 -x121 -x122 x123 -x124 x125 -x126 -x127 -x128 x129 -x130 x131 -x132 x133 -x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 x151 -x152 x153 -x154 x155 -x156 x157 -x158 x159 -x160 -x161 x162 x163 -x164 -x165 x166 x167 -x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 x189 -x190 x191 -x192 x193 -x194 x195 -x196 x197 -x198 x199 -x200 x201 -x202 x203 -x204 x205 -x206 x207 -x208 x209 -x210 x211 -x212 x213 -x214 x215 -x216 -x217 x218 x219 -x220 x221 -x222 x223 -x224 x225 -x226 x227 -x228 x229 -x230 x231 -x232 x233 -x234 x235 -x236 x237 -x238 x239 -x240 x241 -x242 x243 -x244 x245 -x246 x247 -x248 x249 -x250 x251 -x252 x253 -x254 x255 -x256 x257 -x258 x259 -x260 -x261 x262 x263 -x264 x265 -x266 x267 -x268 x269 -x270 x271 -x272 x273 -x274 x275 -x276 x277 -x278 x279 -x280 x281 -x282 x283 -x284 x285 -x286 x287 -x288 x289 -x290 x291 -x292 x293 -x294 x295 -x296 x297 -x298 x299 -x300 x301 -x302 x303 -x304 x305 -x306 x307 -x308 x309 -x310 x311 -x312 x313 -x314 x315 -x316 x317 -x318 x319 -x320 x321 -x322 x323 -x324 x325 -x326 x327 -x328 x329 -x330 x331 -x332 x333 -x334 x335 -x336 x337 -x338 x339 -x340 x341 -x342 x343 -x344 x345 -x346 x347 -x348 x349 -x350 x351 -x352 x353 -x354 x355 -x356 x357 -x358 x359 -x360 x361 -x362 x363 -x364 x365 -x366 x367 -x368 -x369 x370 x371 -x372 x373 -x374 x375 -x376 x377 -x378 -x379 x380 x381 -x382 x383 -x384 -x385 x386 -x387 x388 x389 -x390 -x391 x392 x393 -x394 -x395 x396 -x397 x398 -x399 x400 x401 -x402 -x403 x404 -x405 -x406 x407 -x408 -x409 x410 x411 -x412 -x413 x414 -x415 x416 -x417 x418 x419 -x420 -x421 x422 x423 -x424 -x425 x426 -x427 x428 -x429 x430 x431 -x432 -x433 x434 -x435 x436 x437 -x438 -x439 x440 -x441 x442 x443 -x444 x445 -x446 -x447 x448 -x449 x450 -x451 x452 x453 -x454 -x455 x456 -x457 x458 -x459 x460 x461 -x462 -x463 x464 x465 -x466 -x467 x468 -x469 x470 x471 -x472 -x473 x474 -x475 x476 -x477 x478 x479 -x480 -x481 x482 x483 -x484 -x485 x486 -x487 x488 x489 -x490 -x491 x492 -x493 x494 -x495 x496 x497 -x498 -x499 x500 x501 -x502 -x503 x504 -x505 x506 x507 -x508 -x509 x510 -x511 x512 x513 -x514 -x515 x516 -x517 x518 -x519 x520 x521 -x522 -x523 x524 -x525 x526 x527 -x528 -x529 x530 -x531 x532 x533 -x534 -x535 x536 -x537 x538 x539 -x540 -x541 x542 x543 -x544 -x545 x546 -x547 x548 x549 -x550 -x551 x552 -x553 x554 x555 -x556 -x557 x558 -x559 x560 -x561 x562 x563 -x564 -x565 x566 -x567 x568 x569 -x570 -x571 x572 -x573 x574 x575 -x576 -x577 x578 -x579 x580 x581 -x582 -x583 x584 -x585 x586 x587 -x588 -x589 x590 -x591 x592 x593 -x594 -x595 x596 -x597 x598 x599 -x600 -x601 x602 -x603 x604 x605 -x606 -x607 x608 x609 -x610 -x611 x612 -x613 x614 x615 -x616 -x617 x618 -x619 x620 -x621 x622 x623 -x624 -x625 x626 -x627 x628 x629 -x630 -x631 x632 -x633 x634 x635 -x636 -x637 x638 x639 -x640 -x641 x642 -x643 x644 x645 -x646 -x647 x648 -x649 x650 x651 -x652 -x653 x654 -x655 x656 x657 -x658 -x659 x660 -x661 x662 x663 -x664 -x665 x666 -x667 x668 -x669 x670 x671 -x672 -x673 x674 -x675 x676 x677 -x678 -x679 x680 -x681 x682 x683 -x684 -x685 x686 x687 -x688 -x689 x690 -x691 x692 -x693 x694 x695 -x696 -x697 x698 -x699 x700 x701 -x702 -x703 x704 -x705 x706 x707 -x708 -x709 x710 -x711 x712 x713 -x714 -x715 x716 x717 -x718 -x719 x720 x721 -x722 -x723 x724 -x725 x726 -x727 x728 -x729 x730 x731 -x732 -x733 x734 -x735 x736 x737 -x738 -x739 x740 x741 -x742 -x743 x744 -x745 x746 x747 -x748 -x749 x750 -x751 x752 x753 -x754 -x755 -x756 -x757 x758 -x759 x760 x761 -x762 -x763 x764 -x765 x766 x767 -x768 -x769 x770 x771 -x772 -x773 x774 -x775 x776 -x777 x778 x779 -x780 -x781 x782 x783 -x784 -x785 -x786 -x787 x788 x789 -x790 -x791 x792 -x793 x794 x795 -x796 -x797 x798 -x799 x800 -x801 x802 x803 -x804 -x805 x806 -x807 x808 x809 -x810 -x811 x812 x813 -x814 -x815 x816 -x817 x818 -x819 x820 x821 -x822 -x823 x824 -x825 x826 x827 -x828 -x829 x830 -x831 x832 x833 -x834 -x835 x836 -x837 x838 x839 -x840 -x841 x842 x843 -x844 -x845 x846 -x847 x848 -x849 x850 x851 -x852 -x853 x854 x855 -x856 -x857 x858 -x859 x860 -x861 x862 x863 -x864 -x865 x866 -x867 x868 x869 -x870 -x871 x872 x873 -x874 -x875 x876 -x877 x878 -x879 x880 x881 -x882 -x883 x884 x885 -x886 -x887 x888 -x889 x890 -x891 x892 x893 -x894 -x895 x896 -x897 x898 x899 -x900 -x901 x902 x903 -x904 -x905 x906 -x907 x908 -x909 x910 x911 -x912 -x913 x914 x915 -x916 -x917 x918 -x919 x920 x921 -x922 -x923 x924 -x925 x926 -x927 x928 x929 -x930 -x931 x932 x933 -x934 -x935 x936 -x937 x938 x939 -x940 -x941 x942 -x943 x944 x945 -x946 -x947 x948 -x949 x950 x951 -x952 -x953 x954 -x955 x956 x957 -x958 -x959 x960 -x961 x962 -x963 x964 x965 -x966 -x967 x968 -x969 x970 x971 -x972 -x973 x974 x975 -x976 -x977 x978 -x979 x980 -x981 x982 x983 -x984 -x985 x986 x987 -x988 -x989 x990 -x991 x992 x993 -x994 -x995 x996 -x997 x998 x999 -x1000 -x1001 x1002 -x1003 x1004 -x1005 x1006 x1007 -x1008 -x1009 x1010 -x1011 x1012 x1013 -x1014 -x1015 x1016 -x1017 x1018 x1019 -x1020 -x1021 x1022 x1023 -x1024 -x1025 x1026 -x1027 x1028 x1029 -x1030 -x1031 x1032 -x1033 x1034 x1035 -x1036 -x1037 x1038 -x1039 x1040 -x1041 x1042 x1043 -x1044
c _______________________________________________________________________________
c 
c restarts              : 34
c conflicts             : 66075          (117 /sec)
c decisions             : 192488         (342 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 562.663 s
c _______________________________________________________________________________
#### 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
Raw data (loadavg): 0.91 0.94 0.90 2/54 3609
Raw data (stat): 3609 (runsolver) R 3608 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481535340 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 3609
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 4612 0 0 0 988 11 0 0 25 0 1 0 481535340 22302720 4586 4294967295 134512640 134672761 3221224576 3221223776 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5445 4586 603 41 0 5404 0
vsize: 21780
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 3609
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 4756 0 0 0 1986 12 0 0 25 0 1 0 481535340 22863872 4730 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5582 4730 603 41 0 5541 0
vsize: 22328
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 3609
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 4980 0 0 0 2986 13 0 0 25 0 1 0 481535340 23810048 4954 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5813 4954 603 41 0 5772 0
vsize: 23252
[startup+40.001 s]
Raw data (loadavg): 1.03 0.96 0.91 2/54 3662
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 5179 0 0 0 3982 16 0 0 25 0 1 0 481535340 24625152 5153 4294967295 134512640 134672761 3221224576 3221223680 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6012 5153 603 41 0 5971 0
vsize: 24048
[startup+50.0014 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 3662
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 5368 0 0 0 4981 16 0 0 25 0 1 0 481535340 25436160 5342 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6210 5342 603 41 0 6169 0
vsize: 24840
[startup+60.0011 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 3662
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 5526 0 0 0 5981 17 0 0 25 0 1 0 481535340 25976832 5500 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6342 5500 603 41 0 6301 0
vsize: 25368
[startup+70.0014 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 3662
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 5746 0 0 0 6980 18 0 0 25 0 1 0 481535340 26923008 5720 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6573 5720 603 41 0 6532 0
vsize: 26292
[startup+80.0015 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 3662
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 6022 0 0 0 7979 19 0 0 25 0 1 0 481535340 28147712 5996 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 5996 603 41 0 6831 0
vsize: 27488
[startup+90.0011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 3662
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 6142 0 0 0 8979 19 0 0 25 0 1 0 481535340 28721152 6116 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7012 6116 603 41 0 6971 0
vsize: 28048
[startup+100.001 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 3662
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 6352 0 0 0 9979 19 0 0 25 0 1 0 481535340 29519872 6326 4294967295 134512640 134672761 3221224576 3221223680 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7207 6326 603 41 0 7166 0
vsize: 28828
[startup+110.002 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 6518 0 0 0 10978 20 0 0 25 0 1 0 481535340 30179328 6492 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7368 6492 603 41 0 7327 0
vsize: 29472
[startup+120.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 6729 0 0 0 11978 21 0 0 25 0 1 0 481535340 31121408 6703 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7598 6703 603 41 0 7557 0
vsize: 30392
[startup+130.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 6931 0 0 0 12978 21 0 0 25 0 1 0 481535340 31924224 6905 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7794 6905 603 41 0 7753 0
vsize: 31176
[startup+140.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 7247 0 0 0 13976 22 0 0 25 0 1 0 481535340 33267712 7221 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8122 7221 603 41 0 8081 0
vsize: 32488
[startup+150.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 7428 0 0 0 14976 23 0 0 25 0 1 0 481535340 33939456 7402 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8286 7402 603 41 0 8245 0
vsize: 33144
[startup+160.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 7689 0 0 0 15975 24 0 0 25 0 1 0 481535340 35012608 7663 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8548 7663 603 41 0 8507 0
vsize: 34192
[startup+170.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 7874 0 0 0 16974 25 0 0 25 0 1 0 481535340 35815424 7848 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 7848 603 41 0 8703 0
vsize: 34976
[startup+180.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 7957 0 0 0 17974 25 0 0 25 0 1 0 481535340 36085760 7931 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8810 7931 603 41 0 8769 0
vsize: 35240
[startup+190.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 8145 0 0 0 18974 25 0 0 25 0 1 0 481535340 36888576 8119 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9006 8119 603 41 0 8965 0
vsize: 36024
[startup+200.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 8398 0 0 0 19973 26 0 0 25 0 1 0 481535340 37838848 8372 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9238 8372 603 41 0 9197 0
vsize: 36952
[startup+210.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 8552 0 0 0 20973 27 0 0 25 0 1 0 481535340 38637568 8526 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9433 8526 603 41 0 9392 0
vsize: 37732
[startup+220.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 8677 0 0 0 21973 27 0 0 25 0 1 0 481535340 39186432 8651 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9567 8651 603 41 0 9526 0
vsize: 38268
[startup+230.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 8740 0 0 0 22973 27 0 0 25 0 1 0 481535340 39456768 8714 4294967295 134512640 134672761 3221224576 3221223792 134557677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9633 8714 603 41 0 9592 0
vsize: 38532
[startup+240.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 8936 0 0 0 23973 28 0 0 25 0 1 0 481535340 40300544 8910 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9839 8910 603 41 0 9798 0
vsize: 39356
[startup+250.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 9057 0 0 0 24973 28 0 0 25 0 1 0 481535340 40706048 9031 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9938 9031 603 41 0 9897 0
vsize: 39752
[startup+260.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 9304 0 0 0 25972 29 0 0 25 0 1 0 481535340 41766912 9278 4294967295 134512640 134672761 3221224576 3221223680 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10197 9278 603 41 0 10156 0
vsize: 40788
[startup+270.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 9516 0 0 0 26972 29 0 0 25 0 1 0 481535340 42569728 9490 4294967295 134512640 134672761 3221224576 3221223744 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10393 9490 603 41 0 10352 0
vsize: 41572
[startup+280.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 9652 0 0 0 27972 30 0 0 25 0 1 0 481535340 43233280 9626 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10555 9626 603 41 0 10514 0
vsize: 42220
[startup+290.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 9825 0 0 0 28971 30 0 0 25 0 1 0 481535340 43892736 9799 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10716 9799 603 41 0 10675 0
vsize: 42864
[startup+300.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 10015 0 0 0 29971 31 0 0 25 0 1 0 481535340 44699648 9989 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10913 9989 603 41 0 10872 0
vsize: 43652
[startup+310.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 10100 0 0 0 30971 31 0 0 25 0 1 0 481535340 44978176 10074 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10981 10074 603 41 0 10940 0
vsize: 43924
[startup+320.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 10294 0 0 0 31971 31 0 0 25 0 1 0 481535340 45768704 10268 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11174 10268 603 41 0 11133 0
vsize: 44696
[startup+330.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 10435 0 0 0 32970 32 0 0 25 0 1 0 481535340 46444544 10409 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11339 10409 603 41 0 11298 0
vsize: 45356
[startup+340.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 10545 0 0 0 33970 32 0 0 25 0 1 0 481535340 46850048 10519 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11438 10519 603 41 0 11397 0
vsize: 45752
[startup+350.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 10730 0 0 0 34970 33 0 0 25 0 1 0 481535340 47636480 10704 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11630 10704 603 41 0 11589 0
vsize: 46520
[startup+360.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 10947 0 0 0 35970 33 0 0 25 0 1 0 481535340 48443392 10921 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11827 10921 603 41 0 11786 0
vsize: 47308
[startup+370.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 11239 0 0 0 36969 34 0 0 25 0 1 0 481535340 49704960 11213 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12135 11213 603 41 0 12094 0
vsize: 48540
[startup+380.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 11422 0 0 0 37968 35 0 0 25 0 1 0 481535340 50511872 11396 4294967295 134512640 134672761 3221224576 3221223680 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12332 11396 603 41 0 12291 0
vsize: 49328
[startup+390.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 11527 0 0 0 38968 36 0 0 25 0 1 0 481535340 50909184 11501 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12429 11501 603 41 0 12388 0
vsize: 49716
[startup+400.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3664
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 11679 0 0 0 39968 36 0 0 25 0 1 0 481535340 51441664 11653 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12559 11654 603 41 0 12518 0
vsize: 50236
[startup+410.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 11861 0 0 0 40967 37 0 0 25 0 1 0 481535340 52301824 11835 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12769 11835 603 41 0 12728 0
vsize: 51076
[startup+420.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 12047 0 0 0 41967 37 0 0 25 0 1 0 481535340 53084160 12021 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12960 12021 603 41 0 12919 0
vsize: 51840
[startup+430.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 12324 0 0 0 42966 38 0 0 25 0 1 0 481535340 54169600 12298 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13225 12298 603 41 0 13184 0
vsize: 52900
[startup+440.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 12564 0 0 0 43965 39 0 0 25 0 1 0 481535340 55234560 12538 4294967295 134512640 134672761 3221224576 3221223680 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13485 12538 603 41 0 13444 0
vsize: 53940
[startup+450.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 12817 0 0 0 44964 40 0 0 25 0 1 0 481535340 56311808 12791 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13748 12791 603 41 0 13707 0
vsize: 54992
[startup+460.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 12933 0 0 0 45964 40 0 0 25 0 1 0 481535340 56705024 12907 4294967295 134512640 134672761 3221224576 3221223760 134559392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13844 12907 603 41 0 13803 0
vsize: 55376
[startup+470.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 13204 0 0 0 46963 41 0 0 25 0 1 0 481535340 57774080 13178 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14105 13178 603 41 0 14064 0
vsize: 56420
[startup+480.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 13477 0 0 0 47963 42 0 0 25 0 1 0 481535340 58990592 13451 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14402 13451 603 41 0 14361 0
vsize: 57608
[startup+490.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 13765 0 0 0 48962 43 0 0 25 0 1 0 481535340 60174336 13739 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14691 13739 603 41 0 14650 0
vsize: 58764
[startup+500.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 13899 0 0 0 49962 43 0 0 25 0 1 0 481535340 60706816 13873 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14821 13873 603 41 0 14780 0
vsize: 59284
[startup+510.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 14166 0 0 0 50961 44 0 0 25 0 1 0 481535340 61784064 14140 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15084 14140 603 41 0 15043 0
vsize: 60336
[startup+520.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 14479 0 0 0 51960 45 0 0 25 0 1 0 481535340 62980096 14453 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15376 14453 603 41 0 15335 0
vsize: 61504
[startup+530.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 14727 0 0 0 52960 45 0 0 25 0 1 0 481535340 64073728 14701 4294967295 134512640 134672761 3221224576 3221223808 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15643 14701 603 41 0 15602 0
vsize: 62572
[startup+540.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 14806 0 0 0 53960 46 0 0 25 0 1 0 481535340 64339968 14780 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15708 14780 603 41 0 15667 0
vsize: 62832
[startup+550.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 14806 0 0 0 54960 46 0 0 25 0 1 0 481535340 64339968 14780 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15708 14780 603 41 0 15667 0
vsize: 62832
[startup+560.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 14888 0 0 0 55960 46 0 0 25 0 1 0 481535340 64737280 14862 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15805 14862 603 41 0 15764 0
vsize: 63220
[startup+563.122 s]
Raw data (loadavg): 1.00 0.97 0.91 1/53 3666
Raw data (stat): 3609 (minisat+) R 3608 28546 28545 0 -1 0 14888 0 0 0 55960 46 0 0 25 0 1 0 481535340 64737280 14862 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15805 14862 603 41 0 15764 0
vsize: 0

Child status: 30
Real time (s): 563.121
CPU time (s): 563.176
CPU user time (s): 562.682
CPU system time (s): 0.493924
CPU usage (%): 100.01
Max. virtual memory (Kb): 63220
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	503
#### END VERIFIER DATA ####