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 5803

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-14 01:51:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4204 boxname=wulflinc23 idbench=68 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3e917561f3935db250fdeb1759fbe81d  /oldhome/oroussel/tmp/wulflinc23/normalized-exam.pi.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-exam.pi.opb /oldhome/oroussel/tmp/wulflinc23/normalized-exam.pi.opb
IDLAUNCH: 4204
/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:        893492 kB
Buffers:         34864 kB
Cached:          63408 kB
SwapCached:        192 kB
Active:          53156 kB
Inactive:        48212 kB
HighTotal:      131008 kB
HighFree:        63784 kB
LowTotal:       903652 kB
LowFree:        829708 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34340 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:11:15 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 4204 7 1200.16 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]---> Sorter-cost:364364     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  424371  1015092 |  141457       0        0     nan |  0.000 % |
c |       101 |  424036  1014408 |  155602      92     2161    23.5 |  0.058 % |
c |       251 |  424036  1014408 |  171162     242     6787    28.0 |  0.058 % |
c |       476 |  423968  1014268 |  188279     466    16860    36.2 |  0.067 % |
c |       813 |  423968  1014268 |  207107     803    59732    74.4 |  0.067 % |
c |      1319 |  423968  1014268 |  227817    1309    94229    72.0 |  0.067 % |
c |      2078 |  423968  1014268 |  250599    2068   157551    76.2 |  0.067 % |
c |      3217 |  423968  1014268 |  275659    3207   325686   101.6 |  0.067 % |
c |      4925 |  423935  1014197 |  303225    4911   492482   100.3 |  0.074 % |
c |      7488 |  423935  1014197 |  333548    7474   687932    92.0 |  0.074 % |
c |     11332 |  423935  1014197 |  366903   11318  1459826   129.0 |  0.074 % |
c |     17098 |  423935  1014197 |  403593   17084  2012764   117.8 |  0.074 % |
c |     25747 |  423935  1014197 |  443952   25733  3866374   150.2 |  0.074 % |
c |     38724 |  423935  1014197 |  488347   38710  5530301   142.9 |  0.074 % |
c |     58186 |  423935  1014197 |  537182   58172  8900608   153.0 |  0.074 % |
c |     87380 |  423935  1014197 |  590900   87366 16385719   187.6 |  0.074 % |
c |    131169 |  423913  1014149 |  649991  131150 19718597   150.4 |  0.079 % |
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.91 0.95 0.90 2/54 7323
Raw data (stat): 7323 (runsolver) R 7322 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480767865 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0004 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 21961 0 0 0 943 55 0 0 25 0 1 0 480767865 104542208 20635 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25523 20635 603 41 0 25482 0
vsize: 102092
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 22186 0 0 0 1941 56 0 0 25 0 1 0 480767865 105345024 20860 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25719 20860 603 41 0 25678 0
vsize: 102876
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 22559 0 0 0 2939 58 0 0 25 0 1 0 480767865 106823680 21233 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26080 21233 603 41 0 26039 0
vsize: 104320
[startup+40.0025 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 22669 0 0 0 3938 59 0 0 25 0 1 0 480767865 107356160 21343 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26210 21343 603 41 0 26169 0
vsize: 104840
[startup+50.0036 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 22882 0 0 0 4937 60 0 0 25 0 1 0 480767865 108220416 21556 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26421 21556 603 41 0 26380 0
vsize: 105684
[startup+60.0042 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 23552 0 0 0 5933 63 0 0 25 0 1 0 480767865 110915584 22226 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27079 22226 603 41 0 27038 0
vsize: 108316
[startup+70.0044 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 23852 0 0 0 6932 64 0 0 25 0 1 0 480767865 112132096 22526 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27376 22526 603 41 0 27335 0
vsize: 109504
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 24039 0 0 0 7931 65 0 0 25 0 1 0 480767865 112939008 22713 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27573 22713 603 41 0 27532 0
vsize: 110292
[startup+90.0051 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 24289 0 0 0 8930 66 0 0 25 0 1 0 480767865 113987584 22963 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27829 22963 603 41 0 27788 0
vsize: 111316
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 24441 0 0 0 9928 67 0 0 25 0 1 0 480767865 114528256 23115 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27961 23115 603 41 0 27920 0
vsize: 111844
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 24792 0 0 0 10927 69 0 0 25 0 1 0 480767865 116002816 23466 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28321 23466 603 41 0 28280 0
vsize: 113284
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 25205 0 0 0 11926 70 0 0 25 0 1 0 480767865 117751808 23879 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28748 23879 603 41 0 28707 0
vsize: 114992
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 25321 0 0 0 12925 71 0 0 25 0 1 0 480767865 118153216 23995 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28846 23995 603 41 0 28805 0
vsize: 115384
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 25414 0 0 0 13924 72 0 0 25 0 1 0 480767865 118554624 24088 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28944 24088 603 41 0 28903 0
vsize: 115776
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 25513 0 0 0 14923 73 0 0 25 0 1 0 480767865 118960128 24187 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29043 24187 603 41 0 29002 0
vsize: 116172
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 25638 0 0 0 15922 73 0 0 25 0 1 0 480767865 119492608 24312 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29173 24312 603 41 0 29132 0
vsize: 116692
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 25781 0 0 0 16921 74 0 0 25 0 1 0 480767865 120029184 24455 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29304 24455 603 41 0 29263 0
vsize: 117216
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 26071 0 0 0 17921 75 0 0 25 0 1 0 480767865 121241600 24745 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29600 24745 603 41 0 29559 0
vsize: 118400
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 26373 0 0 0 18919 76 0 0 25 0 1 0 480767865 122454016 25047 4294967295 134512640 134672761 3221224560 3221223684 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29896 25047 603 41 0 29855 0
vsize: 119584
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 26540 0 0 0 19918 77 0 0 25 0 1 0 480767865 123125760 25214 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30060 25214 603 41 0 30019 0
vsize: 120240
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 26692 0 0 0 20917 78 0 0 25 0 1 0 480767865 123797504 25366 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30224 25366 603 41 0 30183 0
vsize: 120896
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 26926 0 0 0 21915 80 0 0 25 0 1 0 480767865 124735488 25600 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30453 25600 603 41 0 30412 0
vsize: 121812
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 27182 0 0 0 22914 81 0 0 25 0 1 0 480767865 125808640 25856 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30715 25856 603 41 0 30674 0
vsize: 122860
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 27398 0 0 0 23912 83 0 0 25 0 1 0 480767865 126742528 26072 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30943 26072 603 41 0 30902 0
vsize: 123772
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 27868 0 0 0 24910 85 0 0 25 0 1 0 480767865 128622592 26542 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31402 26542 603 41 0 31361 0
vsize: 125608
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 28070 0 0 0 25909 86 0 0 25 0 1 0 480767865 129429504 26744 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31599 26744 603 41 0 31558 0
vsize: 126396
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 28302 0 0 0 26908 87 0 0 25 0 1 0 480767865 130375680 26976 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31830 26976 603 41 0 31789 0
vsize: 127320
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 28492 0 0 0 27907 88 0 0 25 0 1 0 480767865 131182592 27166 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32027 27166 603 41 0 31986 0
vsize: 128108
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 28714 0 0 0 28906 89 0 0 25 0 1 0 480767865 132112384 27388 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32254 27388 603 41 0 32213 0
vsize: 129016
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 29156 0 0 0 29904 90 0 0 25 0 1 0 480767865 133857280 27830 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32680 27830 603 41 0 32639 0
vsize: 130720
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 29675 0 0 0 30903 92 0 0 25 0 1 0 480767865 136007680 28349 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33205 28349 603 41 0 33164 0
vsize: 132820
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 30042 0 0 0 31901 94 0 0 25 0 1 0 480767865 137482240 28716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33565 28716 603 41 0 33524 0
vsize: 134260
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 30481 0 0 0 32900 95 0 0 25 0 1 0 480767865 139362304 29155 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34024 29155 603 41 0 33983 0
vsize: 136096
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 30967 0 0 0 33897 98 0 0 25 0 1 0 480767865 141238272 29641 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34482 29641 603 41 0 34441 0
vsize: 137928
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 31389 0 0 0 34895 99 0 0 25 0 1 0 480767865 142983168 30063 4294967295 134512640 134672761 3221224560 3221223664 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34908 30063 603 41 0 34867 0
vsize: 139632
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 31739 0 0 0 35893 102 0 0 25 0 1 0 480767865 144449536 30413 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35266 30413 603 41 0 35225 0
vsize: 141064
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 32022 0 0 0 36892 103 0 0 25 0 1 0 480767865 145653760 30696 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35560 30696 603 41 0 35519 0
vsize: 142240
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 32298 0 0 0 37891 104 0 0 25 0 1 0 480767865 146726912 30972 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35822 30972 603 41 0 35781 0
vsize: 143288
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 32611 0 0 0 38889 105 0 0 25 0 1 0 480767865 147935232 31285 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36117 31285 603 41 0 36076 0
vsize: 144468
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 32959 0 0 0 39888 107 0 0 25 0 1 0 480767865 149676032 31633 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36542 31633 603 41 0 36501 0
vsize: 146168
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 33345 0 0 0 40885 109 0 0 25 0 1 0 480767865 151285760 32019 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36935 32019 603 41 0 36894 0
vsize: 147740
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 33562 0 0 0 41884 110 0 0 25 0 1 0 480767865 152092672 32236 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37132 32236 603 41 0 37091 0
vsize: 148528
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 33801 0 0 0 42883 111 0 0 25 0 1 0 480767865 153038848 32475 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37363 32475 603 41 0 37322 0
vsize: 149452
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 34002 0 0 0 43882 113 0 0 25 0 1 0 480767865 153980928 32676 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37593 32676 603 41 0 37552 0
vsize: 150372
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 34516 0 0 0 44880 114 0 0 25 0 1 0 480767865 156000256 33190 4294967295 134512640 134672761 3221224560 3221223744 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38086 33190 603 41 0 38045 0
vsize: 152344
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 35104 0 0 0 45878 117 0 0 25 0 1 0 480767865 158400512 33778 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38672 33778 603 41 0 38631 0
vsize: 154688
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 35645 0 0 0 46875 119 0 0 25 0 1 0 480767865 160669696 34319 4294967295 134512640 134672761 3221224560 3221223744 134558885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39226 34319 603 41 0 39185 0
vsize: 156904
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 36306 0 0 0 47873 121 0 0 25 0 1 0 480767865 163364864 34980 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39884 34980 603 41 0 39843 0
vsize: 159536
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 36903 0 0 0 48871 123 0 0 25 0 1 0 480767865 165789696 35577 4294967295 134512640 134672761 3221224560 3221223744 134558775 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40476 35577 603 41 0 40435 0
vsize: 161904
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 37529 0 0 0 49870 125 0 0 25 0 1 0 480767865 168337408 36203 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41098 36203 603 41 0 41057 0
vsize: 164392
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 38111 0 0 0 50867 127 0 0 25 0 1 0 480767865 170762240 36785 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41690 36785 603 41 0 41649 0
vsize: 166760
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 38672 0 0 0 51865 129 0 0 25 0 1 0 480767865 173043712 37346 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42247 37346 603 41 0 42206 0
vsize: 168988
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7323
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 39195 0 0 0 52863 132 0 0 25 0 1 0 480767865 175185920 37869 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42770 37869 603 41 0 42729 0
vsize: 171080
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7376
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 39483 0 0 0 53858 133 0 0 25 0 1 0 480767865 176271360 38157 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43035 38157 603 41 0 42994 0
vsize: 172140
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7376
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 39585 0 0 0 54858 133 0 0 25 0 1 0 480767865 176672768 38259 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43133 38259 603 41 0 43092 0
vsize: 172532
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7376
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 39684 0 0 0 55858 134 0 0 25 0 1 0 480767865 177074176 38358 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43231 38358 603 41 0 43190 0
vsize: 172924
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7376
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 39749 0 0 0 56858 134 0 0 25 0 1 0 480767865 177340416 38423 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43296 38423 603 41 0 43255 0
vsize: 173184
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7376
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 39831 0 0 0 57858 134 0 0 25 0 1 0 480767865 177733632 38505 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43392 38505 603 41 0 43351 0
vsize: 173568
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7376
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 39940 0 0 0 58858 134 0 0 25 0 1 0 480767865 178130944 38614 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43489 38614 603 41 0 43448 0
vsize: 173956
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7376
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 40105 0 0 0 59857 135 0 0 25 0 1 0 480767865 178806784 38779 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43654 38779 603 41 0 43613 0
vsize: 174616
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 40390 0 0 0 60857 136 0 0 25 0 1 0 480767865 180011008 39064 4294967295 134512640 134672761 3221224560 3221223616 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43948 39064 603 41 0 43907 0
vsize: 175792
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 40583 0 0 0 61856 136 0 0 25 0 1 0 480767865 180809728 39257 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44143 39257 603 41 0 44102 0
vsize: 176572
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 40762 0 0 0 62856 137 0 0 25 0 1 0 480767865 181481472 39436 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44307 39436 603 41 0 44266 0
vsize: 177228
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 40913 0 0 0 63856 137 0 0 25 0 1 0 480767865 182149120 39587 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44470 39587 603 41 0 44429 0
vsize: 177880
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 41069 0 0 0 64855 138 0 0 25 0 1 0 480767865 182697984 39743 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44604 39743 603 41 0 44563 0
vsize: 178416
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 41192 0 0 0 65855 138 0 0 25 0 1 0 480767865 183234560 39866 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44735 39866 603 41 0 44694 0
vsize: 178940
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 41309 0 0 0 66855 139 0 0 25 0 1 0 480767865 183795712 39983 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44872 39983 603 41 0 44831 0
vsize: 179488
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 41410 0 0 0 67855 139 0 0 25 0 1 0 480767865 184094720 40084 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44945 40084 603 41 0 44904 0
vsize: 179780
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 41527 0 0 0 68854 140 0 0 25 0 1 0 480767865 184631296 40201 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45076 40201 603 41 0 45035 0
vsize: 180304
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 41633 0 0 0 69854 140 0 0 25 0 1 0 480767865 185028608 40307 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45173 40307 603 41 0 45132 0
vsize: 180692
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 41738 0 0 0 70854 140 0 0 25 0 1 0 480767865 185430016 40412 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45271 40412 603 41 0 45230 0
vsize: 181084
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 41831 0 0 0 71854 141 0 0 25 0 1 0 480767865 185831424 40505 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45369 40505 603 41 0 45328 0
vsize: 181476
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 41945 0 0 0 72854 141 0 0 25 0 1 0 480767865 186380288 40619 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45503 40619 603 41 0 45462 0
vsize: 182012
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 42069 0 0 0 73854 141 0 0 25 0 1 0 480767865 186810368 40743 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45608 40743 603 41 0 45567 0
vsize: 182432
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 42206 0 0 0 74853 142 0 0 25 0 1 0 480767865 187482112 40880 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45772 40880 603 41 0 45731 0
vsize: 183088
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 42354 0 0 0 75853 142 0 0 25 0 1 0 480767865 188018688 41028 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45903 41028 603 41 0 45862 0
vsize: 183612
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 42550 0 0 0 76853 143 0 0 25 0 1 0 480767865 188825600 41224 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46100 41224 603 41 0 46059 0
vsize: 184400
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 42725 0 0 0 77852 143 0 0 25 0 1 0 480767865 189497344 41399 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46264 41399 603 41 0 46223 0
vsize: 185056
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 42887 0 0 0 78852 144 0 0 25 0 1 0 480767865 190033920 41561 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46395 41561 603 41 0 46354 0
vsize: 185580
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 43203 0 0 0 79852 144 0 0 25 0 1 0 480767865 191377408 41877 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46723 41877 603 41 0 46682 0
vsize: 186892
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 43336 0 0 0 80851 145 0 0 25 0 1 0 480767865 191942656 42010 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46861 42010 603 41 0 46820 0
vsize: 187444
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 43455 0 0 0 81850 146 0 0 25 0 1 0 480767865 192999424 42129 4294967295 134512640 134672761 3221224560 3221223728 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47119 42129 603 41 0 47078 0
vsize: 188476
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 43485 0 0 0 82850 146 0 0 25 0 1 0 480767865 193138688 42159 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47153 42159 603 41 0 47112 0
vsize: 188612
[startup+840.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7378
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 43785 0 0 0 83849 147 0 0 25 0 1 0 480767865 194342912 42459 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47447 42459 603 41 0 47406 0
vsize: 189788
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 44225 0 0 0 84849 148 0 0 25 0 1 0 480767865 196079616 42899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47871 42899 603 41 0 47830 0
vsize: 191484
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 44662 0 0 0 85848 148 0 0 25 0 1 0 480767865 197832704 43336 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48299 43336 603 41 0 48258 0
vsize: 193196
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 45181 0 0 0 86847 150 0 0 25 0 1 0 480767865 199979008 43855 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48823 43855 603 41 0 48782 0
vsize: 195292
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 45750 0 0 0 87845 152 0 0 25 0 1 0 480767865 202358784 44424 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49404 44424 603 41 0 49363 0
vsize: 197616
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 46344 0 0 0 88844 153 0 0 25 0 1 0 480767865 204759040 45018 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49990 45018 603 41 0 49949 0
vsize: 199960
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 46963 0 0 0 89843 155 0 0 25 0 1 0 480767865 207257600 45637 4294967295 134512640 134672761 3221224560 3221223744 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50600 45637 603 41 0 50559 0
vsize: 202400
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 47561 0 0 0 90841 156 0 0 25 0 1 0 480767865 209788928 46235 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51218 46235 603 41 0 51177 0
vsize: 204872
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 48124 0 0 0 91841 157 0 0 25 0 1 0 480767865 212029440 46798 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51765 46798 603 41 0 51724 0
vsize: 207060
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 48787 0 0 0 92839 158 0 0 25 0 1 0 480767865 214691840 47461 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52415 47461 603 41 0 52374 0
vsize: 209660
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 49322 0 0 0 93838 160 0 0 25 0 1 0 480767865 216948736 47996 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52966 47996 603 41 0 52925 0
vsize: 211864
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 49864 0 0 0 94837 161 0 0 25 0 1 0 480767865 219205632 48538 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53517 48538 603 41 0 53476 0
vsize: 214068
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 50455 0 0 0 95836 163 0 0 25 0 1 0 480767865 221593600 49129 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54100 49129 603 41 0 54059 0
vsize: 216400
[startup+970.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 50896 0 0 0 96835 164 0 0 25 0 1 0 480767865 223428608 49570 4294967295 134512640 134672761 3221224560 3221223664 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54548 49570 603 41 0 54507 0
vsize: 218192
[startup+980.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 51383 0 0 0 97834 165 0 0 25 0 1 0 480767865 225406976 50057 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55031 50057 603 41 0 54990 0
vsize: 220124
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 51900 0 0 0 98834 165 0 0 25 0 1 0 480767865 227508224 50574 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55544 50574 603 41 0 55503 0
vsize: 222176
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 52442 0 0 0 99832 167 0 0 25 0 1 0 480767865 229752832 51116 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56092 51116 603 41 0 56051 0
vsize: 224368
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 52938 0 0 0 100831 168 0 0 25 0 1 0 480767865 231710720 51612 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56570 51612 603 41 0 56529 0
vsize: 226280
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 53439 0 0 0 101830 170 0 0 25 0 1 0 480767865 233820160 52113 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57085 52113 603 41 0 57044 0
vsize: 228340
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 53873 0 0 0 102828 172 0 0 25 0 1 0 480767865 235532288 52547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57503 52547 603 41 0 57462 0
vsize: 230012
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 54316 0 0 0 103827 173 0 0 25 0 1 0 480767865 237375488 52990 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57953 52990 603 41 0 57912 0
vsize: 231812
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 54850 0 0 0 104826 174 0 0 25 0 1 0 480767865 239591424 53524 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58494 53524 603 41 0 58453 0
vsize: 233976
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 55277 0 0 0 105825 175 0 0 25 0 1 0 480767865 241295360 53951 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58910 53951 603 41 0 58869 0
vsize: 235640
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 55738 0 0 0 106824 176 0 0 25 0 1 0 480767865 243286016 54412 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59396 54412 603 41 0 59355 0
vsize: 237584
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 56213 0 0 0 107823 177 0 0 25 0 1 0 480767865 245133312 54887 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59847 54887 603 41 0 59806 0
vsize: 239388
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 56648 0 0 0 108822 179 0 0 25 0 1 0 480767865 246956032 55322 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60292 55322 603 41 0 60251 0
vsize: 241168
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 57142 0 0 0 109821 180 0 0 25 0 1 0 480767865 248934400 55816 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60775 55816 603 41 0 60734 0
vsize: 243100
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 57716 0 0 0 110821 180 0 0 25 0 1 0 480767865 251281408 56390 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61348 56390 603 41 0 61307 0
vsize: 245392
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 58266 0 0 0 111819 182 0 0 25 0 1 0 480767865 253546496 56940 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61901 56940 603 41 0 61860 0
vsize: 247604
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 58818 0 0 0 112818 183 0 0 25 0 1 0 480767865 255787008 57492 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62448 57492 603 41 0 62407 0
vsize: 249792
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 59396 0 0 0 113816 185 0 0 25 0 1 0 480767865 258142208 58070 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63023 58070 603 41 0 62982 0
vsize: 252092
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 59973 0 0 0 114815 187 0 0 25 0 1 0 480767865 260517888 58647 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63603 58647 603 41 0 63562 0
vsize: 254412
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 60383 0 0 0 115813 188 0 0 25 0 1 0 480767865 262234112 59057 4294967295 134512640 134672761 3221224560 3221223744 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64022 59057 603 41 0 63981 0
vsize: 256088
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 60834 0 0 0 116812 190 0 0 25 0 1 0 480767865 264101888 59508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64478 59508 603 41 0 64437 0
vsize: 257912
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 61274 0 0 0 117811 191 0 0 25 0 1 0 480767865 265940992 59948 4294967295 134512640 134672761 3221224560 3221223664 134560269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64927 59948 603 41 0 64886 0
vsize: 259708
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 61741 0 0 0 118810 192 0 0 25 0 1 0 480767865 267792384 60415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65379 60415 603 41 0 65338 0
vsize: 261516
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7380
Raw data (stat): 7323 (minisat+) R 7322 3260 3259 0 -1 0 62230 0 0 0 119809 193 0 0 25 0 1 0 480767865 269750272 60904 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65857 60904 603 41 0 65816 0
vsize: 263428
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 7380
Raw data (stat): 7323 (minisat+) Z 7322 3260 3259 0 -1 12 62233 0 0 0 119810 205 0 0 25 0 1 0 480767865 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.15
CPU time (s): 1200.16
CPU user time (s): 1198.1
CPU system time (s): 2.05669
CPU usage (%): 100.001
Max. virtual memory (Kb): 263428
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####