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-rot.b.opb
MD5SUM	c5ca4962151c0e84eeae44e16faee495
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	116
Optimality of the best value was proved	NO
Number of terms in the objective function	1452
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	1452
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	1452
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.04884
Number of variables	1451
Total number of constraints	2984
Number of constraints which are clauses	2932
Number of constraints which are cardinality constraints (but not clauses)	52
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	81
Trace number 5812

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        820952 kB
Buffers:         36644 kB
Cached:         139464 kB
SwapCached:         12 kB
Active:          53824 kB
Inactive:       125116 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        820700 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            29112 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:17:43 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4208 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2722 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 |    2716    40318 |     905       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 161[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:79826     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |   96666   259448 |   32222       4      142    35.5 |  0.000 % |
c |       104 |   96090   258250 |   35444      84     1557    18.5 |  0.477 % |
c |       254 |   95807   257647 |   38988     223     3994    17.9 |  0.713 % |
c |       479 |   95697   257415 |   42887     445     9637    21.7 |  0.806 % |
c |       817 |   95554   257106 |   47176     770    17278    22.4 |  0.926 % |
c |      1323 |   95554   257106 |   51893    1276    38725    30.3 |  0.926 % |
c |      2084 |   95513   257017 |   57083    2033    62857    30.9 |  0.962 % |
c |      3223 |   95513   257017 |   62791    3172   121787    38.4 |  0.962 % |
c ==============================================================================
c [1mFound solution: 140[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:31458     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3655 |  121148   316447 |   40382    3604   132593    36.8 |  0.962 % |
c |      3756 |  120463   314913 |   44420    3693   134872    36.5 |  1.630 % |
c |      3906 |  120416   314810 |   48862    3839   137077    35.7 |  1.663 % |
c |      4133 |  120416   314810 |   53748    4066   158564    39.0 |  1.663 % |
c |      4470 |  120416   314810 |   59123    4403   175669    39.9 |  1.663 % |
c |      4976 |  120414   314806 |   65035    4908   195052    39.7 |  1.664 % |
c |      5736 |  120414   314806 |   71539    5668   212200    37.4 |  1.664 % |
c |      6876 |  120414   314806 |   78693    6808   300433    44.1 |  1.664 % |
c |      8584 |  120414   314806 |   86562    8516   405981    47.7 |  1.664 % |
c |     11146 |  120414   314806 |   95218   11078   549351    49.6 |  1.664 % |
c |     14990 |  120414   314806 |  104740   14922   992649    66.5 |  1.664 % |
c |     20756 |  120414   314806 |  115214   20688  1847130    89.3 |  1.664 % |
c ==============================================================================
c [1mFound solution: 131[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 |     23606 |  120487   314994 |   40162   23538  2120803    90.1 |  1.664 % |
c |     23707 |  120487   314994 |   44178   23639  2123997    89.9 |  1.669 % |
c |     23858 |  120487   314994 |   48596   23790  2127418    89.4 |  1.669 % |
c |     24084 |  120487   314994 |   53455   24016  2136250    89.0 |  1.669 % |
c |     24423 |  120487   314994 |   58801   24355  2168936    89.1 |  1.669 % |
c |     24930 |  120487   314994 |   64681   24862  2190927    88.1 |  1.669 % |
c |     25690 |  120487   314994 |   71149   25622  2250351    87.8 |  1.669 % |
c |     26829 |  120487   314994 |   78264   26761  2329467    87.0 |  1.669 % |
c |     28537 |  120487   314994 |   86090   28469  2521126    88.6 |  1.669 % |
c |     31099 |  120487   314994 |   94699   31031  2956575    95.3 |  1.669 % |
c |     34945 |  120487   314994 |  104169   34877  3296144    94.5 |  1.669 % |
c ==============================================================================
c [1mFound solution: 126[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 |     38447 |  120502   315039 |   40167   36284  3058166    84.3 |  1.669 % |
c |     38547 |  120502   315039 |   44183   36384  3064283    84.2 |  1.690 % |
c |     38697 |  120497   315028 |   48602   36523  3070350    84.1 |  1.693 % |
c |     38924 |  120497   315028 |   53462   36750  3082794    83.9 |  1.693 % |
c |     39262 |  120497   315028 |   58808   37088  3096288    83.5 |  1.693 % |
c |     39772 |  120497   315028 |   64689   37598  3116481    82.9 |  1.693 % |
c |     40531 |  120497   315028 |   71158   38357  3151938    82.2 |  1.693 % |
c |     41671 |  120497   315028 |   78274   39497  3236587    81.9 |  1.693 % |
c |     43380 |  120497   315028 |   86101   41206  3384508    82.1 |  1.693 % |
c |     45942 |  120497   315028 |   94711   43768  3629811    82.9 |  1.693 % |
c |     49787 |  120497   315028 |  104182   47613  3960899    83.2 |  1.693 % |
c |     55553 |  120495   315024 |  114601   53375  4623847    86.6 |  1.695 % |
c |     64202 |  120462   314954 |  126061   62023  5477750    88.3 |  1.712 % |
c |     77176 |  120462   314954 |  138667   74997  7279187    97.1 |  1.712 % |
c |     96637 |  120462   314954 |  152534   94458  9795188   103.7 |  1.712 % |
c |    125829 |  120462   314954 |  167787  123650 13430259   108.6 |  1.712 % |
c |    169618 |  120462   314954 |  184566  167439 20225061   120.8 |  1.712 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 -x3 x4 -x5 x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 x34 -x35 -x36 -x37 -x38 x39 -x40 -x41 -x42 x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 x51 -x52 -x53 -x54 -x55 x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 x86 -x87 x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 x121 -x122 -x123 x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 x169 -x170 -x171 -x172 -x173 -x174 -x175 x176 -x177 -x178 -x179 -x180 x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 x192 x193 -x194 -x195 -x196 -x197 -x198 -x199 x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 x226 -x227 -x228 -x229 x230 -x231 -x232 -x233 -x234 x235 -x236 -x237 -x238 x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 x316 x317 -x318 -x319 x320 -x321 -x322 x323 -x324 x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 x339 -x340 -x341 -x342 x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 x395 x396 -x397 -x398 -x399 -x400 -x401 -x402 x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 x462 -x463 -x464 -x465 -x466 -x467 x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 x487 -x488 x489 x490 x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 x528 -x529 -x530 -x531 -x532 -x533 x534 -x535 -x536 -x537 x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 x571 -x572 x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 x596 -x597 -x598 -x599 -x600 -x601 -x602 x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 x728 x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -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 x1259 -x1260 x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 x1282 -x1283 -x1284 x1285 -x1286 -x1287 -x1288 x1289 x1290 -x1291 -x1292 x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 -x1336 -x1337 -x1338 -x1339 -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.93 0.98 0.92 2/54 450
Raw data (stat): 450 (runsolver) R 449 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480805013 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.0009 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 6790 0 0 0 982 16 0 0 25 0 1 0 480805013 32034816 6501 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7821 6501 603 41 0 7780 0
vsize: 31284
[startup+20.0021 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 6959 0 0 0 1981 17 0 0 25 0 1 0 480805013 32706560 6670 4294967295 134512640 134672761 3221224560 3221223744 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7985 6670 603 41 0 7944 0
vsize: 31940
[startup+30.0025 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 7228 0 0 0 2980 19 0 0 25 0 1 0 480805013 33775616 6939 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8246 6939 603 41 0 8205 0
vsize: 32984
[startup+40.0032 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 7390 0 0 0 3979 20 0 0 25 0 1 0 480805013 34451456 7101 4294967295 134512640 134672761 3221224560 3221223744 134558730 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8411 7101 603 41 0 8370 0
vsize: 33644
[startup+50.0044 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 7793 0 0 0 4978 21 0 0 25 0 1 0 480805013 36061184 7504 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8804 7504 603 41 0 8763 0
vsize: 35216
[startup+60.0038 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 8009 0 0 0 5977 22 0 0 25 0 1 0 480805013 37081088 7720 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9053 7720 603 41 0 9012 0
vsize: 36212
[startup+70.0045 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 8270 0 0 0 6975 23 0 0 25 0 1 0 480805013 38154240 7981 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9315 7981 603 41 0 9274 0
vsize: 37260
[startup+80.0048 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 8517 0 0 0 7974 25 0 0 25 0 1 0 480805013 39100416 8228 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9546 8228 603 41 0 9505 0
vsize: 38184
[startup+90.0051 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 8774 0 0 0 8973 26 0 0 25 0 1 0 480805013 40177664 8485 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9809 8485 603 41 0 9768 0
vsize: 39236
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 9056 0 0 0 9971 27 0 0 25 0 1 0 480805013 41107456 8767 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10036 8767 603 41 0 9995 0
vsize: 40144
[startup+110.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 9256 0 0 0 10970 28 0 0 25 0 1 0 480805013 42045440 8967 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10265 8967 603 41 0 10224 0
vsize: 41060
[startup+120.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 9577 0 0 0 11969 30 0 0 25 0 1 0 480805013 43249664 9288 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10559 9288 603 41 0 10518 0
vsize: 42236
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 9903 0 0 0 12968 31 0 0 25 0 1 0 480805013 44601344 9614 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10889 9614 603 41 0 10848 0
vsize: 43556
[startup+140.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 450
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 10217 0 0 0 13967 32 0 0 25 0 1 0 480805013 46063616 9928 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11246 9928 603 41 0 11205 0
vsize: 44984
[startup+150.008 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 503
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 10619 0 0 0 14964 33 0 0 25 0 1 0 480805013 47681536 10330 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11641 10330 603 41 0 11600 0
vsize: 46564
[startup+160.007 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 503
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 10671 0 0 0 15964 34 0 0 25 0 1 0 480805013 47812608 10382 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11673 10382 603 41 0 11632 0
vsize: 46692
[startup+170.007 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 503
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 10672 0 0 0 16964 34 0 0 25 0 1 0 480805013 47812608 10383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11673 10383 603 41 0 11632 0
vsize: 46692
[startup+180.007 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 503
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 10674 0 0 0 17964 34 0 0 25 0 1 0 480805013 47812608 10385 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11673 10385 603 41 0 11632 0
vsize: 46692
[startup+190.008 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 503
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 10792 0 0 0 18964 34 0 0 25 0 1 0 480805013 48353280 10503 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11805 10503 603 41 0 11764 0
vsize: 47220
[startup+200.008 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 503
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 11094 0 0 0 19963 35 0 0 25 0 1 0 480805013 49565696 10805 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12101 10805 603 41 0 12060 0
vsize: 48404
[startup+210.007 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 503
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 11270 0 0 0 20962 36 0 0 25 0 1 0 480805013 50241536 10981 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12266 10981 603 41 0 12225 0
vsize: 49064
[startup+220.008 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 11497 0 0 0 21961 37 0 0 25 0 1 0 480805013 51179520 11208 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12495 11208 603 41 0 12454 0
vsize: 49980
[startup+230.008 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 11820 0 0 0 22960 38 0 0 25 0 1 0 480805013 52523008 11531 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12823 11531 603 41 0 12782 0
vsize: 51292
[startup+240.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 11985 0 0 0 23960 39 0 0 25 0 1 0 480805013 53198848 11696 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12988 11696 603 41 0 12947 0
vsize: 51952
[startup+250.008 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 12198 0 0 0 24959 40 0 0 25 0 1 0 480805013 54001664 11909 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13184 11909 603 41 0 13143 0
vsize: 52736
[startup+260.008 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 12444 0 0 0 25958 41 0 0 25 0 1 0 480805013 55074816 12155 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13446 12155 603 41 0 13405 0
vsize: 53784
[startup+270.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 12701 0 0 0 26958 42 0 0 25 0 1 0 480805013 56016896 12412 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13676 12412 603 41 0 13635 0
vsize: 54704
[startup+280.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 12905 0 0 0 27957 42 0 0 25 0 1 0 480805013 56946688 12616 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13903 12616 603 41 0 13862 0
vsize: 55612
[startup+290.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 13103 0 0 0 28957 43 0 0 25 0 1 0 480805013 57753600 12814 4294967295 134512640 134672761 3221224560 3221223760 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14100 12814 603 41 0 14059 0
vsize: 56400
[startup+300.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 13323 0 0 0 29956 44 0 0 25 0 1 0 480805013 58814464 13034 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14359 13034 603 41 0 14318 0
vsize: 57436
[startup+310.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 13557 0 0 0 30956 44 0 0 25 0 1 0 480805013 59879424 13268 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14619 13268 603 41 0 14578 0
vsize: 58476
[startup+320.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 13810 0 0 0 31954 46 0 0 25 0 1 0 480805013 60813312 13521 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14847 13521 603 41 0 14806 0
vsize: 59388
[startup+330.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 14032 0 0 0 32954 46 0 0 25 0 1 0 480805013 61739008 13743 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15073 13743 603 41 0 15032 0
vsize: 60292
[startup+340.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 14276 0 0 0 33953 47 0 0 25 0 1 0 480805013 62803968 13987 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15333 13987 603 41 0 15292 0
vsize: 61332
[startup+350.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 14558 0 0 0 34953 48 0 0 25 0 1 0 480805013 63860736 14269 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15591 14269 603 41 0 15550 0
vsize: 62364
[startup+360.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 14775 0 0 0 35952 49 0 0 25 0 1 0 480805013 64802816 14486 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15821 14486 603 41 0 15780 0
vsize: 63284
[startup+370.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 14916 0 0 0 36952 49 0 0 25 0 1 0 480805013 65335296 14627 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15951 14627 603 41 0 15910 0
vsize: 63804
[startup+380.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 15079 0 0 0 37952 50 0 0 25 0 1 0 480805013 66002944 14790 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16114 14790 603 41 0 16073 0
vsize: 64456
[startup+390.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 15287 0 0 0 38951 50 0 0 25 0 1 0 480805013 66940928 14998 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16343 14998 603 41 0 16302 0
vsize: 65372
[startup+400.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 15547 0 0 0 39951 51 0 0 25 0 1 0 480805013 67997696 15258 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16601 15258 603 41 0 16560 0
vsize: 66404
[startup+410.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 15733 0 0 0 40950 52 0 0 25 0 1 0 480805013 68669440 15444 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16765 15444 603 41 0 16724 0
vsize: 67060
[startup+420.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 15944 0 0 0 41950 52 0 0 25 0 1 0 480805013 69611520 15655 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16995 15655 603 41 0 16954 0
vsize: 67980
[startup+430.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 16144 0 0 0 42949 53 0 0 25 0 1 0 480805013 70418432 15855 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 15855 603 41 0 17151 0
vsize: 68768
[startup+440.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 16360 0 0 0 43948 54 0 0 25 0 1 0 480805013 71221248 16071 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17388 16071 603 41 0 17347 0
vsize: 69552
[startup+450.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 16551 0 0 0 44948 54 0 0 25 0 1 0 480805013 72032256 16262 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17586 16262 603 41 0 17545 0
vsize: 70344
[startup+460.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 16829 0 0 0 45947 55 0 0 25 0 1 0 480805013 73101312 16540 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17847 16540 603 41 0 17806 0
vsize: 71388
[startup+470.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 17053 0 0 0 46947 56 0 0 25 0 1 0 480805013 74035200 16764 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18075 16764 603 41 0 18034 0
vsize: 72300
[startup+480.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 17240 0 0 0 47946 57 0 0 25 0 1 0 480805013 74833920 16951 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18270 16951 603 41 0 18229 0
vsize: 73080
[startup+490.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 505
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 17452 0 0 0 48946 58 0 0 25 0 1 0 480805013 75640832 17163 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18467 17163 603 41 0 18426 0
vsize: 73868
[startup+500.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 17682 0 0 0 49945 58 0 0 25 0 1 0 480805013 76570624 17393 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18694 17393 603 41 0 18653 0
vsize: 74776
[startup+510.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 17817 0 0 0 50944 59 0 0 25 0 1 0 480805013 77107200 17528 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18825 17528 603 41 0 18784 0
vsize: 75300
[startup+520.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 18001 0 0 0 51944 59 0 0 25 0 1 0 480805013 77905920 17712 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19020 17712 603 41 0 18979 0
vsize: 76080
[startup+530.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 18205 0 0 0 52944 60 0 0 25 0 1 0 480805013 78708736 17916 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19216 17916 603 41 0 19175 0
vsize: 76864
[startup+540.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 18347 0 0 0 53943 60 0 0 25 0 1 0 480805013 79380480 18058 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19380 18058 603 41 0 19339 0
vsize: 77520
[startup+550.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 18534 0 0 0 54943 61 0 0 25 0 1 0 480805013 80048128 18245 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19543 18245 603 41 0 19502 0
vsize: 78172
[startup+560.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 18736 0 0 0 55942 62 0 0 25 0 1 0 480805013 80850944 18447 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19739 18447 603 41 0 19698 0
vsize: 78956
[startup+570.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 18882 0 0 0 56942 63 0 0 25 0 1 0 480805013 81518592 18593 4294967295 134512640 134672761 3221224560 3221223744 134558513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19902 18593 603 41 0 19861 0
vsize: 79608
[startup+580.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 19121 0 0 0 57941 63 0 0 25 0 1 0 480805013 82456576 18832 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20131 18832 603 41 0 20090 0
vsize: 80524
[startup+590.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 19319 0 0 0 58941 64 0 0 25 0 1 0 480805013 83259392 19030 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20327 19030 603 41 0 20286 0
vsize: 81308
[startup+600.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 19475 0 0 0 59941 64 0 0 25 0 1 0 480805013 83927040 19186 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20490 19186 603 41 0 20449 0
vsize: 81960
[startup+610.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 19630 0 0 0 60940 65 0 0 25 0 1 0 480805013 84598784 19341 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20654 19341 603 41 0 20613 0
vsize: 82616
[startup+620.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 19790 0 0 0 61940 65 0 0 25 0 1 0 480805013 85135360 19501 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20785 19501 603 41 0 20744 0
vsize: 83140
[startup+630.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 19992 0 0 0 62940 66 0 0 25 0 1 0 480805013 86061056 19703 4294967295 134512640 134672761 3221224560 3221223744 134559588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21011 19703 603 41 0 20970 0
vsize: 84044
[startup+640.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 20205 0 0 0 63939 67 0 0 25 0 1 0 480805013 86863872 19916 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21207 19916 603 41 0 21166 0
vsize: 84828
[startup+650.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 20404 0 0 0 64938 67 0 0 25 0 1 0 480805013 87658496 20115 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21401 20115 603 41 0 21360 0
vsize: 85604
[startup+660.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 20620 0 0 0 65938 68 0 0 25 0 1 0 480805013 88600576 20331 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20331 603 41 0 21590 0
vsize: 86524
[startup+670.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 20817 0 0 0 66937 69 0 0 25 0 1 0 480805013 89407488 20528 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21828 20528 603 41 0 21787 0
vsize: 87312
[startup+680.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 21081 0 0 0 67936 70 0 0 25 0 1 0 480805013 90476544 20792 4294967295 134512640 134672761 3221224560 3221223744 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22089 20792 603 41 0 22048 0
vsize: 88356
[startup+690.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 21266 0 0 0 68935 71 0 0 25 0 1 0 480805013 91152384 20977 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22254 20977 603 41 0 22213 0
vsize: 89016
[startup+700.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 21458 0 0 0 69935 71 0 0 25 0 1 0 480805013 91955200 21169 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22450 21169 603 41 0 22409 0
vsize: 89800
[startup+710.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 21605 0 0 0 70934 72 0 0 25 0 1 0 480805013 92631040 21316 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22615 21316 603 41 0 22574 0
vsize: 90460
[startup+720.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 21876 0 0 0 71933 73 0 0 25 0 1 0 480805013 93700096 21587 4294967295 134512640 134672761 3221224560 3221223664 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22876 21587 603 41 0 22835 0
vsize: 91504
[startup+730.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 22137 0 0 0 72931 75 0 0 25 0 1 0 480805013 94765056 21848 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23136 21848 603 41 0 23095 0
vsize: 92544
[startup+740.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 22430 0 0 0 73931 76 0 0 25 0 1 0 480805013 96493568 22141 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23558 22141 603 41 0 23517 0
vsize: 94232
[startup+750.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 22593 0 0 0 74930 76 0 0 25 0 1 0 480805013 97165312 22304 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23722 22304 603 41 0 23681 0
vsize: 94888
[startup+760.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 22797 0 0 0 75930 77 0 0 25 0 1 0 480805013 97968128 22508 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23918 22508 603 41 0 23877 0
vsize: 95672
[startup+770.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 23007 0 0 0 76930 77 0 0 25 0 1 0 480805013 98766848 22718 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24113 22718 603 41 0 24072 0
vsize: 96452
[startup+780.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 23223 0 0 0 77929 78 0 0 25 0 1 0 480805013 99696640 22934 4294967295 134512640 134672761 3221224560 3221223664 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24340 22934 603 41 0 24299 0
vsize: 97360
[startup+790.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 23458 0 0 0 78929 79 0 0 25 0 1 0 480805013 100626432 23169 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24567 23169 603 41 0 24526 0
vsize: 98268
[startup+800.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 23620 0 0 0 79928 79 0 0 25 0 1 0 480805013 101294080 23331 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24730 23331 603 41 0 24689 0
vsize: 98920
[startup+810.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 23783 0 0 0 80928 79 0 0 25 0 1 0 480805013 101965824 23494 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24894 23494 603 41 0 24853 0
vsize: 99576
[startup+820.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 23988 0 0 0 81928 80 0 0 25 0 1 0 480805013 102776832 23699 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25092 23699 603 41 0 25051 0
vsize: 100368
[startup+830.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 24190 0 0 0 82928 80 0 0 25 0 1 0 480805013 103579648 23901 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25288 23901 603 41 0 25247 0
vsize: 101152
[startup+840.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 24390 0 0 0 83927 81 0 0 25 0 1 0 480805013 104509440 24101 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25515 24101 603 41 0 25474 0
vsize: 102060
[startup+850.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 24635 0 0 0 84926 82 0 0 25 0 1 0 480805013 105443328 24346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25743 24346 603 41 0 25702 0
vsize: 102972
[startup+860.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 24812 0 0 0 85926 83 0 0 25 0 1 0 480805013 106110976 24523 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25906 24523 603 41 0 25865 0
vsize: 103624
[startup+870.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 25025 0 0 0 86926 83 0 0 25 0 1 0 480805013 107036672 24736 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26132 24736 603 41 0 26091 0
vsize: 104528
[startup+880.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 25193 0 0 0 87925 84 0 0 25 0 1 0 480805013 107708416 24904 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26296 24904 603 41 0 26255 0
vsize: 105184
[startup+890.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 25400 0 0 0 88925 84 0 0 25 0 1 0 480805013 108646400 25111 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26525 25111 603 41 0 26484 0
vsize: 106100
[startup+900.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 25601 0 0 0 89925 85 0 0 25 0 1 0 480805013 109453312 25312 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26722 25312 603 41 0 26681 0
vsize: 106888
[startup+910.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 25807 0 0 0 90924 86 0 0 25 0 1 0 480805013 110264320 25518 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26920 25518 603 41 0 26879 0
vsize: 107680
[startup+920.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 26039 0 0 0 91923 87 0 0 25 0 1 0 480805013 111202304 25750 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27149 25750 603 41 0 27108 0
vsize: 108596
[startup+930.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 26232 0 0 0 92922 88 0 0 25 0 1 0 480805013 112005120 25943 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27345 25943 603 41 0 27304 0
vsize: 109380
[startup+940.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 26448 0 0 0 93922 88 0 0 25 0 1 0 480805013 112812032 26159 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27542 26159 603 41 0 27501 0
vsize: 110168
[startup+950.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 26637 0 0 0 94922 89 0 0 25 0 1 0 480805013 113623040 26348 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27740 26348 603 41 0 27699 0
vsize: 110960
[startup+960.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 26845 0 0 0 95921 90 0 0 25 0 1 0 480805013 114425856 26556 4294967295 134512640 134672761 3221224560 3221223696 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27936 26556 603 41 0 27895 0
vsize: 111744
[startup+970.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 27038 0 0 0 96920 90 0 0 25 0 1 0 480805013 115236864 26749 4294967295 134512640 134672761 3221224560 3221223728 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28134 26749 603 41 0 28093 0
vsize: 112536
[startup+980.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 27226 0 0 0 97920 91 0 0 25 0 1 0 480805013 116068352 26937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28337 26937 603 41 0 28296 0
vsize: 113348
[startup+990.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 27403 0 0 0 98919 92 0 0 25 0 1 0 480805013 116740096 27114 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28501 27114 603 41 0 28460 0
vsize: 114004
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 27600 0 0 0 99918 93 0 0 25 0 1 0 480805013 117542912 27311 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28697 27311 603 41 0 28656 0
vsize: 114788
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 27777 0 0 0 100918 93 0 0 25 0 1 0 480805013 118345728 27488 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28893 27488 603 41 0 28852 0
vsize: 115572
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 27915 0 0 0 101918 94 0 0 25 0 1 0 480805013 118882304 27626 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29024 27626 603 41 0 28983 0
vsize: 116096
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 28085 0 0 0 102918 94 0 0 25 0 1 0 480805013 119558144 27796 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29189 27796 603 41 0 29148 0
vsize: 116756
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 28284 0 0 0 103917 95 0 0 25 0 1 0 480805013 120369152 27995 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29387 27995 603 41 0 29346 0
vsize: 117548
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 28551 0 0 0 104917 96 0 0 25 0 1 0 480805013 121442304 28262 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29649 28262 603 41 0 29608 0
vsize: 118596
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 28708 0 0 0 105916 96 0 0 25 0 1 0 480805013 122101760 28419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29810 28419 603 41 0 29769 0
vsize: 119240
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 28854 0 0 0 106915 97 0 0 25 0 1 0 480805013 122769408 28565 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29973 28565 603 41 0 29932 0
vsize: 119892
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 28995 0 0 0 107915 97 0 0 25 0 1 0 480805013 123301888 28706 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30103 28706 603 41 0 30062 0
vsize: 120412
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 29135 0 0 0 108915 98 0 0 25 0 1 0 480805013 123834368 28846 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30233 28846 603 41 0 30192 0
vsize: 120932
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 29279 0 0 0 109914 98 0 0 25 0 1 0 480805013 124375040 28990 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30365 28990 603 41 0 30324 0
vsize: 121460
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 29424 0 0 0 110914 98 0 0 25 0 1 0 480805013 125034496 29135 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30526 29135 603 41 0 30485 0
vsize: 122104
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 29557 0 0 0 111914 99 0 0 25 0 1 0 480805013 125571072 29268 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30657 29268 603 41 0 30616 0
vsize: 122628
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 29735 0 0 0 112913 100 0 0 25 0 1 0 480805013 126255104 29446 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30824 29446 603 41 0 30783 0
vsize: 123296
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 29955 0 0 0 113913 100 0 0 25 0 1 0 480805013 127184896 29666 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31051 29666 603 41 0 31010 0
vsize: 124204
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 30208 0 0 0 114912 101 0 0 25 0 1 0 480805013 128253952 29919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31312 29919 603 41 0 31271 0
vsize: 125248
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 30483 0 0 0 115912 102 0 0 25 0 1 0 480805013 129318912 30194 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31572 30194 603 41 0 31531 0
vsize: 126288
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 30739 0 0 0 116911 103 0 0 25 0 1 0 480805013 130404352 30450 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31837 30450 603 41 0 31796 0
vsize: 127348
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 31027 0 0 0 117910 104 0 0 25 0 1 0 480805013 131608576 30738 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32131 30738 603 41 0 32090 0
vsize: 128524
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 31316 0 0 0 118910 105 0 0 25 0 1 0 480805013 132820992 31027 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32427 31027 603 41 0 32386 0
vsize: 129708
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 507
Raw data (stat): 450 (minisat+) R 449 27222 27221 0 -1 0 31423 0 0 0 119909 105 0 0 25 0 1 0 480805013 133226496 31134 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32526 31134 603 41 0 32485 0
vsize: 130104
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 507
Raw data (stat): 450 (minisat+) Z 449 27222 27221 0 -1 12 31426 0 0 0 119910 111 0 0 25 0 1 0 480805013 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.22
CPU user time (s): 1199.1
CPU system time (s): 1.11383
CPU usage (%): 100.011
Max. virtual memory (Kb): 130104
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####