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-ii8c1.opb
MD5SUM	5573ac468e70af6b65c69997b62e5033
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	302
Optimality of the best value was proved	NO
Number of terms in the objective function	1020
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	1020
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	1020
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.02984
Number of variables	1020
Total number of constraints	3575
Number of constraints which are clauses	3575
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	10
Trace number 6267

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-14 04:02:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4683 boxname=wulflinc23 idbench=171 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5573ac468e70af6b65c69997b62e5033  /oldhome/oroussel/tmp/wulflinc23/normalized-ii8c1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc23/normalized-ii8c1.opb /oldhome/oroussel/tmp/wulflinc23/normalized-ii8c1.opb
IDLAUNCH: 4683
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        889116 kB
Buffers:         35040 kB
Cached:          67788 kB
SwapCached:        192 kB
Active:          54276 kB
Inactive:        51596 kB
HighTotal:      131008 kB
HighFree:        59416 kB
LowTotal:       903652 kB
LowFree:        829700 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34108 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:22:43 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 4683 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3575 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 |    3575     8330 |    1191       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 315[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:47988     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  117207   274087 |   39069       0        0     nan |  0.000 % |
c |       101 |  117207   274087 |   42975     101      494     4.9 |  0.003 % |
c |       251 |  114945   268917 |   47273     173     1854    10.7 |  1.754 % |
c |       476 |  114762   268505 |   52000     394     3106     7.9 |  1.881 % |
c |       815 |  101001   236913 |   57200     378     4449    11.8 | 12.720 % |
c |      1322 |   95466   224126 |   62921     725     8925    12.3 | 17.168 % |
c |      2081 |   91128   214116 |   69213    1409    25919    18.4 | 20.685 % |
c |      3220 |   80658   189950 |   76134    2270    55061    24.3 | 29.245 % |
c |      4928 |   73432   173265 |   83747    3722   165498    44.5 | 35.171 % |
c |      7490 |   60828   144158 |   92122    5868   281499    48.0 | 45.554 % |
c |     11334 |   56772   134748 |  101334    9591   418320    43.6 | 48.987 % |
c |     17101 |   53851   127954 |  111468   15274   945454    61.9 | 51.485 % |
c |     25750 |   51730   123044 |  122615   23692  1461684    61.7 | 53.223 % |
c |     38724 |   50324   119768 |  134876   36616  2123010    58.0 | 54.415 % |
c |     58186 |   48496   115490 |  148364   55460  4023971    72.6 | 55.931 % |
c |     87379 |   47416   112968 |  163200   84609  5801948    68.6 | 56.830 % |
c |    131168 |   47124   112292 |  179520  128376 12327102    96.0 | 57.066 % |
c ==============================================================================
c [1mFound solution: 314[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 |    145883 |   47073   112174 |   15691  143028 14634985   102.3 | 57.066 % |
c |    145984 |   47073   112174 |   17260   19202  2279790   118.7 | 57.102 % |
c |    146134 |   47073   112174 |   18986   19352  2281767   117.9 | 57.102 % |
c |    146360 |   47073   112174 |   20884   19578  2291027   117.0 | 57.102 % |
c |    146698 |   47073   112174 |   22973   19916  2297397   115.4 | 57.102 % |
c |    147205 |   47073   112174 |   25270   20423  2307687   113.0 | 57.102 % |
c |    147970 |   47073   112174 |   27797   21188  2322722   109.6 | 57.102 % |
c |    149109 |   47073   112174 |   30577   22327  2341706   104.9 | 57.102 % |
c |    150817 |   47073   112174 |   33635   24035  2367483    98.5 | 57.102 % |
c |    153379 |   47073   112174 |   36998   26597  2682981   100.9 | 57.102 % |
c |    157224 |   47014   112032 |   40698   30440  3091715   101.6 | 57.159 % |
c |    162990 |   46990   111975 |   44768   36197  3552910    98.2 | 57.182 % |
c |    171640 |   46990   111975 |   49245   44847  4343003    96.8 | 57.182 % |
c |    184614 |   46919   111807 |   54169   57820  5912089   102.2 | 57.244 % |
c ==============================================================================
c [1mFound solution: 313[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 |    193071 |   46978   111958 |   15659   66277  6502077    98.1 | 57.244 % |
c |    193173 |   46978   111958 |   17224   21229  1118081    52.7 | 57.224 % |
c |    193323 |   46978   111958 |   18947   21379  1119827    52.4 | 57.224 % |
c |    193548 |   46978   111958 |   20842   21604  1122490    52.0 | 57.224 % |
c |    193888 |   46751   111424 |   22926   21562  1131909    52.5 | 57.416 % |
c |    194395 |   46751   111424 |   25218   22069  1150494    52.1 | 57.416 % |
c |    195154 |   46751   111424 |   27740   22828  1191420    52.2 | 57.416 % |
c |    196296 |   46751   111424 |   30514   23970  1255943    52.4 | 57.416 % |
c |    198004 |   46666   111226 |   33566   25672  1295965    50.5 | 57.491 % |
c |    200566 |   46666   111226 |   36923   28234  1623555    57.5 | 57.491 % |
c |    204411 |   46666   111226 |   40615   32079  1811376    56.5 | 57.491 % |
c |    210179 |   46666   111226 |   44676   37847  2087126    55.1 | 57.491 % |
c |    218828 |   46666   111226 |   49144   46496  2792296    60.1 | 57.491 % |
c |    231802 |   46666   111226 |   54059   59470  4258051    71.6 | 57.491 % |
c |    251264 |   46666   111226 |   59465   78932  7099865    89.9 | 57.491 % |
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.93 2/54 8396
Raw data (stat): 8396 (runsolver) R 8395 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481556750 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 3751 0 0 0 988 9 0 0 25 0 1 0 481556750 17969152 3578 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4387 3578 603 41 0 4346 0
vsize: 17548
[startup+20.0018 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 3773 0 0 0 1988 10 0 0 25 0 1 0 481556750 18104320 3600 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4420 3600 603 41 0 4379 0
vsize: 17680
[startup+30.002 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 3906 0 0 0 2987 10 0 0 25 0 1 0 481556750 18644992 3733 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4552 3733 603 41 0 4511 0
vsize: 18208
[startup+40.0031 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 4003 0 0 0 3986 11 0 0 25 0 1 0 481556750 19042304 3830 4294967295 134512640 134672761 3221224576 3221223744 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4649 3830 603 41 0 4608 0
vsize: 18596
[startup+50.0037 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 4126 0 0 0 4985 12 0 0 25 0 1 0 481556750 19492864 3953 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 3953 603 41 0 4718 0
vsize: 19036
[startup+60.0038 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 4365 0 0 0 5984 13 0 0 25 0 1 0 481556750 20439040 4192 4294967295 134512640 134672761 3221224576 3221223792 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4990 4192 603 41 0 4949 0
vsize: 19960
[startup+70.0051 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 4676 0 0 0 6983 15 0 0 25 0 1 0 481556750 21766144 4503 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5314 4503 603 41 0 5273 0
vsize: 21256
[startup+80.0056 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 4957 0 0 0 7982 16 0 0 25 0 1 0 481556750 22908928 4784 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5593 4784 603 41 0 5552 0
vsize: 22372
[startup+90.0058 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 5112 0 0 0 8981 17 0 0 25 0 1 0 481556750 23580672 4939 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5757 4939 603 41 0 5716 0
vsize: 23028
[startup+100.006 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 5302 0 0 0 9979 18 0 0 25 0 1 0 481556750 24379392 5129 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5952 5129 603 41 0 5911 0
vsize: 23808
[startup+110.008 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 5465 0 0 0 10978 19 0 0 25 0 1 0 481556750 25051136 5292 4294967295 134512640 134672761 3221224576 3221223680 134559829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6116 5292 603 41 0 6075 0
vsize: 24464
[startup+120.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 5649 0 0 0 11977 20 0 0 25 0 1 0 481556750 25714688 5476 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6278 5476 603 41 0 6237 0
vsize: 25112
[startup+130.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 5823 0 0 0 12976 21 0 0 25 0 1 0 481556750 26513408 5650 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6473 5650 603 41 0 6432 0
vsize: 25892
[startup+140.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 6067 0 0 0 13975 23 0 0 25 0 1 0 481556750 27582464 5894 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6734 5894 603 41 0 6693 0
vsize: 26936
[startup+150.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 6259 0 0 0 14974 24 0 0 25 0 1 0 481556750 28389376 6086 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6931 6086 603 41 0 6890 0
vsize: 27724
[startup+160.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8396
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 6506 0 0 0 15973 25 0 0 25 0 1 0 481556750 29323264 6333 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7159 6333 603 41 0 7118 0
vsize: 28636
[startup+170.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 6644 0 0 0 16972 26 0 0 25 0 1 0 481556750 29859840 6471 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7290 6471 603 41 0 7249 0
vsize: 29160
[startup+180.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 6815 0 0 0 17970 27 0 0 25 0 1 0 481556750 30531584 6642 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7454 6642 603 41 0 7413 0
vsize: 29816
[startup+190.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 7212 0 0 0 18969 29 0 0 25 0 1 0 481556750 32137216 7039 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7846 7039 603 41 0 7805 0
vsize: 31384
[startup+200.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 7664 0 0 0 19966 31 0 0 25 0 1 0 481556750 34013184 7491 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8304 7491 603 41 0 8263 0
vsize: 33216
[startup+210.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 7907 0 0 0 20965 33 0 0 25 0 1 0 481556750 35069952 7734 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8562 7734 603 41 0 8521 0
vsize: 34248
[startup+220.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 8120 0 0 0 21964 34 0 0 25 0 1 0 481556750 35872768 7947 4294967295 134512640 134672761 3221224576 3221223760 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8758 7947 603 41 0 8717 0
vsize: 35032
[startup+230.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 8547 0 0 0 22962 36 0 0 25 0 1 0 481556750 37617664 8374 4294967295 134512640 134672761 3221224576 3221223680 134559981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9184 8374 603 41 0 9143 0
vsize: 36736
[startup+240.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 8701 0 0 0 23961 37 0 0 25 0 1 0 481556750 38281216 8528 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9346 8528 603 41 0 9305 0
vsize: 37384
[startup+250.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 8892 0 0 0 24960 38 0 0 25 0 1 0 481556750 39088128 8719 4294967295 134512640 134672761 3221224576 3221223716 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9543 8719 603 41 0 9502 0
vsize: 38172
[startup+260.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 9043 0 0 0 25959 39 0 0 25 0 1 0 481556750 39624704 8870 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9674 8870 603 41 0 9633 0
vsize: 38696
[startup+270.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 9179 0 0 0 26958 40 0 0 25 0 1 0 481556750 40415232 9006 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9867 9006 603 41 0 9826 0
vsize: 39468
[startup+280.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 9299 0 0 0 27957 41 0 0 25 0 1 0 481556750 40951808 9126 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9998 9126 603 41 0 9957 0
vsize: 39992
[startup+290.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 9414 0 0 0 28956 42 0 0 25 0 1 0 481556750 41349120 9241 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10095 9241 603 41 0 10054 0
vsize: 40380
[startup+300.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 9519 0 0 0 29956 42 0 0 25 0 1 0 481556750 41750528 9346 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10193 9346 603 41 0 10152 0
vsize: 40772
[startup+310.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 9627 0 0 0 30956 42 0 0 25 0 1 0 481556750 42278912 9454 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10322 9454 603 41 0 10281 0
vsize: 41288
[startup+320.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 9781 0 0 0 31954 44 0 0 25 0 1 0 481556750 42815488 9608 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10453 9608 603 41 0 10412 0
vsize: 41812
[startup+330.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 9955 0 0 0 32953 45 0 0 25 0 1 0 481556750 43606016 9782 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10646 9782 603 41 0 10605 0
vsize: 42584
[startup+340.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 10107 0 0 0 33952 46 0 0 25 0 1 0 481556750 44134400 9934 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10775 9934 603 41 0 10734 0
vsize: 43100
[startup+350.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 10247 0 0 0 34951 47 0 0 25 0 1 0 481556750 44810240 10074 4294967295 134512640 134672761 3221224576 3221223680 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10940 10074 603 41 0 10899 0
vsize: 43760
[startup+360.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 10396 0 0 0 35950 48 0 0 25 0 1 0 481556750 45346816 10223 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11071 10223 603 41 0 11030 0
vsize: 44284
[startup+370.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 10556 0 0 0 36950 49 0 0 25 0 1 0 481556750 46018560 10383 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10383 603 41 0 11194 0
vsize: 44940
[startup+380.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 10767 0 0 0 37948 50 0 0 25 0 1 0 481556750 46821376 10594 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11431 10594 603 41 0 11390 0
vsize: 45724
[startup+390.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 11017 0 0 0 38948 51 0 0 25 0 1 0 481556750 47874048 10844 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11688 10844 603 41 0 11647 0
vsize: 46752
[startup+400.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 11290 0 0 0 39946 52 0 0 25 0 1 0 481556750 48939008 11117 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11948 11117 603 41 0 11907 0
vsize: 47792
[startup+410.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 11593 0 0 0 40945 53 0 0 25 0 1 0 481556750 50266112 11420 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12272 11420 603 41 0 12231 0
vsize: 49088
[startup+420.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 11869 0 0 0 41944 55 0 0 25 0 1 0 481556750 51318784 11696 4294967295 134512640 134672761 3221224576 3221223760 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12529 11696 603 41 0 12488 0
vsize: 50116
[startup+430.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 12154 0 0 0 42943 56 0 0 25 0 1 0 481556750 52518912 11981 4294967295 134512640 134672761 3221224576 3221223680 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12822 11981 603 41 0 12781 0
vsize: 51288
[startup+440.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 12443 0 0 0 43942 57 0 0 25 0 1 0 481556750 53714944 12270 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13114 12270 603 41 0 13073 0
vsize: 52456
[startup+450.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 12720 0 0 0 44941 58 0 0 25 0 1 0 481556750 54775808 12547 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13373 12547 603 41 0 13332 0
vsize: 53492
[startup+460.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 12983 0 0 0 45940 59 0 0 25 0 1 0 481556750 55844864 12810 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13634 12810 603 41 0 13593 0
vsize: 54536
[startup+470.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 13262 0 0 0 46938 61 0 0 25 0 1 0 481556750 57044992 13089 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13927 13089 603 41 0 13886 0
vsize: 55708
[startup+480.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 13558 0 0 0 47938 61 0 0 25 0 1 0 481556750 58249216 13385 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14221 13385 603 41 0 14180 0
vsize: 56884
[startup+490.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 13854 0 0 0 48937 63 0 0 25 0 1 0 481556750 59449344 13681 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14514 13681 603 41 0 14473 0
vsize: 58056
[startup+500.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 14128 0 0 0 49936 63 0 0 25 0 1 0 481556750 60526592 13955 4294967295 134512640 134672761 3221224576 3221223804 134559050 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14777 13955 603 41 0 14736 0
vsize: 59108
[startup+510.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 14401 0 0 0 50935 65 0 0 25 0 1 0 481556750 61718528 14228 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15068 14228 603 41 0 15027 0
vsize: 60272
[startup+520.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 14693 0 0 0 51933 66 0 0 25 0 1 0 481556750 62906368 14520 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15358 14520 603 41 0 15317 0
vsize: 61432
[startup+530.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 14968 0 0 0 52932 68 0 0 25 0 1 0 481556750 63963136 14795 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15616 14795 603 41 0 15575 0
vsize: 62464
[startup+540.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 15253 0 0 0 53931 69 0 0 25 0 1 0 481556750 65163264 15080 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15909 15080 603 41 0 15868 0
vsize: 63636
[startup+550.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 15538 0 0 0 54930 70 0 0 25 0 1 0 481556750 66355200 15365 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16200 15365 603 41 0 16159 0
vsize: 64800
[startup+560.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 15828 0 0 0 55930 70 0 0 25 0 1 0 481556750 67424256 15655 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16461 15655 603 41 0 16420 0
vsize: 65844
[startup+570.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 16088 0 0 0 56929 71 0 0 25 0 1 0 481556750 68481024 15915 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16719 15915 603 41 0 16678 0
vsize: 66876
[startup+580.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 16337 0 0 0 57928 72 0 0 25 0 1 0 481556750 69554176 16164 4294967295 134512640 134672761 3221224576 3221223680 134560285 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16981 16164 603 41 0 16940 0
vsize: 67924
[startup+590.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 16599 0 0 0 58927 73 0 0 25 0 1 0 481556750 70615040 16426 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17240 16426 603 41 0 17199 0
vsize: 68960
[startup+600.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 16859 0 0 0 59927 74 0 0 25 0 1 0 481556750 71680000 16686 4294967295 134512640 134672761 3221224576 3221223680 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17500 16686 603 41 0 17459 0
vsize: 70000
[startup+610.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 17039 0 0 0 60926 74 0 0 25 0 1 0 481556750 72486912 16866 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17697 16866 603 41 0 17656 0
vsize: 70788
[startup+620.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 17243 0 0 0 61925 75 0 0 25 0 1 0 481556750 73814016 17070 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18021 17070 603 41 0 17980 0
vsize: 72084
[startup+630.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 17512 0 0 0 62925 76 0 0 25 0 1 0 481556750 74883072 17339 4294967295 134512640 134672761 3221224576 3221223680 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18282 17339 603 41 0 18241 0
vsize: 73128
[startup+640.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 17794 0 0 0 63924 77 0 0 25 0 1 0 481556750 76083200 17621 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18575 17621 603 41 0 18534 0
vsize: 74300
[startup+650.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 18010 0 0 0 64923 78 0 0 25 0 1 0 481556750 76881920 17837 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18770 17837 603 41 0 18729 0
vsize: 75080
[startup+660.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 18295 0 0 0 65923 78 0 0 25 0 1 0 481556750 78086144 18122 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19064 18122 603 41 0 19023 0
vsize: 76256
[startup+670.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 18568 0 0 0 66922 80 0 0 25 0 1 0 481556750 79142912 18395 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19322 18395 603 41 0 19281 0
vsize: 77288
[startup+680.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 18838 0 0 0 67921 80 0 0 25 0 1 0 481556750 80347136 18665 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19616 18665 603 41 0 19575 0
vsize: 78464
[startup+690.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19084 0 0 0 68921 81 0 0 25 0 1 0 481556750 81285120 18911 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18911 603 41 0 19804 0
vsize: 79380
[startup+700.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19350 0 0 0 69920 82 0 0 25 0 1 0 481556750 82354176 19177 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20106 19177 603 41 0 20065 0
vsize: 80424
[startup+710.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 70921 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+720.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 71921 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223680 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+730.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 72921 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134564499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+740.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 73921 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+750.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 74921 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+760.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 75921 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+770.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 76922 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+780.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 77922 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223680 134559916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+790.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 78922 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+800.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 79922 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+810.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 80922 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+820.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 81923 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+830.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 82923 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+840.031 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 83923 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+850.031 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 84923 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+860.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 85924 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+870.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 86924 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+880.031 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 87924 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223712 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+890.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 88924 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223712 134565134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+900.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 89924 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+910.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 90924 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+920.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 91925 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+930.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 92925 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+940.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 93925 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+950.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 94925 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+960.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 95925 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+970.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 96926 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+980.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 97926 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+990.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 98926 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 99926 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 100926 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 101927 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 102927 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 103927 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 104927 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 105927 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 106928 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 107928 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 108928 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 109928 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 110928 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 111929 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 112929 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 113929 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 114929 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 115929 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 116930 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 117930 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 118930 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 8398
Raw data (stat): 8396 (minisat+) R 8395 3260 3259 0 -1 0 19473 0 0 0 119930 82 0 0 25 0 1 0 481556750 83185664 19300 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19300 603 41 0 20268 0
vsize: 81236
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.98 0.93 1/54 8398
Raw data (stat): 8396 (minisat+) Z 8395 3260 3259 0 -1 12 19476 0 0 0 119930 86 0 0 25 0 1 0 481556750 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.08
CPU time (s): 1200.17
CPU user time (s): 1199.31
CPU system time (s): 0.861868
CPU usage (%): 100.008
Max. virtual memory (Kb): 81236
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####