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-exam.pi.opb
MD5SUM	3e917561f3935db250fdeb1759fbe81d
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63
Optimality of the best value was proved	NO
Number of terms in the objective function	4677
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	4677
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	4677
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	1.06784
Number of variables	4676
Total number of constraints	509
Number of constraints which are clauses	509
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	3
Maximum length of a constraint	166
Trace number 6174

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        889028 kB
Buffers:         35008 kB
Cached:          67616 kB
SwapCached:        192 kB
Active:          54372 kB
Inactive:        51252 kB
HighTotal:      131008 kB
HighFree:        59640 kB
LowTotal:       903652 kB
LowFree:        829388 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34456 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:59:11 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 4580 7 1200.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 509 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 |     509    25694 |     169       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 90[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 9344   maxlim: 4587   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   65831   258983 |   21943       0        0     nan |  0.000 % |
c |       101 |   65771   258779 |   24137      92      325     3.5 |  0.157 % |
c |       253 |   65765   258759 |   26551     243     1153     4.7 |  0.164 % |
c |       478 |   65765   258759 |   29206     468     2078     4.4 |  0.164 % |
c |       815 |   65765   258759 |   32126     805     3385     4.2 |  0.164 % |
c |      1322 |   65739   258669 |   35339    1308     5348     4.1 |  0.193 % |
c |      2081 |   65730   258638 |   38873    2063     8542     4.1 |  0.200 % |
c |      3220 |   65730   258638 |   42760    3202    23350     7.3 |  0.200 % |
c |      4931 |   65706   258556 |   47036    4906    82763    16.9 |  0.221 % |
c |      7493 |   65680   258466 |   51740    7462   253235    33.9 |  0.250 % |
c |     11337 |   65657   258387 |   56914   11303   698887    61.8 |  0.278 % |
c |     17104 |   65649   258357 |   62605   17069  1950190   114.3 |  0.285 % |
c |     25755 |   65640   258326 |   68866   25717  4100172   159.4 |  0.292 % |
c |     38730 |   65549   258014 |   75753   38672  8468844   219.0 |  0.406 % |
c |     58191 |   65457   257698 |   83328   58116 14958010   257.4 |  0.520 % |
c |     87384 |   65457   257698 |   91661   19586  7284940   371.9 |  0.520 % |
c |    131174 |   65457   257698 |  100827   63376 20020994   315.9 |  0.520 % |
c |    196862 |   65437   257630 |  110910   44851 15497139   345.5 |  0.549 % |
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 -x42#### 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.99 0.93 2/54 8160
Raw data (stat): 8160 (runsolver) R 8159 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481415559 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.0005 s]
Raw data (loadavg): 0.93 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 7268 0 0 0 978 19 0 0 25 0 1 0 481415559 28102656 5922 4294967295 134512640 134672761 3221224560 3221223684 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6861 5922 603 41 0 6820 0
vsize: 27444
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 7903 0 0 0 1976 22 0 0 25 0 1 0 481415559 30666752 6557 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7487 6557 603 41 0 7446 0
vsize: 29948
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 8947 0 0 0 2973 25 0 0 25 0 1 0 481415559 34979840 7601 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8540 7601 603 41 0 8499 0
vsize: 34160
[startup+40.0012 s]
Raw data (loadavg): 0.96 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 10062 0 0 0 3970 28 0 0 25 0 1 0 481415559 39522304 8716 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9649 8716 603 41 0 9608 0
vsize: 38596
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 11080 0 0 0 4966 31 0 0 25 0 1 0 481415559 43683840 9734 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10665 9734 603 41 0 10624 0
vsize: 42660
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 11817 0 0 0 5964 33 0 0 25 0 1 0 481415559 46772224 10471 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11419 10471 603 41 0 11378 0
vsize: 45676
[startup+70.0022 s]
Raw data (loadavg): 0.97 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 12937 0 0 0 6962 36 0 0 25 0 1 0 481415559 51351552 11591 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12537 11591 603 41 0 12496 0
vsize: 50148
[startup+80.0021 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 14085 0 0 0 7960 38 0 0 25 0 1 0 481415559 56197120 12739 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13720 12739 603 41 0 13679 0
vsize: 54880
[startup+90.0014 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 15107 0 0 0 8957 42 0 0 25 0 1 0 481415559 60358656 13761 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14736 13761 603 41 0 14695 0
vsize: 58944
[startup+100.001 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 16139 0 0 0 9952 46 0 0 25 0 1 0 481415559 64524288 14793 4294967295 134512640 134672761 3221224560 3221223664 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15753 14793 603 41 0 15712 0
vsize: 63012
[startup+110.001 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 17023 0 0 0 10950 48 0 0 25 0 1 0 481415559 68161536 15677 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16641 15677 603 41 0 16600 0
vsize: 66564
[startup+120.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 17931 0 0 0 11948 50 0 0 25 0 1 0 481415559 71794688 16585 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17528 16585 603 41 0 17487 0
vsize: 70112
[startup+130.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 18746 0 0 0 12946 53 0 0 25 0 1 0 481415559 75165696 17400 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18351 17400 603 41 0 18310 0
vsize: 73404
[startup+140.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 19589 0 0 0 13946 53 0 0 25 0 1 0 481415559 78663680 18243 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19205 18243 603 41 0 19164 0
vsize: 76820
[startup+150.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 20450 0 0 0 14944 55 0 0 25 0 1 0 481415559 82157568 19104 4294967295 134512640 134672761 3221224560 3221223664 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20058 19104 603 41 0 20017 0
vsize: 80232
[startup+160.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 21404 0 0 0 15942 57 0 0 25 0 1 0 481415559 86065152 20058 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21012 20058 603 41 0 20971 0
vsize: 84048
[startup+170.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 22190 0 0 0 16941 59 0 0 25 0 1 0 481415559 89292800 20844 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21800 20844 603 41 0 21759 0
vsize: 87200
[startup+180.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 22879 0 0 0 17939 61 0 0 25 0 1 0 481415559 92127232 21533 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22492 21533 603 41 0 22451 0
vsize: 89968
[startup+190 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 23415 0 0 0 18938 62 0 0 25 0 1 0 481415559 94289920 22069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23020 22069 603 41 0 22979 0
vsize: 92080
[startup+200 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 24035 0 0 0 19936 64 0 0 25 0 1 0 481415559 96714752 22689 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23612 22689 603 41 0 23571 0
vsize: 94448
[startup+209.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 24799 0 0 0 20934 66 0 0 25 0 1 0 481415559 100208640 23453 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24465 23453 603 41 0 24424 0
vsize: 97860
[startup+220 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 25587 0 0 0 21932 68 0 0 25 0 1 0 481415559 103415808 24241 4294967295 134512640 134672761 3221224560 3221223712 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25248 24241 603 41 0 25207 0
vsize: 100992
[startup+229.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 26481 0 0 0 22930 70 0 0 25 0 1 0 481415559 107028480 25135 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26130 25135 603 41 0 26089 0
vsize: 104520
[startup+239.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 27372 0 0 0 23929 72 0 0 25 0 1 0 481415559 110620672 26026 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27007 26026 603 41 0 26966 0
vsize: 108028
[startup+250 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 28239 0 0 0 24927 74 0 0 25 0 1 0 481415559 114257920 26893 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27895 26893 603 41 0 27854 0
vsize: 111580
[startup+260 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 29011 0 0 0 25925 76 0 0 25 0 1 0 481415559 117346304 27665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28649 27665 603 41 0 28608 0
vsize: 114596
[startup+270 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 29710 0 0 0 26922 79 0 0 25 0 1 0 481415559 120283136 28364 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29366 28364 603 41 0 29325 0
vsize: 117464
[startup+280 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 30430 0 0 0 27921 81 0 0 25 0 1 0 481415559 123224064 29084 4294967295 134512640 134672761 3221224560 3221223728 134559063 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30084 29084 603 41 0 30043 0
vsize: 120336
[startup+289.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 31028 0 0 0 28919 82 0 0 25 0 1 0 481415559 125620224 29682 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30669 29682 603 41 0 30628 0
vsize: 122676
[startup+299.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 31674 0 0 0 29918 84 0 0 25 0 1 0 481415559 128307200 30328 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31325 30328 603 41 0 31284 0
vsize: 125300
[startup+309.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 32352 0 0 0 30917 85 0 0 25 0 1 0 481415559 131125248 31006 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32013 31006 603 41 0 31972 0
vsize: 128052
[startup+320 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 32894 0 0 0 31916 86 0 0 25 0 1 0 481415559 133271552 31548 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32537 31548 603 41 0 32496 0
vsize: 130148
[startup+329.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33465 0 0 0 32915 87 0 0 25 0 1 0 481415559 135688192 32119 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33127 32119 603 41 0 33086 0
vsize: 132508
[startup+339.998 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 33914 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223664 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+349.998 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 34914 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223712 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+359.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 35914 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223664 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+369.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 36914 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+379.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 37915 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+389.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 38915 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+399.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 39915 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+409.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 40915 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+420 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 41915 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+430 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 42915 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223744 134559274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+440 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 43916 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+450.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 44916 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+460.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 45916 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223664 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+470.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 46916 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+480.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 47916 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+490 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 48917 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+500 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 49917 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+510 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33847 0 0 0 50917 88 0 0 25 0 1 0 481415559 137154560 32501 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32501 603 41 0 33444 0
vsize: 133940
[startup+520 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33848 0 0 0 51916 88 0 0 25 0 1 0 481415559 137154560 32502 4294967295 134512640 134672761 3221224560 3221223684 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32502 603 41 0 33444 0
vsize: 133940
[startup+530 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33848 0 0 0 52917 88 0 0 25 0 1 0 481415559 137154560 32502 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32502 603 41 0 33444 0
vsize: 133940
[startup+540 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33848 0 0 0 53917 88 0 0 25 0 1 0 481415559 137154560 32502 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32502 603 41 0 33444 0
vsize: 133940
[startup+550 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33848 0 0 0 54917 88 0 0 25 0 1 0 481415559 137154560 32502 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32502 603 41 0 33444 0
vsize: 133940
[startup+560 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33848 0 0 0 55917 88 0 0 25 0 1 0 481415559 137154560 32502 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32502 603 41 0 33444 0
vsize: 133940
[startup+570.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33848 0 0 0 56917 88 0 0 25 0 1 0 481415559 137154560 32502 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32502 603 41 0 33444 0
vsize: 133940
[startup+580.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 33848 0 0 0 57918 88 0 0 25 0 1 0 481415559 137154560 32502 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33485 32502 603 41 0 33444 0
vsize: 133940
[startup+590.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 34705 0 0 0 58915 91 0 0 25 0 1 0 481415559 140726272 33359 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34357 33359 603 41 0 34316 0
vsize: 137428
[startup+600 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 35678 0 0 0 59914 92 0 0 25 0 1 0 481415559 144723968 34332 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35333 34332 603 41 0 35292 0
vsize: 141332
[startup+610.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 36303 0 0 0 60913 93 0 0 25 0 1 0 481415559 147267584 34957 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35954 34957 603 41 0 35913 0
vsize: 143816
[startup+620.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 36988 0 0 0 61912 95 0 0 25 0 1 0 481415559 150056960 35642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36635 35642 603 41 0 36594 0
vsize: 146540
[startup+630.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 37510 0 0 0 62911 96 0 0 25 0 1 0 481415559 152182784 36164 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37154 36164 603 41 0 37113 0
vsize: 148616
[startup+640.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 38083 0 0 0 63910 97 0 0 25 0 1 0 481415559 154607616 36737 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37746 36737 603 41 0 37705 0
vsize: 150984
[startup+650 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 38665 0 0 0 64909 98 0 0 25 0 1 0 481415559 156889088 37319 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38303 37319 603 41 0 38262 0
vsize: 153212
[startup+660 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 39273 0 0 0 65908 99 0 0 25 0 1 0 481415559 159436800 37927 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38925 37927 603 41 0 38884 0
vsize: 155700
[startup+670.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 40047 0 0 0 66907 101 0 0 25 0 1 0 481415559 162512896 38701 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39676 38701 603 41 0 39635 0
vsize: 158704
[startup+680.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 40851 0 0 0 67905 103 0 0 25 0 1 0 481415559 165867520 39505 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40495 39505 603 41 0 40454 0
vsize: 161980
[startup+690 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 41686 0 0 0 68903 104 0 0 25 0 1 0 481415559 169332736 40340 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41341 40340 603 41 0 41300 0
vsize: 165364
[startup+700.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 42275 0 0 0 69902 106 0 0 25 0 1 0 481415559 171732992 40929 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41927 40929 603 41 0 41886 0
vsize: 167708
[startup+710 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 42699 0 0 0 70902 106 0 0 25 0 1 0 481415559 173490176 41353 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42356 41353 603 41 0 42315 0
vsize: 169424
[startup+720.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 43249 0 0 0 71901 108 0 0 25 0 1 0 481415559 175644672 41903 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42882 41903 603 41 0 42841 0
vsize: 171528
[startup+730.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 43787 0 0 0 72900 109 0 0 25 0 1 0 481415559 177930240 42441 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43440 42441 603 41 0 43399 0
vsize: 173760
[startup+740.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 44303 0 0 0 73899 110 0 0 25 0 1 0 481415559 179929088 42957 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43928 42957 603 41 0 43887 0
vsize: 175712
[startup+750.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 44848 0 0 0 74899 110 0 0 25 0 1 0 481415559 182202368 43502 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44483 43502 603 41 0 44442 0
vsize: 177932
[startup+760.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45361 0 0 0 75898 111 0 0 25 0 1 0 481415559 184352768 44015 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45008 44015 603 41 0 44967 0
vsize: 180032
[startup+770.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45884 0 0 0 76897 112 0 0 25 0 1 0 481415559 186372096 44538 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45501 44538 603 41 0 45460 0
vsize: 182004
[startup+780.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45914 0 0 0 77897 112 0 0 25 0 1 0 481415559 186507264 44568 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44568 603 41 0 45493 0
vsize: 182136
[startup+790.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45914 0 0 0 78898 112 0 0 25 0 1 0 481415559 186507264 44568 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44568 603 41 0 45493 0
vsize: 182136
[startup+800.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45914 0 0 0 79898 112 0 0 25 0 1 0 481415559 186507264 44568 4294967295 134512640 134672761 3221224560 3221223744 134559400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44568 603 41 0 45493 0
vsize: 182136
[startup+810.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45914 0 0 0 80898 112 0 0 25 0 1 0 481415559 186507264 44568 4294967295 134512640 134672761 3221224560 3221223664 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44568 603 41 0 45493 0
vsize: 182136
[startup+820.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45914 0 0 0 81898 112 0 0 25 0 1 0 481415559 186507264 44568 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44568 603 41 0 45493 0
vsize: 182136
[startup+830.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45914 0 0 0 82898 112 0 0 25 0 1 0 481415559 186507264 44568 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44568 603 41 0 45493 0
vsize: 182136
[startup+840.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45914 0 0 0 83898 112 0 0 25 0 1 0 481415559 186507264 44568 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44568 603 41 0 45493 0
vsize: 182136
[startup+850.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45914 0 0 0 84899 112 0 0 25 0 1 0 481415559 186507264 44568 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44568 603 41 0 45493 0
vsize: 182136
[startup+860.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45914 0 0 0 85899 112 0 0 25 0 1 0 481415559 186507264 44568 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44568 603 41 0 45493 0
vsize: 182136
[startup+870.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45914 0 0 0 86899 112 0 0 25 0 1 0 481415559 186507264 44568 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44568 603 41 0 45493 0
vsize: 182136
[startup+880.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45914 0 0 0 87899 112 0 0 25 0 1 0 481415559 186507264 44568 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44568 603 41 0 45493 0
vsize: 182136
[startup+890.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 88899 112 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+900.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 89899 112 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223692 1075347104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+910.001 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 90899 112 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+920.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 91899 112 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+930.003 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 92899 112 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223744 134558754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+940.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 93899 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+950.002 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 94899 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+960.003 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 95899 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+970.003 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 96899 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+980.003 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 97899 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+990.004 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 98900 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1000 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 99900 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1010 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 100900 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1020 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 101900 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1030 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 102900 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 103901 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 104901 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 105901 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223744 134558771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 106901 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 107901 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1090 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 108901 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 109902 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 110902 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 111902 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 112902 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 113903 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 114903 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223664 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 115903 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223744 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 116903 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 117903 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 118903 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8160
Raw data (stat): 8160 (minisat+) R 8159 3260 3259 0 -1 0 45915 0 0 0 119904 113 0 0 25 0 1 0 481415559 186507264 44569 4294967295 134512640 134672761 3221224560 3221223724 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45534 44569 603 41 0 45493 0
vsize: 182136
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.99 0.93 1/54 8160
Raw data (stat): 8160 (minisat+) Z 8159 3260 3259 0 -1 12 45918 0 0 0 119904 121 0 0 25 0 1 0 481415559 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.1
CPU time (s): 1200.27
CPU user time (s): 1199.05
CPU system time (s): 1.21681
CPU usage (%): 100.013
Max. virtual memory (Kb): 182136
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####