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-ii8b2.opb
MD5SUM	bbfcebd70586668574286ad19a1cd5a8
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	379
Optimality of the best value was proved	NO
Number of terms in the objective function	1152
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	1152
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	1152
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	1.03984
Number of variables	1152
Total number of constraints	4664
Number of constraints which are clauses	4664
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	8
Trace number 5127

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-13 22:01:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3552 boxname=wulflinc17 idbench=168 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bbfcebd70586668574286ad19a1cd5a8  /oldhome/oroussel/tmp/wulflinc17/normalized-ii8b2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc17/normalized-ii8b2.opb /oldhome/oroussel/tmp/wulflinc17/normalized-ii8b2.opb
IDLAUNCH: 3552
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        830104 kB
Buffers:         34352 kB
Cached:         135584 kB
SwapCached:       2376 kB
Active:          53120 kB
Inactive:       122208 kB
HighTotal:      131008 kB
HighFree:         2604 kB
LowTotal:       903652 kB
LowFree:        827500 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23592 kB
Committed_AS:    63700 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:21:47 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3552 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4664 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 |    4664    10368 |    1554       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 418[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2300   maxlim: 734   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |   20702    67632 |    6900       4       53    13.2 |  0.000 % |
c |       105 |   20702    67632 |    7590     105      691     6.6 |  0.231 % |
c |       255 |   20702    67632 |    8349     255     1541     6.0 |  0.231 % |
c |       480 |   20702    67632 |    9183     480     3015     6.3 |  0.231 % |
c |       817 |   20702    67632 |   10102     817     4941     6.0 |  0.231 % |
c |      1324 |   20702    67632 |   11112    1324    29733    22.5 |  0.231 % |
c |      2083 |   20702    67632 |   12223    2083    34482    16.6 |  0.231 % |
c |      3223 |   20702    67632 |   13446    3223    41951    13.0 |  0.231 % |
c |      4933 |   20702    67632 |   14790    4933    66789    13.5 |  0.231 % |
c |      7495 |   20702    67632 |   16269    7495   103656    13.8 |  0.231 % |
c |     11339 |   20702    67632 |   17896   11339   378642    33.4 |  0.231 % |
c |     17105 |   20702    67632 |   19686   17105   680136    39.8 |  0.231 % |
c |     25755 |   20702    67632 |   21655   15701   816278    52.0 |  0.231 % |
c |     38731 |   20702    67632 |   23820   16799   851555    50.7 |  0.231 % |
c |     58192 |   20702    67632 |   26202   24089  1643842    68.2 |  0.231 % |
c |     87385 |   20702    67632 |   28823   24170  3771457   156.0 |  0.231 % |
c |    131174 |   20702    67632 |   31705   16255  2259947   139.0 |  0.231 % |
c |    196858 |   20702    67632 |   34875   23445  3862766   164.8 |  0.231 % |
c |    295384 |   20702    67632 |   38363   35641  7891066   221.4 |  0.231 % |
c |    443174 |   20702    67632 |   42199   28194  4473022   158.7 |  0.231 % |
c 
c *** TERMINATED ***
s SATISFIABLE
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 x#### 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.86 0.95 0.90 2/55 25753
Raw data (stat): 25753 (runsolver) R 25752 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479399366 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.88 0.95 0.90 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 1600 0 0 0 994 4 0 0 25 0 1 0 479399366 8187904 1578 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1999 1578 603 41 0 1958 0
vsize: 7996
[startup+19.9996 s]
Raw data (loadavg): 0.90 0.96 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 2126 0 0 0 1992 5 0 0 25 0 1 0 479399366 10342400 2104 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2525 2104 603 41 0 2484 0
vsize: 10100
[startup+30.0002 s]
Raw data (loadavg): 0.91 0.96 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 2188 0 0 0 2992 5 0 0 25 0 1 0 479399366 10608640 2166 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2590 2166 603 41 0 2549 0
vsize: 10360
[startup+40.0001 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 2400 0 0 0 3992 6 0 0 25 0 1 0 479399366 11415552 2378 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2787 2378 603 41 0 2746 0
vsize: 11148
[startup+50.0004 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 3179 0 0 0 4989 9 0 0 25 0 1 0 479399366 14635008 3157 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3573 3157 603 41 0 3532 0
vsize: 14292
[startup+60 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 3966 0 0 0 5986 12 0 0 25 0 1 0 479399366 17862656 3944 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4361 3944 603 41 0 4320 0
vsize: 17444
[startup+69.9999 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 4887 0 0 0 6984 15 0 0 25 0 1 0 479399366 21622784 4865 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5279 4865 603 41 0 5238 0
vsize: 21116
[startup+80.0002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 4887 0 0 0 7984 15 0 0 25 0 1 0 479399366 21622784 4865 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5279 4865 603 41 0 5238 0
vsize: 21116
[startup+90 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 5107 0 0 0 8983 15 0 0 25 0 1 0 479399366 22568960 5085 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5510 5085 603 41 0 5469 0
vsize: 22040
[startup+100.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 5446 0 0 0 9983 16 0 0 25 0 1 0 479399366 23916544 5424 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5839 5424 603 41 0 5798 0
vsize: 23356
[startup+110.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 5446 0 0 0 10983 16 0 0 25 0 1 0 479399366 23916544 5424 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5839 5424 603 41 0 5798 0
vsize: 23356
[startup+120.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 5446 0 0 0 11983 16 0 0 25 0 1 0 479399366 23916544 5424 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5839 5424 603 41 0 5798 0
vsize: 23356
[startup+130.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 5446 0 0 0 12983 16 0 0 25 0 1 0 479399366 23916544 5424 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5839 5424 603 41 0 5798 0
vsize: 23356
[startup+140 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 5446 0 0 0 13983 16 0 0 25 0 1 0 479399366 23916544 5424 4294967295 134512640 134672761 3221224576 3221223680 134555133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5839 5424 603 41 0 5798 0
vsize: 23356
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 5562 0 0 0 14983 16 0 0 25 0 1 0 479399366 24322048 5540 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5938 5540 603 41 0 5897 0
vsize: 23752
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6294 0 0 0 15981 19 0 0 25 0 1 0 479399366 27455488 6272 4294967295 134512640 134672761 3221224576 3221223760 134559379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6703 6272 603 41 0 6662 0
vsize: 26812
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6792 0 0 0 16979 21 0 0 25 0 1 0 479399366 29478912 6770 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7197 6770 603 41 0 7156 0
vsize: 28788
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6792 0 0 0 17979 21 0 0 25 0 1 0 479399366 29478912 6770 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7197 6770 603 41 0 7156 0
vsize: 28788
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6825 0 0 0 18978 21 0 0 25 0 1 0 479399366 29741056 6803 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6803 603 41 0 7220 0
vsize: 29044
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6826 0 0 0 19979 21 0 0 25 0 1 0 479399366 29741056 6804 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6804 603 41 0 7220 0
vsize: 29044
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6826 0 0 0 20979 21 0 0 25 0 1 0 479399366 29741056 6804 4294967295 134512640 134672761 3221224576 3221223680 134559955 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6804 603 41 0 7220 0
vsize: 29044
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6826 0 0 0 21979 21 0 0 25 0 1 0 479399366 29741056 6804 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6804 603 41 0 7220 0
vsize: 29044
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25753
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6826 0 0 0 22979 21 0 0 25 0 1 0 479399366 29741056 6804 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6804 603 41 0 7220 0
vsize: 29044
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25755
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6826 0 0 0 23979 21 0 0 25 0 1 0 479399366 29741056 6804 4294967295 134512640 134672761 3221224576 3221223760 134558930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6804 603 41 0 7220 0
vsize: 29044
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6826 0 0 0 24979 21 0 0 25 0 1 0 479399366 29741056 6804 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6804 603 41 0 7220 0
vsize: 29044
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6826 0 0 0 25980 21 0 0 25 0 1 0 479399366 29741056 6804 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6804 603 41 0 7220 0
vsize: 29044
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6826 0 0 0 26980 21 0 0 25 0 1 0 479399366 29741056 6804 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6804 603 41 0 7220 0
vsize: 29044
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6826 0 0 0 27980 21 0 0 25 0 1 0 479399366 29741056 6804 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6804 603 41 0 7220 0
vsize: 29044
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 6826 0 0 0 28980 21 0 0 25 0 1 0 479399366 29741056 6804 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6804 603 41 0 7220 0
vsize: 29044
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 7389 0 0 0 29979 22 0 0 25 0 1 0 479399366 32018432 7367 4294967295 134512640 134672761 3221224576 3221223744 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7817 7367 603 41 0 7776 0
vsize: 31268
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 8139 0 0 0 30977 25 0 0 25 0 1 0 479399366 35098624 8117 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8569 8117 603 41 0 8528 0
vsize: 34276
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 8139 0 0 0 31977 25 0 0 25 0 1 0 479399366 35098624 8117 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8569 8117 603 41 0 8528 0
vsize: 34276
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 8139 0 0 0 32977 25 0 0 25 0 1 0 479399366 35098624 8117 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8569 8117 603 41 0 8528 0
vsize: 34276
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 8139 0 0 0 33978 25 0 0 25 0 1 0 479399366 35098624 8117 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8569 8117 603 41 0 8528 0
vsize: 34276
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 8139 0 0 0 34978 25 0 0 25 0 1 0 479399366 35098624 8117 4294967295 134512640 134672761 3221224576 3221223680 134559805 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8569 8117 603 41 0 8528 0
vsize: 34276
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 8706 0 0 0 35977 26 0 0 25 0 1 0 479399366 37388288 8684 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9128 8684 603 41 0 9087 0
vsize: 36512
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9423 0 0 0 36974 28 0 0 25 0 1 0 479399366 40345600 9401 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9850 9401 603 41 0 9809 0
vsize: 39400
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9798 0 0 0 37974 29 0 0 25 0 1 0 479399366 41824256 9776 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10211 9776 603 41 0 10170 0
vsize: 40844
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9798 0 0 0 38974 29 0 0 25 0 1 0 479399366 41824256 9776 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10211 9776 603 41 0 10170 0
vsize: 40844
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9798 0 0 0 39974 29 0 0 25 0 1 0 479399366 41824256 9776 4294967295 134512640 134672761 3221224576 3221223680 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10211 9776 603 41 0 10170 0
vsize: 40844
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9798 0 0 0 40974 29 0 0 25 0 1 0 479399366 41824256 9776 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10211 9776 603 41 0 10170 0
vsize: 40844
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9799 0 0 0 41975 29 0 0 25 0 1 0 479399366 41824256 9777 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10211 9777 603 41 0 10170 0
vsize: 40844
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9919 0 0 0 42974 30 0 0 25 0 1 0 479399366 42360832 9897 4294967295 134512640 134672761 3221224576 3221223760 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9897 603 41 0 10301 0
vsize: 41368
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9934 0 0 0 43974 30 0 0 25 0 1 0 479399366 42360832 9912 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9912 603 41 0 10301 0
vsize: 41368
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9934 0 0 0 44975 30 0 0 25 0 1 0 479399366 42360832 9912 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9912 603 41 0 10301 0
vsize: 41368
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9934 0 0 0 45975 30 0 0 25 0 1 0 479399366 42360832 9912 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9912 603 41 0 10301 0
vsize: 41368
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9934 0 0 0 46975 30 0 0 25 0 1 0 479399366 42360832 9912 4294967295 134512640 134672761 3221224576 3221223744 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9912 603 41 0 10301 0
vsize: 41368
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9935 0 0 0 47975 30 0 0 25 0 1 0 479399366 42360832 9913 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9913 603 41 0 10301 0
vsize: 41368
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9935 0 0 0 48975 30 0 0 25 0 1 0 479399366 42360832 9913 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9913 603 41 0 10301 0
vsize: 41368
[startup+500.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9935 0 0 0 49976 30 0 0 25 0 1 0 479399366 42360832 9913 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9913 603 41 0 10301 0
vsize: 41368
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9935 0 0 0 50976 30 0 0 25 0 1 0 479399366 42360832 9913 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9913 603 41 0 10301 0
vsize: 41368
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9935 0 0 0 51976 30 0 0 25 0 1 0 479399366 42360832 9913 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9913 603 41 0 10301 0
vsize: 41368
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25757
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 9935 0 0 0 52976 30 0 0 25 0 1 0 479399366 42360832 9913 4294967295 134512640 134672761 3221224576 3221223680 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9913 603 41 0 10301 0
vsize: 41368
[startup+540.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 53974 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 54975 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+560.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 55975 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+570.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 56975 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 57975 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 58975 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+600.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 59976 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+610.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 60976 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 61976 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+630.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 62976 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 63976 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+650.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 64977 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 65977 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+670.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 66977 31 0 0 25 0 1 0 479399366 44253184 10352 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10804 10352 603 41 0 10763 0
vsize: 43216
[startup+680.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 67977 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+690.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 68977 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+700.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 69978 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+710.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 70978 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+720.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 71978 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 72978 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 73978 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+750.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 74978 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223760 134559415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+760.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 75979 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 76979 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+780.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 77979 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+790.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 78979 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 79979 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+810.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 80979 31 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10374 0 0 0 81979 32 0 0 25 0 1 0 479399366 44204032 10352 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10352 603 41 0 10751 0
vsize: 43168
[startup+830.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25759
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 82979 32 0 0 25 0 1 0 479399366 44204032 10356 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10356 603 41 0 10751 0
vsize: 43168
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 83979 32 0 0 25 0 1 0 479399366 44204032 10356 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10356 603 41 0 10751 0
vsize: 43168
[startup+850.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 84979 32 0 0 25 0 1 0 479399366 44204032 10356 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10356 603 41 0 10751 0
vsize: 43168
[startup+860.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 85979 32 0 0 25 0 1 0 479399366 44204032 10356 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10356 603 41 0 10751 0
vsize: 43168
[startup+870.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 86980 32 0 0 25 0 1 0 479399366 44204032 10356 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10792 10356 603 41 0 10751 0
vsize: 43168
[startup+880.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 87980 32 0 0 25 0 1 0 479399366 44118016 10351 4294967295 134512640 134672761 3221224576 3221223576 1075349984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10771 10351 603 41 0 10730 0
vsize: 43084
[startup+890.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 88980 32 0 0 25 0 1 0 479399366 44118016 10351 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10771 10351 603 41 0 10730 0
vsize: 43084
[startup+900.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 89980 32 0 0 25 0 1 0 479399366 44118016 10351 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10771 10351 603 41 0 10730 0
vsize: 43084
[startup+910.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 90980 32 0 0 25 0 1 0 479399366 44118016 10351 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10771 10351 603 41 0 10730 0
vsize: 43084
[startup+920.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 91980 32 0 0 25 0 1 0 479399366 44118016 10351 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10771 10351 603 41 0 10730 0
vsize: 43084
[startup+930.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 92981 32 0 0 25 0 1 0 479399366 44118016 10351 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10771 10351 603 41 0 10730 0
vsize: 43084
[startup+940.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 93981 32 0 0 25 0 1 0 479399366 44118016 10351 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10771 10351 603 41 0 10730 0
vsize: 43084
[startup+950.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 94981 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+960.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 95981 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+970.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 96982 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 97982 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+990.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 98982 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 99982 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 100982 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223760 134558914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 101982 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 102983 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223672 1075347332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 103983 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223680 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 104983 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 105983 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 106984 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 107984 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 108984 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 109984 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 110984 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 111984 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25761
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 112985 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25763
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 113985 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25763
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10378 0 0 0 114985 32 0 0 25 0 1 0 479399366 44064768 10338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10758 10338 603 41 0 10717 0
vsize: 43032
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25763
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10470 0 0 0 115985 32 0 0 25 0 1 0 479399366 44470272 10430 4294967295 134512640 134672761 3221224576 3221223744 134561639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10857 10430 603 41 0 10816 0
vsize: 43428
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25763
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10470 0 0 0 116985 32 0 0 25 0 1 0 479399366 44470272 10430 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10857 10430 603 41 0 10816 0
vsize: 43428
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25763
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10476 0 0 0 117985 32 0 0 25 0 1 0 479399366 44605440 10436 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10890 10436 603 41 0 10849 0
vsize: 43560
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25763
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10480 0 0 0 118986 32 0 0 25 0 1 0 479399366 44605440 10440 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10890 10440 603 41 0 10849 0
vsize: 43560
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25763
Raw data (stat): 25753 (minisat+) R 25752 20838 20837 0 -1 0 10481 0 0 0 119986 32 0 0 25 0 1 0 479399366 44605440 10441 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10890 10441 603 41 0 10849 0
vsize: 43560
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 25763
Raw data (stat): 25753 (minisat+) Z 25752 20838 20837 0 -1 12 10484 0 0 0 119986 34 0 0 25 0 1 0 479399366 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.03
CPU time (s): 1200.21
CPU user time (s): 1199.86
CPU system time (s): 0.345947
CPU usage (%): 100.015
Max. virtual memory (Kb): 43560
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####