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-test4.pi.opb
MD5SUM	09c7b63b87fdc5a38ccb26d9b87fe2d9
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	119
Optimality of the best value was proved	NO
Number of terms in the objective function	6140
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	6140
Number of bits of the sum of numbers in the objective function	13
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	6140
Number of bits of the biggest sum of numbers	13
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.07
Number of variables	6139
Total number of constraints	1437
Number of constraints which are clauses	1437
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	5
Maximum length of a constraint	172
Trace number 5430

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        913496 kB
Buffers:         34732 kB
Cached:          61792 kB
SwapCached:       4932 kB
Active:          56620 kB
Inactive:        47672 kB
HighTotal:      131008 kB
HighFree:        65520 kB
LowTotal:       903652 kB
LowFree:        847976 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11436 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:15:00 (client local time) WITH STATUS 10 IN 1200.37 SECONDS
stats: 3834 7 1200.37 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1437 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    1436   109204 |     430       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |    1435   109090 |      --       0       --      -- |     --   | -1/-114
c |         0 |    1435   109090 |     574       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.86772 s)
c ==============================================================================
c [1mFound solution: 180[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 12260   maxlim: 5960   bits: 13/13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   87218   415463 |   26165       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/18339          
c   -- var.elim.:  2000/18339          
c   -- var.elim.:  3000/18339          
c   -- var.elim.:  4000/18339          
c   -- var.elim.:  5000/18339          
c   -- var.elim.:  6000/18339          
c   -- var.elim.:  7000/18339          
c   -- var.elim.:  8000/18339          
c   -- var.elim.:  9000/18339          
c   -- var.elim.:  10000/18339          
c   -- var.elim.:  11000/18339          
c   -- var.elim.:  12000/18339          
c   -- var.elim.:  13000/18339          
c   -- var.elim.:  14000/18339          
c   -- var.elim.:  15000/18339          
c   -- var.elim.:  16000/18339          
c   -- var.elim.:  17000/18339          
c   -- var.elim.:  18000/18339          
c   -- var.elim.:  18339/18339          
c   -- var.elim.:  14/14          
c |         0 |   86789   413728 |      --       0       --      -- |     --   | -398/-1586
c |         0 |   86789   413728 |   34715       0        0     nan |  0.000 % |
c |       100 |   86789   413728 |   38187     100      654     6.5 |  0.364 % |
c |       250 |   86789   413728 |   42005     250     1173     4.7 |  0.364 % |
c |       475 |   86789   413728 |   46206     475     2073     4.4 |  0.364 % |
c |       814 |   86789   413728 |   50827     814     3417     4.2 |  0.364 % |
c |      1320 |   86789   413728 |   55909    1320     5491     4.2 |  0.364 % |
c |      2079 |   86789   413728 |   61500    2079     9004     4.3 |  0.364 % |
c |      3218 |   86789   413728 |   67650    3218    13875     4.3 |  0.364 % |
c |      4926 |   86789   413728 |   74415    4926    21971     4.5 |  0.364 % |
c |      7488 |   86789   413728 |   81857    7488    47121     6.3 |  0.364 % |
c |     11332 |   86789   413728 |   90043   11332   173999    15.4 |  0.364 % |
c |     17098 |   86789   413728 |   99047   17098   421341    24.6 |  0.364 % |
c |     25747 |   86789   413728 |  108952   25747  3581549   139.1 |  0.364 % |
c |     38721 |   86789   413728 |  119847   38721  4827238   124.7 |  0.364 % |
c |     58182 |   86789   413728 |  131832   58182  8070384   138.7 |  0.364 % |
c |     87376 |   86789   413728 |  145015   87376 32515635   372.1 |  0.364 % |
c |    131167 |   86789   413728 |  159517  131167 40122395   305.9 |  0.364 % |
c |    196854 |   86789   413728 |  175468   57874 49698203   858.7 |  0.364 % |
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 -x1340 -x1341 x1342 -x1343 -x1344 -x1345 -x1346 -x1347 -x1348 -x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 x1381 -x1382 -x1383 -x1384 x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 -x1408 -x1409 -x1410 -x1411 -x1412 -x1413 x1414 -x1415 -x1416 -x1417 -x1418 -x1419 -x1420 -x1421 -x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 -x1439 x1440 x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 -x1470 -x1471 -x1472 x1473 -x1474 -x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 -x1498 -x1499 -x1500 -x1501 -x1502 x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 -x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 -x1518 -x1519 -x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 x1527 -x1528 -x1529 -x1530 -x1531 x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 -x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 -x1556 -x1557 -x1558 -x1559 x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 -x1567 -x1568 -x1569 -x1570 -x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 -x1583 x1584 x1585 x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 -x1622 -x1623 -x1624 -x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 -x1633 -x1634 -x1635 -x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 x1650 -x1651 -x1652 -x1653 -x1654 -x1655 -x1656 -x1657 -x1658 -x1659 -x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 -x1676 -x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 -x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 -x1709 -x1710 x1711 -x1712 -x1713 -x1714 x1715 -x1716 -x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 x1735 -x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 -x1743 -x1744 -x1745 -x1746 -x1747 x1748 -x1749 -x1750 -x1751 -x1752 -x1753 x1754 -x1755 -x1756 -x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 -x1765 -x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 -x1787 -x1788 -x1789 -x1790 -x1791 -x1792 -x1793 -x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 -x1801 -x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 x1817 -x1818 -x1819 -x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 x1827 -x1828 -x1829 -x1830 -x1831 -x1832 -x1833 -x1834 -x1835 -x1836 -x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 x1848 -x1849 -x1850 -x1851 -x1852 -x1853 -x1854 -x1855 -x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 -x1876 -x1877 -x1878 -x1879 -x1880 x1881 x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 -x1890 x1891 x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 -x1919 -x1920 -x1921 -x1922 -x1923 -x1924 -x1925 -x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 -x1943 -x1944 -x1945 -x1946 -x1947 -x1948 -x1949 -x1950 -x1951 -x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 -x1962 -x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 -x1970 -x1971 -x1972 -x1973 -x1974 -x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981 -x1982 x1983 -x1984 -x1985 -x1986 -x1987 -x1988 -x1989 -x1990 -x1991 -x1992 -x1993 -x1994 -x1995 -x1996 -x1997 -x1998 -x1999 -x2000 -x2001 -x2002 x2003 -x2004 -x2005 -x2006 -x2007 -x2008 -x2009 -x2010 -x2011 -x2012 -x2013 -x2014 -x2015 -x2016 -x2017 -x2018 -x2019 -x2020 -x2021 -x2022 -x2023 -x2024 -x2025 -x2026 -x2027 -x2028 -x2029 -x2030 -x2031 -x2032 -x2033 -x2034 -x2035 -x2036 -x2037 -x2038 -x2039 -x2040 -x2041 -x2042 -x2043 x2044 -x2045 -x2046 -x2047 -x2048 -x2049 -x2050 -x2051 -x2052 -x2053 -x2054 -x2055 -x2056 -x2057 -x2058 -x2059 -x2060 -x2061 -x2062 -x2063 -x2064 -x2065 -x2066 -x2067 -x2068 -x2069 -x2070 -x2071 -x2072 -x2073 -x2074 -x2075 -x2076 -x2077 -x2078 -x2079 -x2080 -x2081 -x2082 -x2083 -x2084 -x2085 -x2086 -x2087 -x2088 -x2089 -x2090 -x2091 -x2092 -x2093 -x2094 -x2095 -x2096 -x2097 -x2098 -x2099 -x2100 -x2101 -x2102 -x2103 -x2104 -x2105 -x2106 -x2107 -x2108 -x2109 -x2110 -x2111 -x2112 x2113 -x2114 -x2115 -x2116 -x2117 -x2118 -x2119 -x2120 -x2121 -x2122 -x2123 -x2124 -x2125 -x2126 -x2127 -x2128 -x2129 -x2130 -x2131 -x2132 -x2133 -x2134 -x2135 x2136 -x2137 -x2138 -x2139 -x2140 -x2141 -x2142 -x2143 -x2144 -x2145 -x2146 -x2147 -x2148 -x2149 -x2150 -x2151 -x2152 -x2153 -x2154 -x2155 -x2156 -x2157 -x2158 -x2159 -x2160 -x2161 -x2162 -x2163 -x2164 -x2165 -x2166 -x2167 -x2168 -x2169 -x2170 -x2171 -x2172 -x2173 -x2174 -x2175 -x2176 -x2177 -x2178 -x2179 x2180 -x2181 -x2182 -x2183 -x2184 x2185 -x2186 -x2187 -x2188 -x2189 -x2190 -x2191 -x2192 -x2193 -x2194 -x2195 -x2196 -x2197 -x2198 -x2199 -x2200 -x2201 -x2202 -x2203 -x2204 -x2205 -x2206 -x2207 -x2208 -x2209 -x2210 -x2211 -x2212 -x2213 -x2214 -x2215 -x2216 -x2217 -x2218 -x2219 -x2220 -x2221 -x2222 -x2223 -x2224 -x2225 -x2226 -x2227 -x2228 -x2229 -x2230 -x2231 -x2232 -x2233 -x2234 -x2235 -x2236 -x2237 -x2238 -x2239 -x2240 -x2241 -x2242 -x2243 -x2244 -x2245 -x2246 -x2247 -x2248 -x2249 -x2250 -x2251 -x2252 -x2253 -x2254 -x2255 -x2256 -x2257 -x2258 -x2259 -x2260 -x2261 -x2262 -x2263 -x2264 x2265 -x2266 -x2267 -x2268 -x2269 -x2270 -x2271 -x2272 -x2273 -x2274 -x2275 -x2276 -x2277 -x2278 -x2279 -x2280 -x2281 -x2282 -x2283 -x2284 -x2285 -x2286 -x2287 -x2288 -x2289 -x2290 -x2291 -x2292 -x2293 -x2294 -x2295 -x2296 -x2297 -x2298 -x2299 -x2300 -x2301 -x2302 -x2303 -x2304 -x2305 -x2306 -x2307 -x2308 -x2309 -x2310 -x2311 -x2312 -x2313 -x2314 -x2315 x2316 -x2317 -x2318 -x2319 -x2320 -x2321 -x2322 -x2323 -x2324 -x2325 -x2326 -x2327 -x2328 -x2329 -x2330 -x2331 -x2332 -x2333 -x2334 -x2335 -x2336 -x2337 -x2338 -x2339 -x2340 -x2341 x2342 -x2343 -x2344 -x2345 -x2346 -x2347 -x2348 -x2349 -x2350 -x2351 -x2352 -x2353 -x2354 -x2355 -x2356 -x2357 -x2358 -x2359 -x2360 -x2361 -x2362 -x2363 -x2364 -x2365 -x2366 -x2367 -x2368 -x2369 -x2370 -x2371 -x2372 -x2373 -x2374 -x2375 -x2376 -x2377 -x2378 -x2379 -x2380 -x2381 -x2382 -x2383 -x2384 -x2385 -x2386 -x2387 -x2388 -x2389 -x2390 -x2391 -x2392 -x2393 -x2394 -x2395 -x2396 -x2397 -x2398 -x2399 -x2400 -x2401 -x2402 -x2403 x2404 -x2405 -x2406 -x2407 -x2408 -x2409 -x2410 -x2411 -x2412 -x2413 -x2414 -x2415 -x2416 -x2417 -x2418 -x2419 -x2420 -x2421 -x2422 -x2423 -x2424 -x2425 -x2426 -x2427 -x2428 -x2429 -x2430 -x2431 -x2432 -x2433 x2434 -x2435 -x2436 -x2437 -x2438 -x2439 -x2440 -x2441 -x2442 -x2443 -x2444 -x2445 -x2446 -x2447 -x2448 -x2449 -x2450 -x2451 -x2452 -x2453 -x2454 -x2455 -x2456 -x2457 -x2458 -x2459 -x2460 -x2461 -x2462 -x2463 -x2464 -x2465 -x2466 -x2467 -x2468 -x2469 -x2470 -x2471 -x2472 -x2473 -x2474 -x2475 -x2476 -x2477 -x2478 -x2479 -x2480 -x2481 -x2482 -x2483 -x2484 -x2485 -x2486 -x2487 -x2488 -x2489 -x2490 -x2491 -x2492 -x2493 -x2494 -x2495 -x2496 -x2497 x2498 -x2499 -x2500 -x2501 -x2502 -x2503 -x2504 -x2505 -x2506 -x2507 -x2508 -x2509 -x2510 -x2511 -x2512 -x2513 -x2514 -x2515 -x2516 -x2517 -x2518 -x2519 -x2520 -x2521 -x2522 -x2523 -x2524 -x2525 -x2526 -x2527 -x2528 -x2529 -x2530 -x2531 -x2532 -x2533 -x2534 -x2535 -x2536 -x2537 -x2538 -x2539 -x2540 -x2541 -x2542 -x2543 -x2544 -x2545 -x2546 -x2547 -x2548 -x2549 -x2550 -x2551 -x2552 -x2553 -x2554 -x2555 -x2556 -x2557 -x2558 -x2559 -x2560 -x2561 -x2562 -x2563 -x2564 -x2565 -x2566 -x2567 -x2568 -x2569 -x2570 -x2571 -x2572 -x2573 -x2574 -x2575 -x2576 -x2577 -x2578 -x2579 -x2580 -x2581 -x2582 -x2583 -x2584 x2585 -x2586 -x2587 -x2588 -x2589 -x2590 -x2591 -x2592 -x2593 -x2594 -x2595 -x2596 -x2597 -x2598 -x2599 -x2600 -x2601 -x2602 -x2603 -x2604 -x2605 -x2606 -x2607 -x2608 -x2609 -x2610 -x2611 -x2612 -x2613 -x2614 -x2615 -x2616 -x2617 -x2618 -x2619 -x2620 -x2621 -x2622 -x2623 -x2624 -x2625 -x2626 -x2627 -x2628 -x2629 -x2630 -x2631 -x2632 -x2633 -x2634 -x2635 -x2636 -x2637 -x2638 -x2639 -x2640 -x2641 -x2642 -x2643 -x2644 -x2645 -x2646 -x2647 -x2648 -x2649 -x2650 -x2651 -x2652 -x2653 -x2654 -x2655 -x2656 -x2657 -x2658 -x2659 -x2660 -x2661 -x2662 -x2663 -x2664 -x2665 -x2666 -x2667 -x2668 -x2669 -x2670 -x2671 -x2672 -x2673 x2674 -x2675 -x2676 -x2677 -x2678 -x2679 -x2680 -x2681 -x2682 -x2683 -x2684 -x2685 -x2686 -x2687 -x2688 -x2689 -x2690 -x2691 -x2692 -x2693 -x2694 -x2695 -x2696 x2697 -x2698 -x2699 -x2700 x2701 -x2702 -x2703 -x2704 -x2705 -x2706 -x2707 -x2708 -x2709 -x2710 -x2711 -x2712 -x2713 -x2714 -x2715 -x2716 -x2717 -x2718 -x2719 -x2720 -x2721 -x2722 x2723 -x2724 -x2725 -x2726 -x2727 -x2728 -x2729 -x2730 -x2731 x2732 -x2733 -x2734 -x2735 -x2736 -x2737 -x2738 -x2739 -x2740 -x2741 -x2742 -x2743 -x2744 -x2745 -x2746 -x2747 -x2748 -x2749 -x2750 -x2751 -x2752 -x2753 -x2754 x2755 -x2756 -x2757 x2758 x2759 -x2760 -x2761 -x2762 -x2763 -x2764 -x2765 -x2766 -x2767 -x2768 -x2769 -x2770 -x2771 -x2772 -x2773 -x2774 -x2775 -x2776 -x2777 -x2778 -x2779 -x2780 -x2781 -x2782 -x2783 -x2784 -x2785 -x2786 -x2787 -x2788 -x2789 -x2790 -x2791 x2792 -x2793 -x2794 -x2795 -x2796 -x2797 -x2798 -x2799 -x2800 -x2801 -x2802 -x2803 x2804 -x2805 -x2806 -x2807 -x2808 -x2809 -x2810 -x2811 -x2812 -x2813 -x2814 -x2815 -x2816 -x2817 -x2818 -x2819 -x2820 -x2821 -x2822 -x2823 -x2824 -x2825 x2826 -x2827 -x2828 -x2829 -x2830 -x2831 -x2832 -x2833 -x2834 x2835 -x2836 -x2837 -x2838 -x2839 x2840 -x2841 -x2842 -x2843 -x2844 -x2845 x2846 -x2847 -x2848 -x2849 -x2850 -x2851 -x2852 -x2853 -x2854 -x2855 -x2856 -x2857 -x2858 -x2859 x2860 -x2861 -x2862 -x2863 -x2864 -x2865 -x2866 -x2867 -x2868 -x2869 -x2870 -x2871 -x2872 -x2873 -x2874 -x2875 -x2876 -x2877 -x2878 -x2879 -x2880 -x2881 -x2882 -x2883 -x2884 -x2885 -x2886 -x2887 -x2888 -x2889 -x2890 -x2891 -x2892 -x2893 -x2894 x2895 -x2896 -x2897 -x2898 -x2899 -x2900 -x2901 -x2902 -x2903 -x2904 -x2905 -x2906 -x2907 x2908 x2909 -x2910 -x2911 -x2912 -x2913 -x2914 -x2915 -x2916 -x2917 -x2918 -x2919 -x2920 -x2921 -x2922 -x2923 -x2924 -x2925 -x2926 -x2927 -x2928 -x2929 -x2930 -x2931 -x2932 -x2933 -x2934 -x2935 -x2936 x2937 -x2938 -x2939 -x2940 -x2941 -x2942 -x2943 -x2944 -x2945 -x2946 -x2947 -x2948 -x2949 -x2950 -x2951 -x2952 -x2953 -x2954 -x2955 -x2956 -x2957 -x2958 -x2959 -x2960 -x2961 -x2962 -x2963 -x2964 -x2965 -x2966 -x2967 -x2968 -x2969 -x2970 -x2971 -x2972 -x2973 -x2974 -x2975 -x2976 -x2977 -x2978 -x2979 -x2980 -x2981 -x2982 -x2983 -x2984 -x2985 -x2986 -x2987 -x2988 -x2989 -x2990 -x2991 -x2992 -x2993 -x2994 -x2995 -x2996 -x2997 -x2998 -x2999 -x3000 -x3001 -x3002 -x3003 -x3004 -x3005 -x3006 -x3007 -x3008 -x3009 -x3010 -x3011 -x3012 -x3013 -x3014 -x3015 -x3016 -x3017 -x3018 -x3019 -x3020 -x3021 -x3022 -x3023 -x3024 x3025 -x3026 -x3027 -x3028 -x3029 -x3030 -x3031 -x3032 -x3033 -x3034 -x3035 -x3036 -x3037 -x3038 -x3039 -x3040 -x3041 -x3042 -x3043 -x3044 -x3045 -x3046 -x3047 -x3048 -x3049 -x3050 -x3051 -x3052 -x3053 -x3054 -x3055 -x3056 -x3057 -x3058 -x3059 -x3060 -x3061 -x3062 x3063 -x3064 -x3065 -x3066 -x3067 -x3068 -x3069 -x3070 -x3071 -x3072 -x3073 -x3074 -x3075 -x3076 x3077 -x3078 -x3079 -x3080 -x3081 -x3082 -x3083 x3084 -x3085 -x3086 -x3087 -x3088 -x3089 -x3090 -x3091 -x3092 -x3093 -x3094 -x3095 -x3096 -x3097 -x3098 -x3099 -x3100 -x3101 -x3102 -x3103 -x3104 -x3105 -x3106 -x3107 -x3108 -x3109 -x3110 -x3111 -x3112 -x3113 -x3114 -x3115 -x3116 -x3117 -x3118 -x3119 -x3120 -x3121 -x3122 -x3123 -x3124 -x3125 -x3126 -x3127 -x3128 -x3129 -x3130 -x3131 -x3132 -x3133 -x3134 -x3135 -x3136 -x3137 -x3138 -x3139 -x3140 -x3141 -x3142 -x3143 -x3144 -x3145 -x3146 -x3147 -x3148 -x3149 -x3150 -x3151 -x3152 -x3153 -x3154 -x3155 -x3156 -x3157 -x3158 -x3159 -x3160 -x3161 -x3162 x3163 x3164 -x3165 -x3166 -x3167 -x3168 -x3169 -x3170 -x3171 x3172 -x3173 -x3174 -x3175 -x3176 -x3177 -x3178 -x3179 -x3180 -x3181 -x3182 -x3183 -x3184 -x3185 -x3186 -x3187 -x3188 -x3189 -x3190 -x3191 -x3192 -x3193 -x3194 -x3195 -x3196 -x3197 -x3198 -x3199 -x3200 -x3201 -x3202 -x3203 -x3204 -x3205 -x3206 -x3207 -x3208 -x3209 -x3210 -x3211 -x3212 -x3213 -x3214 -x3215 -x3216 -x3217 -x3218 -x3219 -x3220 -x3221 -x3222 -x3223 -x3224 -x3225 -x3226 -x3227 -x3228 -x3229 -x3230 -x3231 -x3232 -x3233 -x3234 -x3235 -x3236 -x3237 -x3238 -x3239 -x3240 -x3241 -x3242 -x3243 -x3244 -x3245 -x3246 -x3247 -x3248 -x3249 -x3250 -x3251 -x3252 -x3253 -x3254 -x3255 -x3256 -x3257 -x3258 -x3259 -x3260 -x3261 -x3262 -x3263 -x3264 -x3265 -x3266 -x3267 -x3268 -x3269 x3270 -x3271 -x3272 -x3273 -x3274 -x3275 -x3276 -x3277 -x3278 -x3279 -x3280 -x3281 -x3282 -x3283 -x3284 -x3285 -x3286 -x3287 -x3288 -x3289 -x3290 -x3291 -x3292 -x3293 -x3294 -x3295 -x3296 -x3297 -x3298 x3299 -x3300 -x3301 -x3302 -x3303 -x3304 -x3305 -x3306 -x3307 -x3308 -x3309 -x3310 -x3311 -x3312 -x3313 -x3314 -x3315 -x3316 -x3317 -x3318 -x3319 -x3320 -x3321 -x3322 -x3323 -x3324 -x3325 -x3326 -x3327 -x3328 -x3329 -x3330 -x3331 -x3332 -x3333 -x3334 -x3335 -x3336 -x3337 -x3338 -x3339 -x3340 -x3341 -x3342 -x3343 -x3344 -x3345 -x3346 -x3347 -x3348 -x3349 -x3350 -x3351 -x3352 -x3353 -x3354 -x3355 -x3356 -x3357 -x3358 -x3359 -x3360 -x3361 -x3362 -x3363 -x3364 -x3365 -x3366 -x3367 -x3368 -x3369 -x3370 -x3371 -x3372 -x3373 -x3374 -x3375 -x3376 -x3377 -x3378 -x3379 -x3380 -x3381 -x3382 -x3383 -x3384 -x3385 -x3386 -x3387 -x3388 -x3389 -x3390 -x3391 -x3392 -x3393 -x3394 -x3395 -x3396 -x3397 -x3398 -x3399 -x3400 -x3401 -x3402 -x3403 -x3404 -x3405 -x3406 -x3407 -x3408 -x3409 -x3410 -x3411 -x3412 -x3413 -x3414 -x3415 -x3416 -x3417 -x3418 -x3419 -x3420 -x3421 -x3422 -x3423 -x3424 -x3425 -x3426 -x3427 -x3428 -x3429 -x3430 -x3431 -x3432 -x3433 -x3434 -x3435 -x3436 -x3437 -x3438 -x3439 -x3440 -x3441 -x3442 -x3443 -x3444 -x3445 -x3446 -x3447 -x3448 -x3449 -x3450 -x3451 -x3452 -x3453 -x3454 -x3455 -x3456 -x3457 -x3458 -x3459 -x3460 -x3461 -x3462 -x3463 -x3464 -x3465 -x3466 -x3467 -x3468 -x3469 -x3470 -x3471 -x3472 -x3473 -x3474 -x3475 -x3476 -x3477 -x3478 -x3479 -x3480 -x3481 -x3482 -x3483 -x3484 -x3485 -x3486 -x3487 -x3488 -x3489 -x3490 -x3491 -x3492 -x3493 -x3494 -x3495 -x3496 -x3497 -x3498 -x3499 -x3500 -x3501 -x3502 -x3503 -x3504 -x3505 -x3506 -x3507 -x3508 -x3509 -x3510 -x3511 -x3512 -x3513 -x3514 -x3515 -x3516 -x3517 -x3518 -x3519 -x3520 -x3521 -x3522 -x3523 -x3524 -x3525 -x3526 -x3527 -x3528 -x3529 -x3530 -x3531 -x3532 -x3533 -x3534 -x3535 -x3536 -x3537 -x3538 -x3539 -x3540 -x3541 -x3542 -x3543 -x3544 -x3545 -x3546 -x3547 -x3548 -x3549 -x3550 -x3551 -x3552 -x3553 -x3554 -x3555 -x3556 -x3557 -x3558 -x3559 -x3560 -x3561 -x3562 -x3563 -x3564 -x3565 -x3566 -x3567 -x3568 -x3569 -x3570 -x3571 -x3572 -x3573 -x3574 -x3575 -x3576 -x3577 -x3578 -x3579 -x3580 -x3581 -x3582 -x3583 -x3584 -x3585 -x3586 -x3587 -x3588 -x3589 -x3590 -x3591 -x3592 -x3593 -x3594 -x3595 -x3596 -x3597 -x3598 -x3599 -x3600 -x3601 -x3602 -x3603 -x3604 -x3605 -x3606 -x3607 -x3608 -x3609 -x3610 -x3611 -x3612 -x3613 -x3614 -x3615 -x3616 -x3617 -x3618 -x3619 -x3620 -x3621 -x3622 -x3623 x3624 -x3625 -x3626 -x3627 -x3628 -x3629 -x3630 -x3631 -x3632 -x3633 -x3634 -x3635 -x3636 -x3637 -x3638 -x3639 -x3640 -x3641 -x3642 -x3643 -x3644 -x3645 -x3646 -x3647 -x3648 -x3649 -x3650 -x3651 x3652 -x3653 -x3654 -x3655 -x3656 -x3657 -x3658 -x3659 x3660 -x3661 -x3662 -x3663 -x3664 -x3665 -x3666 -x3667 -x3668 -x3669 -x3670 -x3671 -x3672 -x3673 -x3674 -x3675 -x3676 -x3677 -x3678 -x3679 -x3680 -x3681 -x3682 -x3683 -x3684 -x3685 -x3686 -x3687 -x3688 -x3689 -x3690 -x3691 -x3692 x3693 -x3694 -x3695 -x3696 -x3697 -x3698 -x3699 -x3700 -x3701 -x3702 -x3703 -x3704 -x3705 -x3706 -x3707 -x3708 -x3709 -x3710 -x3711 -x3712 -x3713 -x3714 -x3715 -x3716 -x3717 -x3718 -x3719 -x3720 -x3721 -x3722 -x3723 -x3724 -x3725 -x3726 -x3727 -x3728 -x3729 -x3730 -x3731 -x3732 -x3733 -x3734 -x3735 -x3736 -x3737 -x3738 -x3739 -x3740 -x3741 -x3742 -x3743 -x3744 -x3745 -x3746 -x3747 -x3748 -x3749 -x3750 -x3751 -x3752 -x3753 -x3754 -x3755 -x3756 -x3757 -x3758 -x3759 -x3760 -x3761 -x3762 -x3763 -x3764 -x3765 -x3766 -x3767 -x3768 -x3769 -x3770 -x3771 -x3772 -x3773 -x3774 -x3775 -x3776 -x3777 -x3778 -x3779 -x3780 -x3781 -x3782 -x3783 -x3784 -x3785 -x3786 -x3787 -x3788 -x3789 -x3790 -x3791 -x3792 -x3793 -x3794 -x3795 -x3796 -x3797 -x3798 -x3799 -x3800 -x3801 -x3802 -x3803 -x3804 -x3805 -x3806 -x3807 -x3808 -x3809 -x3810 -x3811 -x3812 -x3813 -x3814 -x3815 -x3816 -x3817 -x3818 -x3819 -x3820 -x3821 -x3822 -x3823 -x3824 -x3825 -x3826 -x3827 -x3828 -x3829 -x3830 -x3831 -x3832 -x3833 -x3834 -x3835 -x3836 -x3837 -x3838 -x3839 -x3840 -x3841 -x3842 -x3843 -x3844 -x3845 -x3846 -x3847 -x3848 -x3849 -x3850 -x3851 -x3852 -x3853 -x3854 -x3855 -x3856 -x3857 -x3858 -x3859 -x3860 -x3861 -x3862 -x3863 -x3864 -x3865 -x3866 -x3867 -x3868 -x3869 -x3870 -x3871 -x3872 -x3873 -x3874 -x3875 -x3876 -x3877 -x3878 -x3879 -x3880 -x3881 -x3882 -x3883 -x3884 -x3885 -x3886 -x3887 -x3888 -x3889 -x3890 -x3891 -x3892 -x3893 -x3894 -x3895 -x3896 -x3897 -x3898 -x3899 -x3900 -x3901 -x3902 -x3903 -x3904 -x3905 -x3906 -x3907 -x3908 -x3909 -x3910 -x3911 -x3912 -x3913 -x3914 -x3915 -x3916 -x3917 -x3918 -x3919 -x3920 -x3921 -x3922 -x3923 -x3924 -x3925 -x3926 -x3927 -x3928 -x3929 -x3930 -x3931 -x3932 -x3933 -x3934 x3935 -x3936 -x3937 -x3938 -x3939 -x3940 -x3941 -x3942 -x3943 -x3944 -x3945 -x3946 -x3947 -x3948 -x3949 -x3950 -x3951 -x3952 -x3953 -x3954 -x3955 -x3956 -x3957 -x3958 -x3959 -x3960 -x3961 -x3962 -x3963 -x3964 -x3965 -x3966 -x3967 -x3968 -x3969 -x3970 -x3971 -x3972 -x3973 -x3974 -x3975 -x3976 -x3977 -x3978 -x3979 -x3980 -x3981 -x3982 -x3983 -x3984 -x3985 -x3986 -x3987 -x3988 -x3989 -x3990 -x3991 -x3992 -x3993 -x3994 -x3995 -x3996 -x3997 -x3998 -x3999 -x4000 -x4001 -x4002 -x4003 -x4004 -x4005 -x4006 -x4007 -x4008 -x4009 -x4010 -x4011 -x4012 -x4013 -x4014 -x4015 -x4016 -x4017 -x4018 -x4019 -x4020 -x4021 -x4022 -x4023 -x4024 -x4025 -x4026 -x4027 -x4028 -x4029 -x4030 -x4031 -x4032 -x4033 -x4034 -x4035 -x4036 -x4037 -x4038 -x4039 -x4040 -x4041 -x4042 -x4043 -x4044 -x4045 -x4046 -x4047 -x4048 -x4049 -x4050 -x4051 -x4052 -x4053 -x4054 -x4055 -x4056 -x4057 -x4058 -x4059 -x4060 -x4061 -x4062 -x4063 -x4064 -x4065 -x4066 -x4067 -x4068 -x4069 -x4070 x4071 x4072 -x4073 -x4074 -x4075 -x4076 -x4077 -x4078 -x4079 -x4080 -x4081 -x4082 -x4083 -x4084 -x4085 -x4086 -x4087 x4088 -x4089 -x4090 -x4091 -x4092 -x4093 -x4094 x4095 -x4096 -x4097 -x4098 -x4099 -x4100 x4101 -x4102 x4103 -x4104 -x4105 -x4106 -x4107 -x4108 -x4109 x4110 -x4111 -x4112 -x4113 -x4114 -x4115 x4116 -x4117 -x4118 -x4119 -x4120 -x4121 -x4122 -x4123 -x4124 -x4125 -x4126 -x4127 -x4128 -x4129 -x4130 -x4131 -x4132 -x4133 -x4134 -x4135 -x4136 -x4137 -x4138 -x4139 -x4140 -x4141 -x4142 -x4143 -x4144 -x4145 -x4146 x4147 -x4148 -x4149 -x4150 -x4151 -x4152 -x4153 -x4154 -x4155 -x4156 -x4157 -x4158 -x4159 -x4160 -x4161 -x4162 x4163 -x4164 -x4165 -x4166 -x4167 -x4168 -x4169 -x4170 -x4171 -x4172 -x4173 -x4174 -x4175 -x4176 x4177 -x4178 -x4179 -x4180 -x4181 -x4182 -x4183 -x4184 -x4185 -x4186 -x4187 -x4188 -x4189 -x4190 -x4191 -x4192 -x4193 -x4194 -x4195 -x4196 -x4197 -x4198 -x4199 -x4200 -x4201 -x4202 -x4203 -x4204 -x4205 -x4206 -x4207 -x4208 -x4209 -x4210 -x4211 -x4212 -x4213 -x4214 -x4215 -x4216 -x4217 -x4218 -x4219 -x4220 -x4221 -x4222 -x4223 -x4224 -x4225 -x4226 x4227 -x4228 -x4229 -x4230 -x4231 -x4232 -x4233 -x4234 -x4235 -x4236 -x4237 -x4238 x4239 -x4240 -x4241 -x4242 -x4243 -x4244 -x4245 -x4246 -x4247 -x4248 -x4249 -x4250 -x4251 -x4252 -x4253 -x4254 -x4255 -x4256 -x4257 -x4258 -x4259 -x4260 -x4261 -x4262 -x4263 -x4264 -x4265 -x4266 x4267 -x4268 -x4269 -x4270 -x4271 -x4272 -x4273 -x4274 -x4275 -x4276 -x4277 -x4278 -x4279 -x4280 -x4281 -x4282 -x4283 -x4284 -x4285 -x4286 -x4287 -x4288 -x4289 -x4290 -x4291 -x4292 -x4293 -x4294 -x4295 -x4296 x4297 -x4298 -x4299 -x4300 -x4301 -x4302 -x4303 x4304 -x4305 -x4306 -x4307 -x4308 -x4309 -x4310 -x4311 -x4312 -x4313 x4314 -x4315 -x4316 -x4317 -x4318 -x4319 -x4320 -x4321 -x4322 -x4323 -x4324 -x4325 -x4326 -x4327 -x4328 -x4329 -x4330 -x4331 -x4332 -x4333 -x4334 -x4335 -x4336 -x4337 -x4338 -x4339 -x4340 -x4341 -x4342 -x4343 -x4344 -x4345 -x4346 -x4347 -x4348 -x4349 x4350 -x4351 -x4352 -x4353 -x4354 -x4355 -x4356 -x4357 -x4358 -x4359 -x4360 -x4361 -x4362 -x4363 -x4364 -x4365 -x4366 -x4367 -x4368 -x4369 -x4370 -x4371 -x4372 -x4373 -x4374 -x4375 -x4376 -x4377 -x4378 -x4379 -x4380 -x4381 x4382 -x4383 -x4384 -x4385 -x4386 -x4387 -x4388 -x4389 -x4390 -x4391 -x4392 -x4393 -x4394 -x4395 -x4396 -x4397 -x4398 -x4399 -x4400 -x4401 -x4402 -x4403 -x4404 -x4405 -x4406 -x4407 -x4408 -x4409 -x4410 -x4411 -x4412 -x4413 -x4414 -x4415 -x4416 -x4417 -x4418 -x4419 x4420 -x4421 -x4422 -x4423 -x4424 -x4425 -x4426 -x4427 -x4428 -x4429 -x4430 -x4431 -x4432 -x4433 -x4434 -x4435 -x4436 x4437 -x4438 -x4439 -x4440 -x4441 -x4442 -x4443 -x4444 -x4445 -x4446 -x4447 -x4448 -x4449 -x4450 -x4451 -x4452 -x4453 -x4454 -x4455 x4456 -x4457 -x4458 -x4459 -x4460 -x4461 -x4462 -x4463 -x4464 -x4465 -x4466 -x4467 -x4468 -x4469 -x4470 x4471 -x4472 -x4473 -x4474 -x4475 -x4476 -x4477 -x4478 -x4479 -x4480 -x4481 -x4482 -x4483 -x4484 -x4485 -x4486 -x4487 -x4488 -x4489 -x4490 -x4491 -x4492 -x4493 -x4494 -x4495 -x4496 -x4497 -x4498 -x4499 -x4500 -x4501 -x4502 -x4503 -x4504 -x4505 -x4506 -x4507 -x4508 -x4509 -x4510 -x4511 -x4512 -x4513 -x4514 -x4515 -x4516 -x4517 -x4518 -x4519 -x4520 -x4521 -x4522 -x4523 -x4524 -x4525 -x4526 -x4527 -x4528 -x4529 -x4530 -x4531 -x4532 -x4533 -x4534 -x4535 -x4536 -x4537 -x4538 -x4539 -x4540 -x4541 -x4542 -x4543 -x4544 -x4545 -x4546 -x4547 -x4548 -x4549 -x4550 -x4551 -x4552 -x4553 -x4554 -x4555 -x4556 -x4557 -x4558 -x4559 -x4560 -x4561 -x4562 -x4563 -x4564 -x4565 -x4566 -x4567 -x4568 -x4569 -x4570 -x4571 -x4572 -x4573 -x4574 -x4575 -x4576 -x4577 -x4578 -x4579 -x4580 -x4581 -x4582 -x4583 -x4584 -x4585 -x4586 -x4587 -x4588 -x4589 -x4590 -x4591 -x4592 -x4593 -x4594 -x4595 -x4596 -x4597 -x4598 -x4599 -x4600 -x4601 -x4602 -x4603 -x4604 -x4605 -x4606 -x4607 -x4608 -x4609 -x4610 -x4611 -x4612 -x4613 -x4614 -x4615 -x4616 -x4617 -x4618 -x4619 -x4620 -x4621 -x4622 -x4623 -x4624 -x4625 -x4626 -x4627 -x4628 -x4629 -x4630 -x4631 -x4632 -x4633 -x4634 -x4635 x4636 -x4637 -x4638 -x4639 -x4640 -x4641 -x4642 -x4643 -x4644 -x4645 -x4646 -x4647 -x4648 -x4649 -x4650 -x4651 -x4652 -x4653 -x4654 -x4655 -x4656 -x4657 -x4658 -x4659 -x4660 -x4661 -x4662 -x4663 -x4664 -x4665 -x4666 -x4667 -x4668 -x4669 -x4670 -x4671 -x4672 -x4673 -x4674 -x4675 -x4676 -x4677 -x4678 -x4679 -x4680 -x4681 -x4682 -x4683 -x4684 -x4685 -x4686 -x4687 -x4688 -x4689 -x4690 -x4691 -x4692 -x4693 x4694 -x4695 -x4696 -x4697 -x4698 -x4699 -x4700 -x4701 -x4702 -x4703 -x4704 -x4705 -x4706 -x4707 -x4708 -x4709 -x4710 -x4711 -x4712 -x4713 -x4714 -x4715 -x4716 -x4717 -x4718 -x4719 -x4720 -x4721 -x4722 -x4723 -x4724 -x4725 -x4726 -x4727 -x4728 -x4729 -x4730 -x4731 -x4732 -x4733 -x4734 -x4735 -x4736 -x4737 -x4738 -x4739 -x4740 -x4741 -x4742 -x4743 -x4744 -x4745 -x4746 -x4747 -x4748 -x4749 -x4750 -x4751 -x4752 -x4753 -x4754 -x4755 -x4756 -x4757 -x4758 -x4759 -x4760 -x4761 -x4762 -x4763 -x4764 -x4765 -x4766 -x4767 -x4768 -x4769 -x4770 -x4771 -x4772 -x4773 -x4774 -x4775 -x4776 -x4777 -x4778 -x4779 -x4780 -x4781 -x4782 -x4783 -x4784 -x4785 -x4786 -x4787 -x4788 -x4789 -x4790 -x4791 -x4792 -x4793 -x4794 -x4795 -x4796 -x4797 -x4798 -x4799 -x4800 -x4801 -x4802 -x4803 -x4804 -x4805 -x4806 -x4807 -x4808 -x4809 -x4810 -x4811 x4812 -x4813 -x4814 -x4815 -x4816 -x4817 -x4818 -x4819 -x4820 -x4821 -x4822 -x4823 -x4824 -x4825 -x4826 -x4827 -x4828 -x4829 -x4830 -x4831 -x4832 -x4833 -x4834 -x4835 -x4836 -x4837 -x4838 -x4839 -x4840 -x4841 -x4842 -x4843 -x4844 -x4845 -x4846 -x4847 -x4848 -x4849 -x4850 -x4851 -x4852 -x4853 -x4854 -x4855 -x4856 -x4857 -x4858 -x4859 -x4860 -x4861 -x4862 -x4863 -x4864 -x4865 -x4866 -x4867 -x4868 -x4869 -x4870 -x4871 -x4872 -x4873 -x4874 x4875 -x4876 -x4877 -x4878 -x4879 -x4880 -x4881 -x4882 -x4883 -x4884 -x4885 -x4886 -x4887 -x4888 -x4889 -x4890 -x4891 -x4892 -x4893 -x4894 -x4895 -x4896 -x4897 -x4898 -x4899 -x4900 -x4901 -x4902 -x4903 -x4904 -x4905 -x4906 -x4907 -x4908 -x4909 -x4910 -x4911 -x4912 -x4913 -x4914 -x4915 -x4916 -x4917 -x4918 -x4919 -x4920 -x4921 -x4922 -x4923 -x4924 -x4925 -x4926 -x4927 -x4928 -x4929 -x4930 -x4931 -x4932 -x4933 -x4934 -x4935 -x4936 -x4937 -x4938 -x4939 -x4940 -x4941 -x4942 -x4943 -x4944 -x4945 -x4946 -x4947 -x4948 -x4949 -x4950 -x4951 -x4952 -x4953 -x4954 -x4955 -x4956 -x4957 -x4958 -x4959 -x4960 -x4961 -x4962 -x4963 -x4964 -x4965 -x4966 -x4967 -x4968 -x4969 -x4970 -x4971 -x4972 -x4973 -x4974 -x4975 -x4976 -x4977 -x4978 -x4979 -x4980 -x4981 -x4982 -x4983 -x4984 x4985 -x4986 -x4987 -x4988 -x4989 -x4990 x4991 -x4992 -x4993 -x4994 -x4995 -x4996 -x4997 -x4998 -x4999 -x5000 -x5001 -x5002 -x5003 -x5004 -x5005 -x5006 -x5007 -x5008 -x5009 -x5010 -x5011 -x5012 -x5013 x5014 -x5015 -x5016 -x5017 x5018 -x5019 -x5020 -x5021 -x5022 -x5023 -x5024 -x5025 -x5026 -x5027 -x5028 -x5029 -x5030 -x5031 -x5032 -x5033 -x5034 -x5035 -x5036 -x5037 -x5038 -x5039 -x5040 -x5041 -x5042 -x5043 -x5044 -x5045 -x5046 -x5047 -x5048 -x5049 -x5050 -x5051 -x5052 -x5053 -x5054 -x5055 -x5056 -x5057 -x5058 -x5059 -x5060 -x5061 -x5062 -x5063 -x5064 -x5065 -x5066 -x5067 -x5068 -x5069 -x5070 -x5071 x5072 -x5073 -x5074 -x5075 -x5076 -x5077 -x5078 -x5079 -x5080 -x5081 -x5082 -x5083 -x5084 -x5085 -x5086 -x5087 -x5088 -x5089 -x5090 -x5091 -x5092 -x5093 -x5094 -x5095 -x5096 -x5097 -x5098 -x5099 -x5100 -x5101 -x5102 -x5103 -x5104 -x5105 -x5106 -x5107 -x5108 -x5109 -x5110 -x5111 -x5112 -x5113 -x5114 -x5115 -x5116 -x5117 -x5118 -x5119 -x5120 -x5121 -x5122 -x5123 -x5124 -x5125 -x5126 -x5127 -x5128 -x5129 -x5130 -x5131 -x5132 -x5133 -x5134 -x5135 -x5136 -x5137 -x5138 -x5139 -x5140 -x5141 -x5142 -x5143 -x5144 -x5145 -x5146 -x5147 -x5148 -x5149 -x5150 -x5151 -x5152 -x5153 -x5154 -x5155 -x5156 -x5157 -x5158 -x5159 -x5160 -x5161 -x5162 -x5163 -x5164 -x5165 -x5166 -x5167 -x5168 -x5169 -x5170 -x5171 -x5172 -x5173 -x5174 -x5175 -x5176 -x5177 -x5178 -x5179 -x5180 -x5181 -x5182 -x5183 -x5184 -x5185 -x5186 -x5187 -x5188 -x5189 -x5190 -x5191 -x5192 -x5193 -x5194 -x5195 -x5196 -x5197 -x5198 -x5199 -x5200 -x5201 -x5202 -x5203 -x5204 -x5205 -x5206 -x5207 -x5208 -x5209 -x5210 -x5211 -x5212 -x5213 -x5214 -x5215 -x5216 -x5217 -x5218 -x5219 -x5220 -x5221 -x5222 -x5223 -x5224 -x5225 -x5226 -x5227 -x5228 -x5229 -x5230 -x5231 -x5232 -x5233 -x5234 -x5235 -x5236 -x5237 -x5238 -x5239 -x5240 -x5241 -x5242 -x5243 -x5244 -x5245 -x5246 -x5247 -x5248 -x5249 -x5250 -x5251 -x5252 -x5253 -x5254 -x5255 -x5256 -x5257 -x5258 -x5259 -x5260 -x5261 -x5262 -x5263 -x5264 -x5265 -x5266 -x5267 -x5268 -x5269 -x5270 -x5271 -x5272 -x5273 -x5274 -x5275 -x5276 -x5277 -x5278 -x5279 -x5280 -x5281 -x5282 -x5283 -x5284 -x5285 -x5286 -x5287 -x5288 -x5289 -x5290 -x5291 -x5292 -x5293 -x5294 -x5295 -x5296 -x5297 -x5298 -x5299 -x5300 -x5301 -x5302 -x5303 -x5304 -x5305 -x5306 -x5307 -x5308 -x5309 -x5310 -x5311 -x5312 -x5313 -x5314 -x5315 -x5316 -x5317 -x5318 -x5319 -x5320 -x5321 -x5322 -x5323 -x5324 -x5325 -x5326 -x5327 -x5328 -x5329 -x5330 -x5331 -x5332 -x5333 -x5334 -x5335 -x5336 -x5337 -x5338 -x5339 -x5340 -x5341 -x5342 -x5343 -x5344 -x5345 -x5346 -x5347 -x5348 -x5349 -x5350 -x5351 -x5352 -x5353 -x5354 -x5355 -x5356 -x5357 -x5358 -x5359 -x5360 -x5361 -x5362 -x5363 -x5364 -x5365 -x5366 -x5367 -x5368 -x5369 -x5370 -x5371 -x5372 -x5373 -x5374 -x5375 -x5376 -x5377 -x5378 -x5379 -x5380 -x5381 -x5382 -x5383 -x5384 -x5385 -x5386 -x5387 -x5388 -x5389 -x5390 -x5391 -x5392 -x5393 -x5394 -x5395 -x5396 -x5397 -x5398 -x5399 -x5400 -x5401 -x5402 -x5403 -x5404 -x5405 -x5406 -x5407 -x5408 -x5409 -x5410 -x5411 -x5412 -x5413 -x5414 -x5415 -x5416 -x5417 -x5418 -x5419 -x5420 -x5421 -x5422 -x5423 -x5424 -x5425 -x5426 -x5427 -x5428 -x5429 -x5430 -x5431 -x5432 -x5433 -x5434 -x5435 -x5436 -x5437 -x5438 -x5439 -x5440 -x5441 -x5442 -x5443 -x5444 -x5445 -x5446 -x5447 -x5448 -x5449 -x5450 -x5451 -x5452 -x5453 x5454 -x5455 -x5456 -x5457 -x5458 -x5459 -x5460 -x5461 -x5462 -x5463 -x5464 -x5465 -x5466 -x5467 -x5468 -x5469 -x5470 -x5471 -x5472 -x5473 -x5474 -x5475 -x5476 -x5477 -x5478 -x5479 -x5480 -x5481 -x5482 -x5483 -x5484 -x5485 x5486 -x5487 -x5488 -x5489 -x5490 -x5491 -x5492 -x5493 -x5494 -x5495 -x5496 -x5497 -x5498 -x5499 -x5500 -x5501 -x5502 -x5503 -x5504 -x5505 -x5506 -x5507 -x5508 -x5509 -x5510 -x5511 -x5512 -x5513 -x5514 -x5515 -x5516 -x5517 -x5518 -x5519 -x5520 -x5521 -x5522 -x5523 -x5524 -x5525 -x5526 -x5527 -x5528 -x5529 -x5530 -x5531 -x5532 -x5533 -x5534 -x5535 -x5536 -x5537 -x5538 -x5539 -x5540 -x5541 -x5542 -x5543 -x5544 -x5545 -x5546 -x5547 -x5548 -x5549 -x5550 -x5551 -x5552 -x5553 -x5554 -x5555 -x5556 -x5557 -x5558 -x5559 -x5560 -x5561 -x5562 -x5563 -x5564 -x5565 -x5566 -x5567 -x5568 -x5569 -x5570 -x5571 -x5572 -x5573 -x5574 -x5575 -x5576 -x5577 -x5578 -x5579 -x5580 -x5581 -x5582 -x5583 -x5584 -x5585 -x5586 -x5587 -x5588 -x5589 -x5590 -x5591 -x5592 -x5593 -x5594 -x5595 -x5596 -x5597 -x5598 -x5599 -x5600 -x5601 -x5602 -x5603 -x5604 -x5605 -x5606 -x5607 -x5608 -x5609 -x5610 -x5611 -x5612 -x5613 -x5614 -x5615 -x5616 -x5617 -x5618 -x5619 -x5620 -x5621 -x5622 -x5623 -x5624 -x5625 -x5626 -x5627 -x5628 -x5629 -x5630 -x5631 -x5632 -x5633 -x5634 -x5635 -x5636 -x5637 -x5638 -x5639 -x5640 -x5641 -x5642 -x5643 -x5644 -x5645 -x5646 -x5647 -x5648 -x5649 -x5650 -x5651 -x5652 -x5653 -x5654 -x5655 -x5656 -x5657 -x5658 -x5659 -x5660 -x5661 -x5662 -x5663 -x5664 -x5665 -x5666 -x5667 -x5668 -x5669 -x5670 -x5671 -x5672 -x5673 -x5674 -x5675 -x5676 -x5677 -x5678 -x5679 -x5680 -x5681 -x5682 -x5683 -x5684 -x5685 -x5686 -x5687 -x5688 -x5689 -x5690 -x5691 -x5692 -x5693 -x5694 -x5695 -x5696 -x5697 -x5698 -x5699 -x5700 -x5701 -x5702 -x5703 -x5704 -x5705 -x5706 -x5707 -x5708 -x5709 -x5710 -x5711 -x5712 -x5713 -x5714 -x5715 -x5716 -x5717 -x5718 -x5719 -x5720 -x5721 -x5722 -x5723 -x5724 -x5725 -x5726 -x5727 -x5728 -x5729 -x5730 -x5731 -x5732 -x5733 -x5734 -x5735 -x5736 -x5737 -x5738 -x5739 -x5740 -x5741 -x5742 -x5743 -x5744 -x5745 -x5746 -x5747 -x5748 -x5749 -x5750 -x5751 -x5752 -x5753 -x5754 -x5755 -x5756 -x5757 -x5758 -x5759 -x5760 -x5761 -x5762 -x5763 -x5764 -x5765 -x5766 -x5767 -x5768 -x5769 -x5770 -x5771 -x5772 -x5773 -x5774 -x5775 -x5776 -x5777 -x5778 -x5779 -x5780 -x5781 -x5782 -x5783 -x5784 -x5785 -x5786 -x5787 -x5788 -x5789 -x5790 -x5791 -x5792 -x5793 -x5794 -x5795 -x5796 -x5797 -x5798 -x5799 -x5800 -x5801 -x5802 -x5803 -x5804 -x5805 -x5806 -x5807 -x5808 -x5809 -x5810 -x5811 -x5812 -x5813 -x5814 -x5815 -x5816 -x5817 -x5818 -x5819 -x5820 -x5821 -x5822 -x5823 -x5824 -x5825 -x5826 -x5827 -x5828 -x5829 -x5830 -x5831 -x5832 -x5833 -x5834 -x5835 -x5836 -x5837 -x5838 -x5839 -x#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 5621
Raw data (stat): 5621 (runsolver) R 5620 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421847903 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.0011 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 10260 0 0 0 969 29 0 0 25 0 1 0 421847903 40546304 8936 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9899 8936 603 41 0 9858 0
vsize: 39596
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 10328 0 0 0 1969 29 0 0 25 0 1 0 421847903 41000960 9004 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10010 9004 603 41 0 9969 0
vsize: 40040
[startup+30.002 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 10345 0 0 0 2969 29 0 0 25 0 1 0 421847903 41000960 9021 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10010 9021 603 41 0 9969 0
vsize: 40040
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 10396 0 0 0 3969 29 0 0 25 0 1 0 421847903 41271296 9072 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10076 9072 603 41 0 10035 0
vsize: 40304
[startup+50.0029 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 10598 0 0 0 4969 29 0 0 25 0 1 0 421847903 42061824 9274 4294967295 134512640 134672761 3221224560 3221223720 134614557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10269 9274 603 41 0 10228 0
vsize: 41076
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 10814 0 0 0 5969 29 0 0 25 0 1 0 421847903 42856448 9490 4294967295 134512640 134672761 3221224560 3221223744 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10463 9490 603 41 0 10422 0
vsize: 41852
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 11194 0 0 0 6968 31 0 0 25 0 1 0 421847903 44478464 9870 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10859 9870 603 41 0 10818 0
vsize: 43436
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 12937 0 0 0 7963 36 0 0 25 0 1 0 421847903 51580928 11613 4294967295 134512640 134672761 3221224560 3221223744 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12593 11613 603 41 0 12552 0
vsize: 50372
[startup+90.0027 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 14291 0 0 0 8959 40 0 0 25 0 1 0 421847903 57225216 12967 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13971 12967 603 41 0 13930 0
vsize: 55884
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 14668 0 0 0 9958 41 0 0 25 0 1 0 421847903 58675200 13344 4294967295 134512640 134672761 3221224560 3221223600 134603536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14325 13344 603 41 0 14284 0
vsize: 57300
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 15101 0 0 0 10956 43 0 0 25 0 1 0 421847903 60657664 13777 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14809 13777 603 41 0 14768 0
vsize: 59236
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 15501 0 0 0 11955 45 0 0 25 0 1 0 421847903 62251008 14177 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15198 14177 603 41 0 15157 0
vsize: 60792
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 16349 0 0 0 12953 47 0 0 25 0 1 0 421847903 65699840 15025 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16040 15025 603 41 0 15999 0
vsize: 64160
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 17518 0 0 0 13950 50 0 0 25 0 1 0 421847903 70467584 16194 4294967295 134512640 134672761 3221224560 3221223744 134615557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17204 16194 603 41 0 17163 0
vsize: 68816
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 18753 0 0 0 14947 53 0 0 25 0 1 0 421847903 75501568 17429 4294967295 134512640 134672761 3221224560 3221223600 134612471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18433 17429 603 41 0 18392 0
vsize: 73732
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 19536 0 0 0 15945 55 0 0 25 0 1 0 421847903 78671872 18212 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19207 18212 603 41 0 19166 0
vsize: 76828
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 21208 0 0 0 16941 59 0 0 25 0 1 0 421847903 85454848 19884 4294967295 134512640 134672761 3221224560 3221223600 134612851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20863 19884 603 41 0 20822 0
vsize: 83452
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 22724 0 0 0 17938 63 0 0 25 0 1 0 421847903 91639808 21400 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22373 21400 603 41 0 22332 0
vsize: 89492
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 24104 0 0 0 18935 66 0 0 25 0 1 0 421847903 97386496 22780 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23776 22780 603 41 0 23735 0
vsize: 95104
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 25470 0 0 0 19932 69 0 0 25 0 1 0 421847903 103182336 24146 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25191 24146 603 41 0 25150 0
vsize: 100764
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 26937 0 0 0 20929 73 0 0 25 0 1 0 421847903 109178880 25613 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26655 25613 603 41 0 26614 0
vsize: 106620
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 28246 0 0 0 21926 75 0 0 25 0 1 0 421847903 114565120 26922 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27970 26922 603 41 0 27929 0
vsize: 111880
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 29428 0 0 0 22923 79 0 0 25 0 1 0 421847903 119369728 28104 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29143 28104 603 41 0 29102 0
vsize: 116572
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 30652 0 0 0 23920 82 0 0 25 0 1 0 421847903 124461056 29328 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30386 29328 603 41 0 30345 0
vsize: 121544
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 31711 0 0 0 24918 84 0 0 25 0 1 0 421847903 128770048 30387 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31438 30387 603 41 0 31397 0
vsize: 125752
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 32626 0 0 0 25917 86 0 0 25 0 1 0 421847903 132452352 31302 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32337 31302 603 41 0 32296 0
vsize: 129348
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 33700 0 0 0 26914 88 0 0 25 0 1 0 421847903 136863744 32376 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33414 32376 603 41 0 33373 0
vsize: 133656
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 34689 0 0 0 27912 91 0 0 25 0 1 0 421847903 140902400 33365 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34400 33365 603 41 0 34359 0
vsize: 137600
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 35866 0 0 0 28909 93 0 0 25 0 1 0 421847903 145805312 34542 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35597 34542 603 41 0 35556 0
vsize: 142388
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5621
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 36815 0 0 0 29909 94 0 0 25 0 1 0 421847903 149630976 35491 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36531 35491 603 41 0 36490 0
vsize: 146124
[startup+310.009 s]
Raw data (loadavg): 1.07 0.99 0.91 2/58 5667
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 38120 0 0 0 30906 97 0 0 25 0 1 0 421847903 155013120 36796 4294967295 134512640 134672761 3221224560 3221223744 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37845 36796 603 41 0 37804 0
vsize: 151380
[startup+320.009 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 5674
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 39560 0 0 0 31903 101 0 0 25 0 1 0 421847903 160870400 38236 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39275 38236 603 41 0 39234 0
vsize: 157100
[startup+330.01 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 5674
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 40762 0 0 0 32899 104 0 0 25 0 1 0 421847903 165740544 39438 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40464 39438 603 41 0 40423 0
vsize: 161856
[startup+340.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 5674
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 42241 0 0 0 33896 107 0 0 25 0 1 0 421847903 171819008 40917 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41948 40917 603 41 0 41907 0
vsize: 167792
[startup+350.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 5674
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 43305 0 0 0 34894 110 0 0 25 0 1 0 421847903 176177152 41981 4294967295 134512640 134672761 3221224560 3221223432 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43012 41981 603 41 0 42971 0
vsize: 172048
[startup+360.011 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 5674
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 44183 0 0 0 35892 112 0 0 25 0 1 0 421847903 179740672 42859 4294967295 134512640 134672761 3221224560 3221223712 134565146 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43882 42859 603 41 0 43841 0
vsize: 175528
[startup+370.012 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 5674
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 44862 0 0 0 36891 113 0 0 25 0 1 0 421847903 182505472 43538 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44557 43538 603 41 0 44516 0
vsize: 178228
[startup+380.012 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 5674
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 46312 0 0 0 37887 117 0 0 25 0 1 0 421847903 188538880 44988 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46030 44988 603 41 0 45989 0
vsize: 184120
[startup+390.011 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 47449 0 0 0 38884 120 0 0 25 0 1 0 421847903 193126400 46125 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47150 46125 603 41 0 47109 0
vsize: 188600
[startup+400.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 48080 0 0 0 39883 122 0 0 25 0 1 0 421847903 195772416 46756 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47796 46756 603 41 0 47755 0
vsize: 191184
[startup+410.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 48807 0 0 0 40881 124 0 0 25 0 1 0 421847903 198688768 47483 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48508 47483 603 41 0 48467 0
vsize: 194032
[startup+420.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 49370 0 0 0 41879 126 0 0 25 0 1 0 421847903 200937472 48046 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49057 48046 603 41 0 49016 0
vsize: 196228
[startup+430.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 49924 0 0 0 42878 128 0 0 25 0 1 0 421847903 203214848 48600 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49613 48600 603 41 0 49572 0
vsize: 198452
[startup+440.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 50557 0 0 0 43877 129 0 0 25 0 1 0 421847903 205848576 49233 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50256 49233 603 41 0 50215 0
vsize: 201024
[startup+450.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 51155 0 0 0 44875 131 0 0 25 0 1 0 421847903 208375808 49831 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50873 49831 603 41 0 50832 0
vsize: 203492
[startup+460.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 51677 0 0 0 45873 133 0 0 25 0 1 0 421847903 210526208 50353 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51398 50353 603 41 0 51357 0
vsize: 205592
[startup+470.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 52252 0 0 0 46872 134 0 0 25 0 1 0 421847903 213299200 50928 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52075 50928 603 41 0 52034 0
vsize: 208300
[startup+480.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 53345 0 0 0 47870 136 0 0 25 0 1 0 421847903 217739264 52021 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53159 52021 603 41 0 53118 0
vsize: 212636
[startup+490.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 54375 0 0 0 48868 138 0 0 25 0 1 0 421847903 221954048 53051 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54188 53051 603 41 0 54147 0
vsize: 216752
[startup+500.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 55744 0 0 0 49865 142 0 0 25 0 1 0 421847903 227631104 54420 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55574 54420 603 41 0 55533 0
vsize: 222296
[startup+510.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 57011 0 0 0 50863 144 0 0 25 0 1 0 421847903 232833024 55687 4294967295 134512640 134672761 3221224560 3221223600 134612659 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56844 55687 603 41 0 56803 0
vsize: 227376
[startup+520.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 58359 0 0 0 51861 146 0 0 25 0 1 0 421847903 238358528 57035 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58193 57035 603 41 0 58152 0
vsize: 232772
[startup+530.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 59803 0 0 0 52858 149 0 0 25 0 1 0 421847903 244248576 58479 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59631 58479 603 41 0 59590 0
vsize: 238524
[startup+540.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 61180 0 0 0 53855 153 0 0 25 0 1 0 421847903 249868288 59856 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61003 59856 603 41 0 60962 0
vsize: 244012
[startup+550.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 62771 0 0 0 54852 155 0 0 25 0 1 0 421847903 256409600 61447 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62600 61447 603 41 0 62559 0
vsize: 250400
[startup+560.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 64272 0 0 0 55849 159 0 0 25 0 1 0 421847903 262459392 62948 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64077 62948 603 41 0 64036 0
vsize: 256308
[startup+570.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 65427 0 0 0 56847 161 0 0 25 0 1 0 421847903 267292672 64103 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65257 64103 603 41 0 65216 0
vsize: 261028
[startup+580.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 67290 0 0 0 57844 164 0 0 25 0 1 0 421847903 274837504 65966 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67099 65966 603 41 0 67058 0
vsize: 268396
[startup+590.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 68552 0 0 0 58842 166 0 0 25 0 1 0 421847903 280010752 67228 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68362 67228 603 41 0 68321 0
vsize: 273448
[startup+600.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 69515 0 0 0 59840 169 0 0 25 0 1 0 421847903 284000256 68191 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69336 68191 603 41 0 69295 0
vsize: 277344
[startup+610.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 70495 0 0 0 60839 170 0 0 25 0 1 0 421847903 288010240 69171 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70315 69171 603 41 0 70274 0
vsize: 281260
[startup+620.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 71386 0 0 0 61837 171 0 0 25 0 1 0 421847903 291618816 70062 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71196 70062 603 41 0 71155 0
vsize: 284784
[startup+630.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 72577 0 0 0 62835 174 0 0 25 0 1 0 421847903 296562688 71253 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72403 71253 603 41 0 72362 0
vsize: 289612
[startup+640.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5676
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 73766 0 0 0 63832 177 0 0 25 0 1 0 421847903 301457408 72442 4294967295 134512640 134672761 3221224560 3221223568 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73598 72442 603 41 0 73557 0
vsize: 294392
[startup+650.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 74859 0 0 0 64830 179 0 0 25 0 1 0 421847903 305872896 73535 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74676 73535 603 41 0 74635 0
vsize: 298704
[startup+660.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 75788 0 0 0 65828 181 0 0 25 0 1 0 421847903 309669888 74464 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75603 74464 603 41 0 75562 0
vsize: 302412
[startup+670.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 76992 0 0 0 66826 184 0 0 25 0 1 0 421847903 314646528 75668 4294967295 134512640 134672761 3221224560 3221223392 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76818 75668 603 41 0 76777 0
vsize: 307272
[startup+680.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 78009 0 0 0 67824 186 0 0 25 0 1 0 421847903 318808064 76685 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77834 76685 603 41 0 77793 0
vsize: 311336
[startup+690.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 79156 0 0 0 68821 188 0 0 25 0 1 0 421847903 323465216 77832 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78971 77832 603 41 0 78930 0
vsize: 315884
[startup+700.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 80328 0 0 0 69819 191 0 0 25 0 1 0 421847903 328310784 79004 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80154 79004 603 41 0 80113 0
vsize: 320616
[startup+710.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 81290 0 0 0 70817 194 0 0 25 0 1 0 421847903 332140544 79966 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81089 79966 603 41 0 81048 0
vsize: 324356
[startup+720.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 82169 0 0 0 71815 196 0 0 25 0 1 0 421847903 335773696 80845 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81976 80845 603 41 0 81935 0
vsize: 327904
[startup+730.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 82995 0 0 0 72813 198 0 0 25 0 1 0 421847903 339165184 81671 4294967295 134512640 134672761 3221224560 3221223432 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82804 81673 603 41 0 82763 0
vsize: 331216
[startup+740.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 73812 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+750.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 74812 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+760.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 75812 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+770.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 76813 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+780.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 77813 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+790.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 78813 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223600 134613118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+800.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 79813 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+810.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 80813 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+820.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 81813 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+830.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 82814 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+840.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 83814 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+850.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 84814 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+860.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 85814 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+870.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 86815 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+880.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 87815 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+890.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 88815 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+900.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83588 0 0 0 89815 199 0 0 25 0 1 0 421847903 341237760 82071 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82071 603 41 0 83269 0
vsize: 333240
[startup+910.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83589 0 0 0 90815 199 0 0 25 0 1 0 421847903 341237760 82072 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82072 603 41 0 83269 0
vsize: 333240
[startup+920.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83589 0 0 0 91816 199 0 0 25 0 1 0 421847903 341237760 82072 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82072 603 41 0 83269 0
vsize: 333240
[startup+930.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83589 0 0 0 92816 199 0 0 25 0 1 0 421847903 341237760 82072 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82072 603 41 0 83269 0
vsize: 333240
[startup+940.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83589 0 0 0 93816 199 0 0 25 0 1 0 421847903 341237760 82072 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82072 603 41 0 83269 0
vsize: 333240
[startup+950.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83589 0 0 0 94816 199 0 0 25 0 1 0 421847903 341237760 82072 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82072 603 41 0 83269 0
vsize: 333240
[startup+960.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83589 0 0 0 95816 199 0 0 25 0 1 0 421847903 341237760 82072 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82072 603 41 0 83269 0
vsize: 333240
[startup+970.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83589 0 0 0 96816 199 0 0 25 0 1 0 421847903 341237760 82072 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82072 603 41 0 83269 0
vsize: 333240
[startup+980.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83589 0 0 0 97816 199 0 0 25 0 1 0 421847903 341237760 82072 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82072 603 41 0 83269 0
vsize: 333240
[startup+990.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83589 0 0 0 98816 199 0 0 25 0 1 0 421847903 341237760 82072 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82072 603 41 0 83269 0
vsize: 333240
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83589 0 0 0 99816 199 0 0 25 0 1 0 421847903 341237760 82072 4294967295 134512640 134672761 3221224560 3221223600 134612797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82072 603 41 0 83269 0
vsize: 333240
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83589 0 0 0 100816 199 0 0 25 0 1 0 421847903 341237760 82072 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82072 603 41 0 83269 0
vsize: 333240
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83590 0 0 0 101817 199 0 0 25 0 1 0 421847903 341237760 82073 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82073 603 41 0 83269 0
vsize: 333240
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 102817 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 103817 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 104817 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 105818 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 106818 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 107818 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 108818 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 109818 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 110818 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 111819 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 112819 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 113819 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 114819 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 115819 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 116819 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 117820 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 118820 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5678
Raw data (stat): 5621 (minisat+) R 5620 32461 32460 0 -1 0 83591 0 0 0 119820 199 0 0 25 0 1 0 421847903 341237760 82074 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83310 82074 603 41 0 83269 0
vsize: 333240
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 5678
Raw data (stat): 5621 (minisat+) Z 5620 32461 32460 0 -1 12 83592 0 0 0 119821 215 0 0 25 0 1 0 421847903 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.2
CPU time (s): 1200.37
CPU user time (s): 1198.21
CPU system time (s): 2.15467
CPU usage (%): 100.014
Max. virtual memory (Kb): 333240
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####