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 5421

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        903240 kB
Buffers:         33988 kB
Cached:          76984 kB
SwapCached:          4 kB
Active:          56116 kB
Inactive:        57728 kB
HighTotal:      131008 kB
HighFree:        50148 kB
LowTotal:       903652 kB
LowFree:        853092 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11932 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:10:56 (client local time) WITH STATUS 10 IN 1200.34 SECONDS
stats: 3828 7 1200.34 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |     509    25694 |     152       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |     509    25694 |     203       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.408937 s)
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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   65841   259005 |   19752       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/14009          
c   -- var.elim.:  2000/14009          
c   -- var.elim.:  3000/14009          
c   -- var.elim.:  4000/14009          
c   -- var.elim.:  5000/14009          
c   -- var.elim.:  6000/14009          
c   -- var.elim.:  7000/14009          
c   -- var.elim.:  8000/14009          
c   -- var.elim.:  9000/14009          
c   -- var.elim.:  10000/14009          
c   -- var.elim.:  11000/14009          
c   -- var.elim.:  12000/14009          
c   -- var.elim.:  13000/14009          
c   -- var.elim.:  14000/14009          
c   -- var.elim.:  14009/14009          
c   -- var.elim.:  24/24          
c |         0 |   65772   258717 |      --       0       --      -- |     --   | -47/-187
c |         0 |   65772   258717 |   26308       0        0     nan |  0.000 % |
c |       100 |   65772   258717 |   28939     100      356     3.6 |  0.114 % |
c |       250 |   65741   258611 |   31818     249     1145     4.6 |  0.143 % |
c |       475 |   65731   258572 |   34995     471     1991     4.2 |  0.150 % |
c |       812 |   65713   258506 |   38484     806     3232     4.0 |  0.164 % |
c |      1319 |   65713   258506 |   42332    1313     5164     3.9 |  0.164 % |
c |      2078 |   65672   258350 |   46536    2067     8395     4.1 |  0.200 % |
c |      3217 |   65672   258350 |   51190    3206    20657     6.4 |  0.200 % |
c |      4926 |   65642   258246 |   56283    4910   111525    22.7 |  0.228 % |
c |      7488 |   65546   257893 |   61821    7447   274702    36.9 |  0.321 % |
c |     11332 |   65528   257816 |   67985   11280  1037687    92.0 |  0.335 % |
c |     17098 |   65431   257443 |   74672   17034  2219441   130.3 |  0.414 % |
c |     25747 |   65413   257377 |   82117   25654  4689376   182.8 |  0.435 % |
c |     38725 |   65388   257277 |   90294   38626  8766912   227.0 |  0.457 % |
c |     58187 |   65361   257178 |   99283   58080 16369489   281.8 |  0.478 % |
c |     87388 |   65361   257178 |  109211   87281 30832745   353.3 |  0.478 % |
c |    131179 |   65356   257163 |  120123   38417 11887720   309.4 |  0.485 % |
c |    196863 |   65346   257124 |  132115  104100 44324798   425.8 |  0.492 % |
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 -x42#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 23843
Raw data (stat): 23843 (runsolver) R 23842 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421827478 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 8485 0 0 0 980 18 0 0 25 0 1 0 421827478 33013760 7005 4294967295 134512640 134672761 3221224576 3221223776 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8060 7005 603 41 0 8019 0
vsize: 32240
[startup+20 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 8926 0 0 0 1979 19 0 0 25 0 1 0 421827478 34918400 7446 4294967295 134512640 134672761 3221224576 3221223388 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8525 7446 603 41 0 8484 0
vsize: 34100
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 10413 0 0 0 2974 25 0 0 25 0 1 0 421827478 40984576 8933 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10006 8933 603 41 0 9965 0
vsize: 40024
[startup+40.0001 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 11734 0 0 0 3968 30 0 0 25 0 1 0 421827478 46379008 10254 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11323 10254 603 41 0 11282 0
vsize: 45292
[startup+50.0002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 13123 0 0 0 4964 35 0 0 25 0 1 0 421827478 52072448 11643 4294967295 134512640 134672761 3221224576 3221223388 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12713 11643 603 41 0 12672 0
vsize: 50852
[startup+60.0008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 14322 0 0 0 5960 39 0 0 25 0 1 0 421827478 56954880 12842 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13905 12842 603 41 0 13864 0
vsize: 55620
[startup+70.0012 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 15232 0 0 0 6958 41 0 0 25 0 1 0 421827478 60760064 13752 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14834 13752 603 41 0 14793 0
vsize: 59336
[startup+80.0022 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 16184 0 0 0 7956 43 0 0 25 0 1 0 421827478 64692224 14704 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15794 14704 603 41 0 15753 0
vsize: 63176
[startup+90.0019 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 17264 0 0 0 8954 46 0 0 25 0 1 0 421827478 69181440 15784 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16890 15784 603 41 0 16849 0
vsize: 67560
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 18027 0 0 0 9951 48 0 0 25 0 1 0 421827478 72237056 16547 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17636 16547 603 41 0 17595 0
vsize: 70544
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 19171 0 0 0 10948 52 0 0 25 0 1 0 421827478 76996608 17691 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18798 17691 603 41 0 18757 0
vsize: 75192
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 20282 0 0 0 11945 55 0 0 25 0 1 0 421827478 81461248 18802 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19888 18802 603 41 0 19847 0
vsize: 79552
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 21221 0 0 0 12943 58 0 0 25 0 1 0 421827478 85282816 19741 4294967295 134512640 134672761 3221224576 3221223388 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20821 19742 603 41 0 20780 0
vsize: 83284
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 22119 0 0 0 13940 61 0 0 25 0 1 0 421827478 88981504 20639 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21724 20639 603 41 0 21683 0
vsize: 86896
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 23007 0 0 0 14938 63 0 0 25 0 1 0 421827478 92545024 21527 4294967295 134512640 134672761 3221224576 3221223700 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22594 21527 603 41 0 22553 0
vsize: 90376
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 23999 0 0 0 15936 65 0 0 25 0 1 0 421827478 96620544 22519 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23589 22519 603 41 0 23548 0
vsize: 94356
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 24981 0 0 0 16933 68 0 0 25 0 1 0 421827478 100700160 23501 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24585 23501 603 41 0 24544 0
vsize: 98340
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 25881 0 0 0 17932 70 0 0 25 0 1 0 421827478 104390656 24401 4294967295 134512640 134672761 3221224576 3221223712 134614710 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25486 24401 603 41 0 25445 0
vsize: 101944
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 26719 0 0 0 18930 71 0 0 25 0 1 0 421827478 107823104 25239 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26324 25239 603 41 0 26283 0
vsize: 105296
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 27529 0 0 0 19928 74 0 0 25 0 1 0 421827478 111120384 26049 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27129 26049 603 41 0 27088 0
vsize: 108516
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 28502 0 0 0 20925 77 0 0 25 0 1 0 421827478 115064832 27022 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28092 27022 603 41 0 28051 0
vsize: 112368
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 29419 0 0 0 21923 79 0 0 25 0 1 0 421827478 118845440 27939 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29015 27939 603 41 0 28974 0
vsize: 116060
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 30132 0 0 0 22921 81 0 0 25 0 1 0 421827478 121991168 28652 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29783 28652 603 41 0 29742 0
vsize: 119132
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 30765 0 0 0 23919 83 0 0 25 0 1 0 421827478 124616704 29285 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30424 29285 603 41 0 30383 0
vsize: 121696
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 31430 0 0 0 24918 85 0 0 25 0 1 0 421827478 127270912 29950 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31072 29950 603 41 0 31031 0
vsize: 124288
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 32051 0 0 0 25916 87 0 0 25 0 1 0 421827478 129908736 30571 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31716 30571 603 41 0 31675 0
vsize: 126864
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 32693 0 0 0 26914 90 0 0 25 0 1 0 421827478 132538368 31213 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32358 31213 603 41 0 32317 0
vsize: 129432
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 33512 0 0 0 27912 91 0 0 25 0 1 0 421827478 135823360 32032 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33160 32032 603 41 0 33119 0
vsize: 132640
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 34390 0 0 0 28910 94 0 0 25 0 1 0 421827478 139370496 32910 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34026 32910 603 41 0 33985 0
vsize: 136104
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 35087 0 0 0 29908 96 0 0 25 0 1 0 421827478 142254080 33607 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34730 33607 603 41 0 34689 0
vsize: 138920
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 35902 0 0 0 30906 98 0 0 25 0 1 0 421827478 145674240 34422 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35565 34422 603 41 0 35524 0
vsize: 142260
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 36414 0 0 0 31905 99 0 0 25 0 1 0 421827478 147779584 34934 4294967295 134512640 134672761 3221224576 3221223700 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36079 34934 603 41 0 36038 0
vsize: 144316
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 36909 0 0 0 32904 100 0 0 25 0 1 0 421827478 149749760 35429 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36560 35429 603 41 0 36519 0
vsize: 146240
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 37554 0 0 0 33902 102 0 0 25 0 1 0 421827478 152379392 36074 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37202 36074 603 41 0 37161 0
vsize: 148808
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 38241 0 0 0 34901 104 0 0 25 0 1 0 421827478 155144192 36761 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37877 36761 603 41 0 37836 0
vsize: 151508
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 39153 0 0 0 35899 106 0 0 25 0 1 0 421827478 158969856 37673 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38811 37673 603 41 0 38770 0
vsize: 155244
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 40246 0 0 0 36897 108 0 0 25 0 1 0 421827478 163336192 38766 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39877 38766 603 41 0 39836 0
vsize: 159508
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 40770 0 0 0 37895 110 0 0 25 0 1 0 421827478 165576704 39290 4294967295 134512640 134672761 3221224576 3221223720 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40424 39290 603 41 0 40383 0
vsize: 161696
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 41173 0 0 0 38894 111 0 0 25 0 1 0 421827478 167170048 39693 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40813 39693 603 41 0 40772 0
vsize: 163252
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 41853 0 0 0 39892 113 0 0 25 0 1 0 421827478 169922560 40373 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41485 40373 603 41 0 41444 0
vsize: 165940
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 42649 0 0 0 40890 116 0 0 25 0 1 0 421827478 173215744 41169 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42289 41169 603 41 0 42248 0
vsize: 169156
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 43504 0 0 0 41887 118 0 0 25 0 1 0 421827478 176758784 42024 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43154 42024 603 41 0 43113 0
vsize: 172616
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 44478 0 0 0 42886 120 0 0 25 0 1 0 421827478 180690944 42998 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44114 42998 603 41 0 44073 0
vsize: 176456
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 45325 0 0 0 43884 123 0 0 25 0 1 0 421827478 184131584 43845 4294967295 134512640 134672761 3221224576 3221223680 134604304 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44954 43845 603 41 0 44913 0
vsize: 179816
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 45959 0 0 0 44882 124 0 0 25 0 1 0 421827478 186761216 44479 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45596 44480 603 41 0 45555 0
vsize: 182384
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 46557 0 0 0 45881 125 0 0 25 0 1 0 421827478 189255680 45077 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46205 45077 603 41 0 46164 0
vsize: 184820
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 47084 0 0 0 46880 127 0 0 25 0 1 0 421827478 191361024 45604 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46719 45604 603 41 0 46678 0
vsize: 186876
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 47693 0 0 0 47879 128 0 0 25 0 1 0 421827478 193871872 46213 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47332 46213 603 41 0 47291 0
vsize: 189328
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 48508 0 0 0 48877 130 0 0 25 0 1 0 421827478 197206016 47028 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48146 47028 603 41 0 48105 0
vsize: 192584
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 49151 0 0 0 49876 132 0 0 25 0 1 0 421827478 199819264 47671 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48784 47671 603 41 0 48743 0
vsize: 195136
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 49901 0 0 0 50874 134 0 0 25 0 1 0 421827478 202854400 48421 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49525 48421 603 41 0 49484 0
vsize: 198100
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 50443 0 0 0 51873 135 0 0 25 0 1 0 421827478 205201408 48963 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50098 48963 603 41 0 50057 0
vsize: 200392
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51004 0 0 0 52872 137 0 0 25 0 1 0 421827478 207433728 49524 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50643 49524 603 41 0 50602 0
vsize: 202572
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23843
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51865 0 0 0 53870 139 0 0 25 0 1 0 421827478 210968576 50385 4294967295 134512640 134672761 3221224576 3221223200 134645493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50385 603 41 0 51465 0
vsize: 206024
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23846
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 54866 143 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+560.015 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 23896
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 55864 145 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+570.015 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 23896
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 56864 145 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+580.015 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 23896
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 57864 146 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+590.015 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 23896
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 58864 146 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223712 134614741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+600.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 23896
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 59863 146 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+610.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 23896
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 60863 147 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+620.015 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 61863 147 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+630.015 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 62863 147 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+640.016 s]
Raw data (loadavg): 1.02 0.99 0.91 3/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 63863 148 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+650.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 64863 148 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+660.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 65863 148 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+670.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 66862 148 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+680.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 67862 149 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+690.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 68862 149 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+700.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 69862 149 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+710.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 70862 150 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+720.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 71862 150 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+730.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 72862 150 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+740.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 73861 151 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+750.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 74861 151 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+760.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 75861 152 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223616 134613822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+770.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 76861 152 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+780.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 77860 152 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+790.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 78860 153 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+800.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 79860 153 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+810.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 80860 154 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+820.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 81859 154 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+830.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 82859 154 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223776 134610705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+840.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 83859 155 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+850.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 84859 155 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+860.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 85859 155 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+870.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 86859 155 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+880.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 87859 156 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+890.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23898
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 88859 156 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+900.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 89859 156 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+910.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 90858 157 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+920.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 91858 157 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+930.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 51956 0 0 0 92858 157 0 0 25 0 1 0 421827478 210968576 50367 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 50367 603 41 0 51465 0
vsize: 206024
[startup+940.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 52446 0 0 0 93856 159 0 0 25 0 1 0 421827478 213065728 50857 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52018 50857 603 41 0 51977 0
vsize: 208072
[startup+950.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 53003 0 0 0 94854 162 0 0 25 0 1 0 421827478 215310336 51414 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52566 51414 603 41 0 52525 0
vsize: 210264
[startup+960.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 53627 0 0 0 95852 164 0 0 25 0 1 0 421827478 217927680 52038 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53205 52038 603 41 0 53164 0
vsize: 212820
[startup+970.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 54287 0 0 0 96850 166 0 0 25 0 1 0 421827478 220573696 52698 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53851 52698 603 41 0 53810 0
vsize: 215404
[startup+980.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 54979 0 0 0 97848 168 0 0 25 0 1 0 421827478 223453184 53390 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54554 53390 603 41 0 54513 0
vsize: 218216
[startup+990.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 55319 0 0 0 98846 170 0 0 25 0 1 0 421827478 224796672 53730 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54882 53730 603 41 0 54841 0
vsize: 219528
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 55707 0 0 0 99845 172 0 0 25 0 1 0 421827478 226369536 54118 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55266 54118 603 41 0 55225 0
vsize: 221064
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 56251 0 0 0 100844 173 0 0 25 0 1 0 421827478 228597760 54662 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55810 54662 603 41 0 55769 0
vsize: 223240
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 56806 0 0 0 101842 175 0 0 25 0 1 0 421827478 230965248 55217 4294967295 134512640 134672761 3221224576 3221223616 134614212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56388 55217 603 41 0 56347 0
vsize: 225552
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 57533 0 0 0 102840 177 0 0 25 0 1 0 421827478 233848832 55944 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57092 55944 603 41 0 57051 0
vsize: 228368
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 58123 0 0 0 103839 179 0 0 25 0 1 0 421827478 236359680 56534 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57705 56534 603 41 0 57664 0
vsize: 230820
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 58623 0 0 0 104837 181 0 0 25 0 1 0 421827478 238346240 57034 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58190 57034 603 41 0 58149 0
vsize: 232760
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 59345 0 0 0 105834 184 0 0 25 0 1 0 421827478 241364992 57756 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58927 57756 603 41 0 58886 0
vsize: 235708
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 60137 0 0 0 106832 186 0 0 25 0 1 0 421827478 244523008 58548 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59698 58548 603 41 0 59657 0
vsize: 238792
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 60681 0 0 0 107830 188 0 0 25 0 1 0 421827478 246771712 59092 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60247 59092 603 41 0 60206 0
vsize: 240988
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 61163 0 0 0 108828 190 0 0 25 0 1 0 421827478 248745984 59574 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60729 59574 603 41 0 60688 0
vsize: 242916
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 61621 0 0 0 109828 191 0 0 25 0 1 0 421827478 250597376 60032 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61181 60032 603 41 0 61140 0
vsize: 244724
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 62087 0 0 0 110826 193 0 0 25 0 1 0 421827478 252596224 60498 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61669 60498 603 41 0 61628 0
vsize: 246676
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 62592 0 0 0 111825 194 0 0 25 0 1 0 421827478 254578688 61003 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62153 61003 603 41 0 62112 0
vsize: 248612
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 63220 0 0 0 112824 195 0 0 25 0 1 0 421827478 257212416 61631 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62796 61631 603 41 0 62755 0
vsize: 251184
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 63872 0 0 0 113821 197 0 0 25 0 1 0 421827478 259825664 62283 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63434 62283 603 41 0 63393 0
vsize: 253736
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 64246 0 0 0 114821 198 0 0 25 0 1 0 421827478 261390336 62657 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63816 62657 603 41 0 63775 0
vsize: 255264
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 64669 0 0 0 115820 200 0 0 25 0 1 0 421827478 263106560 63080 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64235 63080 603 41 0 64194 0
vsize: 256940
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 65273 0 0 0 116818 201 0 0 25 0 1 0 421827478 265580544 63684 4294967295 134512640 134672761 3221224576 3221223760 134616011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64839 63684 603 41 0 64798 0
vsize: 259356
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 65750 0 0 0 117817 203 0 0 25 0 1 0 421827478 267550720 64161 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65320 64161 603 41 0 65279 0
vsize: 261280
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 66502 0 0 0 118815 205 0 0 25 0 1 0 421827478 270536704 64913 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66049 64913 603 41 0 66008 0
vsize: 264196
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23900
Raw data (stat): 23843 (minisat+) R 23842 20937 20936 0 -1 0 67316 0 0 0 119814 206 0 0 25 0 1 0 421827478 273948672 65727 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66882 65727 603 41 0 66841 0
vsize: 267528
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 23900
Raw data (stat): 23843 (minisat+) Z 23842 20937 20936 0 -1 12 67317 0 0 0 119814 219 0 0 25 0 1 0 421827478 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.15
CPU time (s): 1200.34
CPU user time (s): 1198.15
CPU system time (s): 2.19367
CPU usage (%): 100.016
Max. virtual memory (Kb): 267528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####