PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8a4.opb
MD5SUM	8a77190c2eeefb9e88447a9087adfd6f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	283
Optimality of the best value was proved	NO
Number of terms in the objective function	792
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	792
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	792
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.02084
Number of variables	792
Total number of constraints	3194
Number of constraints which are clauses	3194
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 5891

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-14 02:11:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4302 boxname=wulflinc32 idbench=166 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8a77190c2eeefb9e88447a9087adfd6f  /oldhome/oroussel/tmp/wulflinc32/normalized-ii8a4.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc32/normalized-ii8a4.opb /oldhome/oroussel/tmp/wulflinc32/normalized-ii8a4.opb
IDLAUNCH: 4302
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
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:      1034724 kB
MemFree:        704996 kB
Buffers:         35192 kB
Cached:         182964 kB
SwapCached:       1212 kB
Active:         146512 kB
Inactive:       151992 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        704740 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25428 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:31:29 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 4302 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3194 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 |    3194     8388 |    1064       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 354[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 |         4 |   47626   112246 |   15875       4       26     6.5 |  0.000 % |
c |       104 |   47361   111687 |   17462      93     1225    13.2 |  0.521 % |
c |       254 |   47361   111687 |   19208     243     4630    19.1 |  0.521 % |
c ==============================================================================
c [1mFound solution: 346[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 |       431 |   47442   111960 |   15814     419     7912    18.9 |  0.521 % |
c |       533 |   47360   111784 |   17395     519    11037    21.3 |  0.777 % |
c ==============================================================================
c [1mFound solution: 319[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 |       582 |   47671   112647 |   15890     567    12211    21.5 |  0.777 % |
c |       682 |   47671   112647 |   17479     667    13724    20.6 |  0.860 % |
c |       834 |   47671   112647 |   19226     819    15865    19.4 |  0.860 % |
c |      1060 |   47629   112553 |   21149    1044    23666    22.7 |  0.945 % |
c |      1397 |   46908   110974 |   23264    1363    35493    26.0 |  2.354 % |
c |      1903 |   46287   109586 |   25591    1851    65230    35.2 |  3.588 % |
c ==============================================================================
c [1mFound solution: 294[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 |      2040 |   46486   110113 |   15495    1975    65744    33.3 |  3.588 % |
c |      2141 |   46486   110113 |   17044    2076    68018    32.8 |  3.771 % |
c |      2292 |   46486   110113 |   18748    2227    72609    32.6 |  3.771 % |
c |      2518 |   46433   109991 |   20623    2452    84110    34.3 |  3.882 % |
c |      2857 |   46312   109724 |   22686    2785   100451    36.1 |  4.120 % |
c |      3365 |   46312   109724 |   24954    3293   114048    34.6 |  4.120 % |
c ==============================================================================
c [1mFound solution: 283[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 |      3625 |   46434   110062 |   15478    3553   118845    33.4 |  4.120 % |
c |      3725 |   46354   109900 |   17025    3649   124499    34.1 |  4.296 % |
c |      3875 |   46354   109900 |   18728    3799   129147    34.0 |  4.296 % |
c |      4100 |   46264   109704 |   20601    4022   140449    34.9 |  4.469 % |
c |      4437 |   45953   109018 |   22661    4287   150386    35.1 |  5.077 % |
c |      4943 |   45894   108887 |   24927    4792   219227    45.7 |  5.194 % |
c |      5702 |   45382   107757 |   27420    5532   256414    46.4 |  6.189 % |
c |      6841 |   45339   107666 |   30162    6668   364309    54.6 |  6.267 % |
c |      8549 |   45288   107557 |   33178    8373   491019    58.6 |  6.362 % |
c |     11112 |   45168   107273 |   36496   10923   611414    56.0 |  6.622 % |
c |     14956 |   45122   107167 |   40145   14759   795096    53.9 |  6.719 % |
c |     20724 |   45026   106949 |   44160   20508  1308058    63.8 |  6.918 % |
c |     29373 |   45026   106949 |   48576   29157  2150568    73.8 |  6.918 % |
c |     42347 |   45026   106949 |   53434   42131  2922952    69.4 |  6.918 % |
c |     61808 |   45000   106891 |   58777   21517  1280796    59.5 |  6.970 % |
c |     91000 |   44991   106872 |   64655   50708  3380801    66.7 |  6.986 % |
c |    134789 |   44882   106619 |   71120   46306  3138339    67.8 |  7.220 % |
c |    200473 |   44882   106619 |   78233   57666  3417826    59.3 |  7.220 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v x1 -x2 x3 -x4 x5 -x6 x7 -x8 x9 -x10 -x11 x12 -x13 x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 -x45 x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 -x59 x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 x73 -x74 x75 -x76 -x77 x78 x79 -x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 -x91 x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 x107 -x108 -x109 x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 -x123 x124 x125 -x126 x127 -x128 -x129 x130 x131 -x132 -x133 x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 -x151 x152 x153 -x154 x155 -x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 x171 -x172 -x173 x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 -x187 x188 x189 -x190 x191 -x192 -x193 -x194 x195 -x196 -x197 -x198 -x199 -x200 -x201 x202 -x203 -x204 -x205 x206 -x207 -x208 x209 -x210 -x211 -x212 -x213 x214 -x215 -x216 -x217 -x218 x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 x230 -x231 x232 -x233 x234 -x235 x236 x237 -x238 -x239 x240 -x241 -x242 x243 -x244 -x245 -x246 -x247 -x248 -x249 x250 -x251 -x252 x253 -x254 -x255 x256 -x257 x258 -x259 x260 -x261 x262 -x263 x264 -x265 -x266 -x267 -x268 -x269 -x270 x271 -x272 -x273 x274 -x275 -x276 x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 x286 -x287 -x288 -x289 x290 -x291 -x292 -x293 -x294 x295 -x296 -x297 x298 -x299 -x300 -x301 x302 x303 -x304 -x305 -x306 -x307 -x308 -x309 x310 -x311 -x312 x313 -x314 -x315 x316 -x317 x318 -x319 x320 -x321 x322 -x323 x324 -x325 -x326 -x327 -x328 x329 -x330 -x331 -x332 -x333 x334 -x335 -x336 -x337 x338 -x339 x340 -x341 x342 -x343 x344 x345 -x346 -x347 x348 -x349 x350 -x351 -x352 x353 -x354 -x355 -x356 -x357 x358 -x359 -x360 -x361 -x362 x363 -x364 -x365 -x366 -x367 -x368 -x369 x370 -x371 -x372 x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 x382 -x383 -x384 x385 -x386 -x387 x388 -x389 x390 -x391 x392 -x393 x394 -x395 x396 x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 x415 -x416 -x417 x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 x427 -x428 -x429 x430 -x431 -x432 x433 -x434 -x435 x436 -x437 x438 -x439 x440 -x441 x442 -x443 x444 -x445 x446 x447 -x448 -x449 -x450 -x451 -x452 -x453 x454 -x455 -x456 -x457 x458 -x459 -x460 -x461 -x462 x463 -x464 -x465 x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 x475 -x476 -x477 x478 -x479 -x480 -x481 x482 -x483 -x484 x485 -x486 -x487 -x488 -x489 x490 -x491 -x492 -x493 x494 -x495 x496 -x497 x498 -x499 x500 x501 -x502 -x503 x504 x505 -x506 -x507 x508 -x509 x510 -x511 x512 -x513 x514 -x515 x516 x517 -x518 -x519 x520 -x521 x522 -x523 x524 -x525 x526 -x527 x528 x529 -x530 -x531 x532 -x533 x534 -x535 x536 -x537 x538 -x539 x540 -x541 x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 x550 x551 -x552 -x553 x554 -x555 -x556 x557 -x558 -x559 -x560 -x561 x562 -x563 -x564 x565 -x566 -x567 x568 -x569 x570 -x571 x572 -x573 -x574 -x575 x576 x577 -x578 -x579 x580 -x581 x582 -x583 x584 -x585 x586 -x587 x588 -x589 x590 -x591 -x592 x593 -x594 -x595 -x596 -x597 x598 -x599 -x600 x601 -x602 -x603 x604 -x605 x606 -x607 x608 -x609 x610 -x611 x612 -x613 x614 -x615 -x616 -x617 -x618 x619 -x620 -x621 x622 -x623 -x624 -x625 x626 -x627 x628 -x629 x630 -x631 x632 x633 -x634 -x635 x636 x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 x655 -x656 -x657 x658 -x659 -x660 -x661 x662 x663 -x664 -x665 -x666 -x667 -x668 -x669 x670 -x671 -x672 -x673 x674 -x675 -x676 x677 -x678 -x679 -x680 -x681 x682 -x683 -x684 x685 -x686 -x687 x688 -x689 x690 -x691 x692 -x693 x694 -x695 x696 -x697 x698 -x699 -x700 -x701 -x702 x703 -x704 -x705 x706 -x707 -x708 x709 -x710 -x711 x712 -x713 x714 -x715 x716 -x717 x718 -x719 x720 -x721 x722 -x723 -x724 -x725 -x726 -x727 -x728 -x729 x730 x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738#### 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.98 0.94 2/53 14270
Raw data (stat): 14270 (runsolver) R 14269 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480885839 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0018 s]
Raw data (loadavg): 0.93 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 2779 0 0 0 991 6 0 0 25 0 1 0 480885839 13594624 2703 4294967295 134512640 134672761 3221224560 3221223760 134557916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3319 2703 603 41 0 3278 0
vsize: 13276
[startup+20.0032 s]
Raw data (loadavg): 0.94 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 3051 0 0 0 1990 7 0 0 25 0 1 0 480885839 14671872 2975 4294967295 134512640 134672761 3221224560 3221223696 134560658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3582 2975 603 41 0 3541 0
vsize: 14328
[startup+30.0053 s]
Raw data (loadavg): 0.95 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 3315 0 0 0 2990 8 0 0 25 0 1 0 480885839 15884288 3239 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3878 3239 603 41 0 3837 0
vsize: 15512
[startup+40.0058 s]
Raw data (loadavg): 0.96 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 3557 0 0 0 3988 9 0 0 25 0 1 0 480885839 16822272 3481 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4107 3481 603 41 0 4066 0
vsize: 16428
[startup+50.0065 s]
Raw data (loadavg): 0.96 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 3827 0 0 0 4987 10 0 0 25 0 1 0 480885839 18026496 3751 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4401 3751 603 41 0 4360 0
vsize: 17604
[startup+60.0073 s]
Raw data (loadavg): 0.97 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 4104 0 0 0 5987 11 0 0 25 0 1 0 480885839 19095552 4028 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4662 4028 603 41 0 4621 0
vsize: 18648
[startup+70.0081 s]
Raw data (loadavg): 0.97 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 4458 0 0 0 6985 13 0 0 25 0 1 0 480885839 20574208 4382 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5023 4382 603 41 0 4982 0
vsize: 20092
[startup+80.0098 s]
Raw data (loadavg): 0.98 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 4754 0 0 0 7985 13 0 0 25 0 1 0 480885839 21770240 4678 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5315 4678 603 41 0 5274 0
vsize: 21260
[startup+90.0106 s]
Raw data (loadavg): 0.98 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 5002 0 0 0 8984 15 0 0 25 0 1 0 480885839 22704128 4926 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5543 4926 603 41 0 5502 0
vsize: 22172
[startup+100.011 s]
Raw data (loadavg): 0.98 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 5233 0 0 0 9983 15 0 0 25 0 1 0 480885839 23633920 5157 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5770 5157 603 41 0 5729 0
vsize: 23080
[startup+110.012 s]
Raw data (loadavg): 0.98 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 5436 0 0 0 10983 16 0 0 25 0 1 0 480885839 24555520 5360 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5995 5360 603 41 0 5954 0
vsize: 23980
[startup+120.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 5630 0 0 0 11983 16 0 0 25 0 1 0 480885839 25354240 5554 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6190 5554 603 41 0 6149 0
vsize: 24760
[startup+130.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 5800 0 0 0 12983 17 0 0 25 0 1 0 480885839 26157056 5724 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5724 603 41 0 6345 0
vsize: 25544
[startup+140.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 5975 0 0 0 13982 17 0 0 25 0 1 0 480885839 26832896 5899 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6551 5899 603 41 0 6510 0
vsize: 26204
[startup+150.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 6199 0 0 0 14982 18 0 0 25 0 1 0 480885839 27762688 6123 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6778 6123 603 41 0 6737 0
vsize: 27112
[startup+160.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 6395 0 0 0 15981 19 0 0 25 0 1 0 480885839 28561408 6319 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6973 6319 603 41 0 6932 0
vsize: 27892
[startup+170.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 6571 0 0 0 16980 20 0 0 25 0 1 0 480885839 29229056 6495 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7136 6495 603 41 0 7095 0
vsize: 28544
[startup+180.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 6763 0 0 0 17980 21 0 0 25 0 1 0 480885839 30027776 6687 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7331 6687 603 41 0 7290 0
vsize: 29324
[startup+190.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 6963 0 0 0 18979 22 0 0 25 0 1 0 480885839 30830592 6887 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7527 6887 603 41 0 7486 0
vsize: 30108
[startup+200.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7169 0 0 0 19977 24 0 0 25 0 1 0 480885839 31633408 7093 4294967295 134512640 134672761 3221224560 3221223664 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7723 7093 603 41 0 7682 0
vsize: 30892
[startup+210.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7352 0 0 0 20977 24 0 0 25 0 1 0 480885839 32428032 7276 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7917 7276 603 41 0 7876 0
vsize: 31668
[startup+220.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7521 0 0 0 21976 25 0 0 25 0 1 0 480885839 33091584 7445 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8079 7445 603 41 0 8038 0
vsize: 32316
[startup+230.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7661 0 0 0 22976 26 0 0 25 0 1 0 480885839 33615872 7585 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8207 7585 603 41 0 8166 0
vsize: 32828
[startup+240.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7724 0 0 0 23976 26 0 0 25 0 1 0 480885839 33878016 7648 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8271 7648 603 41 0 8230 0
vsize: 33084
[startup+250.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7724 0 0 0 24975 27 0 0 25 0 1 0 480885839 33878016 7648 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8271 7648 603 41 0 8230 0
vsize: 33084
[startup+260.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7724 0 0 0 25975 28 0 0 25 0 1 0 480885839 33878016 7648 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8271 7648 603 41 0 8230 0
vsize: 33084
[startup+270.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7724 0 0 0 26974 28 0 0 25 0 1 0 480885839 33878016 7648 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8271 7648 603 41 0 8230 0
vsize: 33084
[startup+280.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7725 0 0 0 27974 29 0 0 25 0 1 0 480885839 33878016 7649 4294967295 134512640 134672761 3221224560 3221223664 134560250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8271 7649 603 41 0 8230 0
vsize: 33084
[startup+290.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7729 0 0 0 28974 29 0 0 25 0 1 0 480885839 33878016 7653 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8271 7653 603 41 0 8230 0
vsize: 33084
[startup+300.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7731 0 0 0 29974 30 0 0 25 0 1 0 480885839 33878016 7655 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8271 7655 603 41 0 8230 0
vsize: 33084
[startup+310.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7731 0 0 0 30974 30 0 0 25 0 1 0 480885839 33878016 7655 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8271 7655 603 41 0 8230 0
vsize: 33084
[startup+320.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7731 0 0 0 31974 30 0 0 25 0 1 0 480885839 33878016 7655 4294967295 134512640 134672761 3221224560 3221223744 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8271 7655 603 41 0 8230 0
vsize: 33084
[startup+330.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7737 0 0 0 32974 31 0 0 25 0 1 0 480885839 34033664 7661 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8309 7661 603 41 0 8268 0
vsize: 33236
[startup+340.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7743 0 0 0 33974 31 0 0 25 0 1 0 480885839 34033664 7667 4294967295 134512640 134672761 3221224560 3221223664 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8309 7667 603 41 0 8268 0
vsize: 33236
[startup+350.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7744 0 0 0 34974 31 0 0 25 0 1 0 480885839 34033664 7668 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8309 7668 603 41 0 8268 0
vsize: 33236
[startup+360.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7744 0 0 0 35974 31 0 0 25 0 1 0 480885839 34033664 7668 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8309 7668 603 41 0 8268 0
vsize: 33236
[startup+370.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7750 0 0 0 36975 31 0 0 25 0 1 0 480885839 34033664 7674 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8309 7674 603 41 0 8268 0
vsize: 33236
[startup+380.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7756 0 0 0 37974 31 0 0 25 0 1 0 480885839 34033664 7680 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8309 7680 603 41 0 8268 0
vsize: 33236
[startup+390.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7781 0 0 0 38973 31 0 0 25 0 1 0 480885839 34197504 7705 4294967295 134512640 134672761 3221224560 3221223664 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8349 7705 603 41 0 8308 0
vsize: 33396
[startup+400.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7782 0 0 0 39973 32 0 0 25 0 1 0 480885839 34197504 7706 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8349 7706 603 41 0 8308 0
vsize: 33396
[startup+410.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7782 0 0 0 40973 32 0 0 25 0 1 0 480885839 34197504 7706 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8349 7706 603 41 0 8308 0
vsize: 33396
[startup+420.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7782 0 0 0 41973 32 0 0 25 0 1 0 480885839 34197504 7706 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8349 7706 603 41 0 8308 0
vsize: 33396
[startup+430.049 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7783 0 0 0 42973 32 0 0 25 0 1 0 480885839 34197504 7707 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8349 7707 603 41 0 8308 0
vsize: 33396
[startup+440.049 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7790 0 0 0 43974 32 0 0 25 0 1 0 480885839 34197504 7714 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8349 7714 603 41 0 8308 0
vsize: 33396
[startup+450.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 7935 0 0 0 44973 32 0 0 25 0 1 0 480885839 34856960 7859 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8510 7859 603 41 0 8469 0
vsize: 34040
[startup+460.051 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8084 0 0 0 45973 33 0 0 25 0 1 0 480885839 35643392 8008 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8702 8008 603 41 0 8661 0
vsize: 34808
[startup+470.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8219 0 0 0 46973 33 0 0 25 0 1 0 480885839 36167680 8143 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8830 8143 603 41 0 8789 0
vsize: 35320
[startup+480.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8348 0 0 0 47972 34 0 0 25 0 1 0 480885839 36691968 8272 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8958 8272 603 41 0 8917 0
vsize: 35832
[startup+490.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8433 0 0 0 48972 35 0 0 25 0 1 0 480885839 37101568 8357 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9058 8357 603 41 0 9017 0
vsize: 36232
[startup+500.054 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8433 0 0 0 49972 35 0 0 25 0 1 0 480885839 37101568 8357 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9058 8357 603 41 0 9017 0
vsize: 36232
[startup+510.055 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8444 0 0 0 50973 35 0 0 25 0 1 0 480885839 37240832 8368 4294967295 134512640 134672761 3221224560 3221223696 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8368 603 41 0 9051 0
vsize: 36368
[startup+520.056 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8445 0 0 0 51973 35 0 0 25 0 1 0 480885839 37240832 8369 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8369 603 41 0 9051 0
vsize: 36368
[startup+530.056 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8446 0 0 0 52973 35 0 0 25 0 1 0 480885839 37240832 8370 4294967295 134512640 134672761 3221224560 3221223664 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8370 603 41 0 9051 0
vsize: 36368
[startup+540.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8446 0 0 0 53973 35 0 0 25 0 1 0 480885839 37240832 8370 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8370 603 41 0 9051 0
vsize: 36368
[startup+550.058 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8447 0 0 0 54974 35 0 0 25 0 1 0 480885839 37240832 8371 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8371 603 41 0 9051 0
vsize: 36368
[startup+560.059 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8447 0 0 0 55974 35 0 0 25 0 1 0 480885839 37240832 8371 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8371 603 41 0 9051 0
vsize: 36368
[startup+570.059 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8453 0 0 0 56974 35 0 0 25 0 1 0 480885839 37240832 8377 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8377 603 41 0 9051 0
vsize: 36368
[startup+580.059 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8454 0 0 0 57974 35 0 0 25 0 1 0 480885839 37240832 8378 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8378 603 41 0 9051 0
vsize: 36368
[startup+590.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8454 0 0 0 58974 35 0 0 25 0 1 0 480885839 37240832 8378 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8378 603 41 0 9051 0
vsize: 36368
[startup+600.061 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8454 0 0 0 59975 35 0 0 25 0 1 0 480885839 37240832 8378 4294967295 134512640 134672761 3221224560 3221223664 134559841 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8378 603 41 0 9051 0
vsize: 36368
[startup+610.062 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8454 0 0 0 60975 35 0 0 25 0 1 0 480885839 37240832 8378 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8378 603 41 0 9051 0
vsize: 36368
[startup+620.063 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8460 0 0 0 61974 35 0 0 25 0 1 0 480885839 37240832 8384 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8384 603 41 0 9051 0
vsize: 36368
[startup+630.065 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8474 0 0 0 62975 35 0 0 25 0 1 0 480885839 37240832 8398 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8398 603 41 0 9051 0
vsize: 36368
[startup+640.066 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8474 0 0 0 63975 35 0 0 25 0 1 0 480885839 37240832 8398 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9092 8398 603 41 0 9051 0
vsize: 36368
[startup+650.067 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8487 0 0 0 64975 35 0 0 25 0 1 0 480885839 37437440 8411 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9140 8411 603 41 0 9099 0
vsize: 36560
[startup+660.067 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8489 0 0 0 65975 35 0 0 25 0 1 0 480885839 37437440 8413 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9140 8413 603 41 0 9099 0
vsize: 36560
[startup+670.068 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8490 0 0 0 66976 35 0 0 25 0 1 0 480885839 37437440 8414 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9140 8414 603 41 0 9099 0
vsize: 36560
[startup+680.069 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8490 0 0 0 67976 35 0 0 25 0 1 0 480885839 37437440 8414 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9140 8414 603 41 0 9099 0
vsize: 36560
[startup+690.07 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8490 0 0 0 68976 35 0 0 25 0 1 0 480885839 37437440 8414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9140 8414 603 41 0 9099 0
vsize: 36560
[startup+700.07 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8491 0 0 0 69976 35 0 0 25 0 1 0 480885839 37437440 8415 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9140 8415 603 41 0 9099 0
vsize: 36560
[startup+710.071 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8513 0 0 0 70977 35 0 0 25 0 1 0 480885839 37634048 8437 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9188 8437 603 41 0 9147 0
vsize: 36752
[startup+720.072 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8532 0 0 0 71977 35 0 0 25 0 1 0 480885839 37634048 8456 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9188 8456 603 41 0 9147 0
vsize: 36752
[startup+730.074 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8534 0 0 0 72977 35 0 0 25 0 1 0 480885839 37634048 8458 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9188 8458 603 41 0 9147 0
vsize: 36752
[startup+740.074 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8544 0 0 0 73978 35 0 0 25 0 1 0 480885839 37830656 8468 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9236 8468 603 41 0 9195 0
vsize: 36944
[startup+750.075 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8567 0 0 0 74978 35 0 0 25 0 1 0 480885839 37830656 8491 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9236 8491 603 41 0 9195 0
vsize: 36944
[startup+760.076 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8635 0 0 0 75978 35 0 0 25 0 1 0 480885839 38223872 8559 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9332 8559 603 41 0 9291 0
vsize: 37328
[startup+770.077 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8761 0 0 0 76977 36 0 0 25 0 1 0 480885839 38625280 8685 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9430 8685 603 41 0 9389 0
vsize: 37720
[startup+780.077 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8879 0 0 0 77977 36 0 0 25 0 1 0 480885839 39157760 8803 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9560 8803 603 41 0 9519 0
vsize: 38240
[startup+790.078 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 8987 0 0 0 78977 36 0 0 25 0 1 0 480885839 39550976 8911 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9656 8911 603 41 0 9615 0
vsize: 38624
[startup+800.079 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9104 0 0 0 79977 37 0 0 25 0 1 0 480885839 40083456 9028 4294967295 134512640 134672761 3221224560 3221223664 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9028 603 41 0 9745 0
vsize: 39144
[startup+810.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9104 0 0 0 80977 37 0 0 25 0 1 0 480885839 40083456 9028 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9028 603 41 0 9745 0
vsize: 39144
[startup+820.081 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9104 0 0 0 81978 37 0 0 25 0 1 0 480885839 40083456 9028 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9028 603 41 0 9745 0
vsize: 39144
[startup+830.081 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9106 0 0 0 82978 37 0 0 25 0 1 0 480885839 40083456 9030 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9030 603 41 0 9745 0
vsize: 39144
[startup+840.082 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9106 0 0 0 83978 37 0 0 25 0 1 0 480885839 40083456 9030 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9030 603 41 0 9745 0
vsize: 39144
[startup+850.083 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9114 0 0 0 84978 37 0 0 25 0 1 0 480885839 40083456 9038 4294967295 134512640 134672761 3221224560 3221223664 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9038 603 41 0 9745 0
vsize: 39144
[startup+860.084 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9114 0 0 0 85979 37 0 0 25 0 1 0 480885839 40083456 9038 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9038 603 41 0 9745 0
vsize: 39144
[startup+870.084 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9115 0 0 0 86979 37 0 0 25 0 1 0 480885839 40083456 9039 4294967295 134512640 134672761 3221224560 3221223744 134559033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9039 603 41 0 9745 0
vsize: 39144
[startup+880.085 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9116 0 0 0 87979 37 0 0 25 0 1 0 480885839 40083456 9040 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9040 603 41 0 9745 0
vsize: 39144
[startup+890.086 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9116 0 0 0 88979 37 0 0 25 0 1 0 480885839 40083456 9040 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9040 603 41 0 9745 0
vsize: 39144
[startup+900.087 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9116 0 0 0 89980 37 0 0 25 0 1 0 480885839 40083456 9040 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9040 603 41 0 9745 0
vsize: 39144
[startup+910.088 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9116 0 0 0 90980 37 0 0 25 0 1 0 480885839 40083456 9040 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9040 603 41 0 9745 0
vsize: 39144
[startup+920.089 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9116 0 0 0 91980 37 0 0 25 0 1 0 480885839 40083456 9040 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9040 603 41 0 9745 0
vsize: 39144
[startup+930.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9116 0 0 0 92980 37 0 0 25 0 1 0 480885839 40083456 9040 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9040 603 41 0 9745 0
vsize: 39144
[startup+940.091 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9116 0 0 0 93981 37 0 0 25 0 1 0 480885839 40083456 9040 4294967295 134512640 134672761 3221224560 3221223664 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9786 9040 603 41 0 9745 0
vsize: 39144
[startup+950.092 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9126 0 0 0 94981 37 0 0 25 0 1 0 480885839 40235008 9050 4294967295 134512640 134672761 3221224560 3221223744 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9050 603 41 0 9782 0
vsize: 39292
[startup+960.092 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9127 0 0 0 95981 37 0 0 25 0 1 0 480885839 40235008 9051 4294967295 134512640 134672761 3221224560 3221223744 134558700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9051 603 41 0 9782 0
vsize: 39292
[startup+970.093 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9127 0 0 0 96981 37 0 0 25 0 1 0 480885839 40235008 9051 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9051 603 41 0 9782 0
vsize: 39292
[startup+980.093 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9127 0 0 0 97982 37 0 0 25 0 1 0 480885839 40235008 9051 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9051 603 41 0 9782 0
vsize: 39292
[startup+990.094 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9127 0 0 0 98980 37 0 0 25 0 1 0 480885839 40235008 9051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9051 603 41 0 9782 0
vsize: 39292
[startup+1000.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9127 0 0 0 99981 37 0 0 25 0 1 0 480885839 40235008 9051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9051 603 41 0 9782 0
vsize: 39292
[startup+1010.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9136 0 0 0 100981 37 0 0 25 0 1 0 480885839 40235008 9060 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9060 603 41 0 9782 0
vsize: 39292
[startup+1020.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9149 0 0 0 101981 37 0 0 25 0 1 0 480885839 40235008 9073 4294967295 134512640 134672761 3221224560 3221223664 134559922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9073 603 41 0 9782 0
vsize: 39292
[startup+1030.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9151 0 0 0 102981 37 0 0 25 0 1 0 480885839 40235008 9075 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9075 603 41 0 9782 0
vsize: 39292
[startup+1040.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9152 0 0 0 103981 37 0 0 25 0 1 0 480885839 40235008 9076 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9076 603 41 0 9782 0
vsize: 39292
[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9153 0 0 0 104982 37 0 0 25 0 1 0 480885839 40235008 9077 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9077 603 41 0 9782 0
vsize: 39292
[startup+1060.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9153 0 0 0 105982 37 0 0 25 0 1 0 480885839 40235008 9077 4294967295 134512640 134672761 3221224560 3221223696 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9077 603 41 0 9782 0
vsize: 39292
[startup+1070.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9153 0 0 0 106982 37 0 0 25 0 1 0 480885839 40235008 9077 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9077 603 41 0 9782 0
vsize: 39292
[startup+1080.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9154 0 0 0 107982 37 0 0 25 0 1 0 480885839 40235008 9078 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9078 603 41 0 9782 0
vsize: 39292
[startup+1090.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9155 0 0 0 108983 37 0 0 25 0 1 0 480885839 40235008 9079 4294967295 134512640 134672761 3221224560 3221223776 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9079 603 41 0 9782 0
vsize: 39292
[startup+1100.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9156 0 0 0 109983 37 0 0 25 0 1 0 480885839 40235008 9080 4294967295 134512640 134672761 3221224560 3221223664 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9080 603 41 0 9782 0
vsize: 39292
[startup+1110.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9159 0 0 0 110983 37 0 0 25 0 1 0 480885839 40235008 9083 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9083 603 41 0 9782 0
vsize: 39292
[startup+1120.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9161 0 0 0 111983 37 0 0 25 0 1 0 480885839 40235008 9085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9085 603 41 0 9782 0
vsize: 39292
[startup+1130.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9161 0 0 0 112984 37 0 0 25 0 1 0 480885839 40235008 9085 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9085 603 41 0 9782 0
vsize: 39292
[startup+1140.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9161 0 0 0 113984 37 0 0 25 0 1 0 480885839 40235008 9085 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9085 603 41 0 9782 0
vsize: 39292
[startup+1150.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9161 0 0 0 114984 37 0 0 25 0 1 0 480885839 40235008 9085 4294967295 134512640 134672761 3221224560 3221223704 134565187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9085 603 41 0 9782 0
vsize: 39292
[startup+1160.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9161 0 0 0 115984 37 0 0 25 0 1 0 480885839 40235008 9085 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9085 603 41 0 9782 0
vsize: 39292
[startup+1170.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9161 0 0 0 116985 37 0 0 25 0 1 0 480885839 40235008 9085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9085 603 41 0 9782 0
vsize: 39292
[startup+1180.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9161 0 0 0 117985 37 0 0 25 0 1 0 480885839 40235008 9085 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9085 603 41 0 9782 0
vsize: 39292
[startup+1190.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9161 0 0 0 118985 37 0 0 25 0 1 0 480885839 40235008 9085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9085 603 41 0 9782 0
vsize: 39292
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/53 14270
Raw data (stat): 14270 (minisat+) R 14269 7987 7986 0 -1 0 9161 0 0 0 119985 37 0 0 25 0 1 0 480885839 40235008 9085 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9085 603 41 0 9782 0
vsize: 39292
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.98 0.94 1/53 14270
Raw data (stat): 14270 (minisat+) Z 14269 7987 7986 0 -1 12 9164 0 0 0 119986 39 0 0 25 0 1 0 480885839 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.13
CPU time (s): 1200.26
CPU user time (s): 1199.86
CPU system time (s): 0.396939
CPU usage (%): 100.01
Max. virtual memory (Kb): 39292
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####