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-max1024.pi.opb
MD5SUM	6604a6c0d979e1f2b09762e6e4f70f84
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
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 numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04584
Number of variables	1278
Total number of constraints	1087
Number of constraints which are clauses	1087
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	18
Trace number 5788

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-14 01:47:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4194 boxname=wulflinc8 idbench=58 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6604a6c0d979e1f2b09762e6e4f70f84  /oldhome/oroussel/tmp/wulflinc8/normalized-max1024.pi.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc8/normalized-max1024.pi.opb /oldhome/oroussel/tmp/wulflinc8/normalized-max1024.pi.opb
IDLAUNCH: 4194
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        878772 kB
Buffers:         37428 kB
Cached:          96804 kB
SwapCached:          0 kB
Active:          73260 kB
Inactive:        65672 kB
HighTotal:      131008 kB
HighFree:        28504 kB
LowTotal:       903652 kB
LowFree:        850268 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            11376 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:07:22 (client local time) WITH STATUS 10 IN 1200.15 SECONDS
stats: 4194 7 1200.15 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 [1mFound solution: 300[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:69860     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   85971   205224 |   28657       0        0     nan |  0.000 % |
c |       100 |   84914   203008 |   31522      68      453     6.7 |  1.041 % |
c |       250 |   84059   201168 |   34674     199     1521     7.6 |  1.894 % |
c |       475 |   82900   198609 |   38142     380     2806     7.4 |  3.111 % |
c |       813 |   81889   196392 |   41956     698     5285     7.6 |  4.161 % |
c |      1319 |   81408   195320 |   46152    1186     9049     7.6 |  4.676 % |
c |      2078 |   80971   194353 |   50767    1919    17740     9.2 |  5.135 % |
c |      3219 |   80629   193601 |   55844    3013    32516    10.8 |  5.489 % |
c |      4927 |   80341   192960 |   61428    4679    49894    10.7 |  5.797 % |
c |      7489 |   80213   192665 |   67571    7222    97618    13.5 |  5.942 % |
c |     11333 |   80093   192392 |   74328   11047   174199    15.8 |  6.071 % |
c |     17099 |   79990   192155 |   81761   16787   418802    24.9 |  6.188 % |
c |     25748 |   79929   192022 |   89937   25430   636257    25.0 |  6.247 % |
c ==============================================================================
c [1mFound solution: 292[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 |     33905 |   79903   191991 |   26634   33577  1065587    31.7 |  6.247 % |
c |     34005 |   79903   191991 |   29297   15046   541258    36.0 |  6.406 % |
c |     34155 |   79859   191887 |   32227   15195   543422    35.8 |  6.459 % |
c |     34380 |   79859   191887 |   35449   15420   546677    35.5 |  6.459 % |
c |     34718 |   79859   191887 |   38994   15758   555807    35.3 |  6.459 % |
c |     35224 |   79859   191887 |   42894   16264   563462    34.6 |  6.459 % |
c |     35983 |   79859   191887 |   47183   17023   599538    35.2 |  6.459 % |
c |     37122 |   79859   191887 |   51902   18162   627006    34.5 |  6.459 % |
c |     38830 |   79859   191887 |   57092   19870   672608    33.9 |  6.459 % |
c |     41392 |   79859   191887 |   62801   22432   741323    33.0 |  6.459 % |
c |     45237 |   79770   191690 |   69081   26268   854128    32.5 |  6.553 % |
c |     51006 |   79731   191597 |   75989   32035  1028474    32.1 |  6.600 % |
c |     59656 |   79731   191597 |   83588   40685  1759365    43.2 |  6.600 % |
c |     72631 |   79731   191597 |   91947   53660  2294813    42.8 |  6.600 % |
c |     92092 |   79731   191597 |  101142   73121  4025752    55.1 |  6.600 % |
c |    121285 |   79731   191597 |  111256  102314  7080579    69.2 |  6.600 % |
c |    165074 |   79647   191407 |  122382   48578  2432119    50.1 |  6.692 % |
c |    230758 |   79504   191083 |  134620  114250  7725415    67.6 |  6.849 % |
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 -#### 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.92 0.95 0.91 2/54 31987
Raw data (stat): 31987 (runsolver) R 31986 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 408959796 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 4604 0 0 0 986 11 0 0 25 0 1 0 408959796 21532672 4417 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5257 4417 603 41 0 5216 0
vsize: 21028
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 4722 0 0 0 1985 12 0 0 25 0 1 0 408959796 22069248 4535 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5388 4535 603 41 0 5347 0
vsize: 21552
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 4900 0 0 0 2985 12 0 0 25 0 1 0 408959796 22757376 4713 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5556 4713 603 41 0 5515 0
vsize: 22224
[startup+40.0013 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 5211 0 0 0 3983 13 0 0 25 0 1 0 408959796 24150016 5024 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5896 5024 603 41 0 5855 0
vsize: 23584
[startup+50.0018 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 5362 0 0 0 4983 14 0 0 25 0 1 0 408959796 24690688 5175 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6028 5175 603 41 0 5987 0
vsize: 24112
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 5551 0 0 0 5983 14 0 0 25 0 1 0 408959796 25501696 5364 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6226 5364 603 41 0 6185 0
vsize: 24904
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 5709 0 0 0 6983 14 0 0 25 0 1 0 408959796 26042368 5522 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6358 5522 603 41 0 6317 0
vsize: 25432
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 5929 0 0 0 7983 15 0 0 25 0 1 0 408959796 27111424 5742 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 5742 603 41 0 6578 0
vsize: 26476
[startup+90.0042 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 6083 0 0 0 8982 15 0 0 25 0 1 0 408959796 28037120 5896 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6845 5896 603 41 0 6804 0
vsize: 27380
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 6083 0 0 0 9983 15 0 0 25 0 1 0 408959796 28037120 5896 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6845 5896 603 41 0 6804 0
vsize: 27380
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 6083 0 0 0 10983 15 0 0 25 0 1 0 408959796 28037120 5896 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6845 5896 603 41 0 6804 0
vsize: 27380
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 6178 0 0 0 11982 16 0 0 25 0 1 0 408959796 28438528 5991 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6943 5991 603 41 0 6902 0
vsize: 27772
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 6321 0 0 0 12982 16 0 0 25 0 1 0 408959796 28975104 6134 4294967295 134512640 134672761 3221224560 3221223720 134565155 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7074 6134 603 41 0 7033 0
vsize: 28296
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 6521 0 0 0 13982 17 0 0 25 0 1 0 408959796 29777920 6334 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7270 6334 603 41 0 7229 0
vsize: 29080
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 6773 0 0 0 14981 18 0 0 25 0 1 0 408959796 30855168 6586 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7533 6586 603 41 0 7492 0
vsize: 30132
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 6972 0 0 0 15981 18 0 0 25 0 1 0 408959796 31666176 6785 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7731 6785 603 41 0 7690 0
vsize: 30924
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 7321 0 0 0 16980 20 0 0 25 0 1 0 408959796 33009664 7134 4294967295 134512640 134672761 3221224560 3221223696 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7134 603 41 0 8018 0
vsize: 32236
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 7536 0 0 0 17979 20 0 0 25 0 1 0 408959796 33947648 7349 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8288 7349 603 41 0 8247 0
vsize: 33152
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 7818 0 0 0 18978 21 0 0 25 0 1 0 408959796 35016704 7631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8549 7631 603 41 0 8508 0
vsize: 34196
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 8189 0 0 0 19978 22 0 0 25 0 1 0 408959796 36622336 8002 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8941 8002 603 41 0 8900 0
vsize: 35764
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 8570 0 0 0 20977 23 0 0 25 0 1 0 408959796 38084608 8383 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9298 8383 603 41 0 9257 0
vsize: 37192
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 8889 0 0 0 21977 24 0 0 25 0 1 0 408959796 39686144 8702 4294967295 134512640 134672761 3221224560 3221223664 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9689 8702 603 41 0 9648 0
vsize: 38756
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 9211 0 0 0 22976 24 0 0 25 0 1 0 408959796 41021440 9024 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10015 9024 603 41 0 9974 0
vsize: 40060
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 9445 0 0 0 23976 25 0 0 25 0 1 0 408959796 41951232 9258 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10242 9258 603 41 0 10201 0
vsize: 40968
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 9602 0 0 0 24974 26 0 0 25 0 1 0 408959796 42622976 9415 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10406 9415 603 41 0 10365 0
vsize: 41624
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 9800 0 0 0 25974 27 0 0 25 0 1 0 408959796 43433984 9613 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10604 9613 603 41 0 10563 0
vsize: 42416
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 10017 0 0 0 26973 27 0 0 25 0 1 0 408959796 44232704 9830 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10799 9830 603 41 0 10758 0
vsize: 43196
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 10272 0 0 0 27973 28 0 0 25 0 1 0 408959796 45309952 10085 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11062 10085 603 41 0 11021 0
vsize: 44248
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 10503 0 0 0 28973 28 0 0 25 0 1 0 408959796 46243840 10316 4294967295 134512640 134672761 3221224560 3221223684 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11290 10316 603 41 0 11249 0
vsize: 45160
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 10701 0 0 0 29972 29 0 0 25 0 1 0 408959796 47050752 10514 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11487 10514 603 41 0 11446 0
vsize: 45948
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 10951 0 0 0 30972 29 0 0 25 0 1 0 408959796 47996928 10764 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11718 10764 603 41 0 11677 0
vsize: 46872
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 11196 0 0 0 31972 30 0 0 25 0 1 0 408959796 49074176 11009 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11981 11009 603 41 0 11940 0
vsize: 47924
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 11529 0 0 0 32971 31 0 0 25 0 1 0 408959796 50413568 11342 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12308 11342 603 41 0 12267 0
vsize: 49232
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 11904 0 0 0 33970 32 0 0 25 0 1 0 408959796 51888128 11717 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12668 11717 603 41 0 12627 0
vsize: 50672
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 12198 0 0 0 34969 33 0 0 25 0 1 0 408959796 53088256 12011 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12961 12011 603 41 0 12920 0
vsize: 51844
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 12477 0 0 0 35969 34 0 0 25 0 1 0 408959796 54304768 12290 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13258 12290 603 41 0 13217 0
vsize: 53032
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 12718 0 0 0 36968 35 0 0 25 0 1 0 408959796 55242752 12531 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13487 12531 603 41 0 13446 0
vsize: 53948
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 12964 0 0 0 37966 36 0 0 25 0 1 0 408959796 56184832 12777 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13717 12777 603 41 0 13676 0
vsize: 54868
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13225 0 0 0 38965 36 0 0 25 0 1 0 408959796 57257984 13038 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13979 13038 603 41 0 13938 0
vsize: 55916
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13392 0 0 0 39965 37 0 0 25 0 1 0 408959796 57925632 13205 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14142 13205 603 41 0 14101 0
vsize: 56568
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13554 0 0 0 40965 38 0 0 25 0 1 0 408959796 58601472 13367 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14307 13367 603 41 0 14266 0
vsize: 57228
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13732 0 0 0 41964 38 0 0 25 0 1 0 408959796 59273216 13545 4294967295 134512640 134672761 3221224560 3221223696 134560694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14471 13545 603 41 0 14430 0
vsize: 57884
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 42964 39 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223696 134565054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 43964 39 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 44964 39 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 45965 39 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 46965 39 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 47965 39 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 48965 39 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 49965 39 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 50965 39 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223664 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 51965 39 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 52964 39 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 53964 40 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 54963 40 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 55963 40 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 56963 40 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 57963 40 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 58962 41 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 59962 41 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 60962 41 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 61962 41 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 62962 41 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 63961 42 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 64961 42 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 65960 42 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 66960 43 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 67960 43 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 68959 43 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 69959 44 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 70959 44 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 71958 44 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 72958 44 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 73958 45 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13782 0 0 0 74957 45 0 0 25 0 1 0 408959796 59539456 13595 4294967295 134512640 134672761 3221224560 3221223664 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13595 603 41 0 14495 0
vsize: 58144
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31987
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 13923 0 0 0 75956 46 0 0 25 0 1 0 408959796 60080128 13736 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14668 13736 603 41 0 14627 0
vsize: 58672
[startup+770.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 32034
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 14083 0 0 0 76950 52 0 0 25 0 1 0 408959796 60751872 13896 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14832 13896 603 41 0 14791 0
vsize: 59328
[startup+780.027 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 32040
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 14233 0 0 0 77950 52 0 0 25 0 1 0 408959796 61427712 14046 4294967295 134512640 134672761 3221224560 3221223696 134560714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14997 14046 603 41 0 14956 0
vsize: 59988
[startup+790.027 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 32040
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 14471 0 0 0 78949 53 0 0 25 0 1 0 408959796 62361600 14284 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14284 603 41 0 15184 0
vsize: 60900
[startup+800.027 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 32040
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 14723 0 0 0 79949 54 0 0 25 0 1 0 408959796 63299584 14536 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15454 14536 603 41 0 15413 0
vsize: 61816
[startup+810.028 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32040
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 15058 0 0 0 80948 55 0 0 25 0 1 0 408959796 64774144 14871 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15814 14871 603 41 0 15773 0
vsize: 63256
[startup+820.027 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32040
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 15401 0 0 0 81947 56 0 0 25 0 1 0 408959796 66117632 15214 4294967295 134512640 134672761 3221224560 3221223728 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16142 15214 603 41 0 16101 0
vsize: 64568
[startup+830.027 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32040
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 15751 0 0 0 82946 57 0 0 25 0 1 0 408959796 67596288 15564 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16503 15564 603 41 0 16462 0
vsize: 66012
[startup+840.027 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 16125 0 0 0 83946 58 0 0 25 0 1 0 408959796 69062656 15938 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16861 15938 603 41 0 16820 0
vsize: 67444
[startup+850.027 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 16465 0 0 0 84945 59 0 0 25 0 1 0 408959796 70537216 16278 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17221 16278 603 41 0 17180 0
vsize: 68884
[startup+860.027 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 16853 0 0 0 85944 60 0 0 25 0 1 0 408959796 72011776 16666 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17581 16666 603 41 0 17540 0
vsize: 70324
[startup+870.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 17279 0 0 0 86942 61 0 0 25 0 1 0 408959796 74285056 17092 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18136 17092 603 41 0 18095 0
vsize: 72544
[startup+880.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 17647 0 0 0 87941 63 0 0 25 0 1 0 408959796 75886592 17460 4294967295 134512640 134672761 3221224560 3221223712 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18527 17460 603 41 0 18486 0
vsize: 74108
[startup+890.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 18034 0 0 0 88940 64 0 0 25 0 1 0 408959796 77369344 17847 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 17847 603 41 0 18848 0
vsize: 75556
[startup+900.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 18395 0 0 0 89939 65 0 0 25 0 1 0 408959796 78843904 18208 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19249 18208 603 41 0 19208 0
vsize: 76996
[startup+910.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 18742 0 0 0 90938 66 0 0 25 0 1 0 408959796 80322560 18555 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19610 18555 603 41 0 19569 0
vsize: 78440
[startup+920.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 19073 0 0 0 91938 67 0 0 25 0 1 0 408959796 81674240 18886 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19940 18886 603 41 0 19899 0
vsize: 79760
[startup+930.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 19417 0 0 0 92937 68 0 0 25 0 1 0 408959796 83017728 19230 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20268 19230 603 41 0 20227 0
vsize: 81072
[startup+940.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 19804 0 0 0 93937 68 0 0 25 0 1 0 408959796 84627456 19617 4294967295 134512640 134672761 3221224560 3221223664 134560177 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20661 19617 603 41 0 20620 0
vsize: 82644
[startup+950.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 20196 0 0 0 94936 69 0 0 25 0 1 0 408959796 86237184 20009 4294967295 134512640 134672761 3221224560 3221223664 134555084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21054 20009 603 41 0 21013 0
vsize: 84216
[startup+960.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 20625 0 0 0 95935 70 0 0 25 0 1 0 408959796 87990272 20438 4294967295 134512640 134672761 3221224560 3221223664 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21482 20438 603 41 0 21441 0
vsize: 85928
[startup+970.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 20939 0 0 0 96934 71 0 0 25 0 1 0 408959796 89337856 20752 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21811 20752 603 41 0 21770 0
vsize: 87244
[startup+980.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21240 0 0 0 97934 72 0 0 25 0 1 0 408959796 90554368 21053 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21053 603 41 0 22067 0
vsize: 88432
[startup+990.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21249 0 0 0 98934 72 0 0 25 0 1 0 408959796 90554368 21062 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21062 603 41 0 22067 0
vsize: 88432
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21249 0 0 0 99934 72 0 0 25 0 1 0 408959796 90554368 21062 4294967295 134512640 134672761 3221224560 3221223728 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21062 603 41 0 22067 0
vsize: 88432
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21249 0 0 0 100934 72 0 0 25 0 1 0 408959796 90554368 21062 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21062 603 41 0 22067 0
vsize: 88432
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21249 0 0 0 101934 72 0 0 25 0 1 0 408959796 90554368 21062 4294967295 134512640 134672761 3221224560 3221223664 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21062 603 41 0 22067 0
vsize: 88432
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21249 0 0 0 102934 72 0 0 25 0 1 0 408959796 90554368 21062 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21062 603 41 0 22067 0
vsize: 88432
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21249 0 0 0 103935 72 0 0 25 0 1 0 408959796 90554368 21062 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21062 603 41 0 22067 0
vsize: 88432
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21249 0 0 0 104935 72 0 0 25 0 1 0 408959796 90554368 21062 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21062 603 41 0 22067 0
vsize: 88432
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21249 0 0 0 105935 72 0 0 25 0 1 0 408959796 90554368 21062 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21062 603 41 0 22067 0
vsize: 88432
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32042
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21249 0 0 0 106935 72 0 0 25 0 1 0 408959796 90554368 21062 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21062 603 41 0 22067 0
vsize: 88432
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21249 0 0 0 107935 72 0 0 25 0 1 0 408959796 90554368 21062 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21062 603 41 0 22067 0
vsize: 88432
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21249 0 0 0 108935 72 0 0 25 0 1 0 408959796 90554368 21062 4294967295 134512640 134672761 3221224560 3221223696 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21062 603 41 0 22067 0
vsize: 88432
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21251 0 0 0 109936 72 0 0 25 0 1 0 408959796 90554368 21064 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21064 603 41 0 22067 0
vsize: 88432
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21251 0 0 0 110936 72 0 0 25 0 1 0 408959796 90554368 21064 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21064 603 41 0 22067 0
vsize: 88432
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21251 0 0 0 111936 72 0 0 25 0 1 0 408959796 90554368 21064 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21064 603 41 0 22067 0
vsize: 88432
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21251 0 0 0 112936 72 0 0 25 0 1 0 408959796 90554368 21064 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21064 603 41 0 22067 0
vsize: 88432
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21252 0 0 0 113936 72 0 0 25 0 1 0 408959796 90554368 21065 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21065 603 41 0 22067 0
vsize: 88432
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21252 0 0 0 114936 72 0 0 25 0 1 0 408959796 90554368 21065 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21065 603 41 0 22067 0
vsize: 88432
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21252 0 0 0 115937 72 0 0 25 0 1 0 408959796 90554368 21065 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21065 603 41 0 22067 0
vsize: 88432
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21252 0 0 0 116937 72 0 0 25 0 1 0 408959796 90554368 21065 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21065 603 41 0 22067 0
vsize: 88432
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21252 0 0 0 117937 72 0 0 25 0 1 0 408959796 90554368 21065 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21065 603 41 0 22067 0
vsize: 88432
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21252 0 0 0 118937 72 0 0 25 0 1 0 408959796 90554368 21065 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21065 603 41 0 22067 0
vsize: 88432
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32044
Raw data (stat): 31987 (minisat+) R 31986 26667 26666 0 -1 0 21252 0 0 0 119937 72 0 0 25 0 1 0 408959796 90554368 21065 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22108 21065 603 41 0 22067 0
vsize: 88432
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 32044
Raw data (stat): 31987 (minisat+) Z 31986 26667 26666 0 -1 12 21255 0 0 0 119938 76 0 0 25 0 1 0 408959796 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.07
CPU time (s): 1200.15
CPU user time (s): 1199.38
CPU system time (s): 0.765883
CPU usage (%): 100.006
Max. virtual memory (Kb): 88432
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####