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/synthesis-ptl-cmos-circuits/normalized-C432.opb
MD5SUM	6292e63147fb202dc159fbf5a9ff5c77
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4822
Optimality of the best value was proved	NO
Number of terms in the objective function	771
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	33355
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	33355
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	771
Total number of constraints	1951
Number of constraints which are clauses	1949
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2
Minimum length of a constraint	1
Maximum length of a constraint	42
Trace number 5204

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        904200 kB
Buffers:         33512 kB
Cached:          75464 kB
SwapCached:       2272 kB
Active:          52940 kB
Inactive:        61152 kB
HighTotal:      131008 kB
HighFree:        51660 kB
LowTotal:       903652 kB
LowFree:        852540 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10708 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:46:01 (client local time) WITH STATUS 10 IN 1200.09 SECONDS
stats: 3632 7 1200.09 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1905 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 |    1905     9279 |     635       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 7184[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4048   maxlim: 26171   bits: 16/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   30143   110111 |   10047       0        0     nan |  0.000 % |
c |       100 |   30116   110036 |   11051      99      311     3.1 |  0.415 % |
c |       250 |   29981   109622 |   12156     245      854     3.5 |  0.622 % |
c |       476 |   29981   109622 |   13372     471     1782     3.8 |  0.622 % |
c |       813 |   29981   109622 |   14709     808     3448     4.3 |  0.622 % |
c |      1320 |   29966   109581 |   16180    1314     7143     5.4 |  0.642 % |
c |      2079 |   29966   109581 |   17798    2073    11425     5.5 |  0.642 % |
c |      3218 |   29966   109581 |   19578    3212    36537    11.4 |  0.642 % |
c |      4926 |   29966   109581 |   21536    4920    86706    17.6 |  0.642 % |
c |      7489 |   29960   109564 |   23690    7481   212276    28.4 |  0.663 % |
c |     11335 |   29946   109525 |   26059   11325   336818    29.7 |  0.684 % |
c |     17101 |   29946   109525 |   28665   17091   409552    24.0 |  0.684 % |
c |     25750 |   29946   109525 |   31531   25740   936313    36.4 |  0.684 % |
c |     38725 |   29946   109525 |   34684   21083  1832681    86.9 |  0.684 % |
c |     58186 |   29946   109525 |   38153   20020  2048073   102.3 |  0.684 % |
c |     87381 |   29946   109525 |   41968   24376  3938253   161.6 |  0.684 % |
c |    131170 |   29946   109525 |   46165   40220  3396144    84.4 |  0.684 % |
c |    196854 |   29946   109525 |   50782   43023  7213949   167.7 |  0.684 % |
c |    295381 |   29946   109525 |   55860   30643  4985443   162.7 |  0.684 % |
c |    443170 |   29946   109525 |   61446   54135 11737623   216.8 |  0.684 % |
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#### 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.87 0.95 0.91 2/54 26915
Raw data (stat): 26915 (runsolver) R 26914 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421316428 1052672 99 4294967295 134512640 135381576 3221224480 3221219724 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.0013 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 1439 0 0 0 995 3 0 0 25 0 1 0 421316428 7659520 1416 4294967295 134512640 134672761 3221224576 3221223744 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1870 1416 603 41 0 1829 0
vsize: 7480
[startup+20.002 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 2410 0 0 0 1991 6 0 0 25 0 1 0 421316428 11558912 2387 4294967295 134512640 134672761 3221224576 3221223760 134558890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2822 2387 603 41 0 2781 0
vsize: 11288
[startup+30.0024 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 2841 0 0 0 2990 7 0 0 25 0 1 0 421316428 13307904 2818 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3249 2818 603 41 0 3208 0
vsize: 12996
[startup+40.0026 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 3857 0 0 0 3987 10 0 0 25 0 1 0 421316428 17469440 3834 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3834 603 41 0 4224 0
vsize: 17060
[startup+50.003 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 4629 0 0 0 4984 13 0 0 25 0 1 0 421316428 20701184 4606 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5054 4606 603 41 0 5013 0
vsize: 20216
[startup+60.0027 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 4629 0 0 0 5984 13 0 0 25 0 1 0 421316428 20701184 4606 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5054 4606 603 41 0 5013 0
vsize: 20216
[startup+70.0029 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 4713 0 0 0 6984 13 0 0 25 0 1 0 421316428 21106688 4690 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5153 4690 603 41 0 5112 0
vsize: 20612
[startup+80.0033 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 5602 0 0 0 7981 16 0 0 25 0 1 0 421316428 24735744 5579 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6039 5579 603 41 0 5998 0
vsize: 24156
[startup+90.0031 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 6293 0 0 0 8978 19 0 0 25 0 1 0 421316428 27549696 6270 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6726 6270 603 41 0 6685 0
vsize: 26904
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 6293 0 0 0 9978 19 0 0 25 0 1 0 421316428 27549696 6270 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6726 6270 603 41 0 6685 0
vsize: 26904
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 6293 0 0 0 10978 19 0 0 25 0 1 0 421316428 27549696 6270 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6726 6270 603 41 0 6685 0
vsize: 26904
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 6293 0 0 0 11977 20 0 0 25 0 1 0 421316428 27549696 6270 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6726 6270 603 41 0 6685 0
vsize: 26904
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 6865 0 0 0 12975 22 0 0 25 0 1 0 421316428 29839360 6842 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7285 6842 603 41 0 7244 0
vsize: 29140
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 7093 0 0 0 13975 22 0 0 25 0 1 0 421316428 30781440 7070 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7515 7070 603 41 0 7474 0
vsize: 30060
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 7093 0 0 0 14974 23 0 0 25 0 1 0 421316428 30781440 7070 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7515 7070 603 41 0 7474 0
vsize: 30060
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 7093 0 0 0 15974 23 0 0 25 0 1 0 421316428 30781440 7070 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7515 7070 603 41 0 7474 0
vsize: 30060
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 7097 0 0 0 16973 23 0 0 25 0 1 0 421316428 30781440 7074 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7515 7074 603 41 0 7474 0
vsize: 30060
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 7097 0 0 0 17973 24 0 0 25 0 1 0 421316428 30781440 7074 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7515 7074 603 41 0 7474 0
vsize: 30060
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 7097 0 0 0 18973 24 0 0 25 0 1 0 421316428 30781440 7074 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7515 7074 603 41 0 7474 0
vsize: 30060
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 7097 0 0 0 19972 24 0 0 25 0 1 0 421316428 30781440 7074 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7515 7074 603 41 0 7474 0
vsize: 30060
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 7097 0 0 0 20972 24 0 0 25 0 1 0 421316428 30781440 7074 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7515 7074 603 41 0 7474 0
vsize: 30060
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 7871 0 0 0 21968 28 0 0 25 0 1 0 421316428 34004992 7848 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8302 7848 603 41 0 8261 0
vsize: 33208
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 8052 0 0 0 22968 29 0 0 25 0 1 0 421316428 34672640 8029 4294967295 134512640 134672761 3221224576 3221223680 134560335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8465 8029 603 41 0 8424 0
vsize: 33860
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 8052 0 0 0 23967 29 0 0 25 0 1 0 421316428 34672640 8029 4294967295 134512640 134672761 3221224576 3221223744 134561136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8465 8029 603 41 0 8424 0
vsize: 33860
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 8052 0 0 0 24967 29 0 0 25 0 1 0 421316428 34672640 8029 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8465 8029 603 41 0 8424 0
vsize: 33860
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 8052 0 0 0 25967 29 0 0 25 0 1 0 421316428 34672640 8029 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8465 8029 603 41 0 8424 0
vsize: 33860
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 8615 0 0 0 26965 31 0 0 25 0 1 0 421316428 36945920 8592 4294967295 134512640 134672761 3221224576 3221223680 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9020 8592 603 41 0 8979 0
vsize: 36080
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9106 0 0 0 27963 33 0 0 25 0 1 0 421316428 38973440 9083 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9515 9083 603 41 0 9474 0
vsize: 38060
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 28962 34 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 29962 34 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 30961 35 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 31961 35 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223744 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 32960 36 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 33960 36 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223776 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 34960 36 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 35960 36 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 36959 37 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223744 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 37959 37 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 38958 37 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 39958 38 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9475 0 0 0 40958 38 0 0 25 0 1 0 421316428 40456192 9452 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9877 9452 603 41 0 9836 0
vsize: 39508
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9690 0 0 0 41957 38 0 0 25 0 1 0 421316428 41398272 9667 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10107 9667 603 41 0 10066 0
vsize: 40428
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9976 0 0 0 42955 40 0 0 25 0 1 0 421316428 42643456 9953 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10411 9953 603 41 0 10370 0
vsize: 41644
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9976 0 0 0 43955 40 0 0 25 0 1 0 421316428 42643456 9953 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10411 9953 603 41 0 10370 0
vsize: 41644
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9976 0 0 0 44955 41 0 0 25 0 1 0 421316428 42643456 9953 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10411 9953 603 41 0 10370 0
vsize: 41644
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9991 0 0 0 45954 41 0 0 25 0 1 0 421316428 42643456 9968 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10411 9968 603 41 0 10370 0
vsize: 41644
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9991 0 0 0 46954 41 0 0 25 0 1 0 421316428 42643456 9968 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10411 9968 603 41 0 10370 0
vsize: 41644
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9991 0 0 0 47954 42 0 0 25 0 1 0 421316428 42643456 9968 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10411 9968 603 41 0 10370 0
vsize: 41644
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 9991 0 0 0 48953 42 0 0 25 0 1 0 421316428 42643456 9968 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10411 9968 603 41 0 10370 0
vsize: 41644
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 10873 0 0 0 49950 45 0 0 25 0 1 0 421316428 46264320 10850 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11295 10850 603 41 0 11254 0
vsize: 45180
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11250 0 0 0 50948 47 0 0 25 0 1 0 421316428 47767552 11227 4294967295 134512640 134672761 3221224576 3221223728 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11662 11227 603 41 0 11621 0
vsize: 46648
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11250 0 0 0 51948 48 0 0 25 0 1 0 421316428 47767552 11227 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11662 11227 603 41 0 11621 0
vsize: 46648
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11250 0 0 0 52948 48 0 0 25 0 1 0 421316428 47767552 11227 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11662 11227 603 41 0 11621 0
vsize: 46648
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11250 0 0 0 53947 48 0 0 25 0 1 0 421316428 47767552 11227 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11662 11227 603 41 0 11621 0
vsize: 46648
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11250 0 0 0 54947 48 0 0 25 0 1 0 421316428 47767552 11227 4294967295 134512640 134672761 3221224576 3221223680 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11662 11227 603 41 0 11621 0
vsize: 46648
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11261 0 0 0 55947 48 0 0 25 0 1 0 421316428 47935488 11238 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11703 11238 603 41 0 11662 0
vsize: 46812
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11261 0 0 0 56947 49 0 0 25 0 1 0 421316428 47935488 11238 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11703 11238 603 41 0 11662 0
vsize: 46812
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11261 0 0 0 57946 49 0 0 25 0 1 0 421316428 47935488 11238 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11703 11238 603 41 0 11662 0
vsize: 46812
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11261 0 0 0 58946 49 0 0 25 0 1 0 421316428 47935488 11238 4294967295 134512640 134672761 3221224576 3221223680 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11703 11238 603 41 0 11662 0
vsize: 46812
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11261 0 0 0 59946 49 0 0 25 0 1 0 421316428 47935488 11238 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11703 11238 603 41 0 11662 0
vsize: 46812
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11261 0 0 0 60946 50 0 0 25 0 1 0 421316428 47935488 11238 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11703 11238 603 41 0 11662 0
vsize: 46812
[startup+620.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11261 0 0 0 61945 50 0 0 25 0 1 0 421316428 47935488 11238 4294967295 134512640 134672761 3221224576 3221223680 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11703 11238 603 41 0 11662 0
vsize: 46812
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11261 0 0 0 62945 50 0 0 25 0 1 0 421316428 47935488 11238 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11703 11238 603 41 0 11662 0
vsize: 46812
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11262 0 0 0 63944 51 0 0 25 0 1 0 421316428 47935488 11239 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11703 11239 603 41 0 11662 0
vsize: 46812
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11262 0 0 0 64944 51 0 0 25 0 1 0 421316428 47935488 11239 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11703 11239 603 41 0 11662 0
vsize: 46812
[startup+660.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11262 0 0 0 65944 52 0 0 25 0 1 0 421316428 47935488 11239 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11703 11239 603 41 0 11662 0
vsize: 46812
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11262 0 0 0 66943 52 0 0 25 0 1 0 421316428 47935488 11239 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11703 11239 603 41 0 11662 0
vsize: 46812
[startup+680.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11262 0 0 0 67944 52 0 0 25 0 1 0 421316428 47935488 11239 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11703 11239 603 41 0 11662 0
vsize: 46812
[startup+690.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11262 0 0 0 68944 52 0 0 25 0 1 0 421316428 47935488 11239 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11703 11239 603 41 0 11662 0
vsize: 46812
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11262 0 0 0 69944 52 0 0 25 0 1 0 421316428 47935488 11239 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11703 11239 603 41 0 11662 0
vsize: 46812
[startup+710.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11262 0 0 0 70944 52 0 0 25 0 1 0 421316428 47935488 11239 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11703 11239 603 41 0 11662 0
vsize: 46812
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 11522 0 0 0 71944 53 0 0 25 0 1 0 421316428 48873472 11499 4294967295 134512640 134672761 3221224576 3221223680 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11932 11499 603 41 0 11891 0
vsize: 47728
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 12074 0 0 0 72942 55 0 0 25 0 1 0 421316428 51167232 12051 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12492 12051 603 41 0 12451 0
vsize: 49968
[startup+740.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 12687 0 0 0 73940 57 0 0 25 0 1 0 421316428 53739520 12664 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13120 12664 603 41 0 13079 0
vsize: 52480
[startup+750.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 13284 0 0 0 74939 58 0 0 25 0 1 0 421316428 56147968 13261 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13708 13261 603 41 0 13667 0
vsize: 54832
[startup+760.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 13753 0 0 0 75938 60 0 0 25 0 1 0 421316428 58179584 13730 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14204 13730 603 41 0 14163 0
vsize: 56816
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 14229 0 0 0 76936 61 0 0 25 0 1 0 421316428 60055552 14206 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14662 14206 603 41 0 14621 0
vsize: 58648
[startup+780.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 14792 0 0 0 77935 63 0 0 25 0 1 0 421316428 62455808 14769 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15248 14769 603 41 0 15207 0
vsize: 60992
[startup+790.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 78933 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+800.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 79933 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+810.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 80933 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+820.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 81933 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+830.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 82934 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+840.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 83934 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+850.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 84934 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+860.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 85934 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+870.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 86934 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223760 134559592 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+880.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 87935 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+890.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 88935 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+900.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 89935 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 90935 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+920.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 91935 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 92935 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+940.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 93936 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+950.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 94936 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+960.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 95936 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 96936 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+980.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 97936 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 98936 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 99937 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 100937 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 101937 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15048 0 0 0 102937 64 0 0 25 0 1 0 421316428 63537152 15025 4294967295 134512640 134672761 3221224576 3221223760 134558839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15025 603 41 0 15471 0
vsize: 62048
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 15514 0 0 0 103936 65 0 0 25 0 1 0 421316428 65536000 15491 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16000 15491 603 41 0 15959 0
vsize: 64000
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16017 0 0 0 104934 67 0 0 25 0 1 0 421316428 67534848 15994 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16488 15994 603 41 0 16447 0
vsize: 65952
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16178 0 0 0 105934 67 0 0 25 0 1 0 421316428 68222976 16155 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16155 603 41 0 16615 0
vsize: 66624
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16178 0 0 0 106934 67 0 0 25 0 1 0 421316428 68222976 16155 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16155 603 41 0 16615 0
vsize: 66624
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16178 0 0 0 107935 67 0 0 25 0 1 0 421316428 68222976 16155 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16155 603 41 0 16615 0
vsize: 66624
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16178 0 0 0 108935 67 0 0 25 0 1 0 421316428 68222976 16155 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16155 603 41 0 16615 0
vsize: 66624
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16178 0 0 0 109935 67 0 0 25 0 1 0 421316428 68222976 16155 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16155 603 41 0 16615 0
vsize: 66624
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16178 0 0 0 110935 67 0 0 25 0 1 0 421316428 68222976 16155 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16155 603 41 0 16615 0
vsize: 66624
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16178 0 0 0 111935 67 0 0 25 0 1 0 421316428 68222976 16155 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16155 603 41 0 16615 0
vsize: 66624
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16178 0 0 0 112936 67 0 0 25 0 1 0 421316428 68222976 16155 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16155 603 41 0 16615 0
vsize: 66624
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16178 0 0 0 113936 67 0 0 25 0 1 0 421316428 68222976 16155 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16155 603 41 0 16615 0
vsize: 66624
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16179 0 0 0 114936 67 0 0 25 0 1 0 421316428 68222976 16156 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16156 603 41 0 16615 0
vsize: 66624
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16179 0 0 0 115936 67 0 0 25 0 1 0 421316428 68222976 16156 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16156 603 41 0 16615 0
vsize: 66624
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16179 0 0 0 116936 67 0 0 25 0 1 0 421316428 68222976 16156 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16156 603 41 0 16615 0
vsize: 66624
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16179 0 0 0 117936 67 0 0 25 0 1 0 421316428 68222976 16156 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16156 603 41 0 16615 0
vsize: 66624
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16179 0 0 0 118937 67 0 0 25 0 1 0 421316428 68222976 16156 4294967295 134512640 134672761 3221224576 3221223760 134559604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16156 603 41 0 16615 0
vsize: 66624
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26915
Raw data (stat): 26915 (minisat+) R 26914 24215 24214 0 -1 0 16179 0 0 0 119937 67 0 0 25 0 1 0 421316428 68222976 16156 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 16156 603 41 0 16615 0
vsize: 66624
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 26915
Raw data (stat): 26915 (minisat+) Z 26914 24215 24214 0 -1 12 16182 0 0 0 119937 71 0 0 25 0 1 0 421316428 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.07
CPU time (s): 1200.09
CPU user time (s): 1199.38
CPU system time (s): 0.711891
CPU usage (%): 100.001
Max. virtual memory (Kb): 66624
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####