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 4843

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        910692 kB
Buffers:         26116 kB
Cached:          78060 kB
SwapCached:          0 kB
Active:          33996 kB
Inactive:        73096 kB
HighTotal:      131008 kB
HighFree:        49280 kB
LowTotal:       903652 kB
LowFree:        861412 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11340 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:50:20 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 644 7 1200.21 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.91 0.95 0.90 2/55 1372
Raw data (stat): 1372 (runsolver) R 1371 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 356106529 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0002 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 6823 0 0 0 982 17 0 0 25 0 1 0 356106529 32014336 6519 4294967295 134512640 134672761 3221224640 3221223812 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7816 6519 603 41 0 7775 0
vsize: 31264
[startup+20 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 6987 0 0 0 1981 18 0 0 25 0 1 0 356106529 32686080 6683 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7980 6683 603 41 0 7939 0
vsize: 31920
[startup+30.0006 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 7247 0 0 0 2980 19 0 0 25 0 1 0 356106529 33890304 6943 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8274 6943 603 41 0 8233 0
vsize: 33096
[startup+40.0004 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 7409 0 0 0 3979 20 0 0 25 0 1 0 356106529 34430976 7105 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8406 7105 603 41 0 8365 0
vsize: 33624
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 7788 0 0 0 4978 21 0 0 25 0 1 0 356106529 36036608 7484 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8798 7484 603 41 0 8757 0
vsize: 35192
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 8009 0 0 0 5976 23 0 0 25 0 1 0 356106529 36929536 7705 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9016 7705 603 41 0 8975 0
vsize: 36064
[startup+70.0013 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 8265 0 0 0 6976 23 0 0 25 0 1 0 356106529 38002688 7961 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9278 7961 603 41 0 9237 0
vsize: 37112
[startup+80.0019 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 8507 0 0 0 7975 24 0 0 25 0 1 0 356106529 39079936 8203 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9541 8203 603 41 0 9500 0
vsize: 38164
[startup+90.0015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 8752 0 0 0 8974 25 0 0 25 0 1 0 356106529 40026112 8448 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9772 8448 603 41 0 9731 0
vsize: 39088
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 8994 0 0 0 9974 25 0 0 25 0 1 0 356106529 40968192 8690 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10002 8690 603 41 0 9961 0
vsize: 40008
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 9273 0 0 0 10973 26 0 0 25 0 1 0 356106529 41910272 8969 4294967295 134512640 134672761 3221224640 3221223776 134565078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10232 8969 603 41 0 10191 0
vsize: 40928
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 9543 0 0 0 11973 27 0 0 25 0 1 0 356106529 42983424 9239 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10494 9239 603 41 0 10453 0
vsize: 41976
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 9876 0 0 0 12972 28 0 0 25 0 1 0 356106529 44318720 9572 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10820 9572 603 41 0 10779 0
vsize: 43280
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 10144 0 0 0 13971 29 0 0 25 0 1 0 356106529 45518848 9840 4294967295 134512640 134672761 3221224640 3221223824 134559482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11113 9840 603 41 0 11072 0
vsize: 44452
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 10482 0 0 0 14970 30 0 0 25 0 1 0 356106529 46993408 10178 4294967295 134512640 134672761 3221224640 3221223776 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11473 10178 603 41 0 11432 0
vsize: 45892
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 10792 0 0 0 15969 31 0 0 25 0 1 0 356106529 48033792 10456 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11727 10456 603 41 0 11686 0
vsize: 46908
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 10793 0 0 0 16968 32 0 0 25 0 1 0 356106529 48033792 10457 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11727 10457 603 41 0 11686 0
vsize: 46908
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 10794 0 0 0 17968 32 0 0 25 0 1 0 356106529 48033792 10458 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11727 10458 603 41 0 11686 0
vsize: 46908
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 10796 0 0 0 18968 32 0 0 25 0 1 0 356106529 48033792 10460 4294967295 134512640 134672761 3221224640 3221223808 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11727 10460 603 41 0 11686 0
vsize: 46908
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 11071 0 0 0 19967 33 0 0 25 0 1 0 356106529 49246208 10735 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12023 10735 603 41 0 11982 0
vsize: 48092
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 11281 0 0 0 20966 34 0 0 25 0 1 0 356106529 50044928 10945 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12218 10945 603 41 0 12177 0
vsize: 48872
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 11486 0 0 0 21966 35 0 0 25 0 1 0 356106529 50839552 11150 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12412 11150 603 41 0 12371 0
vsize: 49648
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 11792 0 0 0 22965 36 0 0 25 0 1 0 356106529 52178944 11456 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12739 11456 603 41 0 12698 0
vsize: 50956
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 12037 0 0 0 23963 37 0 0 25 0 1 0 356106529 53125120 11701 4294967295 134512640 134672761 3221224640 3221223808 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12970 11701 603 41 0 12929 0
vsize: 51880
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 12205 0 0 0 24963 38 0 0 25 0 1 0 356106529 53800960 11869 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13135 11869 603 41 0 13094 0
vsize: 52540
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 12433 0 0 0 25962 39 0 0 25 0 1 0 356106529 54743040 12097 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13365 12097 603 41 0 13324 0
vsize: 53460
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 12678 0 0 0 26961 40 0 0 25 0 1 0 356106529 55676928 12342 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13593 12342 603 41 0 13552 0
vsize: 54372
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 12945 0 0 0 27960 41 0 0 25 0 1 0 356106529 56881152 12609 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13887 12609 603 41 0 13846 0
vsize: 55548
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 13089 0 0 0 28959 42 0 0 25 0 1 0 356106529 57421824 12753 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14019 12753 603 41 0 13978 0
vsize: 56076
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 13313 0 0 0 29959 43 0 0 25 0 1 0 356106529 58343424 12977 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14244 12977 603 41 0 14203 0
vsize: 56976
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 13522 0 0 0 30958 44 0 0 25 0 1 0 356106529 59404288 13186 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14503 13186 603 41 0 14462 0
vsize: 58012
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 13777 0 0 0 31956 45 0 0 25 0 1 0 356106529 60469248 13441 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14763 13441 603 41 0 14722 0
vsize: 59052
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 14021 0 0 0 32955 46 0 0 25 0 1 0 356106529 61526016 13685 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15021 13685 603 41 0 14980 0
vsize: 60084
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 14237 0 0 0 33955 47 0 0 25 0 1 0 356106529 62328832 13901 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15217 13901 603 41 0 15176 0
vsize: 60868
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 14513 0 0 0 34954 47 0 0 25 0 1 0 356106529 63406080 14177 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15480 14177 603 41 0 15439 0
vsize: 61920
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 14756 0 0 0 35953 48 0 0 25 0 1 0 356106529 64479232 14420 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15742 14420 603 41 0 15701 0
vsize: 62968
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 14961 0 0 0 36952 49 0 0 25 0 1 0 356106529 65290240 14625 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15940 14625 603 41 0 15899 0
vsize: 63760
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 15091 0 0 0 37952 50 0 0 25 0 1 0 356106529 65826816 14755 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16071 14755 603 41 0 16030 0
vsize: 64284
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 15270 0 0 0 38952 51 0 0 25 0 1 0 356106529 66490368 14934 4294967295 134512640 134672761 3221224640 3221223808 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16233 14934 603 41 0 16192 0
vsize: 64932
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 15506 0 0 0 39951 52 0 0 25 0 1 0 356106529 67559424 15170 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16494 15170 603 41 0 16453 0
vsize: 65976
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 15733 0 0 0 40951 52 0 0 25 0 1 0 356106529 68489216 15397 4294967295 134512640 134672761 3221224640 3221223840 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16721 15397 603 41 0 16680 0
vsize: 66884
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 15928 0 0 0 41950 53 0 0 25 0 1 0 356106529 69292032 15592 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16917 15592 603 41 0 16876 0
vsize: 67668
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 16138 0 0 0 42949 54 0 0 25 0 1 0 356106529 70098944 15802 4294967295 134512640 134672761 3221224640 3221223840 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17114 15802 603 41 0 17073 0
vsize: 68456
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 16340 0 0 0 43948 55 0 0 25 0 1 0 356106529 70909952 16004 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17312 16004 603 41 0 17271 0
vsize: 69248
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 16543 0 0 0 44948 56 0 0 25 0 1 0 356106529 71700480 16207 4294967295 134512640 134672761 3221224640 3221223840 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17505 16207 603 41 0 17464 0
vsize: 70020
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 16724 0 0 0 45947 56 0 0 25 0 1 0 356106529 72519680 16388 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17705 16388 603 41 0 17664 0
vsize: 70820
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 17038 0 0 0 46946 57 0 0 25 0 1 0 356106529 73719808 16702 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17998 16702 603 41 0 17957 0
vsize: 71992
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 17245 0 0 0 47946 58 0 0 25 0 1 0 356106529 74653696 16909 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18226 16909 603 41 0 18185 0
vsize: 72904
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 17433 0 0 0 48945 59 0 0 25 0 1 0 356106529 75325440 17097 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18390 17097 603 41 0 18349 0
vsize: 73560
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 17644 0 0 0 49944 59 0 0 25 0 1 0 356106529 76259328 17308 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18618 17308 603 41 0 18577 0
vsize: 74472
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 17841 0 0 0 50944 60 0 0 25 0 1 0 356106529 77062144 17505 4294967295 134512640 134672761 3221224640 3221223776 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18814 17505 603 41 0 18773 0
vsize: 75256
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 17981 0 0 0 51944 61 0 0 25 0 1 0 356106529 77598720 17645 4294967295 134512640 134672761 3221224640 3221223744 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18945 17645 603 41 0 18904 0
vsize: 75780
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 18188 0 0 0 52943 61 0 0 25 0 1 0 356106529 78393344 17852 4294967295 134512640 134672761 3221224640 3221223732 1075351142 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19139 17852 603 41 0 19098 0
vsize: 76556
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 18354 0 0 0 53942 62 0 0 25 0 1 0 356106529 79065088 18018 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19303 18018 603 41 0 19262 0
vsize: 77212
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 18514 0 0 0 54942 62 0 0 25 0 1 0 356106529 79732736 18178 4294967295 134512640 134672761 3221224640 3221223808 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19466 18178 603 41 0 19425 0
vsize: 77864
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 18708 0 0 0 55941 63 0 0 25 0 1 0 356106529 80535552 18372 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19662 18372 603 41 0 19621 0
vsize: 78648
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 18886 0 0 0 56941 64 0 0 25 0 1 0 356106529 81207296 18550 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19826 18550 603 41 0 19785 0
vsize: 79304
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 19063 0 0 0 57941 64 0 0 25 0 1 0 356106529 82006016 18727 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20021 18727 603 41 0 19980 0
vsize: 80084
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 19283 0 0 0 58941 64 0 0 25 0 1 0 356106529 82948096 18947 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20251 18947 603 41 0 20210 0
vsize: 81004
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 19495 0 0 0 59940 65 0 0 25 0 1 0 356106529 83746816 19159 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20446 19159 603 41 0 20405 0
vsize: 81784
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 19640 0 0 0 60940 66 0 0 25 0 1 0 356106529 84283392 19304 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20577 19304 603 41 0 20536 0
vsize: 82308
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 19775 0 0 0 61939 66 0 0 25 0 1 0 356106529 84819968 19439 4294967295 134512640 134672761 3221224640 3221223776 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20708 19439 603 41 0 20667 0
vsize: 82832
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 19950 0 0 0 62939 67 0 0 25 0 1 0 356106529 85622784 19614 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20904 19614 603 41 0 20863 0
vsize: 83616
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 20161 0 0 0 63938 67 0 0 25 0 1 0 356106529 86425600 19825 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21100 19825 603 41 0 21059 0
vsize: 84400
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 20375 0 0 0 64937 69 0 0 25 0 1 0 356106529 87355392 20039 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21327 20039 603 41 0 21286 0
vsize: 85308
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 20558 0 0 0 65937 69 0 0 25 0 1 0 356106529 88023040 20222 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21490 20222 603 41 0 21449 0
vsize: 85960
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 20778 0 0 0 66936 70 0 0 25 0 1 0 356106529 88961024 20442 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21719 20442 603 41 0 21678 0
vsize: 86876
[startup+680.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 20993 0 0 0 67935 71 0 0 25 0 1 0 356106529 89907200 20657 4294967295 134512640 134672761 3221224640 3221223776 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21950 20657 603 41 0 21909 0
vsize: 87800
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 21239 0 0 0 68935 72 0 0 25 0 1 0 356106529 90836992 20903 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22177 20903 603 41 0 22136 0
vsize: 88708
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 21439 0 0 0 69935 72 0 0 25 0 1 0 356106529 91639808 21103 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22373 21103 603 41 0 22332 0
vsize: 89492
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 21613 0 0 0 70934 73 0 0 25 0 1 0 356106529 92307456 21277 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22536 21277 603 41 0 22495 0
vsize: 90144
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 21773 0 0 0 71933 74 0 0 25 0 1 0 356106529 92979200 21437 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22700 21437 603 41 0 22659 0
vsize: 90800
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 22054 0 0 0 72931 75 0 0 25 0 1 0 356106529 94179328 21718 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22993 21718 603 41 0 22952 0
vsize: 91972
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 22288 0 0 0 73931 76 0 0 25 0 1 0 356106529 95113216 21952 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23221 21952 603 41 0 23180 0
vsize: 92884
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 22589 0 0 0 74930 77 0 0 25 0 1 0 356106529 96841728 22253 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23643 22253 603 41 0 23602 0
vsize: 94572
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 22767 0 0 0 75929 78 0 0 25 0 1 0 356106529 97648640 22431 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23840 22431 603 41 0 23799 0
vsize: 95360
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 22944 0 0 0 76929 79 0 0 25 0 1 0 356106529 98312192 22608 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24002 22608 603 41 0 23961 0
vsize: 96008
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 23176 0 0 0 77928 80 0 0 25 0 1 0 356106529 99246080 22840 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24230 22840 603 41 0 24189 0
vsize: 96920
[startup+790.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 23390 0 0 0 78927 81 0 0 25 0 1 0 356106529 100171776 23054 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24456 23054 603 41 0 24415 0
vsize: 97824
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 23613 0 0 0 79926 82 0 0 25 0 1 0 356106529 100974592 23277 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24652 23277 603 41 0 24611 0
vsize: 98608
[startup+810.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 23779 0 0 0 80926 82 0 0 25 0 1 0 356106529 101773312 23443 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24847 23443 603 41 0 24806 0
vsize: 99388
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 23948 0 0 0 81926 82 0 0 25 0 1 0 356106529 102432768 23612 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25008 23612 603 41 0 24967 0
vsize: 100032
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 24136 0 0 0 82925 83 0 0 25 0 1 0 356106529 103108608 23800 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25173 23800 603 41 0 25132 0
vsize: 100692
[startup+840.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 24347 0 0 0 83925 83 0 0 25 0 1 0 356106529 104038400 24011 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25400 24011 603 41 0 25359 0
vsize: 101600
[startup+850.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 24546 0 0 0 84925 84 0 0 25 0 1 0 356106529 104841216 24210 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25596 24210 603 41 0 25555 0
vsize: 102384
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 24790 0 0 0 85924 84 0 0 25 0 1 0 356106529 105779200 24454 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25825 24454 603 41 0 25784 0
vsize: 103300
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 24966 0 0 0 86923 85 0 0 25 0 1 0 356106529 106582016 24630 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26021 24630 603 41 0 25980 0
vsize: 104084
[startup+880.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 25170 0 0 0 87923 86 0 0 25 0 1 0 356106529 107393024 24834 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26219 24834 603 41 0 26178 0
vsize: 104876
[startup+890.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 25329 0 0 0 88923 86 0 0 25 0 1 0 356106529 108056576 24993 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26381 24993 603 41 0 26340 0
vsize: 105524
[startup+900.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 25540 0 0 0 89922 87 0 0 25 0 1 0 356106529 108851200 25204 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26575 25204 603 41 0 26534 0
vsize: 106300
[startup+910.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 25736 0 0 0 90922 88 0 0 25 0 1 0 356106529 109658112 25400 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26772 25400 603 41 0 26731 0
vsize: 107088
[startup+920.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 25953 0 0 0 91921 89 0 0 25 0 1 0 356106529 110600192 25617 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27002 25617 603 41 0 26961 0
vsize: 108008
[startup+930.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 26171 0 0 0 92921 89 0 0 25 0 1 0 356106529 111534080 25835 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27230 25835 603 41 0 27189 0
vsize: 108920
[startup+940.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 26363 0 0 0 93921 90 0 0 25 0 1 0 356106529 112205824 26027 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27394 26027 603 41 0 27353 0
vsize: 109576
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 26575 0 0 0 94920 91 0 0 25 0 1 0 356106529 113143808 26239 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27623 26239 603 41 0 27582 0
vsize: 110492
[startup+960.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 26763 0 0 0 95919 91 0 0 25 0 1 0 356106529 113950720 26427 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27820 26427 603 41 0 27779 0
vsize: 111280
[startup+970.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 26975 0 0 0 96919 92 0 0 25 0 1 0 356106529 114757632 26639 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28017 26639 603 41 0 27976 0
vsize: 112068
[startup+980.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 27161 0 0 0 97918 92 0 0 25 0 1 0 356106529 115568640 26825 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28215 26825 603 41 0 28174 0
vsize: 112860
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 27351 0 0 0 98918 93 0 0 25 0 1 0 356106529 116383744 27015 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28414 27015 603 41 0 28373 0
vsize: 113656
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 27527 0 0 0 99917 94 0 0 25 0 1 0 356106529 117063680 27191 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28580 27191 603 41 0 28539 0
vsize: 114320
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 27727 0 0 0 100917 94 0 0 25 0 1 0 356106529 117874688 27391 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28778 27391 603 41 0 28737 0
vsize: 115112
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 27897 0 0 0 101916 95 0 0 25 0 1 0 356106529 118538240 27561 4294967295 134512640 134672761 3221224640 3221223808 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28940 27561 603 41 0 28899 0
vsize: 115760
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 28036 0 0 0 102916 96 0 0 25 0 1 0 356106529 119066624 27700 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29069 27700 603 41 0 29028 0
vsize: 116276
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 28211 0 0 0 103915 96 0 0 25 0 1 0 356106529 119869440 27875 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29265 27875 603 41 0 29224 0
vsize: 117060
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 28407 0 0 0 104915 97 0 0 25 0 1 0 356106529 120680448 28071 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29463 28071 603 41 0 29422 0
vsize: 117852
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 28673 0 0 0 105914 98 0 0 25 0 1 0 356106529 121753600 28337 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29725 28337 603 41 0 29684 0
vsize: 118900
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 28829 0 0 0 106914 98 0 0 25 0 1 0 356106529 122417152 28493 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29887 28493 603 41 0 29846 0
vsize: 119548
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 28971 0 0 0 107914 98 0 0 25 0 1 0 356106529 122953728 28635 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30018 28635 603 41 0 29977 0
vsize: 120072
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 29110 0 0 0 108913 99 0 0 25 0 1 0 356106529 123490304 28774 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30149 28774 603 41 0 30108 0
vsize: 120596
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 29250 0 0 0 109913 99 0 0 25 0 1 0 356106529 124018688 28914 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30278 28914 603 41 0 30237 0
vsize: 121112
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 29393 0 0 0 110913 100 0 0 25 0 1 0 356106529 124682240 29057 4294967295 134512640 134672761 3221224640 3221223808 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30440 29057 603 41 0 30399 0
vsize: 121760
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 29536 0 0 0 111912 101 0 0 25 0 1 0 356106529 125214720 29200 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30570 29200 603 41 0 30529 0
vsize: 122280
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 29668 0 0 0 112911 102 0 0 25 0 1 0 356106529 125747200 29332 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30700 29332 603 41 0 30659 0
vsize: 122800
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 29847 0 0 0 113911 102 0 0 25 0 1 0 356106529 126558208 29511 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30898 29511 603 41 0 30857 0
vsize: 123592
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 30065 0 0 0 114910 103 0 0 25 0 1 0 356106529 127365120 29729 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31095 29729 603 41 0 31054 0
vsize: 124380
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 30312 0 0 0 115910 104 0 0 25 0 1 0 356106529 128430080 29976 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31355 29976 603 41 0 31314 0
vsize: 125420
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 30587 0 0 0 116909 105 0 0 25 0 1 0 356106529 129499136 30251 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31616 30251 603 41 0 31575 0
vsize: 126464
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 30832 0 0 0 117908 106 0 0 25 0 1 0 356106529 130560000 30496 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31875 30496 603 41 0 31834 0
vsize: 127500
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 31124 0 0 0 118908 106 0 0 25 0 1 0 356106529 131764224 30788 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32169 30788 603 41 0 32128 0
vsize: 128676
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1372
Raw data (stat): 1372 (minisat+) R 1371 30927 30926 0 -1 0 31402 0 0 0 119907 107 0 0 25 0 1 0 356106529 132837376 31066 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32431 31066 603 41 0 32390 0
vsize: 129724
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 1372
Raw data (stat): 1372 (minisat+) Z 1371 30927 30926 0 -1 12 31405 0 0 0 119907 113 0 0 25 0 1 0 356106529 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.21
CPU user time (s): 1199.08
CPU system time (s): 1.13483
CPU usage (%): 100.011
Max. virtual memory (Kb): 129724
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####