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/logic-synthesis/normalized-alu4.b.opb
MD5SUM	db06e7fbd4f70a4af68f8f196fdb3636
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	50
Optimality of the best value was proved	NO
Number of terms in the objective function	808
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	808
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	808
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03884
Number of variables	807
Total number of constraints	1838
Number of constraints which are clauses	1823
Number of constraints which are cardinality constraints (but not clauses)	15
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	98
Trace number 4824

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-13 20:27:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=545 boxname=wulflinc18 idbench=61 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  db06e7fbd4f70a4af68f8f196fdb3636  /oldhome/oroussel/tmp/wulflinc18/normalized-alu4.b.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc18/normalized-alu4.b.opb
IDLAUNCH: 545
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        908440 kB
Buffers:         34012 kB
Cached:          56176 kB
SwapCached:        320 kB
Active:          49072 kB
Inactive:        44320 kB
HighTotal:      131008 kB
HighFree:        70840 kB
LowTotal:       903652 kB
LowFree:        837600 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27300 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:47:34 (client local time) WITH STATUS 10 IN 1200.15 SECONDS
stats: 545 7 1200.15 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1695 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 |    1694    35961 |     564       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36470     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   42441   131004 |   14147       0        0     nan |  0.000 % |
c |       103 |   42315   130746 |   15561      97     5670    58.5 |  0.508 % |
c |       254 |   42257   130625 |   17117     246     9210    37.4 |  0.616 % |
c |       482 |   42257   130625 |   18829     474    16778    35.4 |  0.616 % |
c |       820 |   42255   130621 |   20712     810    34182    42.2 |  0.620 % |
c ==============================================================================
c [1mFound solution: 63[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1123 |   42283   130700 |   14094    1110    51005    46.0 |  0.620 % |
c |      1224 |   42283   130700 |   15503    1211    56791    46.9 |  0.656 % |
c ==============================================================================
c [1mFound solution: 58[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1350 |   42293   130731 |   14097    1334    61072    45.8 |  0.656 % |
c |      1450 |   42293   130731 |   15506    1434    64885    45.2 |  0.735 % |
c |      1600 |   42293   130731 |   17057    1584    72364    45.7 |  0.735 % |
c |      1825 |   42293   130731 |   18763    1809    90475    50.0 |  0.735 % |
c |      2165 |   42293   130731 |   20639    2149   100442    46.7 |  0.735 % |
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2333 |   42323   130808 |   14107    2317   105896    45.7 |  0.735 % |
c |      2434 |   42323   130808 |   15517    2418   107674    44.5 |  0.741 % |
c |      2586 |   42323   130808 |   17069    2570   113643    44.2 |  0.741 % |
c |      2812 |   42323   130808 |   18776    2796   122642    43.9 |  0.741 % |
c |      3149 |   42323   130808 |   20654    3133   148371    47.4 |  0.741 % |
c |      3655 |   42323   130808 |   22719    3639   188290    51.7 |  0.741 % |
c |      4416 |   42323   130808 |   24991    4400   229246    52.1 |  0.741 % |
c |      5555 |   42323   130808 |   27490    5539   356505    64.4 |  0.741 % |
c |      7263 |   42323   130808 |   30239    7247   491744    67.9 |  0.741 % |
c |      9825 |   42323   130808 |   33263    9809   797859    81.3 |  0.741 % |
c |     13669 |   42323   130808 |   36589   13653  1440093   105.5 |  0.741 % |
c ==============================================================================
c [1mFound solution: 54[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19430 |   42302   130754 |   14100   19343  2037073   105.3 |  0.741 % |
c |     19531 |   42302   130754 |   15510    9773  1091785   111.7 |  0.814 % |
c |     19682 |   42302   130754 |   17061    9924  1098840   110.7 |  0.814 % |
c |     19907 |   42302   130754 |   18767   10149  1110962   109.5 |  0.814 % |
c |     20244 |   42302   130754 |   20643   10486  1137911   108.5 |  0.814 % |
c |     20750 |   42302   130754 |   22708   10992  1183261   107.6 |  0.814 % |
c |     21509 |   42302   130754 |   24979   11751  1271618   108.2 |  0.814 % |
c |     22648 |   42302   130754 |   27476   12890  1364515   105.9 |  0.814 % |
c |     24356 |   42302   130754 |   30224   14598  1522658   104.3 |  0.814 % |
c |     26918 |   42302   130754 |   33247   17160  1804901   105.2 |  0.814 % |
c |     30765 |   42302   130754 |   36571   21007  2183394   103.9 |  0.814 % |
c |     36531 |   42302   130754 |   40228   26773  2754170   102.9 |  0.814 % |
c ==============================================================================
c [1mFound solution: 53[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41162 |   42320   130803 |   14106   31404  3162248   100.7 |  0.814 % |
c |     41263 |   42320   130803 |   15516   12929  1110801    85.9 |  0.817 % |
c |     41416 |   42320   130803 |   17068   13082  1118557    85.5 |  0.817 % |
c |     41642 |   42320   130803 |   18775   13308  1129179    84.8 |  0.817 % |
c |     41979 |   42320   130803 |   20652   13645  1149623    84.3 |  0.817 % |
c |     42486 |   42320   130803 |   22717   14152  1173763    82.9 |  0.817 % |
c |     43245 |   42320   130803 |   24989   14911  1221475    81.9 |  0.817 % |
c |     44384 |   42320   130803 |   27488   16050  1286940    80.2 |  0.817 % |
c |     46093 |   42320   130803 |   30237   17759  1430670    80.6 |  0.817 % |
c |     48656 |   42320   130803 |   33261   20322  1598315    78.6 |  0.817 % |
c |     52500 |   42320   130803 |   36587   24166  1930446    79.9 |  0.817 % |
c |     58268 |   42320   130803 |   40246   29934  2285715    76.4 |  0.817 % |
c |     66922 |   42320   130803 |   44270   38588  3113757    80.7 |  0.817 % |
c |     79899 |   42320   130803 |   48697   16361  2362967   144.4 |  0.817 % |
c |     99360 |   42320   130803 |   53567   35822  5244635   146.4 |  0.817 % |
c |    128552 |   42320   130803 |   58924   23711  3095697   130.6 |  0.817 % |
c |    172341 |   42320   130803 |   64816   19113  1980374   103.6 |  0.817 % |
c |    238028 |   42320   130803 |   71298   32956  2841949    86.2 |  0.817 % |
c ==============================================================================
c [1mFound solution: 52[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    256317 |   42113   130312 |   14037   43501  3635709    83.6 |  0.817 % |
c |    256418 |   42113   130312 |   15440   14391  1134454    78.8 |  1.341 % |
c |    256570 |   42113   130312 |   16984   14543  1144573    78.7 |  1.341 % |
c |    256795 |   42113   130312 |   18683   14768  1155199    78.2 |  1.341 % |
c |    257132 |   42113   130312 |   20551   15105  1168575    77.4 |  1.341 % |
c |    257638 |   42113   130312 |   22606   15611  1202306    77.0 |  1.341 % |
c |    258397 |   42113   130312 |   24867   16370  1247447    76.2 |  1.341 % |
c |    259538 |   42113   130312 |   27354   17511  1340342    76.5 |  1.341 % |
c |    261246 |   42113   130312 |   30089   19219  1556816    81.0 |  1.341 % |
c |    263809 |   42113   130312 |   33098   21782  1674246    76.9 |  1.341 % |
c |    267654 |   42113   130312 |   36408   25627  2061057    80.4 |  1.341 % |
c |    273420 |   42113   130312 |   40049   31393  2429661    77.4 |  1.341 % |
c |    282070 |   42113   130312 |   44054   40043  3047738    76.1 |  1.341 % |
c |    295044 |   42113   130312 |   48459   20186  1894183    93.8 |  1.341 % |
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 #### 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.85 0.95 0.90 2/55 22909
Raw data (stat): 22909 (runsolver) R 22908 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478819043 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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+9.99974 s]
Raw data (loadavg): 0.87 0.95 0.90 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 2751 0 0 0 990 8 0 0 25 0 1 0 478819043 13803520 2719 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3370 2719 603 41 0 3329 0
vsize: 13480
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.96 0.90 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 3613 0 0 0 1985 12 0 0 25 0 1 0 478819043 17420288 3581 4294967295 134512640 134672761 3221224640 3221223744 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4253 3581 603 41 0 4212 0
vsize: 17012
[startup+30.0008 s]
Raw data (loadavg): 0.91 0.96 0.90 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 4218 0 0 0 2984 13 0 0 25 0 1 0 478819043 19849216 4186 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4186 603 41 0 4805 0
vsize: 19384
[startup+40.0003 s]
Raw data (loadavg): 0.92 0.96 0.90 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 4537 0 0 0 3982 14 0 0 25 0 1 0 478819043 21143552 4505 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5162 4505 603 41 0 5121 0
vsize: 20648
[startup+50.0012 s]
Raw data (loadavg): 0.93 0.96 0.90 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 4730 0 0 0 4982 15 0 0 25 0 1 0 478819043 21934080 4698 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5355 4698 603 41 0 5314 0
vsize: 21420
[startup+60.0014 s]
Raw data (loadavg): 0.94 0.96 0.90 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 4730 0 0 0 5982 15 0 0 25 0 1 0 478819043 21934080 4698 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5355 4698 603 41 0 5314 0
vsize: 21420
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 4730 0 0 0 6982 16 0 0 25 0 1 0 478819043 21934080 4698 4294967295 134512640 134672761 3221224640 3221223840 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5355 4698 603 41 0 5314 0
vsize: 21420
[startup+80.0019 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 4883 0 0 0 7982 16 0 0 25 0 1 0 478819043 22605824 4851 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5519 4851 603 41 0 5478 0
vsize: 22076
[startup+90.0021 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 5214 0 0 0 8981 17 0 0 25 0 1 0 478819043 23941120 5182 4294967295 134512640 134672761 3221224640 3221223744 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5845 5182 603 41 0 5804 0
vsize: 23380
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 5544 0 0 0 9980 18 0 0 25 0 1 0 478819043 25272320 5512 4294967295 134512640 134672761 3221224640 3221223808 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6170 5512 603 41 0 6129 0
vsize: 24680
[startup+110.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 5832 0 0 0 10979 18 0 0 25 0 1 0 478819043 26484736 5800 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6466 5800 603 41 0 6425 0
vsize: 25864
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 6020 0 0 0 11979 19 0 0 25 0 1 0 478819043 27160576 5988 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6631 5988 603 41 0 6590 0
vsize: 26524
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 6020 0 0 0 12979 19 0 0 25 0 1 0 478819043 27160576 5988 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6631 5988 603 41 0 6590 0
vsize: 26524
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 6020 0 0 0 13978 19 0 0 25 0 1 0 478819043 27160576 5988 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6631 5988 603 41 0 6590 0
vsize: 26524
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 6020 0 0 0 14978 20 0 0 25 0 1 0 478819043 27160576 5988 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6631 5988 603 41 0 6590 0
vsize: 26524
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 6020 0 0 0 15978 20 0 0 25 0 1 0 478819043 27160576 5988 4294967295 134512640 134672761 3221224640 3221223788 1074733101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6631 5988 603 41 0 6590 0
vsize: 26524
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 6054 0 0 0 16978 20 0 0 25 0 1 0 478819043 27422720 6022 4294967295 134512640 134672761 3221224640 3221223776 134565039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6695 6022 603 41 0 6654 0
vsize: 26780
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 6057 0 0 0 17978 20 0 0 25 0 1 0 478819043 27422720 6025 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6695 6025 603 41 0 6654 0
vsize: 26780
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 6225 0 0 0 18977 21 0 0 25 0 1 0 478819043 28090368 6193 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6858 6193 603 41 0 6817 0
vsize: 27432
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 6746 0 0 0 19976 22 0 0 25 0 1 0 478819043 30228480 6714 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7380 6714 603 41 0 7339 0
vsize: 29520
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 7193 0 0 0 20974 24 0 0 25 0 1 0 478819043 32108544 7161 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7839 7161 603 41 0 7798 0
vsize: 31356
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 7725 0 0 0 21973 25 0 0 25 0 1 0 478819043 34246656 7693 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7693 603 41 0 8320 0
vsize: 33444
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 7751 0 0 0 22973 25 0 0 25 0 1 0 478819043 34377728 7719 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7719 603 41 0 8352 0
vsize: 33572
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 7751 0 0 0 23973 25 0 0 25 0 1 0 478819043 34377728 7719 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7719 603 41 0 8352 0
vsize: 33572
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22909
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 7751 0 0 0 24973 26 0 0 25 0 1 0 478819043 34377728 7719 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7719 603 41 0 8352 0
vsize: 33572
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 7751 0 0 0 25973 26 0 0 25 0 1 0 478819043 34377728 7719 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7719 603 41 0 8352 0
vsize: 33572
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 7751 0 0 0 26974 26 0 0 25 0 1 0 478819043 34377728 7719 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7719 603 41 0 8352 0
vsize: 33572
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 7751 0 0 0 27974 26 0 0 25 0 1 0 478819043 34377728 7719 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7719 603 41 0 8352 0
vsize: 33572
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 7751 0 0 0 28974 26 0 0 25 0 1 0 478819043 34377728 7719 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7719 603 41 0 8352 0
vsize: 33572
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 7751 0 0 0 29974 26 0 0 25 0 1 0 478819043 34377728 7719 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7719 603 41 0 8352 0
vsize: 33572
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 7807 0 0 0 30974 26 0 0 25 0 1 0 478819043 34643968 7775 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8458 7775 603 41 0 8417 0
vsize: 33832
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 8124 0 0 0 31973 27 0 0 25 0 1 0 478819043 35852288 8092 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8753 8092 603 41 0 8712 0
vsize: 35012
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 8459 0 0 0 32972 28 0 0 25 0 1 0 478819043 37322752 8427 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9112 8427 603 41 0 9071 0
vsize: 36448
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 8750 0 0 0 33970 30 0 0 25 0 1 0 478819043 38526976 8718 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9406 8718 603 41 0 9365 0
vsize: 37624
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 9034 0 0 0 34968 32 0 0 25 0 1 0 478819043 39596032 9002 4294967295 134512640 134672761 3221224640 3221223808 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9667 9002 603 41 0 9626 0
vsize: 38668
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 9364 0 0 0 35967 33 0 0 25 0 1 0 478819043 40939520 9332 4294967295 134512640 134672761 3221224640 3221223596 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9995 9332 603 41 0 9954 0
vsize: 39980
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 9612 0 0 0 36967 33 0 0 25 0 1 0 478819043 42004480 9580 4294967295 134512640 134672761 3221224640 3221223784 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10255 9580 603 41 0 10214 0
vsize: 41020
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 9933 0 0 0 37966 34 0 0 25 0 1 0 478819043 43352064 9901 4294967295 134512640 134672761 3221224640 3221223808 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10584 9901 603 41 0 10543 0
vsize: 42336
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 10251 0 0 0 38965 36 0 0 25 0 1 0 478819043 44683264 10219 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10909 10219 603 41 0 10868 0
vsize: 43636
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 10545 0 0 0 39964 36 0 0 25 0 1 0 478819043 45895680 10513 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11205 10513 603 41 0 11164 0
vsize: 44820
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 10815 0 0 0 40964 37 0 0 25 0 1 0 478819043 46993408 10783 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11473 10783 603 41 0 11432 0
vsize: 45892
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11033 0 0 0 41964 37 0 0 25 0 1 0 478819043 47800320 11001 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11001 603 41 0 11629 0
vsize: 46680
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11033 0 0 0 42964 37 0 0 25 0 1 0 478819043 47800320 11001 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11001 603 41 0 11629 0
vsize: 46680
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11034 0 0 0 43964 37 0 0 25 0 1 0 478819043 47800320 11002 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11002 603 41 0 11629 0
vsize: 46680
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11034 0 0 0 44964 37 0 0 25 0 1 0 478819043 47800320 11002 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11002 603 41 0 11629 0
vsize: 46680
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 45965 37 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 46964 37 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 47964 37 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 48964 37 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 49964 38 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 50964 38 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 51965 38 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 52965 38 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223808 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 53965 38 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22911
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 54965 38 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 55965 38 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 56965 38 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223776 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 57965 38 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11035 0 0 0 58966 38 0 0 25 0 1 0 478819043 47800320 11003 4294967295 134512640 134672761 3221224640 3221223764 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11003 603 41 0 11629 0
vsize: 46680
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11036 0 0 0 59966 38 0 0 25 0 1 0 478819043 47800320 11004 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11004 603 41 0 11629 0
vsize: 46680
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11038 0 0 0 60966 38 0 0 25 0 1 0 478819043 47800320 11006 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11006 603 41 0 11629 0
vsize: 46680
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11040 0 0 0 61966 38 0 0 25 0 1 0 478819043 47800320 11008 4294967295 134512640 134672761 3221224640 3221223776 134560650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11008 603 41 0 11629 0
vsize: 46680
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 62966 38 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 63966 38 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 64966 38 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 65966 38 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223824 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 66966 38 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 67966 38 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 68967 38 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 69967 38 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223808 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 70967 38 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 71966 38 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 72966 39 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 73966 39 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 74966 39 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 75965 40 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 76965 40 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 77965 41 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11041 0 0 0 78964 41 0 0 25 0 1 0 478819043 47800320 11009 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11670 11009 603 41 0 11629 0
vsize: 46680
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11044 0 0 0 79964 41 0 0 25 0 1 0 478819043 47800320 11012 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11670 11012 603 41 0 11629 0
vsize: 46680
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11046 0 0 0 80964 42 0 0 25 0 1 0 478819043 48062464 11014 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11734 11014 603 41 0 11693 0
vsize: 46936
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 81964 42 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 82964 42 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 83964 42 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22913
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 84964 42 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223764 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 85963 43 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 86963 43 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 87963 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 88963 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 89963 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 90963 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 91964 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 92964 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+940.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 93964 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 94964 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+960.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 95964 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+970.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 96964 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223776 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 97965 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 98965 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 99965 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 100965 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 101964 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 102964 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 103964 44 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 104964 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 105964 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 106964 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223824 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 107964 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 108964 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 109964 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 110965 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223824 134558673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 111965 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223824 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 112965 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 113965 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22915
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 114965 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223792 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22917
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 115965 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22917
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 116966 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223744 134559905 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22917
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 117966 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22917
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 118966 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223776 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22917
Raw data (stat): 22909 (minisat+) R 22908 20024 20023 0 -1 0 11047 0 0 0 119966 45 0 0 25 0 1 0 478819043 48062464 11015 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11734 11015 603 41 0 11693 0
vsize: 46936
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 22917
Raw data (stat): 22909 (minisat+) Z 22908 20024 20023 0 -1 12 11050 0 0 0 119966 47 0 0 25 0 1 0 478819043 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.06
CPU time (s): 1200.15
CPU user time (s): 1199.67
CPU system time (s): 0.477927
CPU usage (%): 100.007
Max. virtual memory (Kb): 46936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####