PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-14 01:48:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4197 boxname=wulflinc24 idbench=61 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  db06e7fbd4f70a4af68f8f196fdb3636  /oldhome/oroussel/tmp/wulflinc24/normalized-alu4.b.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc24/normalized-alu4.b.opb /oldhome/oroussel/tmp/wulflinc24/normalized-alu4.b.opb
IDLAUNCH: 4197
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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.080
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:        833528 kB
Buffers:         35108 kB
Cached:         123448 kB
SwapCached:       3828 kB
Active:          52016 kB
Inactive:       113204 kB
HighTotal:      131008 kB
HighFree:         5320 kB
LowTotal:       903652 kB
LowFree:        828208 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30304 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:08:05 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 4197 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1695 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1694    35961 |     564       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36470     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   42441   131004 |   14147       0        0     nan |  0.000 % |
c |       103 |   42315   130746 |   15561      97     5670    58.5 |  0.508 % |
c |       254 |   42257   130625 |   17117     246     9210    37.4 |  0.616 % |
c |       482 |   42257   130625 |   18829     474    16778    35.4 |  0.616 % |
c |       820 |   42255   130621 |   20712     810    34182    42.2 |  0.620 % |
c ==============================================================================
c [1mFound solution: 63[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1123 |   42283   130700 |   14094    1110    51005    46.0 |  0.620 % |
c |      1224 |   42283   130700 |   15503    1211    56791    46.9 |  0.656 % |
c ==============================================================================
c [1mFound solution: 58[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1350 |   42293   130731 |   14097    1334    61072    45.8 |  0.656 % |
c |      1450 |   42293   130731 |   15506    1434    64885    45.2 |  0.735 % |
c |      1600 |   42293   130731 |   17057    1584    72364    45.7 |  0.735 % |
c |      1825 |   42293   130731 |   18763    1809    90475    50.0 |  0.735 % |
c |      2165 |   42293   130731 |   20639    2149   100442    46.7 |  0.735 % |
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2333 |   42323   130808 |   14107    2317   105896    45.7 |  0.735 % |
c |      2434 |   42323   130808 |   15517    2418   107674    44.5 |  0.741 % |
c |      2586 |   42323   130808 |   17069    2570   113643    44.2 |  0.741 % |
c |      2812 |   42323   130808 |   18776    2796   122642    43.9 |  0.741 % |
c |      3149 |   42323   130808 |   20654    3133   148371    47.4 |  0.741 % |
c |      3655 |   42323   130808 |   22719    3639   188290    51.7 |  0.741 % |
c |      4416 |   42323   130808 |   24991    4400   229246    52.1 |  0.741 % |
c |      5555 |   42323   130808 |   27490    5539   356505    64.4 |  0.741 % |
c |      7263 |   42323   130808 |   30239    7247   491744    67.9 |  0.741 % |
c |      9825 |   42323   130808 |   33263    9809   797859    81.3 |  0.741 % |
c |     13669 |   42323   130808 |   36589   13653  1440093   105.5 |  0.741 % |
c ==============================================================================
c [1mFound solution: 54[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19430 |   42302   130754 |   14100   19343  2037073   105.3 |  0.741 % |
c |     19531 |   42302   130754 |   15510    9773  1091785   111.7 |  0.814 % |
c |     19682 |   42302   130754 |   17061    9924  1098840   110.7 |  0.814 % |
c |     19907 |   42302   130754 |   18767   10149  1110962   109.5 |  0.814 % |
c |     20244 |   42302   130754 |   20643   10486  1137911   108.5 |  0.814 % |
c |     20750 |   42302   130754 |   22708   10992  1183261   107.6 |  0.814 % |
c |     21509 |   42302   130754 |   24979   11751  1271618   108.2 |  0.814 % |
c |     22648 |   42302   130754 |   27476   12890  1364515   105.9 |  0.814 % |
c |     24356 |   42302   130754 |   30224   14598  1522658   104.3 |  0.814 % |
c |     26918 |   42302   130754 |   33247   17160  1804901   105.2 |  0.814 % |
c |     30765 |   42302   130754 |   36571   21007  2183394   103.9 |  0.814 % |
c |     36531 |   42302   130754 |   40228   26773  2754170   102.9 |  0.814 % |
c ==============================================================================
c [1mFound solution: 53[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41162 |   42320   130803 |   14106   31404  3162248   100.7 |  0.814 % |
c |     41263 |   42320   130803 |   15516   12929  1110801    85.9 |  0.817 % |
c |     41416 |   42320   130803 |   17068   13082  1118557    85.5 |  0.817 % |
c |     41642 |   42320   130803 |   18775   13308  1129179    84.8 |  0.817 % |
c |     41979 |   42320   130803 |   20652   13645  1149623    84.3 |  0.817 % |
c |     42486 |   42320   130803 |   22717   14152  1173763    82.9 |  0.817 % |
c |     43245 |   42320   130803 |   24989   14911  1221475    81.9 |  0.817 % |
c |     44384 |   42320   130803 |   27488   16050  1286940    80.2 |  0.817 % |
c |     46093 |   42320   130803 |   30237   17759  1430670    80.6 |  0.817 % |
c |     48656 |   42320   130803 |   33261   20322  1598315    78.6 |  0.817 % |
c |     52500 |   42320   130803 |   36587   24166  1930446    79.9 |  0.817 % |
c |     58268 |   42320   130803 |   40246   29934  2285715    76.4 |  0.817 % |
c |     66922 |   42320   130803 |   44270   38588  3113757    80.7 |  0.817 % |
c |     79899 |   42320   130803 |   48697   16361  2362967   144.4 |  0.817 % |
c |     99360 |   42320   130803 |   53567   35822  5244635   146.4 |  0.817 % |
c |    128552 |   42320   130803 |   58924   23711  3095697   130.6 |  0.817 % |
c |    172341 |   42320   130803 |   64816   19113  1980374   103.6 |  0.817 % |
c |    238028 |   42320   130803 |   71298   32956  2841949    86.2 |  0.817 % |
c ==============================================================================
c [1mFound solution: 52[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    256317 |   42113   130312 |   14037   43501  3635709    83.6 |  0.817 % |
c |    256418 |   42113   130312 |   15440   14391  1134454    78.8 |  1.341 % |
c |    256570 |   42113   130312 |   16984   14543  1144573    78.7 |  1.341 % |
c |    256795 |   42113   130312 |   18683   14768  1155199    78.2 |  1.341 % |
c |    257132 |   42113   130312 |   20551   15105  1168575    77.4 |  1.341 % |
c |    257638 |   42113   130312 |   22606   15611  1202306    77.0 |  1.341 % |
c |    258397 |   42113   130312 |   24867   16370  1247447    76.2 |  1.341 % |
c |    259538 |   42113   130312 |   27354   17511  1340342    76.5 |  1.341 % |
c |    261246 |   42113   130312 |   30089   19219  1556816    81.0 |  1.341 % |
c |    263809 |   42113   130312 |   33098   21782  1674246    76.9 |  1.341 % |
c |    267654 |   42113   130312 |   36408   25627  2061057    80.4 |  1.341 % |
c |    273420 |   42113   130312 |   40049   31393  2429661    77.4 |  1.341 % |
c |    282070 |   42113   130312 |   44054   40043  3047738    76.1 |  1.341 % |
c |    295044 |   42113   130312 |   48459   20186  1894183    93.8 |  1.341 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 x23 x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 x55 -x56 -x57 x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 x227 x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 x480 x481 -x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 x511 x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 x531 -x532 x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 x622 -x623 -x624 -x625 -x626 x627 -x628 x629 -x630 -x631 -x632 -x633 x634 -x635 -x636 x637 x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 x646 -x647 -x648 -x649 -x650 -x651 -x652 x653 x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 x675 x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 x695 -x696 -x697 -x698 -x699 -x700 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.97 0.91 2/54 2409
Raw data (stat): 2409 (runsolver) R 2408 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480746317 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 2715 0 0 0 990 6 0 0 25 0 1 0 480746317 13684736 2683 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3341 2683 603 41 0 3300 0
vsize: 13364
[startup+20.0001 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 3558 0 0 0 1986 9 0 0 25 0 1 0 480746317 17162240 3526 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4190 3526 603 41 0 4149 0
vsize: 16760
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 4175 0 0 0 2983 12 0 0 25 0 1 0 480746317 19718144 4143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4814 4143 603 41 0 4773 0
vsize: 19256
[startup+40.0007 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 4494 0 0 0 3981 13 0 0 25 0 1 0 480746317 21028864 4462 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5134 4462 603 41 0 5093 0
vsize: 20536
[startup+50.0011 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 4678 0 0 0 4981 14 0 0 25 0 1 0 480746317 21811200 4646 4294967295 134512640 134672761 3221224560 3221223760 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5325 4646 603 41 0 5284 0
vsize: 21300
[startup+60.0011 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 4678 0 0 0 5981 14 0 0 25 0 1 0 480746317 21811200 4646 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5325 4646 603 41 0 5284 0
vsize: 21300
[startup+70.0008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 4678 0 0 0 6981 14 0 0 25 0 1 0 480746317 21811200 4646 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5325 4646 603 41 0 5284 0
vsize: 21300
[startup+80.0012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 4823 0 0 0 7980 15 0 0 25 0 1 0 480746317 22347776 4791 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5456 4791 603 41 0 5415 0
vsize: 21824
[startup+90.0012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 5157 0 0 0 8979 16 0 0 25 0 1 0 480746317 23687168 5125 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5783 5125 603 41 0 5742 0
vsize: 23132
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 5479 0 0 0 9978 17 0 0 25 0 1 0 480746317 25022464 5447 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6109 5447 603 41 0 6068 0
vsize: 24436
[startup+110.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 5764 0 0 0 10977 18 0 0 25 0 1 0 480746317 26234880 5732 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6405 5732 603 41 0 6364 0
vsize: 25620
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 5969 0 0 0 11977 19 0 0 25 0 1 0 480746317 27037696 5937 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6601 5937 603 41 0 6560 0
vsize: 26404
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 5969 0 0 0 12977 19 0 0 25 0 1 0 480746317 27037696 5937 4294967295 134512640 134672761 3221224560 3221223760 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6601 5937 603 41 0 6560 0
vsize: 26404
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 5969 0 0 0 13977 19 0 0 25 0 1 0 480746317 27037696 5937 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6601 5937 603 41 0 6560 0
vsize: 26404
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 5969 0 0 0 14978 19 0 0 25 0 1 0 480746317 27037696 5937 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6601 5937 603 41 0 6560 0
vsize: 26404
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 5969 0 0 0 15978 19 0 0 25 0 1 0 480746317 27037696 5937 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6601 5937 603 41 0 6560 0
vsize: 26404
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 5969 0 0 0 16978 19 0 0 25 0 1 0 480746317 27037696 5937 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6601 5937 603 41 0 6560 0
vsize: 26404
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 6004 0 0 0 17978 19 0 0 25 0 1 0 480746317 27299840 5972 4294967295 134512640 134672761 3221224560 3221223696 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6665 5972 603 41 0 6624 0
vsize: 26660
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 6088 0 0 0 18978 19 0 0 25 0 1 0 480746317 27570176 6056 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6731 6056 603 41 0 6690 0
vsize: 26924
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 6580 0 0 0 19977 21 0 0 25 0 1 0 480746317 29577216 6548 4294967295 134512640 134672761 3221224560 3221223760 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7221 6548 603 41 0 7180 0
vsize: 28884
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 7038 0 0 0 20975 23 0 0 25 0 1 0 480746317 31453184 7006 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7679 7006 603 41 0 7638 0
vsize: 30716
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 7527 0 0 0 21973 24 0 0 25 0 1 0 480746317 33460224 7495 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8169 7495 603 41 0 8128 0
vsize: 32676
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 7712 0 0 0 22973 25 0 0 25 0 1 0 480746317 34254848 7680 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8363 7680 603 41 0 8322 0
vsize: 33452
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 7712 0 0 0 23973 25 0 0 25 0 1 0 480746317 34254848 7680 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8363 7680 603 41 0 8322 0
vsize: 33452
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 7712 0 0 0 24973 25 0 0 25 0 1 0 480746317 34254848 7680 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8363 7680 603 41 0 8322 0
vsize: 33452
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 7712 0 0 0 25973 25 0 0 25 0 1 0 480746317 34254848 7680 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8363 7680 603 41 0 8322 0
vsize: 33452
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 7712 0 0 0 26974 25 0 0 25 0 1 0 480746317 34254848 7680 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8363 7680 603 41 0 8322 0
vsize: 33452
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 7712 0 0 0 27974 25 0 0 25 0 1 0 480746317 34254848 7680 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8363 7680 603 41 0 8322 0
vsize: 33452
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 7712 0 0 0 28974 25 0 0 25 0 1 0 480746317 34254848 7680 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8363 7680 603 41 0 8322 0
vsize: 33452
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 7712 0 0 0 29974 25 0 0 25 0 1 0 480746317 34254848 7680 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8363 7680 603 41 0 8322 0
vsize: 33452
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 7712 0 0 0 30974 25 0 0 25 0 1 0 480746317 34254848 7680 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8363 7680 603 41 0 8322 0
vsize: 33452
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 7952 0 0 0 31974 26 0 0 25 0 1 0 480746317 35201024 7920 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8594 7920 603 41 0 8553 0
vsize: 34376
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 8259 0 0 0 32972 27 0 0 25 0 1 0 480746317 36536320 8227 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8920 8227 603 41 0 8879 0
vsize: 35680
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 8566 0 0 0 33971 29 0 0 25 0 1 0 480746317 37744640 8534 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9215 8534 603 41 0 9174 0
vsize: 36860
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 8851 0 0 0 34969 30 0 0 25 0 1 0 480746317 38952960 8819 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9510 8819 603 41 0 9469 0
vsize: 38040
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 9175 0 0 0 35969 30 0 0 25 0 1 0 480746317 40304640 9143 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9840 9143 603 41 0 9799 0
vsize: 39360
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 9448 0 0 0 36967 32 0 0 25 0 1 0 480746317 41369600 9416 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10100 9416 603 41 0 10059 0
vsize: 40400
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 9727 0 0 0 37967 33 0 0 25 0 1 0 480746317 42577920 9695 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10395 9695 603 41 0 10354 0
vsize: 41580
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10062 0 0 0 38966 34 0 0 25 0 1 0 480746317 43913216 10030 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10721 10030 603 41 0 10680 0
vsize: 42884
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10357 0 0 0 39965 35 0 0 25 0 1 0 480746317 45117440 10325 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11015 10325 603 41 0 10974 0
vsize: 44060
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10610 0 0 0 40965 36 0 0 25 0 1 0 480746317 46084096 10578 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11251 10578 603 41 0 11210 0
vsize: 45004
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10897 0 0 0 41964 37 0 0 25 0 1 0 480746317 47296512 10865 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11547 10865 603 41 0 11506 0
vsize: 46188
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10993 0 0 0 42964 37 0 0 25 0 1 0 480746317 47693824 10961 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10961 603 41 0 11603 0
vsize: 46576
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10994 0 0 0 43964 37 0 0 25 0 1 0 480746317 47693824 10962 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10962 603 41 0 11603 0
vsize: 46576
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10994 0 0 0 44964 37 0 0 25 0 1 0 480746317 47693824 10962 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10962 603 41 0 11603 0
vsize: 46576
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 45964 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 46964 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 47964 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 48964 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 49965 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223728 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 50965 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 51965 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 52965 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 53965 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223664 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 54966 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223664 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 55966 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 56966 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 57966 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 58966 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10995 0 0 0 59966 37 0 0 25 0 1 0 480746317 47693824 10963 4294967295 134512640 134672761 3221224560 3221223744 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10963 603 41 0 11603 0
vsize: 46576
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10996 0 0 0 60967 37 0 0 25 0 1 0 480746317 47693824 10964 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10964 603 41 0 11603 0
vsize: 46576
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 10998 0 0 0 61967 37 0 0 25 0 1 0 480746317 47693824 10966 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10966 603 41 0 11603 0
vsize: 46576
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11000 0 0 0 62967 37 0 0 25 0 1 0 480746317 47693824 10968 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10968 603 41 0 11603 0
vsize: 46576
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 63967 37 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 64967 37 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223760 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 65967 37 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 66967 37 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 67967 37 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 68968 37 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 69968 37 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 70968 37 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2409
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 71968 37 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+730.012 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 2462
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 72968 37 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+740.012 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 2462
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 73968 38 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+750.013 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 2462
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 74968 38 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+760.013 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2462
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 75968 38 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+770.013 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2462
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 76967 39 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+780.014 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2462
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 77967 39 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+790.013 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2462
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 78967 39 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+800.014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11001 0 0 0 79967 40 0 0 25 0 1 0 480746317 47693824 10969 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10969 603 41 0 11603 0
vsize: 46576
[startup+810.015 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11003 0 0 0 80967 40 0 0 25 0 1 0 480746317 47693824 10971 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10971 603 41 0 11603 0
vsize: 46576
[startup+820.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11005 0 0 0 81967 41 0 0 25 0 1 0 480746317 47693824 10973 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10973 603 41 0 11603 0
vsize: 46576
[startup+830.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 82967 41 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+840.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 83967 41 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+850.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 84966 42 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+860.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 85966 42 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+870.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 86966 42 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+880.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 87966 43 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223760 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+890.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 88966 43 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+900.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 89966 43 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223744 134558890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+910.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 90966 43 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+920.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 91966 44 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+930.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 92965 44 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+940.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 93966 44 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+950.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 94965 45 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+960.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 95965 45 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+970.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 96965 45 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+980.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 97965 46 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+990.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 98965 46 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 99965 46 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 100965 47 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 101964 47 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223696 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 102964 47 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 103964 47 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 104964 48 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 105964 48 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 106963 49 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 107963 50 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2464
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 108963 50 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2466
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 109962 50 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2466
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 110962 51 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2466
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 111962 51 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223744 134558834 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2466
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 112962 51 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2466
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 113962 52 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2466
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 114962 52 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2466
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 115962 52 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2466
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 116962 53 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2466
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 117961 53 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2466
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 118961 53 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2466
Raw data (stat): 2409 (minisat+) R 2408 28546 28545 0 -1 0 11007 0 0 0 119961 54 0 0 25 0 1 0 480746317 47955968 10975 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11708 10975 603 41 0 11667 0
vsize: 46832
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 2466
Raw data (stat): 2409 (minisat+) Z 2408 28546 28545 0 -1 12 11010 0 0 0 119961 56 0 0 25 0 1 0 480746317 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.05
CPU time (s): 1200.18
CPU user time (s): 1199.62
CPU system time (s): 0.564914
CPU usage (%): 100.011
Max. virtual memory (Kb): 46832
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####