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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/manquinho/logic-synthesis/normalized-max1024.pi.opb
MD5SUM6604a6c0d979e1f2b09762e6e4f70f84
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 259
Optimality of the best value was proved NO
Number of terms in the objective function 1278
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 1278
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 1278
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.04584
Number of variables1278
Total number of constraints1087
Number of constraints which are clauses1087
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint18

Trace number 4653 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-13 19:29:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3442 boxname=wulflinc31 idbench=58 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6604a6c0d979e1f2b09762e6e4f70f84  /oldhome/oroussel/tmp/wulflinc31/normalized-max1024.pi.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc31/normalized-max1024.pi.opb /oldhome/oroussel/tmp/wulflinc31/normalized-max1024.pi.opb
IDLAUNCH: 3442
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        913180 kB
Buffers:         34264 kB
Cached:          48712 kB
SwapCached:        392 kB
Active:          44228 kB
Inactive:        41924 kB
HighTotal:      131008 kB
HighFree:        78568 kB
LowTotal:       903652 kB
LowFree:        834612 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29644 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:49:40 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3442 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1071 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: =====
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1065     6934 |     355       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 300
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2518   maxlim: 978   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   18645    69710 |    6215       0        0     nan |  0.000 % |
c |       100 |   18645    69710 |    6836     100      316     3.2 |  0.552 % |
c |       250 |   18645    69710 |    7520     250      834     3.3 |  0.552 % |
c |       475 |   18645    69710 |    8272     475     1585     3.3 |  0.552 % |
c |       812 |   18645    69710 |    9099     812     2884     3.6 |  0.552 % |
c |      1318 |   18639    69693 |   10009    1317     6425     4.9 |  0.578 % |
c |      2078 |   18639    69693 |   11010    2077    12012     5.8 |  0.578 % |
c |      3217 |   18639    69693 |   12111    3216    56703    17.6 |  0.578 % |
c |      4925 |   18639    69693 |   13322    4924   156514    31.8 |  0.578 % |
c |      7487 |   18639    69693 |   14654    7486   233821    31.2 |  0.578 % |
c |     11331 |   18639    69693 |   16120   11330   557828    49.2 |  0.578 % |
c |     17099 |   18639    69693 |   17732   17098  1014189    59.3 |  0.578 % |
c |     25748 |   18639    69693 |   19505   16313  1378953    84.5 |  0.578 % |
c |     38722 |   18639    69693 |   21455   19237  1028952    53.5 |  0.578 % |
c |     58184 |   18639    69693 |   23601   16281  1178421    72.4 |  0.578 % |
c |     87376 |   18639    69693 |   25961   21350  1615334    75.7 |  0.578 % |
c |    131168 |   18639    69693 |   28557   24993  2673044   107.0 |  0.578 % |
c |    196853 |   18639    69693 |   31413   15521  2141910   138.0 |  0.578 % |
c |    295379 |   18639    69693 |   34554   28034  3527480   125.8 |  0.578 % |
c |    443171 |   18639    69693 |   38010   32130  2829820    88.1 |  0.578 % |
c |    664854 |   18639    69693 |   41811   29699  6271650   211.2 |  0.578 % |
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 -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.87 0.70 0.37 2/54 25195
Raw data (stat): 25195 (runsolver) R 25194 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478466354 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.89 0.71 0.38 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 2014 0 0 0 993 5 0 0 25 0 1 0 478466354 9842688 1992 4294967295 134512640 134672761 3221224560 3221223408 134565768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2403 1992 603 41 0 2362 0
vsize: 9612
[startup+20.0008 s]
Raw data (loadavg): 0.90 0.72 0.38 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 2417 0 0 0 1990 8 0 0 25 0 1 0 478466354 11460608 2395 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2798 2395 603 41 0 2757 0
vsize: 11192
[startup+30.0012 s]
Raw data (loadavg): 1.00 0.75 0.39 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 2420 0 0 0 2990 8 0 0 25 0 1 0 478466354 11460608 2398 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2798 2398 603 41 0 2757 0
vsize: 11192
[startup+40.0012 s]
Raw data (loadavg): 1.07 0.77 0.41 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 2621 0 0 0 3989 9 0 0 25 0 1 0 478466354 12267520 2599 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2995 2599 603 41 0 2954 0
vsize: 11980
[startup+50.0015 s]
Raw data (loadavg): 1.06 0.78 0.41 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 2813 0 0 0 4987 11 0 0 25 0 1 0 478466354 13066240 2791 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3190 2791 603 41 0 3149 0
vsize: 12760
[startup+60.002 s]
Raw data (loadavg): 1.05 0.78 0.42 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 3118 0 0 0 5985 12 0 0 25 0 1 0 478466354 14282752 3096 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3487 3096 603 41 0 3446 0
vsize: 13948
[startup+70.0019 s]
Raw data (loadavg): 1.04 0.79 0.42 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 3412 0 0 0 6984 14 0 0 25 0 1 0 478466354 15499264 3390 4294967295 134512640 134672761 3221224560 3221223664 134560306 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3784 3390 603 41 0 3743 0
vsize: 15136
[startup+80.003 s]
Raw data (loadavg): 1.04 0.80 0.43 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 3926 0 0 0 7982 15 0 0 25 0 1 0 478466354 17653760 3904 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4310 3904 603 41 0 4269 0
vsize: 17240
[startup+90.0026 s]
Raw data (loadavg): 1.03 0.80 0.44 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 4107 0 0 0 8982 16 0 0 25 0 1 0 478466354 18460672 4085 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4507 4085 603 41 0 4466 0
vsize: 18028
[startup+100.003 s]
Raw data (loadavg): 1.02 0.81 0.44 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 4670 0 0 0 9981 17 0 0 25 0 1 0 478466354 20729856 4648 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5061 4648 603 41 0 5020 0
vsize: 20244
[startup+110.004 s]
Raw data (loadavg): 1.02 0.81 0.45 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 4950 0 0 0 10980 18 0 0 25 0 1 0 478466354 21807104 4928 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5324 4928 603 41 0 5283 0
vsize: 21296
[startup+120.005 s]
Raw data (loadavg): 1.02 0.82 0.45 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 4957 0 0 0 11980 18 0 0 25 0 1 0 478466354 21954560 4935 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5360 4935 603 41 0 5319 0
vsize: 21440
[startup+130.005 s]
Raw data (loadavg): 1.01 0.83 0.46 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 4958 0 0 0 12981 18 0 0 25 0 1 0 478466354 21954560 4936 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5360 4936 603 41 0 5319 0
vsize: 21440
[startup+140.005 s]
Raw data (loadavg): 1.01 0.83 0.46 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 4958 0 0 0 13981 18 0 0 25 0 1 0 478466354 21954560 4936 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5360 4936 603 41 0 5319 0
vsize: 21440
[startup+150.005 s]
Raw data (loadavg): 1.01 0.84 0.47 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 4958 0 0 0 14981 18 0 0 25 0 1 0 478466354 21954560 4936 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5360 4936 603 41 0 5319 0
vsize: 21440
[startup+160.006 s]
Raw data (loadavg): 1.01 0.84 0.47 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5096 0 0 0 15981 18 0 0 25 0 1 0 478466354 22495232 5074 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5492 5074 603 41 0 5451 0
vsize: 21968
[startup+170.006 s]
Raw data (loadavg): 1.01 0.85 0.48 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5587 0 0 0 16980 19 0 0 25 0 1 0 478466354 24526848 5565 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5988 5565 603 41 0 5947 0
vsize: 23952
[startup+180.006 s]
Raw data (loadavg): 1.00 0.85 0.48 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5606 0 0 0 17980 19 0 0 25 0 1 0 478466354 24526848 5584 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5988 5584 603 41 0 5947 0
vsize: 23952
[startup+190.007 s]
Raw data (loadavg): 1.00 0.85 0.49 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5606 0 0 0 18980 19 0 0 25 0 1 0 478466354 24526848 5584 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5988 5584 603 41 0 5947 0
vsize: 23952
[startup+200.007 s]
Raw data (loadavg): 1.00 0.86 0.49 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5606 0 0 0 19981 19 0 0 25 0 1 0 478466354 24526848 5584 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5988 5584 603 41 0 5947 0
vsize: 23952
[startup+210.007 s]
Raw data (loadavg): 1.00 0.86 0.50 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5606 0 0 0 20981 19 0 0 25 0 1 0 478466354 24526848 5584 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5988 5584 603 41 0 5947 0
vsize: 23952
[startup+220.008 s]
Raw data (loadavg): 1.00 0.87 0.50 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5655 0 0 0 21981 20 0 0 25 0 1 0 478466354 24797184 5633 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6054 5633 603 41 0 6013 0
vsize: 24216
[startup+230.009 s]
Raw data (loadavg): 1.00 0.87 0.51 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5660 0 0 0 22980 20 0 0 25 0 1 0 478466354 24797184 5638 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6054 5638 603 41 0 6013 0
vsize: 24216
[startup+240.01 s]
Raw data (loadavg): 1.00 0.87 0.51 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5884 0 0 0 23980 21 0 0 25 0 1 0 478466354 25739264 5862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6284 5862 603 41 0 6243 0
vsize: 25136
[startup+250.009 s]
Raw data (loadavg): 1.00 0.88 0.52 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5884 0 0 0 24980 21 0 0 25 0 1 0 478466354 25739264 5862 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6284 5862 603 41 0 6243 0
vsize: 25136
[startup+260.011 s]
Raw data (loadavg): 1.00 0.88 0.52 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5884 0 0 0 25980 21 0 0 25 0 1 0 478466354 25739264 5862 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6284 5862 603 41 0 6243 0
vsize: 25136
[startup+270.011 s]
Raw data (loadavg): 1.00 0.89 0.53 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5884 0 0 0 26980 21 0 0 25 0 1 0 478466354 25739264 5862 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6284 5862 603 41 0 6243 0
vsize: 25136
[startup+280.011 s]
Raw data (loadavg): 1.00 0.89 0.53 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5890 0 0 0 27981 21 0 0 25 0 1 0 478466354 25739264 5868 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6284 5868 603 41 0 6243 0
vsize: 25136
[startup+290.013 s]
Raw data (loadavg): 1.00 0.89 0.54 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5897 0 0 0 28981 21 0 0 25 0 1 0 478466354 25739264 5875 4294967295 134512640 134672761 3221224560 3221223712 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6284 5875 603 41 0 6243 0
vsize: 25136
[startup+300.012 s]
Raw data (loadavg): 1.00 0.89 0.54 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5911 0 0 0 29981 21 0 0 25 0 1 0 478466354 25890816 5889 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6321 5889 603 41 0 6280 0
vsize: 25284
[startup+310.013 s]
Raw data (loadavg): 1.00 0.90 0.55 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5967 0 0 0 30981 21 0 0 25 0 1 0 478466354 26161152 5945 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5945 603 41 0 6346 0
vsize: 25548
[startup+320.013 s]
Raw data (loadavg): 1.00 0.90 0.55 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5975 0 0 0 31981 21 0 0 25 0 1 0 478466354 26161152 5953 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5953 603 41 0 6346 0
vsize: 25548
[startup+330.014 s]
Raw data (loadavg): 1.00 0.90 0.55 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 5990 0 0 0 32981 21 0 0 25 0 1 0 478466354 26161152 5968 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5968 603 41 0 6346 0
vsize: 25548
[startup+340.014 s]
Raw data (loadavg): 1.00 0.91 0.56 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6187 0 0 0 33981 21 0 0 25 0 1 0 478466354 26976256 6165 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6586 6165 603 41 0 6545 0
vsize: 26344
[startup+350.014 s]
Raw data (loadavg): 1.00 0.91 0.56 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6268 0 0 0 34981 21 0 0 25 0 1 0 478466354 27377664 6246 4294967295 134512640 134672761 3221224560 3221223744 134559550 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6684 6246 603 41 0 6643 0
vsize: 26736
[startup+360.015 s]
Raw data (loadavg): 1.00 0.91 0.57 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6276 0 0 0 35982 21 0 0 25 0 1 0 478466354 27377664 6254 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6684 6254 603 41 0 6643 0
vsize: 26736
[startup+370.015 s]
Raw data (loadavg): 1.00 0.91 0.57 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6292 0 0 0 36982 21 0 0 25 0 1 0 478466354 27541504 6270 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6724 6270 603 41 0 6683 0
vsize: 26896
[startup+380.016 s]
Raw data (loadavg): 1.00 0.92 0.57 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6362 0 0 0 37982 22 0 0 25 0 1 0 478466354 27811840 6340 4294967295 134512640 134672761 3221224560 3221223744 134559274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6790 6340 603 41 0 6749 0
vsize: 27160
[startup+390.017 s]
Raw data (loadavg): 1.00 0.92 0.58 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6362 0 0 0 38982 22 0 0 25 0 1 0 478466354 27811840 6340 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6790 6340 603 41 0 6749 0
vsize: 27160
[startup+400.016 s]
Raw data (loadavg): 1.00 0.92 0.58 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6380 0 0 0 39982 22 0 0 25 0 1 0 478466354 27811840 6358 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6790 6358 603 41 0 6749 0
vsize: 27160
[startup+410.017 s]
Raw data (loadavg): 1.00 0.92 0.59 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6413 0 0 0 40982 22 0 0 25 0 1 0 478466354 28073984 6391 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6854 6391 603 41 0 6813 0
vsize: 27416
[startup+420.017 s]
Raw data (loadavg): 1.00 0.92 0.59 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6416 0 0 0 41982 22 0 0 25 0 1 0 478466354 28073984 6394 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6854 6394 603 41 0 6813 0
vsize: 27416
[startup+430.018 s]
Raw data (loadavg): 1.00 0.93 0.59 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6416 0 0 0 42982 22 0 0 25 0 1 0 478466354 28073984 6394 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6854 6394 603 41 0 6813 0
vsize: 27416
[startup+440.018 s]
Raw data (loadavg): 1.00 0.93 0.60 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6416 0 0 0 43982 22 0 0 25 0 1 0 478466354 28073984 6394 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6854 6394 603 41 0 6813 0
vsize: 27416
[startup+450.018 s]
Raw data (loadavg): 1.00 0.93 0.60 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6416 0 0 0 44982 22 0 0 25 0 1 0 478466354 28073984 6394 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6854 6394 603 41 0 6813 0
vsize: 27416
[startup+460.019 s]
Raw data (loadavg): 1.00 0.93 0.60 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 6720 0 0 0 45982 22 0 0 25 0 1 0 478466354 29417472 6698 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7182 6698 603 41 0 7141 0
vsize: 28728
[startup+470.019 s]
Raw data (loadavg): 1.00 0.93 0.61 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7147 0 0 0 46981 24 0 0 25 0 1 0 478466354 31170560 7125 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7610 7125 603 41 0 7569 0
vsize: 30440
[startup+480.02 s]
Raw data (loadavg): 1.00 0.94 0.61 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7147 0 0 0 47981 24 0 0 25 0 1 0 478466354 31170560 7125 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7610 7125 603 41 0 7569 0
vsize: 30440
[startup+490.02 s]
Raw data (loadavg): 1.00 0.94 0.62 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7147 0 0 0 48981 24 0 0 25 0 1 0 478466354 31170560 7125 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7610 7125 603 41 0 7569 0
vsize: 30440
[startup+500.02 s]
Raw data (loadavg): 1.00 0.94 0.62 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7147 0 0 0 49981 24 0 0 25 0 1 0 478466354 31170560 7125 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7610 7125 603 41 0 7569 0
vsize: 30440
[startup+510.02 s]
Raw data (loadavg): 1.00 0.94 0.62 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7147 0 0 0 50981 24 0 0 25 0 1 0 478466354 31170560 7125 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7610 7125 603 41 0 7569 0
vsize: 30440
[startup+520.019 s]
Raw data (loadavg): 1.00 0.94 0.63 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7360 0 0 0 51981 24 0 0 25 0 1 0 478466354 31977472 7338 4294967295 134512640 134672761 3221224560 3221223744 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7807 7339 603 41 0 7766 0
vsize: 31228
[startup+530.021 s]
Raw data (loadavg): 1.00 0.94 0.63 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7720 0 0 0 52980 25 0 0 25 0 1 0 478466354 33452032 7698 4294967295 134512640 134672761 3221224560 3221223664 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8167 7698 603 41 0 8126 0
vsize: 32668
[startup+540.021 s]
Raw data (loadavg): 1.00 0.94 0.64 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7720 0 0 0 53980 25 0 0 25 0 1 0 478466354 33452032 7698 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8167 7698 603 41 0 8126 0
vsize: 32668
[startup+550.02 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7720 0 0 0 54981 25 0 0 25 0 1 0 478466354 33452032 7698 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8167 7698 603 41 0 8126 0
vsize: 32668
[startup+560.02 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7836 0 0 0 55980 25 0 0 25 0 1 0 478466354 33992704 7814 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7814 603 41 0 8258 0
vsize: 33196
[startup+570.02 s]
Raw data (loadavg): 1.00 0.95 0.65 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7836 0 0 0 56981 25 0 0 25 0 1 0 478466354 33992704 7814 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7814 603 41 0 8258 0
vsize: 33196
[startup+580.021 s]
Raw data (loadavg): 1.00 0.95 0.65 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7836 0 0 0 57981 25 0 0 25 0 1 0 478466354 33992704 7814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7814 603 41 0 8258 0
vsize: 33196
[startup+590.021 s]
Raw data (loadavg): 1.00 0.95 0.65 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7836 0 0 0 58981 25 0 0 25 0 1 0 478466354 33992704 7814 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7814 603 41 0 8258 0
vsize: 33196
[startup+600.022 s]
Raw data (loadavg): 1.00 0.95 0.65 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7836 0 0 0 59981 25 0 0 25 0 1 0 478466354 33992704 7814 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7814 603 41 0 8258 0
vsize: 33196
[startup+610.023 s]
Raw data (loadavg): 1.00 0.95 0.66 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7839 0 0 0 60981 26 0 0 25 0 1 0 478466354 33992704 7817 4294967295 134512640 134672761 3221224560 3221223744 134558667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7817 603 41 0 8258 0
vsize: 33196
[startup+620.023 s]
Raw data (loadavg): 1.00 0.95 0.66 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7839 0 0 0 61981 26 0 0 25 0 1 0 478466354 33992704 7817 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7817 603 41 0 8258 0
vsize: 33196
[startup+630.024 s]
Raw data (loadavg): 1.00 0.95 0.66 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7839 0 0 0 62981 26 0 0 25 0 1 0 478466354 33992704 7817 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7817 603 41 0 8258 0
vsize: 33196
[startup+640.024 s]
Raw data (loadavg): 1.00 0.95 0.67 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7839 0 0 0 63981 26 0 0 25 0 1 0 478466354 33992704 7817 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7817 603 41 0 8258 0
vsize: 33196
[startup+650.024 s]
Raw data (loadavg): 1.00 0.95 0.67 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7839 0 0 0 64981 26 0 0 25 0 1 0 478466354 33992704 7817 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7817 603 41 0 8258 0
vsize: 33196
[startup+660.025 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 7839 0 0 0 65982 26 0 0 25 0 1 0 478466354 33992704 7817 4294967295 134512640 134672761 3221224560 3221223664 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7817 603 41 0 8258 0
vsize: 33196
[startup+670.025 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 8145 0 0 0 66981 27 0 0 25 0 1 0 478466354 35196928 8123 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8593 8123 603 41 0 8552 0
vsize: 34372
[startup+680.027 s]
Raw data (loadavg): 1.00 0.96 0.68 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 9070 0 0 0 67978 29 0 0 25 0 1 0 478466354 39092224 9048 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9544 9048 603 41 0 9503 0
vsize: 38176
[startup+690.028 s]
Raw data (loadavg): 1.00 0.96 0.68 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 9824 0 0 0 68976 32 0 0 25 0 1 0 478466354 42180608 9802 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10298 9802 603 41 0 10257 0
vsize: 41192
[startup+700.027 s]
Raw data (loadavg): 1.00 0.96 0.68 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 69973 35 0 0 25 0 1 0 478466354 45264896 10547 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11051 10547 603 41 0 11010 0
vsize: 44204
[startup+710.027 s]
Raw data (loadavg): 1.00 0.96 0.69 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 70973 35 0 0 25 0 1 0 478466354 45264896 10547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11051 10547 603 41 0 11010 0
vsize: 44204
[startup+720.027 s]
Raw data (loadavg): 1.00 0.96 0.69 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 71973 35 0 0 25 0 1 0 478466354 45264896 10547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11051 10547 603 41 0 11010 0
vsize: 44204
[startup+730.028 s]
Raw data (loadavg): 1.00 0.96 0.69 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 72974 35 0 0 25 0 1 0 478466354 45264896 10547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11051 10547 603 41 0 11010 0
vsize: 44204
[startup+740.028 s]
Raw data (loadavg): 1.00 0.96 0.70 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 73974 35 0 0 25 0 1 0 478466354 45264896 10547 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11051 10547 603 41 0 11010 0
vsize: 44204
[startup+750.028 s]
Raw data (loadavg): 1.00 0.96 0.70 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 74974 35 0 0 25 0 1 0 478466354 45174784 10547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10547 603 41 0 10988 0
vsize: 44116
[startup+760.029 s]
Raw data (loadavg): 1.00 0.97 0.70 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 75974 35 0 0 25 0 1 0 478466354 45174784 10547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10547 603 41 0 10988 0
vsize: 44116
[startup+770.029 s]
Raw data (loadavg): 1.00 0.97 0.70 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 76974 35 0 0 25 0 1 0 478466354 45174784 10547 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10547 603 41 0 10988 0
vsize: 44116
[startup+780.03 s]
Raw data (loadavg): 1.00 0.97 0.71 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 77974 35 0 0 25 0 1 0 478466354 45174784 10547 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10547 603 41 0 10988 0
vsize: 44116
[startup+790.029 s]
Raw data (loadavg): 1.00 0.97 0.71 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 78975 35 0 0 25 0 1 0 478466354 45174784 10547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10547 603 41 0 10988 0
vsize: 44116
[startup+800.029 s]
Raw data (loadavg): 1.00 0.97 0.71 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 79975 35 0 0 25 0 1 0 478466354 45174784 10547 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10547 603 41 0 10988 0
vsize: 44116
[startup+810.03 s]
Raw data (loadavg): 1.00 0.97 0.72 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 80975 35 0 0 25 0 1 0 478466354 45174784 10547 4294967295 134512640 134672761 3221224560 3221223744 134558934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10547 603 41 0 10988 0
vsize: 44116
[startup+820.029 s]
Raw data (loadavg): 1.00 0.97 0.72 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 81975 35 0 0 25 0 1 0 478466354 45174784 10547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10547 603 41 0 10988 0
vsize: 44116
[startup+830.03 s]
Raw data (loadavg): 1.00 0.97 0.72 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 82975 35 0 0 25 0 1 0 478466354 45174784 10547 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10547 603 41 0 10988 0
vsize: 44116
[startup+840.031 s]
Raw data (loadavg): 1.00 0.97 0.72 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 83976 35 0 0 25 0 1 0 478466354 45174784 10547 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10547 603 41 0 10988 0
vsize: 44116
[startup+850.031 s]
Raw data (loadavg): 1.00 0.97 0.73 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 84976 35 0 0 25 0 1 0 478466354 45174784 10547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10547 603 41 0 10988 0
vsize: 44116
[startup+860.031 s]
Raw data (loadavg): 1.00 0.97 0.73 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10569 0 0 0 85976 35 0 0 25 0 1 0 478466354 45174784 10547 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10547 603 41 0 10988 0
vsize: 44116
[startup+870.031 s]
Raw data (loadavg): 1.00 0.97 0.73 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10570 0 0 0 86976 35 0 0 25 0 1 0 478466354 45174784 10548 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10548 603 41 0 10988 0
vsize: 44116
[startup+880.032 s]
Raw data (loadavg): 1.00 0.97 0.73 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10571 0 0 0 87976 35 0 0 25 0 1 0 478466354 45174784 10549 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10549 603 41 0 10988 0
vsize: 44116
[startup+890.032 s]
Raw data (loadavg): 1.00 0.97 0.74 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10633 0 0 0 88976 36 0 0 25 0 1 0 478466354 45445120 10611 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11095 10611 603 41 0 11054 0
vsize: 44380
[startup+900.032 s]
Raw data (loadavg): 1.00 0.97 0.74 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10638 0 0 0 89976 36 0 0 25 0 1 0 478466354 45445120 10616 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11095 10616 603 41 0 11054 0
vsize: 44380
[startup+910.033 s]
Raw data (loadavg): 1.00 0.97 0.74 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10644 0 0 0 90976 36 0 0 25 0 1 0 478466354 45588480 10622 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10622 603 41 0 11089 0
vsize: 44520
[startup+920.033 s]
Raw data (loadavg): 1.00 0.97 0.74 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10646 0 0 0 91977 36 0 0 25 0 1 0 478466354 45588480 10624 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10624 603 41 0 11089 0
vsize: 44520
[startup+930.034 s]
Raw data (loadavg): 1.00 0.97 0.74 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10646 0 0 0 92977 36 0 0 25 0 1 0 478466354 45588480 10624 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10624 603 41 0 11089 0
vsize: 44520
[startup+940.034 s]
Raw data (loadavg): 1.00 0.97 0.75 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10646 0 0 0 93977 36 0 0 25 0 1 0 478466354 45588480 10624 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10624 603 41 0 11089 0
vsize: 44520
[startup+950.035 s]
Raw data (loadavg): 1.00 0.97 0.75 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10646 0 0 0 94977 36 0 0 25 0 1 0 478466354 45588480 10624 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10624 603 41 0 11089 0
vsize: 44520
[startup+960.036 s]
Raw data (loadavg): 1.00 0.97 0.75 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10646 0 0 0 95977 36 0 0 25 0 1 0 478466354 45588480 10624 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10624 603 41 0 11089 0
vsize: 44520
[startup+970.036 s]
Raw data (loadavg): 1.00 0.97 0.75 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10646 0 0 0 96978 36 0 0 25 0 1 0 478466354 45588480 10624 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10624 603 41 0 11089 0
vsize: 44520
[startup+980.037 s]
Raw data (loadavg): 1.00 0.97 0.75 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10646 0 0 0 97978 36 0 0 25 0 1 0 478466354 45588480 10624 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10624 603 41 0 11089 0
vsize: 44520
[startup+990.037 s]
Raw data (loadavg): 1.00 0.97 0.75 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10646 0 0 0 98978 36 0 0 25 0 1 0 478466354 45588480 10624 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10624 603 41 0 11089 0
vsize: 44520
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.97 0.76 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10658 0 0 0 99978 36 0 0 25 0 1 0 478466354 45588480 10636 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11130 10636 603 41 0 11089 0
vsize: 44520
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.97 0.76 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 10713 0 0 0 100978 36 0 0 25 0 1 0 478466354 45862912 10691 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11197 10691 603 41 0 11156 0
vsize: 44788
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.97 0.76 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11498 0 0 0 101977 37 0 0 25 0 1 0 478466354 49053696 11476 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11976 11476 603 41 0 11935 0
vsize: 47904
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.97 0.76 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11986 0 0 0 102976 38 0 0 25 0 1 0 478466354 51056640 11964 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12465 11964 603 41 0 12424 0
vsize: 49860
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.97 0.76 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11986 0 0 0 103976 38 0 0 25 0 1 0 478466354 51056640 11964 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12465 11964 603 41 0 12424 0
vsize: 49860
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.97 0.77 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11986 0 0 0 104976 38 0 0 25 0 1 0 478466354 51056640 11964 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12465 11964 603 41 0 12424 0
vsize: 49860
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.97 0.77 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11986 0 0 0 105976 39 0 0 25 0 1 0 478466354 51056640 11964 4294967295 134512640 134672761 3221224560 3221223656 1075347310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11964 603 41 0 12424 0
vsize: 49860
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.97 0.77 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 106975 39 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.97 0.77 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 107975 39 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.97 0.77 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 108975 40 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.97 0.78 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 109975 40 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.97 0.78 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 110974 41 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.97 0.78 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 111974 41 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.97 0.78 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 112974 42 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.97 0.78 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 113974 42 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.97 0.79 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 114973 42 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.97 0.79 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 115973 42 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.97 0.79 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 116973 43 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.97 0.79 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 117973 43 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.97 0.79 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 118973 43 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.97 0.80 2/54 25195
Raw data (stat): 25195 (minisat+) R 25194 23176 23175 0 -1 0 11989 0 0 0 119972 44 0 0 25 0 1 0 478466354 51056640 11967 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11967 603 41 0 12424 0
vsize: 49860
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.97 0.80 1/54 25195
Raw data (stat): 25195 (minisat+) Z 25194 23176 23175 0 -1 12 11992 0 0 0 119973 46 0 0 25 0 1 0 478466354 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.08
CPU time (s): 1200.2
CPU user time (s): 1199.73
CPU system time (s): 0.464929
CPU usage (%): 100.01
Max. virtual memory (Kb): 49860
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####