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-bench1.pi.opb
MD5SUM	773129c71f80eff294fafd0a8a5769cd
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	121
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.72874
Number of variables	4676
Total number of constraints	398
Number of constraints which are clauses	398
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	2
Maximum length of a constraint	80
Trace number 4658

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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:      1034724 kB
MemFree:        754036 kB
Buffers:         33436 kB
Cached:         135760 kB
SwapCached:       1212 kB
Active:         137464 kB
Inactive:       112084 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        753780 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2244 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25204 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:52:33 (client local time) WITH STATUS 10 IN 1200.38 SECONDS
stats: 3447 7 1200.38 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 398 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 |     398     9563 |     132       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 173[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 9344   maxlim: 4504   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   65711   242815 |   21903       0        0     nan |  0.000 % |
c |       102 |   65653   242619 |   24093      93      353     3.8 |  0.150 % |
c |       252 |   65653   242619 |   26502     243      956     3.9 |  0.150 % |
c |       477 |   65653   242619 |   29152     468     1805     3.9 |  0.150 % |
c |       814 |   65638   242568 |   32068     801     3016     3.8 |  0.164 % |
c |      1320 |   65612   242478 |   35275    1302     4844     3.7 |  0.193 % |
c |      2079 |   65589   242399 |   38802    2058     7662     3.7 |  0.221 % |
c |      3218 |   65565   242310 |   42682    3194    24494     7.7 |  0.250 % |
c |      4927 |   65502   242102 |   46951    4891    47743     9.8 |  0.335 % |
c |      7489 |   65502   242102 |   51646    7453   121180    16.3 |  0.335 % |
c |     11333 |   65502   242102 |   56810   11297   404516    35.8 |  0.335 % |
c |     17099 |   65502   242102 |   62491   17063   654586    38.4 |  0.335 % |
c |     25749 |   65502   242102 |   68740   25713  1739953    67.7 |  0.335 % |
c |     38723 |   65502   242102 |   75615   38687  4836023   125.0 |  0.335 % |
c |     58184 |   65502   242102 |   83176   58148  9782736   168.2 |  0.335 % |
c |     87377 |   65502   242102 |   91494   19192  5603954   292.0 |  0.335 % |
c |    131166 |   65502   242102 |  100643   62981 14029470   222.8 |  0.335 % |
c |    196850 |   65502   242102 |  110708   43751 16930914   387.0 |  0.335 % |
c |    295377 |   65502   242102 |  121778   47055 13596290   288.9 |  0.335 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 -x3 -x4 x5 -x6 -x7 -x8 x9 x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 x22 -x23 -x24 -x25 -x26 x27 x28 x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 x45 x46 -x47 -x48 -x49 -x50 x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 x78 x79 x80 -x81 -x82 -x83 x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 x137 -x138 -x139 x140 -x141 x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 x241 x242 x243 -x244 x245 -x246 -x247 -x248 x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 x279 -x280 -x281 -x282 -x283 x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 x441 x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 x544 x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 x601 -x602 -x603 -x604 -x605 -x606 -x607 x608 -x609 -x610 -x611 -x612 -x613 -x614 x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 x717 -x718 x719 -x720 -x721 -x722 x723 -x724 -x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 -x765 -x766 -x767 x768 x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 x873 -x874 -x875 -x876 -x877 x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 x1028 -x1029 x1030 -x1031 -x1032 -x1033 x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 x1336 -x1337 -x1338 -x1339 -x1340 -x1341 -x1342 -x1343 -x1344 x1345 -x1346 -x1347 -x1348 -x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 -x1408 -x1409 -x1410 x1411 -x1412 -x1413 -x1414 -x1415 -x1416 -x1417 x1418 -x1419 x1420 -x1421 -x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 -x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 -x1470 -x1471 -x1472 -x1473 -x1474 -x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 -x1498 -x1499 -x1500 -x1501 -x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 -x1518 -x1519 -x1520 -x1521 -x1522 -x1523 x1524 -x1525 -x1526 -x1527 -x1528 -x1529 -x1530 -x1531 -x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 -x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 x1567 -x1568 -x1569 -x1570 -x1571 -x1572 -x1573 -x1574 x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 -x1622 -x1623 -x1624 -x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 x1633 -x1634 -x1635 x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 -x1654 -x1655 -x1656 -x1657 -x1658 -x1659 -x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 -x1676 -x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 x1709 -x1710 -x1711 -x1712 -x1713 -x1714 -x1715 -x1716 -x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 -x1743 -x1744 -x1745 -x1746 -x1747 -x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 -x1765 -x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 x1787 -x1788 -x1789 -x1790 -x1791 -x1792 -x1793 -x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 -x1801 -x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 x1818 x1819 -x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 -x1827 -x1828 -x1829 -x1830 -x1831 -x1832 x1833 -x1834 -x1835 -x1836 -x1837 -x1838 -x1839 x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 -x1848 -x1849 -x1850 x1851 -x1852 -x1853 -x1854 -x1855 x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 x1876 -x1877 -x1878 x1879 -x1880 -x1881 -x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 -x1919 -x1920 -x1921 x1922 -x1923 -x1924 -x1925 -x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 -x1943 -x1944 -x1945 -x1946 -x1947 -x1948 -x1949 -x1950 -x1951 -x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 -x1962 -x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 -x1970 -x1971 -x1972 -x1973 -x1974 -x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981 -x1982 -x1983 -x1984 -x1985 -x1986 -x1987 -x1988 -x1989 -x1990 -x1991 -x1992 -x1993 -x1994 -x1995 -x1996 -x1997 -x1998 -x1999 -x2000 -x2001 x2002 -x2003 -x2004 -x2005 -x2006 -x2007 -x2008 -x2009 -x2010 -x2011 -x2012 -x2013 -x2014 -x2015 -x2016 -x2017 -x2018 -x2019 -x2020 -x2021 -x2022 -x2023 -x2024 -x2025 -x2026 -x2027 -x2028 -x2029 -x2030 -x2031 -x2032 -x2033 -x2034 -x2035 -x2036 -x2037 -x2038 -x2039 -x2040 -x2041 -x2042 -x2043 -x2044 -x2045 -x2046 -x2047 -x2048 -x2049 -x2050 -x2051 -x2052 -x2053 -x2054 -x2055 -x2056 -x2057 -x2058 -x2059 -x2060 -x2061 -x2062 -x2063 -x2064 -x2065 -x2066 x2067 -x2068 -x2069 -x2070 -x2071 -x2072 -x2073 -x2074 x2075 x2076 -x2077 -x2078 -x2079 -x2080 -x2081 -x2082 x2083 -x2084 -x2085 -x2086 -x2087 -x2088 -x2089 -x2090 -x2091 -x2092 -x2093 -x2094 -x2095 -x2096 -x2097 -x2098 -x2099 -x2100 -x2101 -x2102 -x2103 -x2104 -x2105 -x2106 -x2107 -x2108 -x2109 -x2110 -x2111 -x2112 -x2113 -x2114 -x2115 -x2116 -x2117 -x2118 -x2119 -x2120 -x2121 -x2122 -x2123 -x2124 -x2125 x2126 -x2127 -x2128 -x2129 x2130 -x2131 -x2132 -x2133 -x2134 -x2135 -x2136 x2137 -x2138 -x2139 -x2140 -x2141 -x2142 -x2143 -x2144 -x2145 -x2146 -x2147 -x2148 -x2149 x2150 -x2151 -x2152 -x2153 -x2154 -x2155 -x2156 -x2157 -x2158 -x2159 -x2160 -x2161 -x2162 -x2163 -x2164 -x2165 -x2166 -x2167 -x2168 -x2169 -x2170 -x2171 x2172 -x2173 -x2174 -x2175 -x2176 -x2177 -x2178 -x2179 -x2180 -x2181 x2182 -x2183 -x2184 -x2185 -x2186 -x2187 -x2188 -x2189 -x2190 -x2191 -x2192 -x2193 -x2194 -x2195 -x2196 -x2197 -x2198 -x2199 -x2200 -x2201 -x2202 x2203 -x2204 -x2205 x2206 -x2207 -x2208 -x2209 -x2210 -x2211 -x2212 -x2213 -x2214 -x2215 -x2216 -x2217 -x2218 -x2219 -x2220 -x2221 -x2222 -x2223 -x2224 -x2225 -x2226 -x2227 -x2228 -x2229 -x2230 -x2231 -x2232 -x2233 -x2234 -x2235 -x2236 -x2237 -x2238 -x2239 -x2240 -x2241 -x2242 -x2243 -x2244 -x2245 -x2246 -x2247 -x2248 -x2249 -x2250 -x2251 -x2252 x2253 -x2254 -x2255 -x2256 -x2257 -x2258 -x2259 x2260 -x2261 -x2262 -x2263 -x2264 -x2265 x2266 -x2267 -x2268 -x2269 -x2270 -x2271 -x2272 -x2273 -x2274 -x2275 -x2276 -x2277 -x2278 -x2279 -x2280 x2281 -x2282 -x2283 -x2284 -x2285 -x2286 -x2287 -x2288 -x2289 -x2290 -x2291 -x2292 -x2293 -x2294 -x2295 -x2296 -x2297 -x2298 -x2299 -x2300 -x2301 -x2302 x2303 -x2304 -x2305 -x2306 -x2307 -x2308 -x2309 -x2310 -x2311 -x2312 -x2313 -x2314 -x2315 -x2316 -x2317 -x2318 -x2319 -x2320 -x2321 -x2322 -x2323 -x2324 -x2325 -x2326 -x2327 -x2328 -x2329 -x2330 -x2331 -x2332 -x2333 -x2334 -x2335 -x2336 -x2337 -x2338 -x2339 -x2340 -x2341 -x2342 -x2343 -x2344 -x2345 -x2346 -x2347 -x2348 x2349 -x2350 -x2351 -x2352 -x2353 -x2354 -x2355 -x2356 -x2357 -x2358 -x2359 -x2360 -x2361 -x2362 -x2363 -x2364 -x2365 -x2366 -x2367 -x2368 -x2369 -x2370 -x2371 -x2372 x2373 -x2374 -x2375 -x2376 -x2377 -x2378 -x2379 -x2380 -x2381 -x2382 -x2383 -x2384 -x2385 -x2386 -x2387 -x2388 -x2389 -x2390 -x2391 -x2392 -x2393 -x2394 -x2395 x2396 -x2397 -x2398 -x2399 -x2400 -x2401 -x2402 -x2403 -x2404 -x2405 -x2406 -x2407 -x2408 -x2409 -x2410 -x2411 -x2412 -x2413 -x2414 -x2415 -x2416 -x2417 -x2418 -x2419 -x2420 -x2421 -x2422 -x2423 -x2424 -x2425 -x2426 -x2427 -x2428 -x2429 -x2430 -x2431 -x2432 -x2433 -x2434 -x2435 -x2436 -x2437 -x2438 -x2439 -x2440 -x2441 -x2442 -x2443 -x2444 -x2445 -x2446 -x2447 -x2448 -x2449 -x2450 -x2451 -x2452 -x2453 -x2454 -x2455 -x2456 -x2457 -x2458 -x2459 -x2460 -x2461 -x2462 -x2463 -x2464 -x2465 -x2466 -x2467 -x2468 -x2469 -x2470 -x2471 -x2472 -x2473 -x2474 -x2475 -x2476 -x2477 -x2478 -x2479 -x2480 -x2481 -x2482 -x2483 -x2484 -x2485 -x2486 -x2487 -x2488 -x2489 -x2490 -x2491 -x2492 -x2493 -x2494 -x2495 -x2496 -x2497 -x2498 -x2499 -x2500 -x2501 -x2502 -x2503 -x2504 -x2505 -x2506 -x2507 -x2508 -x2509 -x2510 -x2511 -x2512 -x2513 -x2514 -x2515 -x2516 -x2517 -x2518 -x2519 -x2520 -x2521 -x2522 -x2523 -x2524 -x2525 -x2526 -x2527 -x2528 -x2529 -x2530 -x2531 -x2532 -x2533 -x2534 -x2535 -x2536 -x2537 -x2538 -x2539 -x2540 -x2541 -x2542 -x2543 -x2544 -x2545 -x2546 -x2547 -x2548 -x2549 -x2550 -x2551 -x2552 -x2553 -x2554 -x2555 -x2556 -x2557 -x2558 -x2559 -x2560 -x2561 x2562 -x2563 -x2564 -x2565 -x2566 -x2567 -x2568 -x2569 -x2570 -x2571 -x2572 -x2573 -x2574 -x2575 -x2576 -x2577 -x2578 -x2579 x2580 -x2581 -x2582 -x2583 -x2584 -x2585 -x2586 -x2587 -x2588 -x2589 -x2590 -x2591 -x2592 -x2593 -x2594 -x2595 -x2596 -x2597 -x2598 -x2599 -x2600 -x2601 -x2602 -x2603 -x2604 -x2605 -x2606 -x2607 -x2608 x2609 -x2610 x2611 -x2612 -x2613 -x2614 -x2615 -x2616 -x2617 -x2618 -x2619 -x2620 -x2621 -x2622 x2623 -x2624 -x2625 -x2626 -x2627 -x2628 -x2629 -x2630 -x2631 -x2632 -x2633 -x2634 -x2635 -x2636 x2637 -x2638 -x2639 -x2640 -x2641 -x2642 -x2643 -x2644 -x2645 -x2646 -x2647 -x2648 -x2649 -x2650 -x2651 -x2652 -x2653 -x2654 -x2655 -x2656 -x2657 -x2658 -x2659 -x2660 -x2661 -x2662 x2663 -x2664 -x2665 -x2666 -x2667 -x2668 x2669 -x2670 -x2671 -x2672 -x2673 -x2674 -x2675 -x2676 -x2677 -x2678 -x2679 -x2680 -x2681 -x2682 x2683 -x2684 -x2685 -x2686 -x2687 -x2688 -x2689 -x2690 -x2691 -x2692 -x2693 -x2694 -x2695 -x2696 -x2697 -x2698 -x2699 -x2700 x2701 -x2702 -x2703 -x2704 -x2705 -x2706 x2707 -x2708 -x2709 -x2710 -x2711 -x2712 -x2713 -x2714 -x2715 -x2716 -x2717 -x2718 -x2719 -x2720 -x2721 -x2722 -x2723 -x2724 -x2725 -x2726 -x2727 x2728 -x2729 -x2730 -x2731 -x2732 -x2733 -x2734 -x2735 -x2736 -x2737 -x2738 -x2739 -x2740 -x2741 -x2742 -x2743 -x2744 -x2745 -x2746 -x2747 -x2748 -x2749 -x2750 -x2751 -x2752 -x2753 -x2754 -x2755 -x2756 -x2757 -x2758 x2759 -x2760 -x2761 -x2762 -x2763 -x2764 x2765 -x2766 -x2767 -x2768 -x2769 -x2770 -x2771 -x2772 -x2773 -x2774 -x2775 -x2776 -x2777 -x2778 -x2779 -x2780 -x2781 -x2782 -x2783 -x2784 -x2785 x2786 -x2787 -x2788 -x2789 -x2790 -x2791 -x2792 -x2793 -x2794 -x2795 -x2796 -x2797 -x2798 -x2799 -x2800 -x2801 -x2802 -x2803 -x2804 -x2805 -x2806 -x2807 -x2808 -x2809 -x2810 -x2811 -x2812 -x2813 -x2814 -x2815 x2816 -x2817 -x2818 -x2819 -x2820 -x2821 -x2822 -x2823 -x2824 -x2825 -x2826 -x2827 -x2828 -x2829 -x2830 -x2831 -x2832 -x2833 -x2834 -x2835 -x2836 -x2837 -x2838 -x2839 x2840 -x2841 -x2842 -x2843 -x2844 -x2845 -x2846 -x2847 -x2848 -x2849 -x2850 -x2851 -x2852 -x2853 -x2854 -x2855 -x2856 -x2857 -x2858 -x2859 -x2860 -x2861 -x2862 -x2863 -x2864 -x2865 -x2866 -x2867 -x2868 -x2869 -x2870 -x2871 x2872 -x2873 -x2874 -x2875 -x2876 -x2877 -x2878 -x2879 -x2880 -x2881 -x2882 -x2883 -x2884 -x2885 -x2886 -x2887 -x2888 -x2889 -x2890 -x2891 -x2892 -x2893 -x2894 -x2895 -x2896 -x2897 -x2898 -x2899 -x2900 -x2901 -x2902 -x2903 -x2904 -x2905 -x2906 -x2907 -x2908 -x2909 -x2910 -x2911 -x2912 -x2913 -x2914 x2915 -x2916 -x2917 x2918 -x2919 -x2920 -x2921 -x2922 -x2923 -x2924 -x2925 -x2926 -x2927 -x2928 -x2929 -x2930 -x2931 x2932 -x2933 -x2934 -x2935 -x2936 -x2937 -x2938 -x2939 -x2940 -x2941 -x2942 -x2943 -x2944 -x2945 -x2946 -x2947 -x2948 -x2949 -x2950 -x2951 -x2952 -x2953 -x2954 -x2955 -x2956 -x2957 -x2958 -x2959 -x2960 -x2961 -x2962 -x2963 -x2964 -x2965 -x2966 -x2967 -x2968 -x2969 -x2970 -x2971 -x2972 -x2973 -x2974 -x2975 -x2976 -x2977 -x2978 -x2979 -x2980 -x2981 x2982 -x2983 -x2984 -x2985 -x2986 -x2987 -x2988 -x2989 -x2990 -x2991 -x2992 -x2993 -x2994 -x2995 -x2996 -x2997 -x2998 x2999 -x3000 -x3001 -x3002 -x3003 -x3004 -x3005 -x3006 -x3007 -x3008 -x3009 -x3010 -x3011 -x3012 -x3013 -x3014 -x3015 -x3016 -x3017 -x3018 -x3019 -x3020 -x3021 -x3022 -x3023 -x3024 -x3025 -x3026 -x3027 -x3028 -x3029 -x3030 -x3031 -x3032 -x3033 -x3034 -x3035 -x3036 -x3037 -x3038 -x3039 -x3040 -x3041 -x3042 -x3043 -x3044 -x3045 -x3046 -x3047 -x3048 -x3049 -x3050 -x3051 -x3052 -x3053 -x3054 -x3055 -x3056 -x3057 -x3058 -x3059 -x3060 -x3061 -x3062 -x3063 -x3064 -x3065 -x3066 -x3067 -x3068 -x3069 -x3070 -x3071 -x3072 -x3073 -x3074 -x3075 -x3076 -x3077 -x3078 -x3079 -x3080 -x3081 -x3082 -x3083 -x3084 -x3085 -x3086 -x3087 -x3088 -x3089 -x3090 -x3091 -x3092 -x3093 -x3094 -x3095 -x3096 -x3097 -x3098 -x3099 -x3100 -x3101 -x3102 -x3103 -x3104 -x3105 -x3106 -x3107 -x3108 -x3109 -x3110 -x3111 -x3112 -x3113 -x3114 -x3115 -x3116 -x3117 -x3118 -x3119 -x3120 -x3121 -x3122 -x3123 -x3124 -x3125 -x3126 -x3127 x3128 -x3129 -x3130 -x3131 -x3132 -x3133 -x3134 -x3135 -x3136 -x3137 -x3138 -x3139 -x3140 -x3141 -x3142 -x3143 -x3144 -x3145 -x3146 x3147 -x3148 -x3149 -x3150 -x3151 -x3152 -x3153 -x3154 -x3155 -x3156 -x3157 -x3158 -x3159 -x3160 -x3161 -x3162 -x3163 -x3164 -x3165 -x3166 -x3167 -x3168 -x3169 -x3170 -x3171 -x3172 -x3173 -x3174 -x3175 -x3176 -x3177 -x3178 -x3179 -x3180 -x3181 -x3182 -x3183 -x3184 -x3185 -x3186 -x3187 -x3188 -x3189 -x3190 -x3191 -x3192 -x3193 -x3194 -x3195 -x3196 -x3197 -x3198 -x3199 -x3200 -x3201 -x3202 -x3203 -x3204 -x3205 -x3206 -x3207 -x3208 -x3209 -x3210 -x3211 -x3212 -x3213 -x3214 -x3215 -x3216 -x3217 -x3218 -x3219 -x3220 -x3221 -x3222 -x3223 -x3224 -x3225 -x3226 -x3227 -x3228 -x3229 -x3230 -x3231 -x3232 -x3233 -x3234 -x3235 -x3236 -x3237 -x3238 -x3239 -x3240 -x3241 -x3242 -x3243 -x3244 -x3245 -x3246 -x3247 -x3248 -x3249 -x3250 -x3251 -x3252 -x3253 -x3254 -x3255 -x3256 -x3257 -x3258 -x3259 -x3260 -x3261 -x3262 -x3263 -x3264 -x3265 -x3266 -x3267 -x3268 -x3269 -x3270 -x3271 -x3272 -x3273 -x3274 -x3275 -x3276 -x3277 -x3278 -x3279 x3280 -x3281 -x3282 -x3283 -x3284 -x3285 -x3286 -x3287 -x3288 -x3289 -x3290 -x3291 -x3292 -x3293 -x3294 -x3295 -x3296 -x3297 -x3298 -x3299 -x3300 -x3301 -x3302 -x3303 -x3304 -x3305 -x3306 -x3307 -x3308 -x3309 x3310 -x3311 -x3312 -x3313 -x3314 -x3315 -x3316 x3317 -x3318 -x3319 -x3320 -x3321 -x3322 -x3323 -x3324 -x3325 -x3326 -x3327 -x3328 -x3329 -x3330 -x3331 -x3332 -x3333 -x3334 -x3335 -x3336 -x3337 -x3338 -x3339 -x3340 -x3341 -x3342 -x3343 -x3344 -x3345 -x3346 -x3347 -x3348 -x3349 -x3350 -x3351 -x3352 -x3353 -x3354 -x3355 -x3356 -x3357 -x3358 -x3359 -x3360 x3361 -x3362 -x3363 -x3364 -x3365 -x3366 -x3367 -x3368 -x3369 -x3370 -x3371 -x3372 -x3373 -x3374 -x3375 -x3376 -x3377 -x3378 -x3379 -x3380 -x3381 -x3382 -x3383 -x3384 -x3385 -x3386 -x3387 -x3388 -x3389 -x3390 -x3391 -x3392 -x3393 -x3394 -x3395 -x3396 -x3397 -x3398 -x3399 -x3400 -x3401 -x3402 -x3403 -x3404 -x3405 x3406 -x3407 -x3408 -x3409 x3410 -x3411 -x3412 -x3413 -x3414 -x3415 -x3416 -x3417 -x3418 -x3419 -x3420 -x3421 -x3422 -x3423 -x3424 -x3425 -x3426 -x3427 -x3428 -x3429 -x3430 -x3431 -x3432 -x3433 -x3434 -x3435 -x3436 -x3437 -x3438 -x3439 x3440 -x3441 -x3442 -x3443 -x3444 -x3445 -x3446 -x3447 -x3448 -x3449 -x3450 -x3451 -x3452 -x3453 -x3454 -x3455 -x3456 -x3457 -x3458 -x3459 -x3460 -x3461 -x3462 -x3463 -x3464 -x3465 -x3466 -x3467 -x3468 -x3469 -x3470 -x3471 x3472 -x3473 -x3474 -x3475 -x3476 -x3477 -x3478 -x3479 -x3480 -x3481 -x3482 -x3483 -x3484 -x3485 -x3486 -x3487 -x3488 -x3489 -x3490 -x3491 -x3492 -x3493 -x3494 -x3495 -x3496 -x3497 -x3498 -x3499 -x3500 -x3501 -x3502 -x3503 -x3504 -x3505 -x3506 -x3507 -x3508 -x3509 -x3510 -x3511 -x3512 x3513 -x3514 -x3515 -x3516 -x3517 -x3518 -x3519 -x3520 -x3521 -x3522 -x3523 -x3524 -x3525 -x3526 -x3527 -x3528 -x3529 -x3530 -x3531 -x3532 -x3533 -x3534 -x3535 -x3536 -x3537 -x3538 -x3539 -x3540 -x3541 -x3542 -x3543 -x3544 -x3545 -x3546 -x3547 -x3548 -x3549 -x3550 -x3551 -x3552 -x3553 -x3554 -x3555 -x3556 -x3557 -x3558 -x3559 -x3560 -x3561 -x3562 -x3563 -x3564 -x3565 -x3566 -x3567 -x3568 -x3569 -x3570 -x3571 -x3572 -x3573 -x3574 -x3575 -x3576 -x3577 -x3578 -x3579 -x3580 -x3581 -x3582 -x3583 -x3584 -x3585 -x3586 -x3587 -x3588 -x3589 -x3590 -x3591 -x3592 -x3593 -x3594 -x3595 -x3596 -x3597 -x3598 -x3599 -x3600 -x3601 -x3602 -x3603 -x3604 x3605 -x3606 -x3607 -x3608 -x3609 -x3610 -x3611 -x3612 -x3613 -x3614 -x3615 -x3616 -x3617 -x3618 -x3619 -x3620 -x3621 -x3622 -x3623 -x3624 -x3625 -x3626 -x3627 -x3628 -x3629 -x3630 -x3631 -x3632 -x3633 -x3634 -x3635 -x3636 -x3637 -x3638 -x3639 -x3640 -x3641 -x3642 -x3643 -x3644 -x3645 -x3646 -x3647 -x3648 -x3649 -x3650 -x3651 -x3652 -x3653 -x3654 -x3655 -x3656 -x3657 -x3658 -x3659 -x3660 -x3661 -x3662 -x3663 -x3664 -x3665 -x3666 -x3667 -x3668 -x3669 -x3670 -x3671 -x3672 -x3673 -x3674 -x3675 -x3676 -x3677 -x3678 -x3679 x3680 -x3681 -x3682 -x3683 -x3684 -x3685 -x3686 -x3687 -x3688 -x3689 -x3690 -x3691 -x3692 -x3693 -x3694 -x3695 -x3696 -x3697 -x3698 -x3699 -x3700 -x3701 -x3702 -x3703 -x3704 -x3705 -x3706 -x3707 -x3708 -x3709 -x3710 x3711 -x3712 -x3713 -x3714 -x3715 -x3716 -x3717 -x3718 -x3719 -x3720 -x3721 -x3722 -x3723 -x3724 -x3725 -x3726 -x3727 -x3728 -x3729 -x3730 -x3731 -x3732 -x3733 -x3734 -x3735 -x3736 -x3737 -x3738 -x3739 -x3740 -x3741 -x3742 -x3743 -x3744 -x3745 -x3746 -x3747 -x3748 -x3749 -x3750 -x3751 -x3752 -x3753 -x3754 -x3755 -x3756 -x3757 -x3758 -x3759 -x3760 -x3761 -x3762 -x3763 -x3764 -x3765 -x3766 -x3767 -x3768 -x3769 -x3770 -x3771 -x3772 -x3773 -x3774 -x3775 -x3776 -x3777 -x3778 -x3779 -x3780 -x3781 -x3782 x3783 -x3784 -x3785 -x3786 -x3787 -x3788 -x3789 -x3790 -x3791 -x3792 -x3793 -x3794 -x3795 -x3796 -x3797 -x3798 -x3799 -x3800 -x3801 -x3802 -x3803 -x3804 -x3805 -x3806 -x3807 -x3808 -x3809 -x3810 -x3811 -x3812 -x3813 -x3814 -x3815 -x3816 -x3817 -x3818 -x3819 -x3820 -x3821 -x3822 -x3823 -x3824 -x3825 -x3826 -x3827 -x3828 -x3829 -x3830 -x3831 -x3832 -x3833 -x3834 -x3835 -x3836 -x3837 -x3838 -x3839 -x3840 -x3841 -x3842 -x3843 -x3844 -x3845 -x3846 -x3847 -x3848 -x3849 -x3850 -x3851 -x3852 -x3853 -x3854 -x3855 -x3856 -x3857 -x3858 -x3859 -x3860 -x3861 -x3862 -x3863 x3864 -x3865 -x3866 -x3867 -x3868 -x3869 -x3870 -x3871 -x3872 -x3873 -x3874 -x3875 -x3876 -x3877 -x3878 -x3879 -x3880 -x3881 -x3882 -x3883 -x3884 -x3885 -x3886 -x3887 -x3888 -x3889 -x3890 -x3891 -x3892 -x3893 -x3894 -x3895 -x3896 -x3897 -x3898 -x3899 -x3900 -x3901 -x3902 -x3903 -x3904 -x3905 -x3906 -x3907 -x3908 -x3909 -x3910 -x3911 -x3912 -x3913 -x3914 -x3915 -x3916 -x3917 -x3918 -x3919 -x3920 -x3921 -x3922 -x3923 -x3924 -x3925 -x3926 -x3927 -x3928 -x3929 -x3930 -x3931 -x3932 -x3933 -x3934 -x3935 -x3936 -x3937 x3938 -x3939 -x3940 -x3941 -x3942 -x3943 -x3944 -x3945 -x3946 -x3947 -x3948 -x3949 -x3950 -x3951 -x3952 -x3953 -x3954 -x3955 -x3956 -x3957 -x3958 -x3959 -x3960 -x3961 -x3962 -x3963 -x3964 -x3965 -x3966 -x3967 -x3968 -x3969 -x3970 -x3971 x3972 -x3973 -x3974 -x3975 -x3976 -x3977 -x3978 -x3979 -x3980 -x3981 -x3982 -x3983 -x3984 -x3985 -x3986 -x3987 -x3988 -x3989 x3990 -x3991 -x3992 -x3993 -x3994 -x3995 -x3996 -x3997 -x3998 -x3999 -x4000 -x4001 -x4002 -x4003 -x4004 -x4005 -x4006 -x4007 -x4008 -x4009 -x4010 -x4011 -x4012 -x4013 -x4014 -x4015 -x4016 -x4017 -x4018 -x4019 -x4020 -x4021 -x4022 -x4023 -x4024 -x4025 -x4026 -x4027 -x4028 -x4029 -x4030 -x4031 -x4032 -x4033 -x4034 -x4035 x4036 -x4037 -x4038 -x4039 -x4040 -x4041 -x4042 -x4043 -x4044 -x4045 -x4046 -x4047 -x4048 -x4049 -x4050 -x4051 -x4052 -x4053 -x4054 -x4055 -x4056 -x4057 -x4058 -x4059 -x4060 -x4061 -x4062 -x4063 -x4064 -x4065 -x4066 -x4067 -x4068 -x4069 -x4070 -x4071 -x4072 -x4073 -x4074 -x4075 -x4076 -x4077 -x4078 -x4079 -x4080 -x4081 -x4082 -x4083 -x4084 -x4085 -x4086 -x4087 -x4088 -x4089 -x4090 -x4091 -x4092 -x4093 -x4094 -x4095 -x4096 -x4097 -x4098 -x4099 -x4100 -x4101 -x4102 -x4103 -x4104 -x4105 -x4106 -x4107 -x4108 -x4109 -x4110 -x4111 -x4112 -x4113 -x4114 -x4115 -x4116 -x4117 -x4118 -x4119 -x4120 -x4121 -x4122 -x4123 -x4124 -x4125 -x4126 -x4127 -x4128 -x4129 -x4130 -x4131 -x4132 -x4133 -x4134 -x4135 -x4136 -x4137 -x4138 x4139 -x4140 -x4141 -x4142 -x4143 -x4144 -x4145 -x4146 -x4147 -x4148 -x4149 -x4150 -x4151 -x4152 -x4153 -x4154 -x4155 -x4156 -x4157 -x4158 -x4159 -x4160 -x4161 -x4162 -x4163 -x4164 -x4165 -x4166 -x4167 -x4168 -x4169 -x4170 -x4171 -x4172 -x4173 -x4174 -x4175 -x4176 -x4177 -x4178 -x4179 -x4180 -x4181 -x4182 -x4183 -x4184 -x4185 -x4186 -x4187 -x4188 -x4189 -x4190 -x4191 -x4192 -x4193 -x4194 -x4195 -x4196 -x4197 -x4198 -x4199 -x4200 -x4201 -x4202 -x4203 -x4204 -x4205 -x4206 -x4207 -x4208 -x4209 -x4210 -x4211 -x4212 -x4213 -x4214 -x4215 -x4216 -x4217 -x4218 -x4219 -x4220 -x4221 -x4222 -x4223 -x4224 -x4225 -x4226 -x4227 -x4228 -x4229 -x4230 -x4231 -x4232 -x4233 -x4234 -x4235 -x4236 -x4237 -x4238 -x4239 -x4240 -x4241 -x4242 -x4243 -x4244 -x4245 -x4246 -x4247 -x4248 -x4249 -x4250 -x4251 -x4252 -x4253 -x4254 -x4255 -x4256 -x4257 -x4258 -x4259 -x4260 -x4261 -x4262 -x4263 -x4264 -x4265 -x4266 -x4267 -x4268 -x4269 -x4270 -x4271 -x4272 -x427#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.61 0.26 2/53 10704
Raw data (stat): 10704 (runsolver) R 10703 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478491881 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.92 0.62 0.27 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 1742 0 0 0 993 4 0 0 25 0 1 0 478491881 9154560 1717 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2235 1717 603 41 0 2194 0
vsize: 8940
[startup+20.002 s]
Raw data (loadavg): 0.93 0.63 0.27 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 2334 0 0 0 1992 5 0 0 25 0 1 0 478491881 11513856 2309 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2811 2309 603 41 0 2770 0
vsize: 11244
[startup+30.0038 s]
Raw data (loadavg): 0.94 0.64 0.28 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 3294 0 0 0 2990 8 0 0 25 0 1 0 478491881 15486976 3269 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3781 3269 603 41 0 3740 0
vsize: 15124
[startup+40.0045 s]
Raw data (loadavg): 0.95 0.65 0.29 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 4081 0 0 0 3987 11 0 0 25 0 1 0 478491881 18722816 4056 4294967295 134512640 134672761 3221224560 3221223684 134566045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4571 4056 603 41 0 4530 0
vsize: 18284
[startup+50.0062 s]
Raw data (loadavg): 0.96 0.67 0.29 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 5066 0 0 0 4985 13 0 0 25 0 1 0 478491881 22888448 5041 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5588 5041 603 41 0 5547 0
vsize: 22352
[startup+60.0068 s]
Raw data (loadavg): 0.96 0.68 0.30 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 6208 0 0 0 5981 17 0 0 25 0 1 0 478491881 27459584 6183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6704 6183 603 41 0 6663 0
vsize: 26816
[startup+70.0077 s]
Raw data (loadavg): 0.97 0.69 0.31 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 7201 0 0 0 6979 19 0 0 25 0 1 0 478491881 31506432 7176 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7692 7176 603 41 0 7651 0
vsize: 30768
[startup+80.0095 s]
Raw data (loadavg): 0.97 0.70 0.31 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 8461 0 0 0 7976 23 0 0 25 0 1 0 478491881 36749312 8436 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8972 8436 603 41 0 8931 0
vsize: 35888
[startup+90.01 s]
Raw data (loadavg): 0.98 0.71 0.32 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 9617 0 0 0 8972 27 0 0 25 0 1 0 478491881 41455616 9592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10121 9592 603 41 0 10080 0
vsize: 40484
[startup+100.011 s]
Raw data (loadavg): 0.98 0.71 0.33 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 10731 0 0 0 9970 29 0 0 25 0 1 0 478491881 46006272 10706 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11232 10706 603 41 0 11191 0
vsize: 44928
[startup+110.011 s]
Raw data (loadavg): 0.98 0.72 0.33 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 11771 0 0 0 10968 32 0 0 25 0 1 0 478491881 50171904 11746 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12249 11746 603 41 0 12208 0
vsize: 48996
[startup+120.011 s]
Raw data (loadavg): 0.98 0.73 0.34 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 12738 0 0 0 11964 35 0 0 25 0 1 0 478491881 54214656 12713 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12714 603 41 0 13195 0
vsize: 52944
[startup+130.012 s]
Raw data (loadavg): 0.99 0.74 0.35 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 13781 0 0 0 12962 38 0 0 25 0 1 0 478491881 58388480 13756 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14255 13756 603 41 0 14214 0
vsize: 57020
[startup+140.013 s]
Raw data (loadavg): 0.99 0.75 0.36 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 14771 0 0 0 13959 41 0 0 25 0 1 0 478491881 62689280 14746 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15305 14746 603 41 0 15264 0
vsize: 61220
[startup+150.013 s]
Raw data (loadavg): 0.99 0.76 0.36 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 15618 0 0 0 14956 44 0 0 25 0 1 0 478491881 66187264 15593 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15593 603 41 0 16118 0
vsize: 64636
[startup+160.014 s]
Raw data (loadavg): 0.99 0.76 0.37 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 16532 0 0 0 15954 47 0 0 25 0 1 0 478491881 69943296 16507 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17076 16507 603 41 0 17035 0
vsize: 68304
[startup+170.015 s]
Raw data (loadavg): 0.99 0.77 0.37 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 17429 0 0 0 16951 50 0 0 25 0 1 0 478491881 73576448 17404 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17963 17404 603 41 0 17922 0
vsize: 71852
[startup+180.069 s]
Raw data (loadavg): 0.99 0.78 0.38 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 18298 0 0 0 17952 53 0 0 25 0 1 0 478491881 77209600 18273 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18850 18273 603 41 0 18809 0
vsize: 75400
[startup+190.073 s]
Raw data (loadavg): 0.99 0.79 0.39 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 19055 0 0 0 18952 55 0 0 25 0 1 0 478491881 80306176 19030 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19606 19030 603 41 0 19565 0
vsize: 78424
[startup+200.074 s]
Raw data (loadavg): 0.99 0.79 0.39 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 19689 0 0 0 19950 57 0 0 25 0 1 0 478491881 82857984 19664 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20229 19664 603 41 0 20188 0
vsize: 80916
[startup+210.075 s]
Raw data (loadavg): 0.99 0.80 0.40 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 20411 0 0 0 20948 60 0 0 25 0 1 0 478491881 85819392 20386 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20952 20386 603 41 0 20911 0
vsize: 83808
[startup+220.075 s]
Raw data (loadavg): 0.99 0.80 0.40 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 21100 0 0 0 21946 61 0 0 25 0 1 0 478491881 88657920 21075 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21645 21075 603 41 0 21604 0
vsize: 86580
[startup+230.076 s]
Raw data (loadavg): 0.99 0.81 0.41 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 21742 0 0 0 22946 63 0 0 25 0 1 0 478491881 91217920 21717 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22270 21718 603 41 0 22229 0
vsize: 89080
[startup+240.077 s]
Raw data (loadavg): 0.99 0.82 0.42 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 22463 0 0 0 23944 64 0 0 25 0 1 0 478491881 94175232 22438 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22992 22438 603 41 0 22951 0
vsize: 91968
[startup+250.079 s]
Raw data (loadavg): 0.99 0.82 0.42 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 24942 66 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+260.08 s]
Raw data (loadavg): 0.99 0.83 0.43 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 25942 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223696 134560694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+270.08 s]
Raw data (loadavg): 0.99 0.83 0.43 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 26942 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223728 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+280.081 s]
Raw data (loadavg): 0.99 0.84 0.44 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 27942 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+290.081 s]
Raw data (loadavg): 0.99 0.84 0.44 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 28942 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+300.082 s]
Raw data (loadavg): 0.99 0.85 0.45 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 29942 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+310.082 s]
Raw data (loadavg): 0.99 0.85 0.46 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 30942 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+320.083 s]
Raw data (loadavg): 0.99 0.86 0.46 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 31943 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+330.084 s]
Raw data (loadavg): 0.99 0.86 0.47 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 32943 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223664 134560260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+340.085 s]
Raw data (loadavg): 0.99 0.86 0.47 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 33943 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223760 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+350.086 s]
Raw data (loadavg): 0.99 0.87 0.48 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 34943 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223664 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+360.086 s]
Raw data (loadavg): 0.99 0.87 0.48 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 35943 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+370.087 s]
Raw data (loadavg): 0.99 0.88 0.49 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 36943 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+380.088 s]
Raw data (loadavg): 0.99 0.88 0.49 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 37943 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+390.088 s]
Raw data (loadavg): 0.99 0.88 0.50 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 38943 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+400.089 s]
Raw data (loadavg): 0.99 0.89 0.50 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 39944 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+410.09 s]
Raw data (loadavg): 0.99 0.89 0.51 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23169 0 0 0 40944 67 0 0 25 0 1 0 478491881 97132544 23144 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 23144 603 41 0 23673 0
vsize: 94856
[startup+420.091 s]
Raw data (loadavg): 0.99 0.89 0.51 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 23511 0 0 0 41943 68 0 0 25 0 1 0 478491881 98480128 23486 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24043 23486 603 41 0 24002 0
vsize: 96172
[startup+430.091 s]
Raw data (loadavg): 0.99 0.89 0.52 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 24391 0 0 0 42941 70 0 0 25 0 1 0 478491881 102191104 24366 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24949 24366 603 41 0 24908 0
vsize: 99796
[startup+440.092 s]
Raw data (loadavg): 0.99 0.90 0.52 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 25215 0 0 0 43938 73 0 0 25 0 1 0 478491881 105525248 25190 4294967295 134512640 134672761 3221224560 3221223744 134559383 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25763 25190 603 41 0 25722 0
vsize: 103052
[startup+450.093 s]
Raw data (loadavg): 0.99 0.90 0.52 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 26008 0 0 0 44937 75 0 0 25 0 1 0 478491881 108720128 25983 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26543 25983 603 41 0 26502 0
vsize: 106172
[startup+460.094 s]
Raw data (loadavg): 0.99 0.90 0.53 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 26827 0 0 0 45935 77 0 0 25 0 1 0 478491881 112103424 26802 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27369 26802 603 41 0 27328 0
vsize: 109476
[startup+470.094 s]
Raw data (loadavg): 0.99 0.91 0.53 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 27618 0 0 0 46933 79 0 0 25 0 1 0 478491881 115458048 27593 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28188 27593 603 41 0 28147 0
vsize: 112752
[startup+480.094 s]
Raw data (loadavg): 0.99 0.91 0.54 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 28444 0 0 0 47931 82 0 0 25 0 1 0 478491881 118812672 28419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29007 28419 603 41 0 28966 0
vsize: 116028
[startup+490.095 s]
Raw data (loadavg): 0.99 0.91 0.54 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 29171 0 0 0 48929 84 0 0 25 0 1 0 478491881 121733120 29146 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29720 29146 603 41 0 29679 0
vsize: 118880
[startup+500.096 s]
Raw data (loadavg): 0.99 0.91 0.55 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 29874 0 0 0 49927 86 0 0 25 0 1 0 478491881 124694528 29849 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30443 29849 603 41 0 30402 0
vsize: 121772
[startup+510.096 s]
Raw data (loadavg): 0.99 0.92 0.55 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 30560 0 0 0 50926 87 0 0 25 0 1 0 478491881 127508480 30535 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31130 30535 603 41 0 31089 0
vsize: 124520
[startup+520.097 s]
Raw data (loadavg): 0.99 0.92 0.56 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 31069 0 0 0 51924 89 0 0 25 0 1 0 478491881 129548288 31044 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31628 31044 603 41 0 31587 0
vsize: 126512
[startup+530.098 s]
Raw data (loadavg): 0.99 0.92 0.56 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 31601 0 0 0 52923 90 0 0 25 0 1 0 478491881 131719168 31576 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32158 31576 603 41 0 32117 0
vsize: 128632
[startup+540.099 s]
Raw data (loadavg): 0.99 0.92 0.56 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 32099 0 0 0 53923 91 0 0 25 0 1 0 478491881 133869568 32074 4294967295 134512640 134672761 3221224560 3221223744 134559607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32683 32074 603 41 0 32642 0
vsize: 130732
[startup+550.1 s]
Raw data (loadavg): 0.99 0.92 0.57 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 32571 0 0 0 54922 92 0 0 25 0 1 0 478491881 135745536 32546 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33141 32546 603 41 0 33100 0
vsize: 132564
[startup+560.101 s]
Raw data (loadavg): 0.99 0.93 0.57 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33017 0 0 0 55922 93 0 0 25 0 1 0 478491881 137502720 32992 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33570 32992 603 41 0 33529 0
vsize: 134280
[startup+570.102 s]
Raw data (loadavg): 0.99 0.93 0.58 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33508 0 0 0 56921 94 0 0 25 0 1 0 478491881 139517952 33483 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34062 33483 603 41 0 34021 0
vsize: 136248
[startup+580.102 s]
Raw data (loadavg): 0.99 0.93 0.58 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33608 0 0 0 57920 95 0 0 25 0 1 0 478491881 139923456 33583 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33583 603 41 0 34120 0
vsize: 136644
[startup+590.103 s]
Raw data (loadavg): 0.99 0.93 0.58 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33608 0 0 0 58920 95 0 0 25 0 1 0 478491881 139923456 33583 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33583 603 41 0 34120 0
vsize: 136644
[startup+600.103 s]
Raw data (loadavg): 0.99 0.93 0.59 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33608 0 0 0 59921 95 0 0 25 0 1 0 478491881 139923456 33583 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33583 603 41 0 34120 0
vsize: 136644
[startup+610.104 s]
Raw data (loadavg): 0.99 0.94 0.59 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33608 0 0 0 60921 95 0 0 25 0 1 0 478491881 139923456 33583 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33583 603 41 0 34120 0
vsize: 136644
[startup+620.104 s]
Raw data (loadavg): 0.99 0.94 0.60 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33608 0 0 0 61921 95 0 0 25 0 1 0 478491881 139923456 33583 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33583 603 41 0 34120 0
vsize: 136644
[startup+630.105 s]
Raw data (loadavg): 0.99 0.94 0.60 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33609 0 0 0 62921 95 0 0 25 0 1 0 478491881 139923456 33584 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33584 603 41 0 34120 0
vsize: 136644
[startup+640.105 s]
Raw data (loadavg): 0.99 0.94 0.60 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33610 0 0 0 63922 95 0 0 25 0 1 0 478491881 139923456 33585 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33585 603 41 0 34120 0
vsize: 136644
[startup+650.106 s]
Raw data (loadavg): 0.99 0.94 0.61 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33610 0 0 0 64922 95 0 0 25 0 1 0 478491881 139923456 33585 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33585 603 41 0 34120 0
vsize: 136644
[startup+660.107 s]
Raw data (loadavg): 0.99 0.94 0.61 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33610 0 0 0 65922 95 0 0 25 0 1 0 478491881 139923456 33585 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33585 603 41 0 34120 0
vsize: 136644
[startup+670.107 s]
Raw data (loadavg): 0.99 0.94 0.62 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33610 0 0 0 66922 95 0 0 25 0 1 0 478491881 139923456 33585 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33585 603 41 0 34120 0
vsize: 136644
[startup+680.108 s]
Raw data (loadavg): 0.99 0.95 0.62 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33610 0 0 0 67923 95 0 0 25 0 1 0 478491881 139923456 33585 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33585 603 41 0 34120 0
vsize: 136644
[startup+690.109 s]
Raw data (loadavg): 0.99 0.95 0.62 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33610 0 0 0 68923 95 0 0 25 0 1 0 478491881 139923456 33585 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33585 603 41 0 34120 0
vsize: 136644
[startup+700.11 s]
Raw data (loadavg): 0.99 0.95 0.63 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33610 0 0 0 69923 95 0 0 25 0 1 0 478491881 139923456 33585 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33585 603 41 0 34120 0
vsize: 136644
[startup+710.111 s]
Raw data (loadavg): 0.99 0.95 0.63 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33610 0 0 0 70923 95 0 0 25 0 1 0 478491881 139923456 33585 4294967295 134512640 134672761 3221224560 3221223664 134555205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33585 603 41 0 34120 0
vsize: 136644
[startup+720.111 s]
Raw data (loadavg): 0.99 0.95 0.63 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33610 0 0 0 71924 95 0 0 25 0 1 0 478491881 139923456 33585 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33585 603 41 0 34120 0
vsize: 136644
[startup+730.112 s]
Raw data (loadavg): 0.99 0.95 0.64 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33610 0 0 0 72924 95 0 0 25 0 1 0 478491881 139923456 33585 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33585 603 41 0 34120 0
vsize: 136644
[startup+740.113 s]
Raw data (loadavg): 0.99 0.95 0.64 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33610 0 0 0 73924 95 0 0 25 0 1 0 478491881 139923456 33585 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34161 33585 603 41 0 34120 0
vsize: 136644
[startup+750.115 s]
Raw data (loadavg): 0.99 0.95 0.64 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 74923 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+760.115 s]
Raw data (loadavg): 0.99 0.95 0.65 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 75923 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+770.115 s]
Raw data (loadavg): 0.99 0.95 0.65 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 76923 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+780.116 s]
Raw data (loadavg): 0.99 0.96 0.65 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 77924 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+790.116 s]
Raw data (loadavg): 0.99 0.96 0.66 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 78924 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+800.117 s]
Raw data (loadavg): 0.99 0.96 0.66 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 79924 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+810.118 s]
Raw data (loadavg): 0.99 0.96 0.66 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 80924 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+820.119 s]
Raw data (loadavg): 0.99 0.96 0.66 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 81925 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+830.12 s]
Raw data (loadavg): 0.99 0.96 0.67 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 82925 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+840.12 s]
Raw data (loadavg): 0.99 0.96 0.67 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 83925 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+850.122 s]
Raw data (loadavg): 0.99 0.96 0.67 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 84925 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+860.123 s]
Raw data (loadavg): 0.99 0.96 0.68 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 85926 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+870.124 s]
Raw data (loadavg): 0.99 0.96 0.68 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 86926 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+880.124 s]
Raw data (loadavg): 0.99 0.97 0.68 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 87926 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+890.125 s]
Raw data (loadavg): 0.99 0.97 0.68 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 88926 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+900.126 s]
Raw data (loadavg): 0.99 0.97 0.69 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 89927 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+910.126 s]
Raw data (loadavg): 0.99 0.97 0.69 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 90927 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+920.126 s]
Raw data (loadavg): 0.99 0.97 0.69 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 91927 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+930.127 s]
Raw data (loadavg): 0.99 0.97 0.70 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 92927 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+940.128 s]
Raw data (loadavg): 0.99 0.97 0.70 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33611 0 0 0 93928 95 0 0 25 0 1 0 478491881 139923456 33586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34161 33586 603 41 0 34120 0
vsize: 136644
[startup+950.129 s]
Raw data (loadavg): 0.99 0.97 0.70 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 33977 0 0 0 94927 96 0 0 25 0 1 0 478491881 141393920 33952 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34520 33952 603 41 0 34479 0
vsize: 138080
[startup+960.129 s]
Raw data (loadavg): 0.99 0.97 0.71 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 34591 0 0 0 95925 98 0 0 25 0 1 0 478491881 143945728 34566 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35143 34566 603 41 0 35102 0
vsize: 140572
[startup+970.13 s]
Raw data (loadavg): 0.99 0.97 0.71 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 35175 0 0 0 96923 100 0 0 25 0 1 0 478491881 146366464 35150 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35734 35150 603 41 0 35693 0
vsize: 142936
[startup+980.131 s]
Raw data (loadavg): 0.99 0.97 0.71 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 35706 0 0 0 97922 102 0 0 25 0 1 0 478491881 148512768 35681 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36258 35681 603 41 0 36217 0
vsize: 145032
[startup+990.132 s]
Raw data (loadavg): 0.99 0.97 0.71 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 36300 0 0 0 98921 103 0 0 25 0 1 0 478491881 150925312 36275 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36847 36275 603 41 0 36806 0
vsize: 147388
[startup+1000.13 s]
Raw data (loadavg): 0.99 0.97 0.72 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 36709 0 0 0 99920 104 0 0 25 0 1 0 478491881 152686592 36684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37277 36684 603 41 0 37236 0
vsize: 149108
[startup+1010.13 s]
Raw data (loadavg): 0.99 0.97 0.72 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 37222 0 0 0 100919 106 0 0 25 0 1 0 478491881 154836992 37197 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37802 37197 603 41 0 37761 0
vsize: 151208
[startup+1020.13 s]
Raw data (loadavg): 0.99 0.97 0.72 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 37694 0 0 0 101918 107 0 0 25 0 1 0 478491881 156708864 37669 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38259 37669 603 41 0 38218 0
vsize: 153036
[startup+1030.14 s]
Raw data (loadavg): 0.99 0.97 0.73 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 38115 0 0 0 102917 108 0 0 25 0 1 0 478491881 158445568 38090 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38683 38090 603 41 0 38642 0
vsize: 154732
[startup+1040.14 s]
Raw data (loadavg): 0.99 0.97 0.73 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 38603 0 0 0 103917 108 0 0 25 0 1 0 478491881 160452608 38578 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39173 38578 603 41 0 39132 0
vsize: 156692
[startup+1050.14 s]
Raw data (loadavg): 0.99 0.97 0.73 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39047 0 0 0 104916 109 0 0 25 0 1 0 478491881 162193408 39022 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39598 39022 603 41 0 39557 0
vsize: 158392
[startup+1060.14 s]
Raw data (loadavg): 0.99 0.97 0.73 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39324 0 0 0 105916 110 0 0 25 0 1 0 478491881 163397632 39299 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39299 603 41 0 39851 0
vsize: 159568
[startup+1070.14 s]
Raw data (loadavg): 0.99 0.97 0.73 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39324 0 0 0 106916 110 0 0 25 0 1 0 478491881 163397632 39299 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39299 603 41 0 39851 0
vsize: 159568
[startup+1080.14 s]
Raw data (loadavg): 0.99 0.97 0.74 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39324 0 0 0 107916 110 0 0 25 0 1 0 478491881 163397632 39299 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39299 603 41 0 39851 0
vsize: 159568
[startup+1090.14 s]
Raw data (loadavg): 0.99 0.97 0.74 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39324 0 0 0 108917 110 0 0 25 0 1 0 478491881 163397632 39299 4294967295 134512640 134672761 3221224560 3221223664 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39299 603 41 0 39851 0
vsize: 159568
[startup+1100.14 s]
Raw data (loadavg): 0.99 0.97 0.74 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39325 0 0 0 109917 110 0 0 25 0 1 0 478491881 163397632 39300 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39300 603 41 0 39851 0
vsize: 159568
[startup+1110.14 s]
Raw data (loadavg): 0.99 0.97 0.74 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39325 0 0 0 110917 110 0 0 25 0 1 0 478491881 163397632 39300 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39300 603 41 0 39851 0
vsize: 159568
[startup+1120.14 s]
Raw data (loadavg): 0.99 0.97 0.74 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39325 0 0 0 111917 110 0 0 25 0 1 0 478491881 163397632 39300 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39300 603 41 0 39851 0
vsize: 159568
[startup+1130.14 s]
Raw data (loadavg): 0.99 0.97 0.75 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39325 0 0 0 112918 110 0 0 25 0 1 0 478491881 163397632 39300 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39300 603 41 0 39851 0
vsize: 159568
[startup+1140.14 s]
Raw data (loadavg): 0.99 0.97 0.75 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39325 0 0 0 113918 110 0 0 25 0 1 0 478491881 163397632 39300 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39300 603 41 0 39851 0
vsize: 159568
[startup+1150.14 s]
Raw data (loadavg): 0.99 0.97 0.75 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39325 0 0 0 114918 110 0 0 25 0 1 0 478491881 163397632 39300 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39300 603 41 0 39851 0
vsize: 159568
[startup+1160.15 s]
Raw data (loadavg): 0.99 0.97 0.75 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39325 0 0 0 115918 110 0 0 25 0 1 0 478491881 163397632 39300 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39300 603 41 0 39851 0
vsize: 159568
[startup+1170.15 s]
Raw data (loadavg): 0.99 0.97 0.75 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39325 0 0 0 116919 110 0 0 25 0 1 0 478491881 163397632 39300 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39300 603 41 0 39851 0
vsize: 159568
[startup+1180.15 s]
Raw data (loadavg): 0.99 0.97 0.76 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39325 0 0 0 117919 110 0 0 25 0 1 0 478491881 163397632 39300 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39300 603 41 0 39851 0
vsize: 159568
[startup+1190.15 s]
Raw data (loadavg): 0.99 0.97 0.76 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39326 0 0 0 118919 110 0 0 25 0 1 0 478491881 163397632 39301 4294967295 134512640 134672761 3221224560 3221223776 134557677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39892 39301 603 41 0 39851 0
vsize: 159568
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.76 2/53 10704
Raw data (stat): 10704 (minisat+) R 10703 7987 7986 0 -1 0 39326 0 0 0 119919 110 0 0 25 0 1 0 478491881 163397632 39301 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39892 39301 603 41 0 39851 0
vsize: 159568
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.24 s]
Raw data (loadavg): 0.99 0.97 0.76 1/53 10704
Raw data (stat): 10704 (minisat+) Z 10703 7987 7986 0 -1 12 39329 0 0 0 119920 118 0 0 25 0 1 0 478491881 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.24
CPU time (s): 1200.38
CPU user time (s): 1199.2
CPU system time (s): 1.18182
CPU usage (%): 100.012
Max. virtual memory (Kb): 159568
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####