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 4663

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        921208 kB
Buffers:         34064 kB
Cached:          55184 kB
SwapCached:       4932 kB
Active:          52352 kB
Inactive:        44728 kB
HighTotal:      131008 kB
HighFree:        71960 kB
LowTotal:       903652 kB
LowFree:        849248 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10792 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:04:06 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 3452 7 1200.24 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 |   65821   258945 |   21940       0        0     nan |  0.000 % |
c |       101 |   65763   258749 |   24134      92      313     3.4 |  0.157 % |
c |       251 |   65763   258749 |   26547     242     1221     5.0 |  0.157 % |
c |       476 |   65754   258718 |   29202     460     2174     4.7 |  0.164 % |
c |       814 |   65748   258698 |   32122     797     3441     4.3 |  0.171 % |
c |      1320 |   65748   258698 |   35334    1303     5262     4.0 |  0.171 % |
c |      2080 |   65748   258698 |   38868    2063     8272     4.0 |  0.171 % |
c |      3219 |   65722   258601 |   42754    3198    24140     7.5 |  0.200 % |
c |      4928 |   65652   258370 |   47030    4896    71112    14.5 |  0.292 % |
c |      7490 |   65626   258280 |   51733    7453   467800    62.8 |  0.321 % |
c |     11339 |   65600   258190 |   56906   11295   902266    79.9 |  0.349 % |
c |     17106 |   65577   258111 |   62597   17059  1975016   115.8 |  0.378 % |
c |     25755 |   65500   257844 |   68857   25692  3672834   143.0 |  0.471 % |
c |     38732 |   65491   257813 |   75742   38659  7032359   181.9 |  0.478 % |
c |     58194 |   65491   257813 |   83317   58121 13074291   224.9 |  0.478 % |
c |     87387 |   65491   257813 |   91648   22203  5350239   241.0 |  0.478 % |
c |    131176 |   65485   257793 |  100813   65991 17503863   265.2 |  0.485 % |
c |    196861 |   65470   257742 |  110895   48817  9789208   200.5 |  0.499 % |
c |    295389 |   65470   257742 |  121984   51894 16652287   320.9 |  0.499 % |
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.99 0.97 0.74 2/54 2220
Raw data (stat): 2220 (runsolver) R 2219 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420342300 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 1817 0 0 0 993 5 0 0 25 0 1 0 420342300 9375744 1792 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2289 1792 603 41 0 2248 0
vsize: 9156
[startup+20.0013 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 2596 0 0 0 1990 7 0 0 25 0 1 0 420342300 12496896 2571 4294967295 134512640 134672761 3221224560 3221223684 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2571 603 41 0 3010 0
vsize: 12204
[startup+30.0018 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 3768 0 0 0 2988 10 0 0 25 0 1 0 420342300 17403904 3743 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4249 3743 603 41 0 4208 0
vsize: 16996
[startup+40.002 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 4751 0 0 0 3984 13 0 0 25 0 1 0 420342300 21311488 4726 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5203 4726 603 41 0 5162 0
vsize: 20812
[startup+50.0027 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 5740 0 0 0 4982 16 0 0 25 0 1 0 420342300 25354240 5715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6190 5715 603 41 0 6149 0
vsize: 24760
[startup+60.0022 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 6692 0 0 0 5979 19 0 0 25 0 1 0 420342300 29253632 6667 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7142 6667 603 41 0 7101 0
vsize: 28568
[startup+70.0023 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 7558 0 0 0 6977 21 0 0 25 0 1 0 420342300 32890880 7533 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8030 7533 603 41 0 7989 0
vsize: 32120
[startup+80.003 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 8558 0 0 0 7974 24 0 0 25 0 1 0 420342300 37068800 8533 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9050 8533 603 41 0 9009 0
vsize: 36200
[startup+90.0025 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 9354 0 0 0 8973 26 0 0 25 0 1 0 420342300 40296448 9329 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9838 9329 603 41 0 9797 0
vsize: 39352
[startup+100.004 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 10065 0 0 0 9970 29 0 0 25 0 1 0 420342300 43122688 10040 4294967295 134512640 134672761 3221224560 3221223664 134560390 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10528 10040 603 41 0 10487 0
vsize: 42112
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 10877 0 0 0 10967 32 0 0 25 0 1 0 420342300 46493696 10852 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11351 10852 603 41 0 11310 0
vsize: 45404
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 11683 0 0 0 11965 34 0 0 25 0 1 0 420342300 49737728 11658 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12143 11658 603 41 0 12102 0
vsize: 48572
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 12559 0 0 0 12964 35 0 0 25 0 1 0 420342300 53379072 12534 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13032 12534 603 41 0 12991 0
vsize: 52128
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 13254 0 0 0 13962 37 0 0 25 0 1 0 420342300 56205312 13229 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13722 13229 603 41 0 13681 0
vsize: 54888
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 13993 0 0 0 14961 39 0 0 25 0 1 0 420342300 59314176 13968 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14481 13968 603 41 0 14440 0
vsize: 57924
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 14667 0 0 0 15959 41 0 0 25 0 1 0 420342300 62009344 14642 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15139 14642 603 41 0 15098 0
vsize: 60556
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 15320 0 0 0 16958 42 0 0 25 0 1 0 420342300 64679936 15295 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15791 15295 603 41 0 15750 0
vsize: 63164
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 15971 0 0 0 17955 45 0 0 25 0 1 0 420342300 67375104 15946 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16449 15946 603 41 0 16408 0
vsize: 65796
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 16764 0 0 0 18953 47 0 0 25 0 1 0 420342300 70602752 16739 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17237 16739 603 41 0 17196 0
vsize: 68948
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 17540 0 0 0 19950 50 0 0 25 0 1 0 420342300 73826304 17515 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18024 17515 603 41 0 17983 0
vsize: 72096
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 18529 0 0 0 20947 53 0 0 25 0 1 0 420342300 78000128 18504 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19043 18504 603 41 0 19002 0
vsize: 76172
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 19521 0 0 0 21945 55 0 0 25 0 1 0 420342300 82137088 19496 4294967295 134512640 134672761 3221224560 3221223664 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20053 19496 603 41 0 20012 0
vsize: 80212
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 20488 0 0 0 22943 57 0 0 25 0 1 0 420342300 86011904 20463 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20999 20463 603 41 0 20958 0
vsize: 83996
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 21488 0 0 0 23942 59 0 0 25 0 1 0 420342300 90169344 21463 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22014 21463 603 41 0 21973 0
vsize: 88056
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 22386 0 0 0 24940 61 0 0 25 0 1 0 420342300 93892608 22361 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22923 22361 603 41 0 22882 0
vsize: 91692
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 23193 0 0 0 25938 63 0 0 25 0 1 0 420342300 97079296 23168 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23701 23168 603 41 0 23660 0
vsize: 94804
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 24060 0 0 0 26935 66 0 0 25 0 1 0 420342300 100700160 24035 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24585 24035 603 41 0 24544 0
vsize: 98340
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 24692 0 0 0 27933 68 0 0 25 0 1 0 420342300 103243776 24667 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25206 24667 603 41 0 25165 0
vsize: 100824
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 28933 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 29933 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 30933 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223664 134560136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 31933 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 32933 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 33933 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 34933 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 35933 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 36933 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223664 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 37934 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 38934 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 39934 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 40934 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 41934 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223712 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 42934 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 43934 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 44934 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 45935 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 46935 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 47935 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25146 0 0 0 48935 69 0 0 25 0 1 0 420342300 105123840 25121 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 25121 603 41 0 25624 0
vsize: 102660
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 25526 0 0 0 49935 70 0 0 25 0 1 0 420342300 106602496 25501 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26026 25501 603 41 0 25985 0
vsize: 104104
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 26003 0 0 0 50933 72 0 0 25 0 1 0 420342300 108605440 25978 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26515 25978 603 41 0 26474 0
vsize: 106060
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 26571 0 0 0 51931 74 0 0 25 0 1 0 420342300 110899200 26546 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27075 26546 603 41 0 27034 0
vsize: 108300
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 27101 0 0 0 52930 75 0 0 25 0 1 0 420342300 113057792 27076 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27602 27076 603 41 0 27561 0
vsize: 110408
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 27634 0 0 0 53929 77 0 0 25 0 1 0 420342300 115212288 27609 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28128 27609 603 41 0 28087 0
vsize: 112512
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28150 0 0 0 54928 78 0 0 25 0 1 0 420342300 117362688 28125 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28125 603 41 0 28612 0
vsize: 114612
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 55928 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 56928 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 57928 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 58928 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 59929 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 60929 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 61929 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 62929 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223664 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 63929 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 64929 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 65929 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223744 134558931 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 66929 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 67930 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 68930 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 69930 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 70930 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 71930 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 72931 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 73931 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 74931 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 75931 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 76931 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 77932 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 78932 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 79932 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 80932 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 81932 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28162 0 0 0 82932 78 0 0 25 0 1 0 420342300 117362688 28137 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28653 28137 603 41 0 28612 0
vsize: 114612
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 28494 0 0 0 83932 79 0 0 25 0 1 0 420342300 118841344 28469 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29014 28469 603 41 0 28973 0
vsize: 116056
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 29268 0 0 0 84931 80 0 0 25 0 1 0 420342300 121929728 29243 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29768 29243 603 41 0 29727 0
vsize: 119072
[startup+860.027 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 30092 0 0 0 85928 83 0 0 25 0 1 0 420342300 125284352 30067 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30587 30067 603 41 0 30546 0
vsize: 122348
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 30845 0 0 0 86927 84 0 0 25 0 1 0 420342300 128385024 30820 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31344 30820 603 41 0 31303 0
vsize: 125376
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 31443 0 0 0 87926 85 0 0 25 0 1 0 420342300 130805760 31418 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31935 31418 603 41 0 31894 0
vsize: 127740
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 32115 0 0 0 88924 87 0 0 25 0 1 0 420342300 133627904 32090 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32624 32090 603 41 0 32583 0
vsize: 130496
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 32803 0 0 0 89922 89 0 0 25 0 1 0 420342300 136450048 32778 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33313 32778 603 41 0 33272 0
vsize: 133252
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 33368 0 0 0 90922 90 0 0 25 0 1 0 420342300 138727424 33343 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33869 33343 603 41 0 33828 0
vsize: 135476
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 34048 0 0 0 91921 92 0 0 25 0 1 0 420342300 141557760 34023 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34560 34023 603 41 0 34519 0
vsize: 138240
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 34738 0 0 0 92919 94 0 0 25 0 1 0 420342300 144379904 34713 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35249 34713 603 41 0 35208 0
vsize: 140996
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35335 0 0 0 93918 95 0 0 25 0 1 0 420342300 146792448 35310 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35838 35310 603 41 0 35797 0
vsize: 143352
[startup+950.028 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 2220
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 94917 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 2223
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 95918 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+970.03 s]
Raw data (loadavg): 1.07 0.99 0.88 2/54 2273
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 96917 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+980.03 s]
Raw data (loadavg): 1.06 0.99 0.88 2/54 2273
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 97918 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+990.03 s]
Raw data (loadavg): 1.05 0.99 0.88 2/54 2273
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 98918 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1000.03 s]
Raw data (loadavg): 1.04 0.99 0.88 2/54 2273
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 99918 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1010.03 s]
Raw data (loadavg): 1.03 0.99 0.88 2/54 2273
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 100918 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1020.03 s]
Raw data (loadavg): 1.03 0.99 0.88 2/54 2273
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 101918 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223760 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1030.03 s]
Raw data (loadavg): 1.02 0.99 0.88 2/54 2273
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 102919 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1040.03 s]
Raw data (loadavg): 1.02 0.99 0.88 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 103919 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1050.03 s]
Raw data (loadavg): 1.02 0.99 0.88 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 104919 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1060.03 s]
Raw data (loadavg): 1.01 0.99 0.89 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 105919 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1070.03 s]
Raw data (loadavg): 1.01 0.99 0.89 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 106919 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1080.03 s]
Raw data (loadavg): 1.01 0.99 0.89 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 107919 95 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1090.03 s]
Raw data (loadavg): 1.01 0.99 0.89 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 108918 96 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 109919 96 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 110919 96 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 111919 96 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 112919 96 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223664 134554988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 113919 96 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 114919 96 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 115920 96 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 116920 96 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 117920 96 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 118920 96 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 2275
Raw data (stat): 2220 (minisat+) R 2219 32461 32460 0 -1 0 35450 0 0 0 119920 96 0 0 25 0 1 0 420342300 147197952 35425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35937 35425 603 41 0 35896 0
vsize: 143748
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.90 1/54 2275
Raw data (stat): 2220 (minisat+) Z 2219 32461 32460 0 -1 12 35453 0 0 0 119921 102 0 0 25 0 1 0 420342300 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.24
CPU user time (s): 1199.22
CPU system time (s): 1.02784
CPU usage (%): 100.011
Max. virtual memory (Kb): 143748
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####