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-apex4.a.opb
MD5SUM	4a690348e685ba516d0f6942be0bf113
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	779
Optimality of the best value was proved	NO
Number of terms in the objective function	4317
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	4317
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	4317
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	1175.06
Number of variables	4316
Total number of constraints	11912
Number of constraints which are clauses	11912
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	1
Maximum length of a constraint	160
Trace number 5792

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-14 01:48:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4198 boxname=wulflinc27 idbench=62 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4a690348e685ba516d0f6942be0bf113  /oldhome/oroussel/tmp/wulflinc27/normalized-apex4.a.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc27/normalized-apex4.a.opb /oldhome/oroussel/tmp/wulflinc27/normalized-apex4.a.opb
IDLAUNCH: 4198
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        846860 kB
Buffers:         34612 kB
Cached:         115908 kB
SwapCached:       3160 kB
Active:          69464 kB
Inactive:        87108 kB
HighTotal:      131008 kB
HighFree:        11704 kB
LowTotal:       903652 kB
LowFree:        835156 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25640 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:08:05 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 4198 7 1200.28 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 8778 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 |    7372    46237 |    2457       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:320684     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         8 |  385639   929014 |  128546       8       86    10.8 |  0.000 % |
c |       109 |  384094   925767 |  141400      72      614     8.5 |  0.411 % |
c |       260 |  383138   923717 |  155540     193     1589     8.2 |  0.624 % |
c |       485 |  382363   922048 |  171094     399     4329    10.8 |  0.800 % |
c |       822 |  382105   921484 |  188204     727     7339    10.1 |  0.859 % |
c |      1328 |  381647   920470 |  207024    1216    11758     9.7 |  0.968 % |
c |      2088 |  381573   920314 |  227727    1974    57800    29.3 |  0.984 % |
c |      3227 |  381305   919718 |  250499    3098    80875    26.1 |  1.048 % |
c |      4935 |  381184   919453 |  275549    4803   140380    29.2 |  1.076 % |
c |      7497 |  381182   919449 |  303104    7364   219868    29.9 |  1.076 % |
c |     11342 |  381182   919449 |  333415   11209   415051    37.0 |  1.076 % |
c |     17108 |  381120   919313 |  366756   16973  1053324    62.1 |  1.090 % |
c |     25758 |  381117   919306 |  403432   25620  1384658    54.0 |  1.091 % |
c |     38732 |  381070   919201 |  443775   38593  2612677    67.7 |  1.102 % |
c |     58193 |  381020   919093 |  488153   58053  4840683    83.4 |  1.114 % |
c |     87386 |  381020   919093 |  536968   87246  8785356   100.7 |  1.114 % |
c |    131176 |  381020   919093 |  590665  131036 13925725   106.3 |  1.114 % |
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 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (runsolver) R 23499 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480747673 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0007 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 18547 0 0 0 957 41 0 0 25 0 1 0 480747673 81002496 18002 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19776 18002 603 41 0 19735 0
vsize: 79104
[startup+20.0012 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 18754 0 0 0 1956 42 0 0 25 0 1 0 480747673 81813504 18209 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19974 18209 603 41 0 19933 0
vsize: 79896
[startup+30.0011 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 18877 0 0 0 2955 43 0 0 25 0 1 0 480747673 82354176 18332 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20106 18332 603 41 0 20065 0
vsize: 80424
[startup+40.0011 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 18991 0 0 0 3954 43 0 0 25 0 1 0 480747673 82759680 18446 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20205 18446 603 41 0 20164 0
vsize: 80820
[startup+50.0017 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 19101 0 0 0 4954 44 0 0 25 0 1 0 480747673 83296256 18556 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20336 18556 603 41 0 20295 0
vsize: 81344
[startup+60.0018 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 19201 0 0 0 5954 44 0 0 25 0 1 0 480747673 83693568 18656 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20433 18656 603 41 0 20392 0
vsize: 81732
[startup+70.0026 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 19362 0 0 0 6953 45 0 0 25 0 1 0 480747673 84365312 18817 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20597 18817 603 41 0 20556 0
vsize: 82388
[startup+80.0031 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 19497 0 0 0 7953 45 0 0 25 0 1 0 480747673 84901888 18952 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20728 18952 603 41 0 20687 0
vsize: 82912
[startup+90.0029 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 19852 0 0 0 8952 47 0 0 25 0 1 0 480747673 86376448 19307 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21088 19307 603 41 0 21047 0
vsize: 84352
[startup+100.003 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 20187 0 0 0 9951 48 0 0 25 0 1 0 480747673 87801856 19642 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21436 19642 603 41 0 21395 0
vsize: 85744
[startup+110.004 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 20245 0 0 0 10950 49 0 0 25 0 1 0 480747673 87937024 19700 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21469 19700 603 41 0 21428 0
vsize: 85876
[startup+120.005 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 20312 0 0 0 11949 49 0 0 25 0 1 0 480747673 88203264 19767 4294967295 134512640 134672761 3221224560 3221223760 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21534 19767 603 41 0 21493 0
vsize: 86136
[startup+130.005 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 20375 0 0 0 12949 50 0 0 25 0 1 0 480747673 88473600 19830 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21600 19830 603 41 0 21559 0
vsize: 86400
[startup+140.004 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 20599 0 0 0 13948 51 0 0 25 0 1 0 480747673 89415680 20054 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21830 20054 603 41 0 21789 0
vsize: 87320
[startup+150.005 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 20672 0 0 0 14948 51 0 0 25 0 1 0 480747673 89681920 20127 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21895 20127 603 41 0 21854 0
vsize: 87580
[startup+160.005 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 20763 0 0 0 15948 51 0 0 25 0 1 0 480747673 90087424 20218 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21994 20218 603 41 0 21953 0
vsize: 87976
[startup+170.006 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 20822 0 0 0 16948 51 0 0 25 0 1 0 480747673 90357760 20277 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22060 20277 603 41 0 22019 0
vsize: 88240
[startup+180.006 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 21033 0 0 0 17947 52 0 0 25 0 1 0 480747673 91156480 20488 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22255 20488 603 41 0 22214 0
vsize: 89020
[startup+190.006 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 21317 0 0 0 18946 53 0 0 25 0 1 0 480747673 92368896 20772 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22551 20772 603 41 0 22510 0
vsize: 90204
[startup+200.006 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 21438 0 0 0 19946 54 0 0 25 0 1 0 480747673 92766208 20893 4294967295 134512640 134672761 3221224560 3221223684 134566115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22648 20893 603 41 0 22607 0
vsize: 90592
[startup+210.006 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 21615 0 0 0 20946 54 0 0 25 0 1 0 480747673 93569024 21070 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22844 21070 603 41 0 22803 0
vsize: 91376
[startup+220.007 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 21964 0 0 0 21945 55 0 0 25 0 1 0 480747673 94920704 21419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23174 21419 603 41 0 23133 0
vsize: 92696
[startup+230.006 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 22153 0 0 0 22944 56 0 0 25 0 1 0 480747673 95731712 21608 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23372 21608 603 41 0 23331 0
vsize: 93488
[startup+240.007 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 22300 0 0 0 23944 56 0 0 25 0 1 0 480747673 96272384 21755 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23504 21755 603 41 0 23463 0
vsize: 94016
[startup+250.007 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 22458 0 0 0 24943 57 0 0 25 0 1 0 480747673 96948224 21913 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23669 21913 603 41 0 23628 0
vsize: 94676
[startup+260.007 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 22628 0 0 0 25943 58 0 0 25 0 1 0 480747673 97611776 22083 4294967295 134512640 134672761 3221224560 3221223664 134559953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23831 22083 603 41 0 23790 0
vsize: 95324
[startup+270.007 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 22814 0 0 0 26943 58 0 0 25 0 1 0 480747673 98410496 22269 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24026 22269 603 41 0 23985 0
vsize: 96104
[startup+280.008 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 23021 0 0 0 27943 59 0 0 25 0 1 0 480747673 99217408 22476 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24223 22476 603 41 0 24182 0
vsize: 96892
[startup+290.007 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 23218 0 0 0 28942 59 0 0 25 0 1 0 480747673 100024320 22673 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24420 22673 603 41 0 24379 0
vsize: 97680
[startup+300.008 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 23413 0 0 0 29942 60 0 0 25 0 1 0 480747673 100831232 22868 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24617 22868 603 41 0 24576 0
vsize: 98468
[startup+310.008 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 23615 0 0 0 30941 60 0 0 25 0 1 0 480747673 101621760 23070 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24810 23070 603 41 0 24769 0
vsize: 99240
[startup+320.009 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 23772 0 0 0 31941 61 0 0 25 0 1 0 480747673 102289408 23227 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24973 23227 603 41 0 24932 0
vsize: 99892
[startup+330.009 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 23925 0 0 0 32941 62 0 0 25 0 1 0 480747673 102965248 23380 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25138 23380 603 41 0 25097 0
vsize: 100552
[startup+340.009 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 24076 0 0 0 33941 62 0 0 25 0 1 0 480747673 103501824 23531 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25269 23531 603 41 0 25228 0
vsize: 101076
[startup+350.009 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 24247 0 0 0 34941 62 0 0 25 0 1 0 480747673 104173568 23702 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25433 23702 603 41 0 25392 0
vsize: 101732
[startup+360.009 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 24421 0 0 0 35940 63 0 0 25 0 1 0 480747673 104984576 23876 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25631 23876 603 41 0 25590 0
vsize: 102524
[startup+370.011 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 24583 0 0 0 36940 63 0 0 25 0 1 0 480747673 105652224 24038 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25794 24038 603 41 0 25753 0
vsize: 103176
[startup+380.011 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 24667 0 0 0 37939 64 0 0 25 0 1 0 480747673 105918464 24122 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25859 24122 603 41 0 25818 0
vsize: 103436
[startup+390.011 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 24838 0 0 0 38938 64 0 0 25 0 1 0 480747673 106582016 24293 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26021 24293 603 41 0 25980 0
vsize: 104084
[startup+400.012 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 25011 0 0 0 39938 65 0 0 25 0 1 0 480747673 107388928 24466 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26218 24466 603 41 0 26177 0
vsize: 104872
[startup+410.011 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 25161 0 0 0 40937 66 0 0 25 0 1 0 480747673 107925504 24616 4294967295 134512640 134672761 3221224560 3221223712 134542664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26349 24616 603 41 0 26308 0
vsize: 105396
[startup+420.012 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 25356 0 0 0 41937 66 0 0 25 0 1 0 480747673 108732416 24811 4294967295 134512640 134672761 3221224560 3221223744 134558914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26546 24811 603 41 0 26505 0
vsize: 106184
[startup+430.013 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 25539 0 0 0 42936 68 0 0 25 0 1 0 480747673 109789184 24994 4294967295 134512640 134672761 3221224560 3221223664 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26804 24994 603 41 0 26763 0
vsize: 107216
[startup+440.013 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 25712 0 0 0 43936 68 0 0 25 0 1 0 480747673 110456832 25167 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26967 25167 603 41 0 26926 0
vsize: 107868
[startup+450.013 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 25875 0 0 0 44935 69 0 0 25 0 1 0 480747673 111120384 25330 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27129 25330 603 41 0 27088 0
vsize: 108516
[startup+460.013 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 26038 0 0 0 45935 69 0 0 25 0 1 0 480747673 111788032 25493 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27292 25493 603 41 0 27251 0
vsize: 109168
[startup+470.013 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 26230 0 0 0 46935 70 0 0 25 0 1 0 480747673 112590848 25685 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27488 25685 603 41 0 27447 0
vsize: 109952
[startup+480.013 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 26462 0 0 0 47934 71 0 0 25 0 1 0 480747673 113516544 25917 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27714 25917 603 41 0 27673 0
vsize: 110856
[startup+490.013 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 26687 0 0 0 48933 71 0 0 25 0 1 0 480747673 114450432 26142 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27942 26142 603 41 0 27901 0
vsize: 111768
[startup+500.014 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 26920 0 0 0 49933 72 0 0 25 0 1 0 480747673 115380224 26375 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28169 26375 603 41 0 28128 0
vsize: 112676
[startup+510.014 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 27099 0 0 0 50932 73 0 0 25 0 1 0 480747673 116047872 26554 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28332 26554 603 41 0 28291 0
vsize: 113328
[startup+520.015 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 27279 0 0 0 51932 73 0 0 25 0 1 0 480747673 116850688 26734 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28528 26734 603 41 0 28487 0
vsize: 114112
[startup+530.014 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 27458 0 0 0 52931 74 0 0 25 0 1 0 480747673 117518336 26913 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28691 26913 603 41 0 28650 0
vsize: 114764
[startup+540.014 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 27680 0 0 0 53931 74 0 0 25 0 1 0 480747673 118452224 27135 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28919 27135 603 41 0 28878 0
vsize: 115676
[startup+550.015 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 27889 0 0 0 54931 75 0 0 25 0 1 0 480747673 119390208 27344 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29148 27344 603 41 0 29107 0
vsize: 116592
[startup+560.016 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 28092 0 0 0 55931 75 0 0 25 0 1 0 480747673 120180736 27547 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29341 27547 603 41 0 29300 0
vsize: 117364
[startup+570.016 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 28313 0 0 0 56931 76 0 0 25 0 1 0 480747673 121110528 27768 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29568 27768 603 41 0 29527 0
vsize: 118272
[startup+580.017 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 28516 0 0 0 57930 76 0 0 25 0 1 0 480747673 121917440 27971 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29765 27971 603 41 0 29724 0
vsize: 119060
[startup+590.016 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 28710 0 0 0 58930 77 0 0 25 0 1 0 480747673 122716160 28165 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29960 28165 603 41 0 29919 0
vsize: 119840
[startup+600.016 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 28875 0 0 0 59929 77 0 0 25 0 1 0 480747673 123383808 28330 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30123 28330 603 41 0 30082 0
vsize: 120492
[startup+610.017 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 28973 0 0 0 60928 77 0 0 25 0 1 0 480747673 123789312 28428 4294967295 134512640 134672761 3221224560 3221223696 134560575 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30222 28428 603 41 0 30181 0
vsize: 120888
[startup+620.019 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 29027 0 0 0 61927 78 0 0 25 0 1 0 480747673 123924480 28482 4294967295 134512640 134672761 3221224560 3221223728 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30255 28482 603 41 0 30214 0
vsize: 121020
[startup+630.018 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 29246 0 0 0 62927 79 0 0 25 0 1 0 480747673 124866560 28701 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30485 28701 603 41 0 30444 0
vsize: 121940
[startup+640.018 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 29874 0 0 0 63925 80 0 0 25 0 1 0 480747673 127418368 29329 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31108 29329 603 41 0 31067 0
vsize: 124432
[startup+650.019 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 30432 0 0 0 64924 82 0 0 25 0 1 0 480747673 129699840 29887 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31665 29887 603 41 0 31624 0
vsize: 126660
[startup+660.019 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 30627 0 0 0 65923 83 0 0 25 0 1 0 480747673 130510848 30082 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31863 30082 603 41 0 31822 0
vsize: 127452
[startup+670.02 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 30742 0 0 0 66923 83 0 0 25 0 1 0 480747673 130916352 30197 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31962 30197 603 41 0 31921 0
vsize: 127848
[startup+680.019 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 31004 0 0 0 67922 84 0 0 25 0 1 0 480747673 131985408 30459 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32223 30459 603 41 0 32182 0
vsize: 128892
[startup+690.019 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 31318 0 0 0 68921 85 0 0 25 0 1 0 480747673 133332992 30773 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32552 30773 603 41 0 32511 0
vsize: 130208
[startup+700.019 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 31568 0 0 0 69921 85 0 0 25 0 1 0 480747673 134270976 31023 4294967295 134512640 134672761 3221224560 3221223664 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32781 31023 603 41 0 32740 0
vsize: 131124
[startup+710.019 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 31858 0 0 0 70920 86 0 0 25 0 1 0 480747673 135479296 31313 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33076 31313 603 41 0 33035 0
vsize: 132304
[startup+720.02 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 23500
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 32228 0 0 0 71919 87 0 0 25 0 1 0 480747673 136953856 31683 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33436 31683 603 41 0 33395 0
vsize: 133744
[startup+730.02 s]
Raw data (loadavg): 1.23 1.04 0.95 2/54 23553
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 32600 0 0 0 72919 88 0 0 25 0 1 0 480747673 138424320 32055 4294967295 134512640 134672761 3221224560 3221223696 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33795 32055 603 41 0 33754 0
vsize: 135180
[startup+740.019 s]
Raw data (loadavg): 1.19 1.03 0.95 2/54 23553
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 32988 0 0 0 73917 89 0 0 25 0 1 0 480747673 140046336 32443 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34191 32443 603 41 0 34150 0
vsize: 136764
[startup+750.019 s]
Raw data (loadavg): 1.16 1.03 0.95 2/54 23553
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 33231 0 0 0 74916 91 0 0 25 0 1 0 480747673 141000704 32686 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34424 32686 603 41 0 34383 0
vsize: 137696
[startup+760.019 s]
Raw data (loadavg): 1.14 1.03 0.95 2/54 23553
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 33790 0 0 0 75915 92 0 0 25 0 1 0 480747673 143282176 33245 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34981 33245 603 41 0 34940 0
vsize: 139924
[startup+770.02 s]
Raw data (loadavg): 1.12 1.03 0.95 2/54 23553
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 34063 0 0 0 76914 94 0 0 25 0 1 0 480747673 144494592 33518 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35277 33518 603 41 0 35236 0
vsize: 141108
[startup+780.02 s]
Raw data (loadavg): 1.10 1.03 0.95 2/54 23553
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 34271 0 0 0 77913 94 0 0 25 0 1 0 480747673 145305600 33726 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35475 33726 603 41 0 35434 0
vsize: 141900
[startup+790.02 s]
Raw data (loadavg): 1.08 1.03 0.95 2/54 23553
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 34437 0 0 0 78913 94 0 0 25 0 1 0 480747673 145985536 33892 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35641 33892 603 41 0 35600 0
vsize: 142564
[startup+800.02 s]
Raw data (loadavg): 1.07 1.03 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 34804 0 0 0 79912 95 0 0 25 0 1 0 480747673 147988480 34259 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36130 34259 603 41 0 36089 0
vsize: 144520
[startup+810.02 s]
Raw data (loadavg): 1.06 1.02 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 35261 0 0 0 80911 96 0 0 25 0 1 0 480747673 149872640 34716 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36590 34716 603 41 0 36549 0
vsize: 146360
[startup+820.021 s]
Raw data (loadavg): 1.05 1.02 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 35720 0 0 0 81910 98 0 0 25 0 1 0 480747673 151756800 35175 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37050 35175 603 41 0 37009 0
vsize: 148200
[startup+830.022 s]
Raw data (loadavg): 1.04 1.02 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 35950 0 0 0 82909 99 0 0 25 0 1 0 480747673 152694784 35405 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37279 35405 603 41 0 37238 0
vsize: 149116
[startup+840.022 s]
Raw data (loadavg): 1.03 1.02 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 36168 0 0 0 83909 99 0 0 25 0 1 0 480747673 153493504 35623 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37474 35623 603 41 0 37433 0
vsize: 149896
[startup+850.023 s]
Raw data (loadavg): 1.03 1.02 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 36405 0 0 0 84909 100 0 0 25 0 1 0 480747673 154574848 35860 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37738 35860 603 41 0 37697 0
vsize: 150952
[startup+860.023 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 36631 0 0 0 85908 100 0 0 25 0 1 0 480747673 155377664 36086 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37934 36086 603 41 0 37893 0
vsize: 151736
[startup+870.024 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 36935 0 0 0 86908 101 0 0 25 0 1 0 480747673 156725248 36390 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38263 36390 603 41 0 38222 0
vsize: 153052
[startup+880.024 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 37281 0 0 0 87907 102 0 0 25 0 1 0 480747673 158064640 36736 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38590 36736 603 41 0 38549 0
vsize: 154360
[startup+890.024 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 37784 0 0 0 88905 104 0 0 25 0 1 0 480747673 160202752 37239 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39112 37239 603 41 0 39071 0
vsize: 156448
[startup+900.025 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 38347 0 0 0 89904 106 0 0 25 0 1 0 480747673 162484224 37802 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39669 37802 603 41 0 39628 0
vsize: 158676
[startup+910.024 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 38916 0 0 0 90903 107 0 0 25 0 1 0 480747673 164773888 38371 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40228 38371 603 41 0 40187 0
vsize: 160912
[startup+920.025 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 39579 0 0 0 91902 108 0 0 25 0 1 0 480747673 167444480 39034 4294967295 134512640 134672761 3221224560 3221223664 134560136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40880 39034 603 41 0 40839 0
vsize: 163520
[startup+930.026 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 40236 0 0 0 92901 110 0 0 25 0 1 0 480747673 170119168 39691 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41533 39691 603 41 0 41492 0
vsize: 166132
[startup+940.026 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 40942 0 0 0 93899 111 0 0 25 0 1 0 480747673 173076480 40397 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42255 40397 603 41 0 42214 0
vsize: 169020
[startup+950.027 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 41399 0 0 0 94898 113 0 0 25 0 1 0 480747673 174952448 40854 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42713 40854 603 41 0 42672 0
vsize: 170852
[startup+960.027 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 41957 0 0 0 95897 114 0 0 25 0 1 0 480747673 177233920 41412 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43270 41412 603 41 0 43229 0
vsize: 173080
[startup+970.027 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 42482 0 0 0 96895 116 0 0 25 0 1 0 480747673 179380224 41937 4294967295 134512640 134672761 3221224560 3221223664 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43794 41937 603 41 0 43753 0
vsize: 175176
[startup+980.027 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 43181 0 0 0 97893 118 0 0 25 0 1 0 480747673 182210560 42636 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44485 42636 603 41 0 44444 0
vsize: 177940
[startup+990.027 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 43880 0 0 0 98892 119 0 0 25 0 1 0 480747673 185040896 43335 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45176 43335 603 41 0 45135 0
vsize: 180704
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 44585 0 0 0 99891 121 0 0 25 0 1 0 480747673 187883520 44040 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45870 44040 603 41 0 45829 0
vsize: 183480
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 45272 0 0 0 100890 122 0 0 25 0 1 0 480747673 190722048 44727 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46563 44727 603 41 0 46522 0
vsize: 186252
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 45898 0 0 0 101888 124 0 0 25 0 1 0 480747673 193282048 45353 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47188 45353 603 41 0 47147 0
vsize: 188752
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 46537 0 0 0 102887 125 0 0 25 0 1 0 480747673 195989504 45992 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47849 45992 603 41 0 47808 0
vsize: 191396
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 47140 0 0 0 103886 126 0 0 25 0 1 0 480747673 198365184 46595 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48429 46595 603 41 0 48388 0
vsize: 193716
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 47762 0 0 0 104885 128 0 0 25 0 1 0 480747673 200912896 47217 4294967295 134512640 134672761 3221224560 3221223664 134559955 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49051 47217 603 41 0 49010 0
vsize: 196204
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23555
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 48425 0 0 0 105884 129 0 0 25 0 1 0 480747673 203706368 47880 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49733 47880 603 41 0 49692 0
vsize: 198932
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 49047 0 0 0 106882 130 0 0 25 0 1 0 480747673 206258176 48502 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50356 48502 603 41 0 50315 0
vsize: 201424
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 49658 0 0 0 107881 132 0 0 25 0 1 0 480747673 208764928 49113 4294967295 134512640 134672761 3221224560 3221223744 134558374 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50968 49113 603 41 0 50927 0
vsize: 203872
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 50216 0 0 0 108880 133 0 0 25 0 1 0 480747673 211075072 49671 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51532 49671 603 41 0 51491 0
vsize: 206128
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 50754 0 0 0 109879 134 0 0 25 0 1 0 480747673 213225472 50209 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52057 50209 603 41 0 52016 0
vsize: 208228
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 51262 0 0 0 110878 136 0 0 25 0 1 0 480747673 215363584 50717 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52579 50717 603 41 0 52538 0
vsize: 210316
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 51668 0 0 0 111877 137 0 0 25 0 1 0 480747673 216969216 51123 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52971 51123 603 41 0 52930 0
vsize: 211884
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 52018 0 0 0 112877 137 0 0 25 0 1 0 480747673 218435584 51473 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53329 51473 603 41 0 53288 0
vsize: 213316
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 52496 0 0 0 113877 138 0 0 25 0 1 0 480747673 220307456 51951 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53786 51951 603 41 0 53745 0
vsize: 215144
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 53035 0 0 0 114876 139 0 0 25 0 1 0 480747673 222601216 52490 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54346 52490 603 41 0 54305 0
vsize: 217384
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 53538 0 0 0 115875 139 0 0 25 0 1 0 480747673 224616448 52993 4294967295 134512640 134672761 3221224560 3221223708 134559754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54838 52993 603 41 0 54797 0
vsize: 219352
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 54039 0 0 0 116875 140 0 0 25 0 1 0 480747673 226775040 53494 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55365 53494 603 41 0 55324 0
vsize: 221460
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 54518 0 0 0 117874 141 0 0 25 0 1 0 480747673 228659200 53973 4294967295 134512640 134672761 3221224560 3221223632 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55825 53973 603 41 0 55784 0
vsize: 223300
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 55017 0 0 0 118874 141 0 0 25 0 1 0 480747673 230793216 54472 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56346 54472 603 41 0 56305 0
vsize: 225384
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 23557
Raw data (stat): 23500 (minisat+) R 23499 18865 18864 0 -1 0 55460 0 0 0 119874 142 0 0 25 0 1 0 480747673 232525824 54915 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56769 54915 603 41 0 56728 0
vsize: 227076
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 23557
Raw data (stat): 23500 (minisat+) Z 23499 18865 18864 0 -1 12 55463 0 0 0 119875 152 0 0 25 0 1 0 480747673 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.28
CPU user time (s): 1198.75
CPU system time (s): 1.52677
CPU usage (%): 100.011
Max. virtual memory (Kb): 227076
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####