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 6186

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        840120 kB
Buffers:         35188 kB
Cached:         121996 kB
SwapCached:       3160 kB
Active:          71712 kB
Inactive:        91520 kB
HighTotal:      131008 kB
HighFree:         5572 kB
LowTotal:       903652 kB
LowFree:        834548 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25620 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:02:34 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 4586 7 1200.28 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1437   109318 |     479       0        0     nan |  0.000 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   87214   415673 |   29071       0        0     nan |  0.000 % |
c |       100 |   86997   414918 |   31978      68      418     6.1 |  0.272 % |
c |       251 |   86979   414860 |   35175     217     1338     6.2 |  0.293 % |
c |       476 |   86968   414817 |   38693     441     2357     5.3 |  0.304 % |
c |       814 |   86968   414817 |   42562     779     3691     4.7 |  0.304 % |
c |      1320 |   86936   414713 |   46819    1279     5735     4.5 |  0.337 % |
c |      2079 |   86936   414713 |   51501    2038     8729     4.3 |  0.337 % |
c |      3218 |   86927   414684 |   56651    3176    13620     4.3 |  0.348 % |
c |      4926 |   86911   414632 |   62316    4881    21764     4.5 |  0.364 % |
c |      7488 |   86911   414632 |   68547    7443    43067     5.8 |  0.364 % |
c |     11332 |   86911   414632 |   75402   11287    93912     8.3 |  0.364 % |
c |     17099 |   86911   414632 |   82942   17054  1590252    93.2 |  0.364 % |
c |     25748 |   86911   414632 |   91237   25703  2015498    78.4 |  0.364 % |
c |     38724 |   86911   414632 |  100360   38679  3252791    84.1 |  0.364 % |
c |     58189 |   86911   414632 |  110397   58144  5810744    99.9 |  0.364 % |
c |     87383 |   86911   414632 |  121436   87338 20762972   237.7 |  0.364 % |
c |    131173 |   86911   414632 |  133580   23253  1960308    84.3 |  0.364 % |
c |    196858 |   86911   414632 |  146938   88938 14659528   164.8 |  0.364 % |
c |    295388 |   86911   414632 |  161632   56835  3568955    62.8 |  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 -x5840 -x5841 -x5842 -x5843 -x5844 -x5845 -x5846 -x5847 -x5848 -x5849 -x5850 -x5851 -x5852 -x5853 -x5854 -x5855 -x5856 -x5857 -x5858 -x5859 -x5860 -x5861 -x5862 -x5863 -x5864 -x5865 -x5866 -x5867 -x5868 -x5869 -x5870 -x5871 -x5872 -x5873 -x5874 -x5875 -x5876 -x5877 -x5878 -x5879 -x5880 -x5881 -x5882 -x5883 -x5884 -x5885 -x5886 -x5887 -x5888 -x5889 -x5890 -x5891 -x5892 -x5893 -x5894 -x5895 -x5896 -x5897 -x5898 -x5899 -x5900 -x5901 -x5902 -x5903 -x5904 -x5905 -x5906 -x5907 -x5908 -x5909 -x5910 -x5911 -x5912 -x5913 -x5914 -x5915 -x5916 -x5917 -x5918 -x5919 -x5920 -x5921 -x5922 -x5923 -x5924 -x5925 -x5926 -x5927 -x5928 -x5929 -x5930 -x5931 -x5932 -x5933 -x5934 -x5935 -x5936 -x5937 -x5938 -x5939 -x5940 -x5941 -x5942 -x5943 -x5944 -x5945 -x5946 -x5947 -x5948 -x5949 -x5950 -x5951 -x5952 -x5953 -x5954 -x5955 -x5956 -x5957 -x5958 -x5959 -x5960 -x5961 -x5962 -x5963 -x5964 -x5965 -x5966 -x5967 -x5968 -x5969 -x5970 -x5971 -x5972 -x5973 -x5974 -x5975 -x5976 -x5977 -x5978 -x5979 -x5980 -x5981 -x5982 -x5983 -x5984 -x5985 -x5986 -x5987 -x5988 -x5989 -x5990 -x5991 -x5992 -x5993 -x5994 -x5995 -x5996 -x5997 -x5998 -x5999 -x6000 -x6001 -x6002 -x6003 -x6004 -x6005 -x6006 -x6007 -x6008 -x6009 -x6010 -x6011 -x6012 -x6013 -x6014 -x6015 -x6016 -x6017 -x6018 -x6019 -x6020 -x6021 -x6022 -x6023 -x6024 -x6025 -x6026 -x6027 -x6028 -x6029 -x60#### 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/54 24883
Raw data (stat): 24883 (runsolver) R 24882 18865 18864 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 481434630 1052672 97 4294967295 134512640 135381576 3221224464 3221219864 134516963 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 8612 0 0 0 976 22 0 0 25 0 1 0 481434630 33177600 7391 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8100 7391 603 41 0 8059 0
vsize: 32400
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 8642 0 0 0 1976 22 0 0 25 0 1 0 481434630 33312768 7421 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8133 7421 603 41 0 8092 0
vsize: 32532
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 8679 0 0 0 2976 23 0 0 25 0 1 0 481434630 33447936 7458 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8166 7458 603 41 0 8125 0
vsize: 32664
[startup+40.0026 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 8741 0 0 0 3976 23 0 0 25 0 1 0 481434630 33718272 7520 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8232 7520 603 41 0 8191 0
vsize: 32928
[startup+50.0034 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 8795 0 0 0 4975 24 0 0 25 0 1 0 481434630 33853440 7574 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8265 7574 603 41 0 8224 0
vsize: 33060
[startup+60.0028 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 9561 0 0 0 5973 26 0 0 25 0 1 0 481434630 37085184 8340 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9054 8340 603 41 0 9013 0
vsize: 36216
[startup+70.0038 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 10521 0 0 0 6970 29 0 0 25 0 1 0 481434630 41029632 9300 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10017 9300 603 41 0 9976 0
vsize: 40068
[startup+80.0049 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 11016 0 0 0 7969 30 0 0 25 0 1 0 481434630 43057152 9795 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10512 9795 603 41 0 10471 0
vsize: 42048
[startup+90.0051 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 11730 0 0 0 8967 33 0 0 25 0 1 0 481434630 46014464 10509 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11234 10509 603 41 0 11193 0
vsize: 44936
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 12393 0 0 0 9965 35 0 0 25 0 1 0 481434630 48701440 11172 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11890 11172 603 41 0 11849 0
vsize: 47560
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 12695 0 0 0 10964 36 0 0 25 0 1 0 481434630 49913856 11474 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12186 11474 603 41 0 12145 0
vsize: 48744
[startup+120.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 13171 0 0 0 11963 37 0 0 25 0 1 0 481434630 51929088 11950 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12678 11950 603 41 0 12637 0
vsize: 50712
[startup+130.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 13518 0 0 0 12962 39 0 0 25 0 1 0 481434630 53280768 12297 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13008 12297 603 41 0 12967 0
vsize: 52032
[startup+140.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 14142 0 0 0 13960 41 0 0 25 0 1 0 481434630 55844864 12921 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13634 12921 603 41 0 13593 0
vsize: 54536
[startup+150.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 14523 0 0 0 14958 42 0 0 25 0 1 0 481434630 57462784 13302 4294967295 134512640 134672761 3221224560 3221223744 134559512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14029 13303 603 41 0 13988 0
vsize: 56116
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 15161 0 0 0 15957 44 0 0 25 0 1 0 481434630 60014592 13940 4294967295 134512640 134672761 3221224560 3221223728 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14652 13940 603 41 0 14611 0
vsize: 58608
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 16092 0 0 0 16954 46 0 0 25 0 1 0 481434630 63778816 14871 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15571 14871 603 41 0 15530 0
vsize: 62284
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 17248 0 0 0 17951 49 0 0 25 0 1 0 481434630 68472832 16027 4294967295 134512640 134672761 3221224560 3221223744 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 16027 603 41 0 16676 0
vsize: 66868
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 18414 0 0 0 18947 53 0 0 25 0 1 0 481434630 73572352 17193 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 17193 603 41 0 17921 0
vsize: 71848
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 19477 0 0 0 19946 55 0 0 25 0 1 0 481434630 77856768 18256 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19008 18256 603 41 0 18967 0
vsize: 76032
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 20505 0 0 0 20944 57 0 0 25 0 1 0 481434630 82034688 19284 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20028 19284 603 41 0 19987 0
vsize: 80112
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 21616 0 0 0 21941 60 0 0 25 0 1 0 481434630 86695936 20395 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21166 20395 603 41 0 21125 0
vsize: 84664
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 22646 0 0 0 22938 63 0 0 25 0 1 0 481434630 90828800 21425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22175 21425 603 41 0 22134 0
vsize: 88700
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 23738 0 0 0 23937 65 0 0 25 0 1 0 481434630 95272960 22517 4294967295 134512640 134672761 3221224560 3221223744 134558851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23260 22517 603 41 0 23219 0
vsize: 93040
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 24802 0 0 0 24933 68 0 0 25 0 1 0 481434630 99708928 23581 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24343 23581 603 41 0 24302 0
vsize: 97372
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 25863 0 0 0 25930 72 0 0 25 0 1 0 481434630 104026112 24642 4294967295 134512640 134672761 3221224560 3221223664 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25397 24642 603 41 0 25356 0
vsize: 101588
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 26867 0 0 0 26928 74 0 0 25 0 1 0 481434630 108068864 25646 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26384 25646 603 41 0 26343 0
vsize: 105536
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 27796 0 0 0 27924 78 0 0 25 0 1 0 481434630 111947776 26575 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27331 26575 603 41 0 27290 0
vsize: 109324
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 28838 0 0 0 28923 80 0 0 25 0 1 0 481434630 116252672 27617 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28382 27617 603 41 0 28341 0
vsize: 113528
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 29793 0 0 0 29920 83 0 0 25 0 1 0 481434630 120164352 28572 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29337 28572 603 41 0 29296 0
vsize: 117348
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 30380 0 0 0 30918 84 0 0 25 0 1 0 481434630 122441728 29159 4294967295 134512640 134672761 3221224560 3221223728 134564490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 29159 603 41 0 29852 0
vsize: 119572
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 30965 0 0 0 31917 86 0 0 25 0 1 0 481434630 124870656 29744 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30486 29744 603 41 0 30445 0
vsize: 121944
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 31419 0 0 0 32916 87 0 0 25 0 1 0 481434630 126754816 30198 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30946 30198 603 41 0 30905 0
vsize: 123784
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 32111 0 0 0 33914 89 0 0 25 0 1 0 481434630 129581056 30890 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31636 30890 603 41 0 31595 0
vsize: 126544
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 32737 0 0 0 34912 91 0 0 25 0 1 0 481434630 132136960 31516 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32260 31516 603 41 0 32219 0
vsize: 129040
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 33477 0 0 0 35910 93 0 0 25 0 1 0 481434630 135114752 32256 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32987 32256 603 41 0 32946 0
vsize: 131948
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 34614 0 0 0 36907 96 0 0 25 0 1 0 481434630 139829248 33393 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34138 33393 603 41 0 34097 0
vsize: 136552
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 35643 0 0 0 37904 99 0 0 25 0 1 0 481434630 144027648 34422 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35163 34422 603 41 0 35122 0
vsize: 140652
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 36651 0 0 0 38902 102 0 0 25 0 1 0 481434630 148099072 35430 4294967295 134512640 134672761 3221224560 3221223684 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36157 35430 603 41 0 36116 0
vsize: 144628
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 37257 0 0 0 39900 103 0 0 25 0 1 0 481434630 150519808 36036 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36748 36036 603 41 0 36707 0
vsize: 146992
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 37990 0 0 0 40898 106 0 0 25 0 1 0 481434630 153612288 36769 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37503 36769 603 41 0 37462 0
vsize: 150012
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 38717 0 0 0 41896 109 0 0 25 0 1 0 481434630 156573696 37496 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38226 37496 603 41 0 38185 0
vsize: 152904
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 42893 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 43893 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 44893 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 45893 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 46893 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 47894 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 48894 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 49894 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 50894 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 51894 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223744 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 52894 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 53894 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 54894 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 55895 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 56895 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 57895 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 58895 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 59895 112 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 60895 113 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39165 0 0 0 61895 113 0 0 25 0 1 0 481434630 158334976 37944 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38656 37944 603 41 0 38615 0
vsize: 154624
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39166 0 0 0 62894 113 0 0 25 0 1 0 481434630 158334976 37945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37945 603 41 0 38615 0
vsize: 154624
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39166 0 0 0 63894 113 0 0 25 0 1 0 481434630 158334976 37945 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37945 603 41 0 38615 0
vsize: 154624
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39166 0 0 0 64894 113 0 0 25 0 1 0 481434630 158334976 37945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37945 603 41 0 38615 0
vsize: 154624
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39166 0 0 0 65895 113 0 0 25 0 1 0 481434630 158334976 37945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37945 603 41 0 38615 0
vsize: 154624
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39166 0 0 0 66895 113 0 0 25 0 1 0 481434630 158334976 37945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37945 603 41 0 38615 0
vsize: 154624
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39166 0 0 0 67895 113 0 0 25 0 1 0 481434630 158334976 37945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38656 37945 603 41 0 38615 0
vsize: 154624
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39170 0 0 0 68895 113 0 0 25 0 1 0 481434630 158859264 37949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37949 603 41 0 38743 0
vsize: 155136
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39174 0 0 0 69895 113 0 0 25 0 1 0 481434630 158859264 37953 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37953 603 41 0 38743 0
vsize: 155136
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39177 0 0 0 70895 114 0 0 25 0 1 0 481434630 158859264 37956 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37956 603 41 0 38743 0
vsize: 155136
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39182 0 0 0 71895 114 0 0 25 0 1 0 481434630 158859264 37961 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37961 603 41 0 38743 0
vsize: 155136
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39187 0 0 0 72895 114 0 0 25 0 1 0 481434630 158859264 37966 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37966 603 41 0 38743 0
vsize: 155136
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39191 0 0 0 73896 114 0 0 25 0 1 0 481434630 158859264 37970 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37970 603 41 0 38743 0
vsize: 155136
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 74896 114 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223664 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 75896 114 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 76896 114 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 77896 114 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 78896 114 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 79896 114 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 80896 114 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 81896 114 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 82895 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 83895 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 84895 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 85895 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223696 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 86896 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223744 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 87896 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 88896 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 89896 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+910.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 90896 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 91896 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 92896 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 93897 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 94897 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+960.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 95897 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 96897 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 97897 115 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+990.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 98897 116 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 99898 116 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 100898 116 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 101898 116 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 102898 116 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 103898 116 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24883
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 104898 116 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+1060.03 s]
Raw data (loadavg): 1.23 1.02 0.93 2/54 24936
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 105898 117 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+1070.03 s]
Raw data (loadavg): 1.20 1.02 0.93 2/54 24936
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 106898 117 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+1080.03 s]
Raw data (loadavg): 1.17 1.02 0.93 2/54 24936
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 107898 117 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+1090.03 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 24936
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39193 0 0 0 108898 117 0 0 25 0 1 0 481434630 158859264 37972 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38784 37972 603 41 0 38743 0
vsize: 155136
[startup+1100.03 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 24936
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 39816 0 0 0 109897 118 0 0 25 0 1 0 481434630 161443840 38595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39415 38595 603 41 0 39374 0
vsize: 157660
[startup+1110.03 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 24936
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 40839 0 0 0 110895 121 0 0 25 0 1 0 481434630 165629952 39618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40437 39618 603 41 0 40396 0
vsize: 161748
[startup+1120.03 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 24936
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 41851 0 0 0 111893 122 0 0 25 0 1 0 481434630 169824256 40630 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41461 40630 603 41 0 41420 0
vsize: 165844
[startup+1130.03 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 24938
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 42805 0 0 0 112891 124 0 0 25 0 1 0 481434630 173744128 41584 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42418 41584 603 41 0 42377 0
vsize: 169672
[startup+1140.03 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 24938
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 43745 0 0 0 113888 127 0 0 25 0 1 0 481434630 177520640 42524 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43340 42524 603 41 0 43299 0
vsize: 173360
[startup+1150.03 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 24938
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 44800 0 0 0 114887 129 0 0 25 0 1 0 481434630 181850112 43579 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44397 43579 603 41 0 44356 0
vsize: 177588
[startup+1160.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 24938
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 45852 0 0 0 115884 132 0 0 25 0 1 0 481434630 186138624 44631 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45444 44631 603 41 0 45403 0
vsize: 181776
[startup+1170.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 24938
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 46842 0 0 0 116882 134 0 0 25 0 1 0 481434630 190201856 45621 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46436 45621 603 41 0 46395 0
vsize: 185744
[startup+1180.03 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 24938
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 47665 0 0 0 117880 136 0 0 25 0 1 0 481434630 193593344 46444 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47264 46444 603 41 0 47223 0
vsize: 189056
[startup+1190.03 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 24938
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 48456 0 0 0 118878 139 0 0 25 0 1 0 481434630 196870144 47235 4294967295 134512640 134672761 3221224560 3221223744 134558836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48064 47235 603 41 0 48023 0
vsize: 192256
[startup+1200.03 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 24938
Raw data (stat): 24883 (minisat+) R 24882 18865 18864 0 -1 0 49220 0 0 0 119876 141 0 0 25 0 1 0 481434630 199962624 47999 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48819 47999 603 41 0 48778 0
vsize: 195276
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.02 1.01 0.93 1/54 24938
Raw data (stat): 24883 (minisat+) Z 24882 18865 18864 0 -1 12 49223 0 0 0 119877 150 0 0 25 0 1 0 481434630 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.14
CPU time (s): 1200.28
CPU user time (s): 1198.78
CPU system time (s): 1.50277
CPU usage (%): 100.012
Max. virtual memory (Kb): 195276
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####