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/een/normalized-seymour.opb
MD5SUM	23a177449585151350479e80b33e6416
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	353
Optimality of the best value was proved	NO
Number of terms in the objective function	1372
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	1372
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1372
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04984
Number of variables	1255
Total number of constraints	4827
Number of constraints which are clauses	4827
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	19
Trace number 6930

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        827376 kB
Buffers:         41488 kB
Cached:         141500 kB
SwapCached:          0 kB
Active:         112244 kB
Inactive:        73852 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        827124 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:               8 kB
Writeback:           0 kB
Mapped:           7204 kB
Slab:            15388 kB
Committed_AS:    92812 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 20:50:08 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 5003 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4827 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    4827    33432 |    1448       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |    4827    33432 |    1930       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.270958 s)
c ==============================================================================
c [1mFound solution: 349[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:76410     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   98923   253123 |   29676       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/63340          
c   -- var.elim.:  2000/63340          
c   -- var.elim.:  3000/63340          
c   -- var.elim.:  4000/63340          
c   -- var.elim.:  5000/63340          
c   -- var.elim.:  6000/63340          
c   -- var.elim.:  7000/63340          
c   -- var.elim.:  8000/63340          
c   -- var.elim.:  9000/63340          
c   -- var.elim.:  10000/63340          
c   -- var.elim.:  11000/63340          
c   -- var.elim.:  12000/63340          
c   -- var.elim.:  13000/63340          
c   -- var.elim.:  14000/63340          
c   -- var.elim.:  15000/63340          
c   -- var.elim.:  16000/63340          
c   -- var.elim.:  17000/63340          
c   -- var.elim.:  18000/63340          
c   -- var.elim.:  19000/63340          
c   -- var.elim.:  20000/63340          
c   -- var.elim.:  21000/63340          
c   -- var.elim.:  22000/63340          
c   -- var.elim.:  23000/63340          
c   -- var.elim.:  24000/63340          
c   -- var.elim.:  25000/63340          
c   -- var.elim.:  26000/63340          
c   -- var.elim.:  27000/63340          
c   -- var.elim.:  28000/63340          
c   -- var.elim.:  29000/63340          
c   -- var.elim.:  30000/63340          
c   -- var.elim.:  31000/63340          
c   -- var.elim.:  32000/63340          
c   -- var.elim.:  33000/63340          
c   -- var.elim.:  34000/63340          
c   -- var.elim.:  35000/63340          
c   -- var.elim.:  36000/63340          
c   -- var.elim.:  37000/63340          
c   -- var.elim.:  38000/63340          
c   -- var.elim.:  39000/63340          
c   -- var.elim.:  40000/63340          
c   -- var.elim.:  41000/63340          
c   -- var.elim.:  42000/63340          
c   -- var.elim.:  43000/63340          
c   -- var.elim.:  44000/63340          
c   -- var.elim.:  45000/63340          
c   -- var.elim.:  46000/63340          
c   -- var.elim.:  47000/63340          
c   -- var.elim.:  48000/63340          
c   -- var.elim.:  49000/63340          
c   -- var.elim.:  50000/63340          
c   -- var.elim.:  51000/63340          
c   -- var.elim.:  52000/63340          
c   -- var.elim.:  53000/63340          
c   -- var.elim.:  54000/63340          
c   -- var.elim.:  55000/63340          
c   -- var.elim.:  56000/63340          
c   -- var.elim.:  57000/63340          
c   -- var.elim.:  58000/63340          
c   -- var.elim.:  59000/63340          
c   -- var.elim.:  60000/63340          
c   -- var.elim.:  61000/63340          
c   -- var.elim.:  62000/63340          
c   -- var.elim.:  63000/63340          
c   -- var.elim.:  63340/63340          
c   -- var.elim.:  1000/31501          
c   -- var.elim.:  2000/31501          
c   -- var.elim.:  3000/31501          
c   -- var.elim.:  4000/31501          
c   -- var.elim.:  5000/31501          
c   -- var.elim.:  6000/31501          
c   -- var.elim.:  7000/31501          
c   -- var.elim.:  8000/31501          
c   -- var.elim.:  9000/31501          
c   -- var.elim.:  10000/31501          
c   -- var.elim.:  11000/31501          
c   -- var.elim.:  12000/31501          
c   -- var.elim.:  13000/31501          
c   -- var.elim.:  14000/31501          
c   -- var.elim.:  15000/31501          
c   -- var.elim.:  16000/31501          
c   -- var.elim.:  17000/31501          
c   -- var.elim.:  18000/31501          
c   -- var.elim.:  19000/31501          
c   -- var.elim.:  20000/31501          
c   -- var.elim.:  21000/31501          
c   -- var.elim.:  22000/31501          
c   -- var.elim.:  23000/31501          
c   -- var.elim.:  24000/31501          
c   -- var.elim.:  25000/31501          
c   -- var.elim.:  26000/31501          
c   -- var.elim.:  27000/31501          
c   -- var.elim.:  28000/31501          
c   -- var.elim.:  29000/31501          
c   -- var.elim.:  30000/31501          
c   -- var.elim.:  31000/31501          
c   -- var.elim.:  31501/31501          
c   -- var.elim.:  135/135          
c   -- subsuming                       
c   -- var.elim.:  1000/27399          
c   -- var.elim.:  2000/27399          
c   -- var.elim.:  3000/27399          
c   -- var.elim.:  4000/27399          
c   -- var.elim.:  5000/27399          
c   -- var.elim.:  6000/27399          
c   -- var.elim.:  7000/27399          
c   -- var.elim.:  8000/27399          
c   -- var.elim.:  9000/27399          
c   -- var.elim.:  10000/27399          
c   -- var.elim.:  11000/27399          
c   -- var.elim.:  12000/27399          
c   -- var.elim.:  13000/27399          
c   -- var.elim.:  14000/27399          
c   -- var.elim.:  15000/27399          
c   -- var.elim.:  16000/27399          
c   -- var.elim.:  17000/27399          
c   -- var.elim.:  18000/27399          
c   -- var.elim.:  19000/27399          
c   -- var.elim.:  20000/27399          
c   -- var.elim.:  21000/27399          
c   -- var.elim.:  22000/27399          
c   -- var.elim.:  23000/27399          
c   -- var.elim.:  24000/27399          
c   -- var.elim.:  25000/27399          
c   -- var.elim.:  26000/27399          
c   -- var.elim.:  27000/27399          
c   -- var.elim.:  27399/27399          
c   -- var.elim.:  155/155          
c |         0 |   65988   616374 |      --       0       --      -- |     --   | -32935/363252
c |         0 |   65988   616374 |   26395       0        0     nan |  0.000 % |
c |       100 |   65305   609235 |   28734      82     1504    18.3 |  3.430 % |
c |       250 |   64592   601845 |   31262     216     4331    20.1 |  4.551 % |
c |       475 |   63673   592324 |   33899     411     9694    23.6 |  5.989 % |
c |       813 |   62662   581533 |   36697     700    17633    25.2 |  7.567 % |
c |      1320 |   61902   573600 |   39877    1173    39145    33.4 |  8.761 % |
c |      2079 |   61517   569920 |   43592    1898    66607    35.1 |  9.365 % |
c |      3218 |   61444   569268 |   47894    3030   122098    40.3 |  9.479 % |
c |      4926 |   61311   567836 |   52570    4728   228055    48.2 |  9.682 % |
c |      7488 |   60948   563896 |   57484    7246   351996    48.6 | 10.209 % |
c |     11334 |   60762   561628 |   63040   11081   671828    60.6 | 10.454 % |
c |     17100 |   60514   558671 |   69061   16813  1691517   100.6 | 10.781 % |
c |     25751 |   60330   556593 |   75736   25434  2693402   105.9 | 11.016 % |
c |     38725 |   60278   555785 |   83238   38381  4929337   128.4 | 11.089 % |
c |     58186 |   60183   554656 |   91417   57838  7189961   124.3 | 11.222 % |
c |     87379 |   60049   553365 |  100335   87000 10950351   125.9 | 11.397 % |
c |    131169 |   60000   552693 |  110279   36626  8105741   221.3 | 11.467 % |
c |    196854 |   60000   552693 |  121307  102311 20312412   198.5 | 11.467 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x0 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 x739 x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 x765 -x766 x767 x768 -x769 -x770 -x771 -x772 x773 -x774 x775 x776 -x777 x778 x779 x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 x808 x809 -x810 -x811 -x812 -x813 x814 -x815 x816 -x817 x818 -x819 -x820 -x821 -x822 -x823 -x824 x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 x837 -x838 x839 -x840 x841 -x842 -x843 -x844 x845 x846 -x847 -x848 -x849 -x850 x851 x852 x853 -x854 -x855 -x856 -x857 -x858 x859 -x860 -x861 -x862 -x863 -x864 x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 x875 -x876 -x877 x878 x879 -x880 x881 -x882 -x883 -x884 x885 x886 -x887 x888 -x889 x890 -x891 x892 -x893 -x894 -x895 x896 x897 x898 -x899 -x900 x901 x902 -x903 -x904 -x905 x906 -x907 -x908 -x909 -x910 -x911 x912 x913 -x914 x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 x923 x924 x925 -x926 x927 -x928 -x929 -x930 x931 -x932 -x933 -x934 -x935 -x936 -x937 x938 -x939 -x940 x941 -x942 -x943 x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 x964 -x965 -x966 x967 -x968 -x969 x970 x971 x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 x1007 -x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 x1076 -x1077 x1078 -x1079 x1080 -x1081 -x1082 x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 x1104 -x1105 -x1106 x1107 x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 x1116 -x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 x1145 -x1146 -x1147 -x1148 x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 x1161 -x1162 x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 x1183 x1184 -x1185 -x1186 x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 x1227 -x1228 x1229 -x1230 -x1231 -x1232 x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 x1244 -x1245 -x1246 -x1247 x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1#### 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.00 0.00 0.00 2/56 26390
Raw data (stat): 26390 (runsolver) R 26389 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 372407057 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.0008 s]
Raw data (loadavg): 0.15 0.03 0.01 2/56 26390
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9466 0 0 0 960 39 0 0 25 0 1 0 372407057 40992768 9205 4294967295 134512640 134672761 3221224576 3221223024 134643987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10008 9205 603 41 0 9967 0
vsize: 40032
[startup+20.0036 s]
Raw data (loadavg): 0.28 0.06 0.02 2/56 26390
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9471 0 0 0 1960 39 0 0 25 0 1 0 372407057 40992768 9210 4294967295 134512640 134672761 3221224576 3221223024 134644032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10008 9210 603 41 0 9967 0
vsize: 40032
[startup+30.0044 s]
Raw data (loadavg): 0.39 0.09 0.03 2/56 26390
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9471 0 0 0 2960 39 0 0 25 0 1 0 372407057 40992768 9210 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10008 9210 603 41 0 9967 0
vsize: 40032
[startup+40.0041 s]
Raw data (loadavg): 0.49 0.12 0.04 2/56 26390
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9503 0 0 0 3960 39 0 0 25 0 1 0 372407057 41254912 9242 4294967295 134512640 134672761 3221224576 3221223024 134643577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10072 9242 603 41 0 10031 0
vsize: 40288
[startup+50.0039 s]
Raw data (loadavg): 0.56 0.15 0.05 2/56 26390
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9504 0 0 0 4960 39 0 0 25 0 1 0 372407057 41254912 9243 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10072 9243 603 41 0 10031 0
vsize: 40288
[startup+60.0041 s]
Raw data (loadavg): 0.63 0.18 0.06 2/56 26390
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9504 0 0 0 5960 40 0 0 25 0 1 0 372407057 41254912 9243 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10072 9243 603 41 0 10031 0
vsize: 40288
[startup+70.0044 s]
Raw data (loadavg): 0.69 0.21 0.07 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9504 0 0 0 6960 40 0 0 25 0 1 0 372407057 41254912 9243 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10072 9243 603 41 0 10031 0
vsize: 40288
[startup+80.0052 s]
Raw data (loadavg): 0.73 0.23 0.08 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9504 0 0 0 7960 40 0 0 25 0 1 0 372407057 41254912 9243 4294967295 134512640 134672761 3221224576 3221223004 134542656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10072 9243 603 41 0 10031 0
vsize: 40288
[startup+90.0049 s]
Raw data (loadavg): 0.77 0.26 0.09 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9609 0 0 0 8959 42 0 0 25 0 1 0 372407057 41463808 9286 4294967295 134512640 134672761 3221224576 3221223024 134644016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9286 603 41 0 10082 0
vsize: 40492
[startup+100.005 s]
Raw data (loadavg): 0.81 0.28 0.10 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9609 0 0 0 9959 42 0 0 25 0 1 0 372407057 41463808 9286 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9286 603 41 0 10082 0
vsize: 40492
[startup+110.005 s]
Raw data (loadavg): 0.84 0.30 0.11 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9609 0 0 0 10959 42 0 0 25 0 1 0 372407057 41463808 9286 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9286 603 41 0 10082 0
vsize: 40492
[startup+120.006 s]
Raw data (loadavg): 0.86 0.33 0.12 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9612 0 0 0 11959 42 0 0 25 0 1 0 372407057 41463808 9289 4294967295 134512640 134672761 3221224576 3221223024 134643636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9289 603 41 0 10082 0
vsize: 40492
[startup+130.006 s]
Raw data (loadavg): 0.88 0.35 0.12 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9612 0 0 0 12959 42 0 0 25 0 1 0 372407057 41463808 9289 4294967295 134512640 134672761 3221224576 3221223024 134643961 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9289 603 41 0 10082 0
vsize: 40492
[startup+140.007 s]
Raw data (loadavg): 0.90 0.37 0.13 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9612 0 0 0 13959 42 0 0 25 0 1 0 372407057 41463808 9289 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9289 603 41 0 10082 0
vsize: 40492
[startup+150.007 s]
Raw data (loadavg): 0.92 0.39 0.14 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9612 0 0 0 14959 42 0 0 25 0 1 0 372407057 41463808 9289 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9289 603 41 0 10082 0
vsize: 40492
[startup+160.006 s]
Raw data (loadavg): 0.93 0.41 0.15 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9616 0 0 0 15959 42 0 0 25 0 1 0 372407057 41463808 9293 4294967295 134512640 134672761 3221224576 3221223024 134643532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9293 603 41 0 10082 0
vsize: 40492
[startup+170.006 s]
Raw data (loadavg): 0.94 0.43 0.16 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9616 0 0 0 16959 43 0 0 25 0 1 0 372407057 41463808 9293 4294967295 134512640 134672761 3221224576 3221223024 134644032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10123 9293 603 41 0 10082 0
vsize: 40492
[startup+180.007 s]
Raw data (loadavg): 0.95 0.45 0.17 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 17959 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221223040 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+190.008 s]
Raw data (loadavg): 0.95 0.46 0.18 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 18959 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221222976 134604645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+200.007 s]
Raw data (loadavg): 0.96 0.48 0.19 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 19959 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221222800 134621186 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+210.008 s]
Raw data (loadavg): 0.97 0.50 0.19 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 20959 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221223040 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+220.009 s]
Raw data (loadavg): 0.97 0.51 0.20 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 21959 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221222976 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+230.01 s]
Raw data (loadavg): 0.98 0.53 0.21 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 22959 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221222704 134566560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+240.01 s]
Raw data (loadavg): 0.98 0.54 0.22 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 23960 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221223072 134607032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+250.01 s]
Raw data (loadavg): 0.98 0.56 0.22 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 24960 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221222976 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+260.01 s]
Raw data (loadavg): 0.98 0.57 0.23 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 25960 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221223056 134606994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+270.01 s]
Raw data (loadavg): 0.99 0.59 0.24 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 26960 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221223040 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+280.01 s]
Raw data (loadavg): 0.99 0.60 0.25 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 27960 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221223072 134606971 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+290.01 s]
Raw data (loadavg): 0.99 0.61 0.26 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 28960 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221222912 134603565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+300.01 s]
Raw data (loadavg): 0.99 0.62 0.26 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 29961 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221223040 134644291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+310.011 s]
Raw data (loadavg): 0.99 0.64 0.27 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 30961 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221223120 134621095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+320.01 s]
Raw data (loadavg): 0.99 0.65 0.28 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 31961 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221223120 134621062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+330.01 s]
Raw data (loadavg): 0.99 0.66 0.29 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 9927 0 0 0 32961 43 0 0 25 0 1 0 372407057 42483712 9510 4294967295 134512640 134672761 3221224576 3221223120 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10372 9510 603 41 0 10331 0
vsize: 41488
[startup+340.01 s]
Raw data (loadavg): 0.99 0.67 0.29 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 10016 0 0 0 33961 43 0 0 25 0 1 0 372407057 41308160 9253 4294967295 134512640 134672761 3221224576 3221223024 134644016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10085 9253 603 41 0 10044 0
vsize: 40340
[startup+350.01 s]
Raw data (loadavg): 0.99 0.68 0.30 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 10016 0 0 0 34961 43 0 0 25 0 1 0 372407057 41308160 9253 4294967295 134512640 134672761 3221224576 3221223024 134643996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10085 9253 603 41 0 10044 0
vsize: 40340
[startup+360.01 s]
Raw data (loadavg): 0.99 0.69 0.31 2/56 26392
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 10016 0 0 0 35961 43 0 0 25 0 1 0 372407057 41308160 9253 4294967295 134512640 134672761 3221224576 3221223024 134643556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10085 9253 603 41 0 10044 0
vsize: 40340
[startup+370.009 s]
Raw data (loadavg): 0.99 0.70 0.31 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 10016 0 0 0 36961 43 0 0 25 0 1 0 372407057 41308160 9253 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10085 9253 603 41 0 10044 0
vsize: 40340
[startup+380.01 s]
Raw data (loadavg): 0.99 0.71 0.32 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 10016 0 0 0 37962 43 0 0 25 0 1 0 372407057 41308160 9253 4294967295 134512640 134672761 3221224576 3221223024 134644008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10085 9253 603 41 0 10044 0
vsize: 40340
[startup+390.011 s]
Raw data (loadavg): 0.99 0.72 0.33 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 10016 0 0 0 38962 43 0 0 25 0 1 0 372407057 41308160 9253 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10085 9253 603 41 0 10044 0
vsize: 40340
[startup+400.011 s]
Raw data (loadavg): 0.99 0.73 0.33 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 10039 0 0 0 39962 43 0 0 25 0 1 0 372407057 41443328 9276 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10118 9276 603 41 0 10077 0
vsize: 40472
[startup+410.01 s]
Raw data (loadavg): 0.99 0.74 0.34 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 10041 0 0 0 40962 43 0 0 25 0 1 0 372407057 41443328 9278 4294967295 134512640 134672761 3221224576 3221223744 134564457 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10118 9278 603 41 0 10077 0
vsize: 40472
[startup+420.011 s]
Raw data (loadavg): 0.99 0.74 0.35 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 10060 0 0 0 41962 44 0 0 25 0 1 0 372407057 41443328 9297 4294967295 134512640 134672761 3221224576 3221223520 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10118 9297 603 41 0 10077 0
vsize: 40472
[startup+430.011 s]
Raw data (loadavg): 0.99 0.75 0.35 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 10224 0 0 0 42962 44 0 0 25 0 1 0 372407057 42094592 9461 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10277 9461 603 41 0 10236 0
vsize: 41108
[startup+440.011 s]
Raw data (loadavg): 0.99 0.76 0.36 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 10628 0 0 0 43962 45 0 0 25 0 1 0 372407057 43810816 9865 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10696 9865 603 41 0 10655 0
vsize: 42784
[startup+450.011 s]
Raw data (loadavg): 0.99 0.77 0.37 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 11684 0 0 0 44958 48 0 0 25 0 1 0 372407057 48226304 10921 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11774 10921 603 41 0 11733 0
vsize: 47096
[startup+460.012 s]
Raw data (loadavg): 0.99 0.77 0.37 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 12266 0 0 0 45957 49 0 0 25 0 1 0 372407057 50475008 11503 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12323 11503 603 41 0 12282 0
vsize: 49292
[startup+470.011 s]
Raw data (loadavg): 0.99 0.78 0.38 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 13099 0 0 0 46954 52 0 0 25 0 1 0 372407057 53907456 12336 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13161 12336 603 41 0 13120 0
vsize: 52644
[startup+480.012 s]
Raw data (loadavg): 0.99 0.79 0.38 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 14391 0 0 0 47951 56 0 0 25 0 1 0 372407057 59293696 13628 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14476 13628 603 41 0 14435 0
vsize: 57904
[startup+490.013 s]
Raw data (loadavg): 0.99 0.79 0.39 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 15059 0 0 0 48949 58 0 0 25 0 1 0 372407057 62050304 14296 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15149 14296 603 41 0 15108 0
vsize: 60596
[startup+500.013 s]
Raw data (loadavg): 0.99 0.80 0.40 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 15748 0 0 0 49947 60 0 0 25 0 1 0 372407057 64827392 14985 4294967295 134512640 134672761 3221224576 3221223760 134615698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15827 14985 603 41 0 15786 0
vsize: 63308
[startup+510.014 s]
Raw data (loadavg): 0.99 0.81 0.40 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 16461 0 0 0 50945 62 0 0 25 0 1 0 372407057 67743744 15698 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16539 15698 603 41 0 16498 0
vsize: 66156
[startup+520.014 s]
Raw data (loadavg): 0.99 0.81 0.41 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 17094 0 0 0 51944 64 0 0 25 0 1 0 372407057 70258688 16331 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17153 16331 603 41 0 17112 0
vsize: 68612
[startup+530.015 s]
Raw data (loadavg): 0.99 0.82 0.41 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 17606 0 0 0 52942 65 0 0 25 0 1 0 372407057 72380416 16843 4294967295 134512640 134672761 3221224576 3221223760 134615679 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17671 16843 603 41 0 17630 0
vsize: 70684
[startup+540.015 s]
Raw data (loadavg): 0.99 0.82 0.42 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 18491 0 0 0 53939 68 0 0 25 0 1 0 372407057 75931648 17728 4294967295 134512640 134672761 3221224576 3221223760 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18538 17728 603 41 0 18497 0
vsize: 74152
[startup+550.014 s]
Raw data (loadavg): 0.99 0.83 0.43 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 19174 0 0 0 54937 71 0 0 25 0 1 0 372407057 78979072 18411 4294967295 134512640 134672761 3221224576 3221223712 134614710 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19282 18411 603 41 0 19241 0
vsize: 77128
[startup+560.015 s]
Raw data (loadavg): 0.99 0.83 0.43 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 19854 0 0 0 55935 73 0 0 25 0 1 0 372407057 81760256 19091 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19961 19091 603 41 0 19920 0
vsize: 79844
[startup+570.015 s]
Raw data (loadavg): 0.99 0.84 0.44 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 20372 0 0 0 56933 75 0 0 25 0 1 0 372407057 83865600 19609 4294967295 134512640 134672761 3221224576 3221223776 134610709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20475 19609 603 41 0 20434 0
vsize: 81900
[startup+580.015 s]
Raw data (loadavg): 0.99 0.84 0.44 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 20913 0 0 0 57932 76 0 0 25 0 1 0 372407057 86110208 20150 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20150 603 41 0 20982 0
vsize: 84092
[startup+590.016 s]
Raw data (loadavg): 0.99 0.85 0.45 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 21576 0 0 0 58931 77 0 0 25 0 1 0 372407057 88752128 20813 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21668 20813 603 41 0 21627 0
vsize: 86672
[startup+600.016 s]
Raw data (loadavg): 0.99 0.85 0.45 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 22068 0 0 0 59929 79 0 0 25 0 1 0 372407057 90857472 21305 4294967295 134512640 134672761 3221224576 3221223616 134612385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22182 21305 603 41 0 22141 0
vsize: 88728
[startup+610.016 s]
Raw data (loadavg): 0.99 0.86 0.46 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 22781 0 0 0 60927 81 0 0 25 0 1 0 372407057 93769728 22018 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22893 22018 603 41 0 22852 0
vsize: 91572
[startup+620.016 s]
Raw data (loadavg): 0.99 0.86 0.46 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 23660 0 0 0 61926 83 0 0 25 0 1 0 372407057 97329152 22897 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23762 22897 603 41 0 23721 0
vsize: 95048
[startup+630.016 s]
Raw data (loadavg): 0.99 0.86 0.47 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 24572 0 0 0 62923 86 0 0 25 0 1 0 372407057 101015552 23809 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24662 23809 603 41 0 24621 0
vsize: 98648
[startup+640.016 s]
Raw data (loadavg): 0.99 0.87 0.47 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 25230 0 0 0 63920 88 0 0 25 0 1 0 372407057 103645184 24467 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25304 24467 603 41 0 25263 0
vsize: 101216
[startup+650.016 s]
Raw data (loadavg): 0.99 0.87 0.48 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 25934 0 0 0 64919 90 0 0 25 0 1 0 372407057 106528768 25171 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26008 25171 603 41 0 25967 0
vsize: 104032
[startup+660.018 s]
Raw data (loadavg): 0.99 0.88 0.48 2/56 26394
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26299 0 0 0 65918 91 0 0 25 0 1 0 372407057 107589632 25397 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25397 603 41 0 26226 0
vsize: 105068
[startup+670.018 s]
Raw data (loadavg): 0.99 0.88 0.49 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26299 0 0 0 66918 91 0 0 25 0 1 0 372407057 107589632 25397 4294967295 134512640 134672761 3221224576 3221223744 134615864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25397 603 41 0 26226 0
vsize: 105068
[startup+680.018 s]
Raw data (loadavg): 0.99 0.88 0.49 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26299 0 0 0 67918 91 0 0 25 0 1 0 372407057 107589632 25397 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25397 603 41 0 26226 0
vsize: 105068
[startup+690.018 s]
Raw data (loadavg): 0.99 0.89 0.50 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26299 0 0 0 68918 92 0 0 25 0 1 0 372407057 107589632 25397 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25397 603 41 0 26226 0
vsize: 105068
[startup+700.018 s]
Raw data (loadavg): 0.99 0.89 0.50 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26299 0 0 0 69918 92 0 0 25 0 1 0 372407057 107589632 25397 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25397 603 41 0 26226 0
vsize: 105068
[startup+710.019 s]
Raw data (loadavg): 0.99 0.89 0.51 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 70918 92 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+720.019 s]
Raw data (loadavg): 0.99 0.90 0.51 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 71918 92 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+730.019 s]
Raw data (loadavg): 0.99 0.90 0.52 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 72918 92 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+740.019 s]
Raw data (loadavg): 0.99 0.90 0.52 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 73918 92 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+750.019 s]
Raw data (loadavg): 0.99 0.90 0.53 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 74918 92 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223712 134614576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+760.02 s]
Raw data (loadavg): 0.99 0.91 0.53 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 75918 92 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+770.02 s]
Raw data (loadavg): 0.99 0.91 0.54 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 76918 93 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+780.02 s]
Raw data (loadavg): 0.99 0.91 0.54 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 77918 93 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+790.02 s]
Raw data (loadavg): 0.99 0.91 0.55 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 78918 93 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+800.02 s]
Raw data (loadavg): 0.99 0.92 0.55 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 79918 93 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+810.021 s]
Raw data (loadavg): 0.99 0.92 0.56 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 80918 93 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+820.022 s]
Raw data (loadavg): 0.99 0.92 0.56 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 81918 93 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+830.021 s]
Raw data (loadavg): 0.99 0.92 0.56 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26300 0 0 0 82918 93 0 0 25 0 1 0 372407057 107589632 25398 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26267 25398 603 41 0 26226 0
vsize: 105068
[startup+840.022 s]
Raw data (loadavg): 0.99 0.92 0.57 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 26603 0 0 0 83918 94 0 0 25 0 1 0 372407057 108912640 25701 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26590 25701 603 41 0 26549 0
vsize: 106360
[startup+850.022 s]
Raw data (loadavg): 0.99 0.93 0.57 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 27039 0 0 0 84917 95 0 0 25 0 1 0 372407057 110637056 26137 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27011 26137 603 41 0 26970 0
vsize: 108044
[startup+860.023 s]
Raw data (loadavg): 0.99 0.93 0.58 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 27504 0 0 0 85915 97 0 0 25 0 1 0 372407057 112619520 26602 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27495 26602 603 41 0 27454 0
vsize: 109980
[startup+870.023 s]
Raw data (loadavg): 0.99 0.93 0.58 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 27919 0 0 0 86914 98 0 0 25 0 1 0 372407057 114335744 27017 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27914 27017 603 41 0 27873 0
vsize: 111656
[startup+880.023 s]
Raw data (loadavg): 0.99 0.93 0.58 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 28329 0 0 0 87913 99 0 0 25 0 1 0 372407057 115945472 27427 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28307 27427 603 41 0 28266 0
vsize: 113228
[startup+890.023 s]
Raw data (loadavg): 0.99 0.93 0.59 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 28768 0 0 0 88912 100 0 0 25 0 1 0 372407057 117837824 27866 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28769 27866 603 41 0 28728 0
vsize: 115076
[startup+900.023 s]
Raw data (loadavg): 0.99 0.94 0.59 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 29168 0 0 0 89911 102 0 0 25 0 1 0 372407057 119431168 28266 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29158 28266 603 41 0 29117 0
vsize: 116632
[startup+910.024 s]
Raw data (loadavg): 0.99 0.94 0.59 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 29541 0 0 0 90910 103 0 0 25 0 1 0 372407057 121008128 28639 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29543 28639 603 41 0 29502 0
vsize: 118172
[startup+920.024 s]
Raw data (loadavg): 0.99 0.94 0.60 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 29915 0 0 0 91909 104 0 0 25 0 1 0 372407057 122462208 29013 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29898 29013 603 41 0 29857 0
vsize: 119592
[startup+930.025 s]
Raw data (loadavg): 0.99 0.94 0.60 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 30285 0 0 0 92907 106 0 0 25 0 1 0 372407057 124051456 29383 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30286 29383 603 41 0 30245 0
vsize: 121144
[startup+940.025 s]
Raw data (loadavg): 0.99 0.94 0.61 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 30652 0 0 0 93907 106 0 0 25 0 1 0 372407057 125558784 29750 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30654 29750 603 41 0 30613 0
vsize: 122616
[startup+950.025 s]
Raw data (loadavg): 0.99 0.94 0.61 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 31011 0 0 0 94906 108 0 0 25 0 1 0 372407057 127012864 30109 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31009 30109 603 41 0 30968 0
vsize: 124036
[startup+960.026 s]
Raw data (loadavg): 0.99 0.94 0.61 2/56 26396
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 31386 0 0 0 95905 109 0 0 25 0 1 0 372407057 128598016 30484 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31396 30484 603 41 0 31355 0
vsize: 125584
[startup+970.026 s]
Raw data (loadavg): 0.99 0.95 0.62 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 31757 0 0 0 96904 110 0 0 25 0 1 0 372407057 130088960 30855 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31760 30855 603 41 0 31719 0
vsize: 127040
[startup+980.026 s]
Raw data (loadavg): 0.99 0.95 0.62 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 32082 0 0 0 97903 111 0 0 25 0 1 0 372407057 131407872 31180 4294967295 134512640 134672761 3221224576 3221223720 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32082 31180 603 41 0 32041 0
vsize: 128328
[startup+990.027 s]
Raw data (loadavg): 0.99 0.95 0.63 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 32481 0 0 0 98901 113 0 0 25 0 1 0 372407057 133054464 31579 4294967295 134512640 134672761 3221224576 3221223616 134603506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32484 31579 603 41 0 32443 0
vsize: 129936
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.95 0.63 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 33042 0 0 0 99899 115 0 0 25 0 1 0 372407057 135413760 32140 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33060 32140 603 41 0 33019 0
vsize: 132240
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.95 0.63 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 33507 0 0 0 100897 117 0 0 25 0 1 0 372407057 137252864 32605 4294967295 134512640 134672761 3221224576 3221223616 134612634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33509 32605 603 41 0 33468 0
vsize: 134036
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.95 0.64 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 34121 0 0 0 101896 119 0 0 25 0 1 0 372407057 139755520 33219 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34120 33219 603 41 0 34079 0
vsize: 136480
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.95 0.64 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 34651 0 0 0 102894 121 0 0 25 0 1 0 372407057 142000128 33749 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34668 33749 603 41 0 34627 0
vsize: 138672
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.95 0.64 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35033 0 0 0 103893 122 0 0 25 0 1 0 372407057 143466496 34131 4294967295 134512640 134672761 3221224576 3221223720 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35026 34131 603 41 0 34985 0
vsize: 140104
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.95 0.65 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 104892 123 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223700 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.95 0.65 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 105892 123 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.96 0.65 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 106892 123 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 107892 124 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 108892 124 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 109892 124 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 110892 124 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223712 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 111892 124 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 112892 124 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 113892 124 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.96 0.68 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 114892 124 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134616011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.96 0.68 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 115892 124 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.68 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 116892 125 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.68 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 117892 125 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 118892 125 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/56 26398
Raw data (stat): 26390 (minisat+) R 26389 12452 12451 0 -1 0 35358 0 0 0 119892 125 0 0 25 0 1 0 372407057 144080896 34300 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34300 603 41 0 35135 0
vsize: 140704
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.69 1/56 26398
Raw data (stat): 26390 (minisat+) Z 26389 12452 12451 0 -1 12 35359 0 0 0 119892 133 0 0 25 0 1 0 372407057 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.11
CPU time (s): 1200.26
CPU user time (s): 1198.93
CPU system time (s): 1.3358
CPU usage (%): 100.013
Max. virtual memory (Kb): 140704
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####