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 4838

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-13 20:29:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=608 boxname=wulflinc15 idbench=68 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  3e917561f3935db250fdeb1759fbe81d  /oldhome/oroussel/tmp/wulflinc15/normalized-exam.pi.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc15/normalized-exam.pi.opb
IDLAUNCH: 608
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        926952 kB
Buffers:         34552 kB
Cached:          51840 kB
SwapCached:       2144 kB
Active:          56992 kB
Inactive:        34368 kB
HighTotal:      131008 kB
HighFree:        75292 kB
LowTotal:       903652 kB
LowFree:        851660 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10880 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:49:50 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 608 7 1200.25 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.84 0.95 0.90 2/54 31691
Raw data (stat): 31691 (runsolver) R 31690 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420615868 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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+9.99996 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 7273 0 0 0 979 19 0 0 25 0 1 0 420615868 28147712 5927 4294967295 134512640 134672761 3221224640 3221223764 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6872 5927 603 41 0 6831 0
vsize: 27488
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.95 0.90 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 7806 0 0 0 1976 21 0 0 25 0 1 0 420615868 30339072 6460 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7407 6460 603 41 0 7366 0
vsize: 29628
[startup+30.0019 s]
Raw data (loadavg): 0.90 0.95 0.90 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 8857 0 0 0 2974 23 0 0 25 0 1 0 420615868 34652160 7511 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8460 7511 603 41 0 8419 0
vsize: 33840
[startup+40.0014 s]
Raw data (loadavg): 0.92 0.95 0.90 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 9938 0 0 0 3971 26 0 0 25 0 1 0 420615868 39018496 8592 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9526 8592 603 41 0 9485 0
vsize: 38104
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.96 0.90 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 10797 0 0 0 4970 28 0 0 25 0 1 0 420615868 42504192 9451 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10377 9451 603 41 0 10336 0
vsize: 41508
[startup+60.0023 s]
Raw data (loadavg): 0.94 0.96 0.90 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 11773 0 0 0 5967 31 0 0 25 0 1 0 420615868 46546944 10427 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11364 10427 603 41 0 11323 0
vsize: 45456
[startup+70.0029 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 12698 0 0 0 6965 33 0 0 25 0 1 0 420615868 50323456 11352 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12286 11352 603 41 0 12245 0
vsize: 49144
[startup+80.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 13677 0 0 0 7962 36 0 0 25 0 1 0 420615868 54489088 12331 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13303 12331 603 41 0 13262 0
vsize: 53212
[startup+90.0035 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 14461 0 0 0 8961 38 0 0 25 0 1 0 420615868 57589760 13115 4294967295 134512640 134672761 3221224640 3221223792 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13115 603 41 0 14019 0
vsize: 56240
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 15288 0 0 0 9957 41 0 0 25 0 1 0 420615868 61087744 13942 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14914 13942 603 41 0 14873 0
vsize: 59656
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 16047 0 0 0 10954 43 0 0 25 0 1 0 420615868 64184320 14701 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15670 14701 603 41 0 15629 0
vsize: 62680
[startup+120.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 16806 0 0 0 11952 46 0 0 25 0 1 0 420615868 67276800 15460 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16425 15460 603 41 0 16384 0
vsize: 65700
[startup+130.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 17778 0 0 0 12949 48 0 0 25 0 1 0 420615868 71196672 16432 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17382 16432 603 41 0 17341 0
vsize: 69528
[startup+140.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 18471 0 0 0 13947 51 0 0 25 0 1 0 420615868 74035200 17125 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18075 17125 603 41 0 18034 0
vsize: 72300
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 19209 0 0 0 14945 53 0 0 25 0 1 0 420615868 76996608 17863 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18798 17863 603 41 0 18757 0
vsize: 75192
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 19933 0 0 0 15942 56 0 0 25 0 1 0 420615868 79962112 18587 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19522 18587 603 41 0 19481 0
vsize: 78088
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 20573 0 0 0 16940 58 0 0 25 0 1 0 420615868 82665472 19227 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20182 19227 603 41 0 20141 0
vsize: 80728
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 21263 0 0 0 17939 59 0 0 25 0 1 0 420615868 85483520 19917 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20870 19917 603 41 0 20829 0
vsize: 83480
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 22005 0 0 0 18937 62 0 0 25 0 1 0 420615868 88567808 20659 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21623 20659 603 41 0 21582 0
vsize: 86492
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 22695 0 0 0 19935 64 0 0 25 0 1 0 420615868 91394048 21349 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22313 21349 603 41 0 22272 0
vsize: 89252
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 23644 0 0 0 20933 66 0 0 25 0 1 0 420615868 95531008 22298 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23323 22298 603 41 0 23282 0
vsize: 93292
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 24643 0 0 0 21931 69 0 0 25 0 1 0 420615868 99561472 23297 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24307 23297 603 41 0 24266 0
vsize: 97228
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 25651 0 0 0 22928 72 0 0 25 0 1 0 420615868 103718912 24305 4294967295 134512640 134672761 3221224640 3221223808 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25322 24305 603 41 0 25281 0
vsize: 101288
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 26633 0 0 0 23926 74 0 0 25 0 1 0 420615868 107712512 25287 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26297 25287 603 41 0 26256 0
vsize: 105188
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 27560 0 0 0 24924 76 0 0 25 0 1 0 420615868 111456256 26214 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27211 26214 603 41 0 27170 0
vsize: 108844
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 28439 0 0 0 25922 78 0 0 25 0 1 0 420615868 115056640 27093 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28090 27093 603 41 0 28049 0
vsize: 112360
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 29209 0 0 0 26920 81 0 0 25 0 1 0 420615868 118153216 27863 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28846 27863 603 41 0 28805 0
vsize: 115384
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 29971 0 0 0 27918 83 0 0 25 0 1 0 420615868 121376768 28625 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29633 28625 603 41 0 29592 0
vsize: 118532
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30604 0 0 0 28917 84 0 0 25 0 1 0 420615868 123940864 29258 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30259 29258 603 41 0 30218 0
vsize: 121036
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 29916 84 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223824 134559516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 30916 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 31916 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223744 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 32916 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 33916 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 34917 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 35917 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 36917 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 37917 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 38918 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 39918 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 40918 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 41918 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223808 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 42918 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223840 134557857 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 43917 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 44917 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30663 0 0 0 45918 85 0 0 25 0 1 0 420615868 124215296 29317 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29317 603 41 0 30285 0
vsize: 121304
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30664 0 0 0 46918 85 0 0 25 0 1 0 420615868 124215296 29318 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29318 603 41 0 30285 0
vsize: 121304
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30664 0 0 0 47918 85 0 0 25 0 1 0 420615868 124215296 29318 4294967295 134512640 134672761 3221224640 3221223808 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29318 603 41 0 30285 0
vsize: 121304
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30664 0 0 0 48918 85 0 0 25 0 1 0 420615868 124215296 29318 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29318 603 41 0 30285 0
vsize: 121304
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 30770 0 0 0 49918 85 0 0 25 0 1 0 420615868 124616704 29424 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30424 29424 603 41 0 30383 0
vsize: 121696
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 31334 0 0 0 50917 86 0 0 25 0 1 0 420615868 126906368 29988 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30983 29988 603 41 0 30942 0
vsize: 123932
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 31872 0 0 0 51917 87 0 0 25 0 1 0 420615868 129056768 30526 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31508 30526 603 41 0 31467 0
vsize: 126032
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 32422 0 0 0 52916 88 0 0 25 0 1 0 420615868 131338240 31076 4294967295 134512640 134672761 3221224640 3221223656 1075353266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 31076 603 41 0 32024 0
vsize: 128260
[startup+540.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 32946 0 0 0 53915 90 0 0 25 0 1 0 420615868 133492736 31600 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32591 31600 603 41 0 32550 0
vsize: 130364
[startup+550.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33502 0 0 0 54913 92 0 0 25 0 1 0 420615868 135766016 32156 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33146 32156 603 41 0 33105 0
vsize: 132584
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 55912 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 56913 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 57913 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 58913 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223904 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 59913 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 60913 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223776 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+620.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 61914 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 62914 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 63914 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+650.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 64914 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223744 134559784 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 65914 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223744 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+670.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 66914 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 67914 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 68914 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 69915 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 70915 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+720.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 71915 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223764 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 72915 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 73915 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+750.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 74916 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134564744 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+760.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 75916 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+770.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 76916 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223776 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+780.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 77916 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 78917 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+800.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 79917 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+810.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 80917 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+820.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 81917 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+830.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 82917 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+840.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 33675 0 0 0 83918 92 0 0 25 0 1 0 420615868 136437760 32329 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32329 603 41 0 33269 0
vsize: 133240
[startup+850.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 34433 0 0 0 84915 95 0 0 25 0 1 0 420615868 139530240 33087 4294967295 134512640 134672761 3221224640 3221223776 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34065 33087 603 41 0 34024 0
vsize: 136260
[startup+860.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 35257 0 0 0 85913 97 0 0 25 0 1 0 420615868 142893056 33911 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34886 33911 603 41 0 34845 0
vsize: 139544
[startup+870.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 36018 0 0 0 86911 100 0 0 25 0 1 0 420615868 146116608 34672 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35673 34672 603 41 0 35632 0
vsize: 142692
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 36667 0 0 0 87909 102 0 0 25 0 1 0 420615868 148668416 35321 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36296 35321 603 41 0 36255 0
vsize: 145184
[startup+890.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 37345 0 0 0 88907 104 0 0 25 0 1 0 420615868 151486464 35999 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36984 35999 603 41 0 36943 0
vsize: 147936
[startup+900.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 38038 0 0 0 89905 106 0 0 25 0 1 0 420615868 154312704 36692 4294967295 134512640 134672761 3221224640 3221223744 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37674 36692 603 41 0 37633 0
vsize: 150696
[startup+910.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 38637 0 0 0 90904 107 0 0 25 0 1 0 420615868 156733440 37291 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38265 37291 603 41 0 38224 0
vsize: 153060
[startup+920.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 39231 0 0 0 91903 108 0 0 25 0 1 0 420615868 159154176 37885 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38856 37885 603 41 0 38815 0
vsize: 155424
[startup+930.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 39956 0 0 0 92902 110 0 0 25 0 1 0 420615868 162107392 38610 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39577 38610 603 41 0 39536 0
vsize: 158308
[startup+940.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40612 0 0 0 93900 111 0 0 25 0 1 0 420615868 164802560 39266 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40235 39266 603 41 0 40194 0
vsize: 160940
[startup+950.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 94899 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+960.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 95900 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+970.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 96900 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+980.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 97900 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+990.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 98900 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 99900 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 100900 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 101901 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 102901 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 103901 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 104901 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 105902 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 106902 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 107902 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 108901 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223744 134560160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 109902 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 110902 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 111902 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 112902 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 113902 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 114903 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 115903 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134564459 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 116903 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223744 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 117903 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 118903 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31691
Raw data (stat): 31691 (minisat+) R 31690 29151 29150 0 -1 0 40968 0 0 0 119903 112 0 0 25 0 1 0 420615868 166273024 39622 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40594 39622 603 41 0 40553 0
vsize: 162376
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31691
Raw data (stat): 31691 (minisat+) Z 31690 29151 29150 0 -1 12 40971 0 0 0 119904 120 0 0 25 0 1 0 420615868 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.13
CPU time (s): 1200.25
CPU user time (s): 1199.05
CPU system time (s): 1.20282
CPU usage (%): 100.01
Max. virtual memory (Kb): 162376
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####