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 4827

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-13 20:27:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=563 boxname=wulflinc17 idbench=63 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  773129c71f80eff294fafd0a8a5769cd  /oldhome/oroussel/tmp/wulflinc17/normalized-bench1.pi.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc17/normalized-bench1.pi.opb
IDLAUNCH: 563
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        849996 kB
Buffers:         34248 kB
Cached:         115764 kB
SwapCached:       2376 kB
Active:          51360 kB
Inactive:       103992 kB
HighTotal:      131008 kB
HighFree:        11704 kB
LowTotal:       903652 kB
LowFree:        838292 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23652 kB
Committed_AS:    63696 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:47:40 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 563 7 1200.23 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.85 0.94 0.90 2/55 25061
Raw data (stat): 25061 (runsolver) R 25060 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478834572 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 7248 0 3 0 977 17 0 0 25 0 1 0 478834572 28073984 5905 4294967295 134512640 134672761 3221224640 3221223792 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6854 5905 603 41 0 6813 0
vsize: 27416
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 7684 0 3 0 1975 19 0 0 25 0 1 0 478834572 29892608 6341 4294967295 134512640 134672761 3221224640 3221223808 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7298 6341 603 41 0 7257 0
vsize: 29192
[startup+30.0007 s]
Raw data (loadavg): 0.91 0.94 0.90 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 8430 0 3 0 2974 20 0 0 25 0 1 0 478834572 32935936 7087 4294967295 134512640 134672761 3221224640 3221223744 134560352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8041 7087 603 41 0 8000 0
vsize: 32164
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 9419 0 3 0 3971 22 0 0 25 0 1 0 478834572 36970496 8076 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9026 8076 603 41 0 8985 0
vsize: 36104
[startup+50.0013 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 10220 0 3 0 4969 24 0 0 25 0 1 0 478834572 40194048 8877 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9813 8877 603 41 0 9772 0
vsize: 39252
[startup+60.0012 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 11364 0 3 0 5966 28 0 0 25 0 1 0 478834572 45039616 10021 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10996 10021 603 41 0 10955 0
vsize: 43984
[startup+70.0018 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 12463 0 3 0 6963 31 0 0 25 0 1 0 478834572 49487872 11120 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12082 11120 603 41 0 12041 0
vsize: 48328
[startup+80.0011 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 13602 0 3 0 7960 34 0 0 25 0 1 0 478834572 54185984 12259 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13229 12259 603 41 0 13188 0
vsize: 52916
[startup+90.0011 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 14860 0 3 0 8957 37 0 0 25 0 1 0 478834572 59297792 13517 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14477 13517 603 41 0 14436 0
vsize: 57908
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 15963 0 3 0 9953 41 0 0 25 0 1 0 478834572 63737856 14620 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15561 14620 603 41 0 15520 0
vsize: 62244
[startup+110 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 17110 0 3 0 10950 44 0 0 25 0 1 0 478834572 68423680 15767 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16705 15767 603 41 0 16664 0
vsize: 66820
[startup+120.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 18064 0 3 0 11948 46 0 0 25 0 1 0 478834572 72327168 16721 4294967295 134512640 134672761 3221224640 3221223744 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17658 16721 603 41 0 17617 0
vsize: 70632
[startup+130 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 19150 0 3 0 12945 50 0 0 25 0 1 0 478834572 76771328 17807 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18743 17807 603 41 0 18702 0
vsize: 74972
[startup+140.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 20183 0 3 0 13943 52 0 0 25 0 1 0 478834572 81334272 18840 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19857 18840 603 41 0 19816 0
vsize: 79428
[startup+150.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 21069 0 3 0 14941 54 0 0 25 0 1 0 478834572 84832256 19726 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20711 19726 603 41 0 20670 0
vsize: 82844
[startup+160 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 22008 0 3 0 15940 56 0 0 25 0 1 0 478834572 88731648 20665 4294967295 134512640 134672761 3221224640 3221223744 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21663 20665 603 41 0 21622 0
vsize: 86652
[startup+170.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25061
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 22938 0 3 0 16938 57 0 0 25 0 1 0 478834572 92491776 21595 4294967295 134512640 134672761 3221224640 3221223640 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22581 21595 603 41 0 22540 0
vsize: 90324
[startup+180.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 23832 0 3 0 17935 60 0 0 25 0 1 0 478834572 96235520 22489 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23495 22489 603 41 0 23454 0
vsize: 93980
[startup+190.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 24609 0 3 0 18933 63 0 0 25 0 1 0 478834572 99336192 23266 4294967295 134512640 134672761 3221224640 3221223744 134560269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24252 23266 603 41 0 24211 0
vsize: 97008
[startup+200 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 25260 0 3 0 19932 64 0 0 25 0 1 0 478834572 102023168 23917 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24908 23917 603 41 0 24867 0
vsize: 99632
[startup+210 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 26007 0 3 0 20931 66 0 0 25 0 1 0 478834572 105115648 24664 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25663 24664 603 41 0 25622 0
vsize: 102652
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 26734 0 3 0 21929 67 0 0 25 0 1 0 478834572 108072960 25391 4294967295 134512640 134672761 3221224640 3221223744 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26385 25391 603 41 0 26344 0
vsize: 105540
[startup+230 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 27379 0 3 0 22927 70 0 0 25 0 1 0 478834572 110759936 26036 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27041 26036 603 41 0 27000 0
vsize: 108164
[startup+240 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28155 0 3 0 23925 72 0 0 25 0 1 0 478834572 113868800 26812 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27800 26812 603 41 0 27759 0
vsize: 111200
[startup+250 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 24924 73 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 25923 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+270 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 26923 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+279.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 27923 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+290 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 28924 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 29924 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 30924 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+320 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 31924 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223808 134560811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+330 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 32924 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+340 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 33925 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+349.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 34925 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223744 134555096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+359.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 35925 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+370 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 36925 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+379.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 37925 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+390 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 38925 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223824 134558934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+400 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28707 0 3 0 39926 74 0 0 25 0 1 0 478834572 116146176 27364 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28356 27364 603 41 0 28315 0
vsize: 113424
[startup+409.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 28805 0 3 0 40925 74 0 0 25 0 1 0 478834572 116547584 27462 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28454 27462 603 41 0 28413 0
vsize: 113816
[startup+419.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 29718 0 3 0 41923 77 0 0 25 0 1 0 478834572 120295424 28375 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29369 28375 603 41 0 29328 0
vsize: 117476
[startup+430 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 30600 0 3 0 42921 79 0 0 25 0 1 0 478834572 123936768 29257 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 29257 603 41 0 30217 0
vsize: 121032
[startup+440 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 31425 0 3 0 43919 81 0 0 25 0 1 0 478834572 127287296 30082 4294967295 134512640 134672761 3221224640 3221223744 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31076 30082 603 41 0 31035 0
vsize: 124304
[startup+450 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 32278 0 3 0 44917 83 0 0 25 0 1 0 478834572 130797568 30935 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31933 30935 603 41 0 31892 0
vsize: 127732
[startup+459.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 33085 0 3 0 45915 85 0 0 25 0 1 0 478834572 134144000 31742 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32750 31742 603 41 0 32709 0
vsize: 131000
[startup+470 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25063
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 33941 0 3 0 46912 88 0 0 25 0 1 0 478834572 137633792 32598 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33602 32598 603 41 0 33561 0
vsize: 134408
[startup+480 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 34705 0 3 0 47911 90 0 0 25 0 1 0 478834572 140861440 33362 4294967295 134512640 134672761 3221224640 3221223744 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34390 33362 603 41 0 34349 0
vsize: 137560
[startup+490 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 35434 0 3 0 48909 92 0 0 25 0 1 0 478834572 143826944 34091 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35114 34091 603 41 0 35073 0
vsize: 140456
[startup+500 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 36137 0 3 0 49907 94 0 0 25 0 1 0 478834572 146653184 34794 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35804 34794 603 41 0 35763 0
vsize: 143216
[startup+510 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 36668 0 3 0 50906 95 0 0 25 0 1 0 478834572 148815872 35325 4294967295 134512640 134672761 3221224640 3221223808 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36332 35325 603 41 0 36291 0
vsize: 145328
[startup+520.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 37211 0 3 0 51906 96 0 0 25 0 1 0 478834572 151109632 35868 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36892 35868 603 41 0 36851 0
vsize: 147568
[startup+530.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 37713 0 3 0 52905 97 0 0 25 0 1 0 478834572 153120768 36370 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37383 36370 603 41 0 37342 0
vsize: 149532
[startup+540.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 38216 0 3 0 53904 98 0 0 25 0 1 0 478834572 155271168 36873 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37908 36873 603 41 0 37867 0
vsize: 151632
[startup+550.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 38684 0 3 0 54903 100 0 0 25 0 1 0 478834572 157155328 37341 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38368 37341 603 41 0 38327 0
vsize: 153472
[startup+560.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39146 0 3 0 55902 100 0 0 25 0 1 0 478834572 159043584 37803 4294967295 134512640 134672761 3221224640 3221223744 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37803 603 41 0 38788 0
vsize: 155316
[startup+570.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39146 0 3 0 56902 100 0 0 25 0 1 0 478834572 159043584 37803 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37803 603 41 0 38788 0
vsize: 155316
[startup+580.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39146 0 3 0 57902 100 0 0 25 0 1 0 478834572 159043584 37803 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37803 603 41 0 38788 0
vsize: 155316
[startup+590.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39146 0 3 0 58903 100 0 0 25 0 1 0 478834572 159043584 37803 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37803 603 41 0 38788 0
vsize: 155316
[startup+600 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39146 0 3 0 59903 100 0 0 25 0 1 0 478834572 159043584 37803 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37803 603 41 0 38788 0
vsize: 155316
[startup+610.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39146 0 3 0 60903 100 0 0 25 0 1 0 478834572 159043584 37803 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37803 603 41 0 38788 0
vsize: 155316
[startup+620.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39147 0 3 0 61903 100 0 0 25 0 1 0 478834572 159043584 37804 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37804 603 41 0 38788 0
vsize: 155316
[startup+630.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39147 0 3 0 62903 100 0 0 25 0 1 0 478834572 159043584 37804 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37804 603 41 0 38788 0
vsize: 155316
[startup+640.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39147 0 3 0 63904 100 0 0 25 0 1 0 478834572 159043584 37804 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37804 603 41 0 38788 0
vsize: 155316
[startup+650 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39147 0 3 0 64904 100 0 0 25 0 1 0 478834572 159043584 37804 4294967295 134512640 134672761 3221224640 3221223764 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37804 603 41 0 38788 0
vsize: 155316
[startup+660 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39147 0 3 0 65904 100 0 0 25 0 1 0 478834572 159043584 37804 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37804 603 41 0 38788 0
vsize: 155316
[startup+670.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39147 0 3 0 66904 100 0 0 25 0 1 0 478834572 159043584 37804 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37804 603 41 0 38788 0
vsize: 155316
[startup+680 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39147 0 3 0 67904 100 0 0 25 0 1 0 478834572 159043584 37804 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37804 603 41 0 38788 0
vsize: 155316
[startup+690 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39147 0 3 0 68905 100 0 0 25 0 1 0 478834572 159043584 37804 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37804 603 41 0 38788 0
vsize: 155316
[startup+700.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 69905 100 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+710 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 70905 100 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+720 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 71905 100 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223744 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+730.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 72905 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223792 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+740.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 73905 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+750.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 74905 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+760 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 75905 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+770.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25065
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 76905 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+780.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 77906 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+790.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 78906 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223776 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+800.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 79906 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+810.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 80906 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223744 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+820.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 81906 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+830.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 82907 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+840.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 83907 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+850.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 84907 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+860.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 85907 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+870.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 86907 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+880.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 87908 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+890.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 88908 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+900.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 89908 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+910.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39148 0 3 0 90908 101 0 0 25 0 1 0 478834572 159043584 37805 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38829 37805 603 41 0 38788 0
vsize: 155316
[startup+920.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39207 0 3 0 91908 101 0 0 25 0 1 0 478834572 159313920 37864 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38895 37864 603 41 0 38854 0
vsize: 155580
[startup+930.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 39815 0 3 0 92906 103 0 0 25 0 1 0 478834572 161738752 38472 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39487 38472 603 41 0 39446 0
vsize: 157948
[startup+940.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 40448 0 3 0 93904 105 0 0 25 0 1 0 478834572 164331520 39105 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40120 39105 603 41 0 40079 0
vsize: 160480
[startup+950.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 41018 0 3 0 94903 107 0 0 25 0 1 0 478834572 166600704 39675 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40674 39675 603 41 0 40633 0
vsize: 162696
[startup+960.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 41631 0 3 0 95901 109 0 0 25 0 1 0 478834572 169144320 40288 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41295 40288 603 41 0 41254 0
vsize: 165180
[startup+970.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 42109 0 3 0 96899 110 0 0 25 0 1 0 478834572 171147264 40766 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41784 40766 603 41 0 41743 0
vsize: 167136
[startup+980.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 42625 0 3 0 97898 112 0 0 25 0 1 0 478834572 173285376 41282 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42306 41282 603 41 0 42265 0
vsize: 169224
[startup+990.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 43103 0 3 0 98897 113 0 0 25 0 1 0 478834572 175165440 41760 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42765 41760 603 41 0 42724 0
vsize: 171060
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 43561 0 3 0 99895 115 0 0 25 0 1 0 478834572 177049600 42218 4294967295 134512640 134672761 3221224640 3221223840 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43225 42218 603 41 0 43184 0
vsize: 172900
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44033 0 3 0 100894 116 0 0 25 0 1 0 478834572 179077120 42690 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43720 42690 603 41 0 43679 0
vsize: 174880
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44538 0 3 0 101892 118 0 0 25 0 1 0 478834572 181100544 43195 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44214 43195 603 41 0 44173 0
vsize: 176856
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44863 0 3 0 102891 120 0 0 25 0 1 0 478834572 182431744 43520 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43520 603 41 0 44498 0
vsize: 178156
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44863 0 3 0 103891 120 0 0 25 0 1 0 478834572 182431744 43520 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43520 603 41 0 44498 0
vsize: 178156
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44863 0 3 0 104892 120 0 0 25 0 1 0 478834572 182431744 43520 4294967295 134512640 134672761 3221224640 3221223744 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43520 603 41 0 44498 0
vsize: 178156
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44863 0 3 0 105892 120 0 0 25 0 1 0 478834572 182431744 43520 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43520 603 41 0 44498 0
vsize: 178156
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25067
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 106892 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 107892 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 108892 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 109893 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 110893 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 111893 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 112893 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 113893 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 114894 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 115893 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223804 134564510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 116893 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223808 134560811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 117893 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 118893 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25069
Raw data (stat): 25061 (minisat+) R 25060 20838 20837 0 -1 0 44864 0 3 0 119893 120 0 0 25 0 1 0 478834572 182431744 43521 4294967295 134512640 134672761 3221224640 3221223824 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 43521 603 41 0 44498 0
vsize: 178156
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 25069
Raw data (stat): 25061 (minisat+) Z 25060 20838 20837 0 -1 12 44867 0 3 0 119894 128 0 0 25 0 1 0 478834572 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.1
CPU time (s): 1200.23
CPU user time (s): 1198.95
CPU system time (s): 1.2828
CPU usage (%): 100.011
Max. virtual memory (Kb): 178156
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####