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 5797

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        897328 kB
Buffers:         37884 kB
Cached:          79960 kB
SwapCached:          0 kB
Active:          73000 kB
Inactive:        47736 kB
HighTotal:      131008 kB
HighFree:        47180 kB
LowTotal:       903652 kB
LowFree:        850148 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11008 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:09:32 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 4199 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]---> Sorter-cost:364364     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  428686  1009203 |  142895       0        0     nan |  0.000 % |
c |       100 |  427674  1007096 |  157184      68      758    11.1 |  0.431 % |
c |       251 |  427509  1006741 |  172902     214     2943    13.8 |  0.464 % |
c |       477 |  427505  1006733 |  190193     439     7599    17.3 |  0.465 % |
c |       814 |  427398  1006506 |  209212     772    14326    18.6 |  0.486 % |
c |      1320 |  427322  1006336 |  230133    1275    24570    19.3 |  0.502 % |
c |      2081 |  427082  1005822 |  253147    2019    50596    25.1 |  0.547 % |
c |      3222 |  426930  1005490 |  278461    3148    97857    31.1 |  0.578 % |
c |      4930 |  426904  1005432 |  306308    4855   156652    32.3 |  0.583 % |
c |      7494 |  426807  1005219 |  336938    7409   488726    66.0 |  0.604 % |
c |     11338 |  426807  1005219 |  370632   11253   657687    58.4 |  0.604 % |
c |     17104 |  426805  1005215 |  407696   17018  1092625    64.2 |  0.604 % |
c |     25753 |  426689  1004953 |  448465   25644  2084904    81.3 |  0.629 % |
c |     38728 |  426689  1004953 |  493312   38619  3225833    83.5 |  0.629 % |
c |     58190 |  426689  1004953 |  542643   58081  4428413    76.2 |  0.629 % |
c |     87383 |  426689  1004953 |  596907   87274  9168285   105.1 |  0.629 % |
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.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (runsolver) R 27445 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422541694 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+9.9997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 22048 0 0 0 941 57 0 0 25 0 1 0 422541694 104484864 20716 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25509 20716 603 41 0 25468 0
vsize: 102036
[startup+19.9998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 22193 0 0 0 1940 57 0 0 25 0 1 0 422541694 104886272 20861 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25607 20861 603 41 0 25566 0
vsize: 102428
[startup+30.0003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 22255 0 0 0 2939 58 0 0 25 0 1 0 422541694 105156608 20923 4294967295 134512640 134672761 3221224560 3221223700 1074733057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25673 20923 603 41 0 25632 0
vsize: 102692
[startup+39.9996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 22336 0 0 0 3938 58 0 0 25 0 1 0 422541694 105562112 21004 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25772 21004 603 41 0 25731 0
vsize: 103088
[startup+50.0006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 22413 0 0 0 4938 59 0 0 25 0 1 0 422541694 105832448 21081 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25838 21081 603 41 0 25797 0
vsize: 103352
[startup+60.0012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 22471 0 0 0 5938 59 0 0 25 0 1 0 422541694 106102784 21139 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25904 21139 603 41 0 25863 0
vsize: 103616
[startup+70.0007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 22514 0 0 0 6937 59 0 0 25 0 1 0 422541694 106237952 21182 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25937 21182 603 41 0 25896 0
vsize: 103748
[startup+80.0015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 22560 0 0 0 7937 59 0 0 25 0 1 0 422541694 106373120 21228 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25970 21228 603 41 0 25929 0
vsize: 103880
[startup+90.0011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 22656 0 0 0 8937 60 0 0 25 0 1 0 422541694 106778624 21324 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26069 21324 603 41 0 26028 0
vsize: 104276
[startup+100.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 22794 0 0 0 9937 60 0 0 25 0 1 0 422541694 107311104 21462 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26199 21462 603 41 0 26158 0
vsize: 104796
[startup+110.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 22915 0 0 0 10937 60 0 0 25 0 1 0 422541694 107847680 21583 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26330 21583 603 41 0 26289 0
vsize: 105320
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 22946 0 0 0 11936 61 0 0 25 0 1 0 422541694 107982848 21614 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26363 21614 603 41 0 26322 0
vsize: 105452
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23010 0 0 0 12937 61 0 0 25 0 1 0 422541694 108249088 21678 4294967295 134512640 134672761 3221224560 3221223696 134560658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26428 21678 603 41 0 26387 0
vsize: 105712
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23100 0 0 0 13937 61 0 0 25 0 1 0 422541694 108650496 21768 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26526 21768 603 41 0 26485 0
vsize: 106104
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23155 0 0 0 14937 61 0 0 25 0 1 0 422541694 108916736 21823 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26591 21823 603 41 0 26550 0
vsize: 106364
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23213 0 0 0 15937 61 0 0 25 0 1 0 422541694 109051904 21881 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26624 21881 603 41 0 26583 0
vsize: 106496
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23441 0 0 0 16936 62 0 0 25 0 1 0 422541694 109998080 22109 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26855 22109 603 41 0 26814 0
vsize: 107420
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23625 0 0 0 17936 63 0 0 25 0 1 0 422541694 110772224 22293 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27044 22293 603 41 0 27003 0
vsize: 108176
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23678 0 0 0 18936 63 0 0 25 0 1 0 422541694 111042560 22346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27110 22346 603 41 0 27069 0
vsize: 108440
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23726 0 0 0 19936 63 0 0 25 0 1 0 422541694 111177728 22394 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27143 22394 603 41 0 27102 0
vsize: 108572
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23756 0 0 0 20936 63 0 0 25 0 1 0 422541694 111312896 22424 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27176 22424 603 41 0 27135 0
vsize: 108704
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23808 0 0 0 21936 63 0 0 25 0 1 0 422541694 111583232 22476 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27242 22476 603 41 0 27201 0
vsize: 108968
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23844 0 0 0 22936 63 0 0 25 0 1 0 422541694 111718400 22512 4294967295 134512640 134672761 3221224560 3221223696 134560694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27275 22512 603 41 0 27234 0
vsize: 109100
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23887 0 0 0 23936 63 0 0 25 0 1 0 422541694 111853568 22555 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27308 22555 603 41 0 27267 0
vsize: 109232
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 23976 0 0 0 24936 63 0 0 25 0 1 0 422541694 112259072 22644 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27407 22644 603 41 0 27366 0
vsize: 109628
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 24079 0 0 0 25936 64 0 0 25 0 1 0 422541694 112660480 22747 4294967295 134512640 134672761 3221224560 3221223696 134560686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27505 22747 603 41 0 27464 0
vsize: 110020
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 24173 0 0 0 26936 64 0 0 25 0 1 0 422541694 113061888 22841 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27603 22841 603 41 0 27562 0
vsize: 110412
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 24258 0 0 0 27936 64 0 0 25 0 1 0 422541694 113332224 22926 4294967295 134512640 134672761 3221224560 3221223744 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27669 22926 603 41 0 27628 0
vsize: 110676
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 24382 0 0 0 28936 65 0 0 25 0 1 0 422541694 113868800 23050 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27800 23050 603 41 0 27759 0
vsize: 111200
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 24495 0 0 0 29935 65 0 0 25 0 1 0 422541694 114409472 23163 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27932 23163 603 41 0 27891 0
vsize: 111728
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 24682 0 0 0 30935 66 0 0 25 0 1 0 422541694 115081216 23350 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28096 23350 603 41 0 28055 0
vsize: 112384
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 24764 0 0 0 31934 66 0 0 25 0 1 0 422541694 115482624 23432 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28194 23432 603 41 0 28153 0
vsize: 112776
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 24833 0 0 0 32934 67 0 0 25 0 1 0 422541694 115748864 23501 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28259 23501 603 41 0 28218 0
vsize: 113036
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 24877 0 0 0 33934 67 0 0 25 0 1 0 422541694 115884032 23545 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28292 23545 603 41 0 28251 0
vsize: 113168
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 24959 0 0 0 34933 67 0 0 25 0 1 0 422541694 116289536 23627 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28391 23627 603 41 0 28350 0
vsize: 113564
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25022 0 0 0 35934 67 0 0 25 0 1 0 422541694 116559872 23690 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28457 23690 603 41 0 28416 0
vsize: 113828
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25094 0 0 0 36934 68 0 0 25 0 1 0 422541694 116822016 23762 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28521 23762 603 41 0 28480 0
vsize: 114084
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25143 0 0 0 37934 68 0 0 25 0 1 0 422541694 116953088 23811 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28553 23811 603 41 0 28512 0
vsize: 114212
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25187 0 0 0 38934 68 0 0 25 0 1 0 422541694 117088256 23855 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28586 23855 603 41 0 28545 0
vsize: 114344
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25231 0 0 0 39934 68 0 0 25 0 1 0 422541694 117358592 23899 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28652 23899 603 41 0 28611 0
vsize: 114608
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25291 0 0 0 40934 68 0 0 25 0 1 0 422541694 117755904 23959 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28749 23959 603 41 0 28708 0
vsize: 114996
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25332 0 0 0 41934 68 0 0 25 0 1 0 422541694 117891072 24000 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28782 24000 603 41 0 28741 0
vsize: 115128
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25427 0 0 0 42934 69 0 0 25 0 1 0 422541694 118292480 24095 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28880 24095 603 41 0 28839 0
vsize: 115520
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25568 0 0 0 43933 69 0 0 25 0 1 0 422541694 118829056 24236 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29011 24236 603 41 0 28970 0
vsize: 116044
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25711 0 0 0 44933 70 0 0 25 0 1 0 422541694 119365632 24379 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29142 24379 603 41 0 29101 0
vsize: 116568
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25797 0 0 0 45933 70 0 0 25 0 1 0 422541694 119771136 24465 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29241 24465 603 41 0 29200 0
vsize: 116964
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25825 0 0 0 46933 70 0 0 25 0 1 0 422541694 119906304 24493 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29274 24493 603 41 0 29233 0
vsize: 117096
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25864 0 0 0 47933 70 0 0 25 0 1 0 422541694 120041472 24532 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29307 24532 603 41 0 29266 0
vsize: 117228
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25929 0 0 0 48933 70 0 0 25 0 1 0 422541694 120311808 24597 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29373 24597 603 41 0 29332 0
vsize: 117492
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 25991 0 0 0 49934 70 0 0 25 0 1 0 422541694 120582144 24659 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29439 24659 603 41 0 29398 0
vsize: 117756
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26030 0 0 0 50934 70 0 0 25 0 1 0 422541694 120717312 24698 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29472 24698 603 41 0 29431 0
vsize: 117888
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26078 0 0 0 51933 71 0 0 25 0 1 0 422541694 120852480 24746 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29505 24746 603 41 0 29464 0
vsize: 118020
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26187 0 0 0 52931 72 0 0 25 0 1 0 422541694 121393152 24855 4294967295 134512640 134672761 3221224560 3221223664 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29637 24855 603 41 0 29596 0
vsize: 118548
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26225 0 0 0 53931 72 0 0 25 0 1 0 422541694 121528320 24893 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29670 24893 603 41 0 29629 0
vsize: 118680
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26295 0 0 0 54931 72 0 0 25 0 1 0 422541694 121798656 24963 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29736 24963 603 41 0 29695 0
vsize: 118944
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26405 0 0 0 55931 72 0 0 25 0 1 0 422541694 122204160 25073 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29835 25073 603 41 0 29794 0
vsize: 119340
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26479 0 0 0 56931 72 0 0 25 0 1 0 422541694 122470400 25147 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29900 25147 603 41 0 29859 0
vsize: 119600
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26519 0 0 0 57931 72 0 0 25 0 1 0 422541694 122736640 25187 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29965 25187 603 41 0 29924 0
vsize: 119860
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26617 0 0 0 58931 73 0 0 25 0 1 0 422541694 123006976 25285 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30031 25285 603 41 0 29990 0
vsize: 120124
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26691 0 0 0 59931 74 0 0 25 0 1 0 422541694 123408384 25359 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30129 25359 603 41 0 30088 0
vsize: 120516
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26768 0 0 0 60931 74 0 0 25 0 1 0 422541694 123678720 25436 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30195 25436 603 41 0 30154 0
vsize: 120780
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26807 0 0 0 61931 74 0 0 25 0 1 0 422541694 123813888 25475 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30228 25475 603 41 0 30187 0
vsize: 120912
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27446
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26936 0 0 0 62931 75 0 0 25 0 1 0 422541694 124350464 25604 4294967295 134512640 134672761 3221224560 3221223712 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30359 25604 603 41 0 30318 0
vsize: 121436
[startup+640.018 s]
Raw data (loadavg): 1.07 0.99 0.91 3/57 27495
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 26988 0 0 0 63931 75 0 0 25 0 1 0 422541694 124620800 25656 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30425 25656 603 41 0 30384 0
vsize: 121700
[startup+650.018 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 27499
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27085 0 0 0 64931 75 0 0 25 0 1 0 422541694 125026304 25753 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30524 25753 603 41 0 30483 0
vsize: 122096
[startup+660.018 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 27499
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27137 0 0 0 65930 75 0 0 25 0 1 0 422541694 125161472 25805 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30557 25805 603 41 0 30516 0
vsize: 122228
[startup+670.018 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 27499
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27188 0 0 0 66930 76 0 0 25 0 1 0 422541694 125431808 25856 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30623 25856 603 41 0 30582 0
vsize: 122492
[startup+680.018 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 27499
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27295 0 0 0 67930 76 0 0 25 0 1 0 422541694 125837312 25963 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30722 25963 603 41 0 30681 0
vsize: 122888
[startup+690.018 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 27499
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27385 0 0 0 68930 76 0 0 25 0 1 0 422541694 126107648 26053 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30788 26053 603 41 0 30747 0
vsize: 123152
[startup+700.018 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 27499
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27442 0 0 0 69930 76 0 0 25 0 1 0 422541694 126377984 26110 4294967295 134512640 134672761 3221224560 3221223760 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30854 26110 603 41 0 30813 0
vsize: 123416
[startup+710.019 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27537 0 0 0 70930 77 0 0 25 0 1 0 422541694 126783488 26205 4294967295 134512640 134672761 3221224560 3221223712 1074743855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30953 26205 603 41 0 30912 0
vsize: 123812
[startup+720.019 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27615 0 0 0 71929 77 0 0 25 0 1 0 422541694 127049728 26283 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31018 26283 603 41 0 30977 0
vsize: 124072
[startup+730.019 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27726 0 0 0 72929 77 0 0 25 0 1 0 422541694 127590400 26394 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31150 26394 603 41 0 31109 0
vsize: 124600
[startup+740.018 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27774 0 0 0 73929 77 0 0 25 0 1 0 422541694 127725568 26442 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31183 26442 603 41 0 31142 0
vsize: 124732
[startup+750.019 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27849 0 0 0 74929 78 0 0 25 0 1 0 422541694 127995904 26517 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31249 26517 603 41 0 31208 0
vsize: 124996
[startup+760.018 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27894 0 0 0 75930 78 0 0 25 0 1 0 422541694 128262144 26562 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31314 26562 603 41 0 31273 0
vsize: 125256
[startup+770.018 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 27968 0 0 0 76930 78 0 0 25 0 1 0 422541694 128532480 26636 4294967295 134512640 134672761 3221224560 3221223760 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31380 26636 603 41 0 31339 0
vsize: 125520
[startup+780.018 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28004 0 0 0 77930 78 0 0 25 0 1 0 422541694 128667648 26672 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31413 26672 603 41 0 31372 0
vsize: 125652
[startup+790.018 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28038 0 0 0 78930 78 0 0 25 0 1 0 422541694 128802816 26706 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31446 26706 603 41 0 31405 0
vsize: 125784
[startup+800.019 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28070 0 0 0 79930 78 0 0 25 0 1 0 422541694 128937984 26738 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31479 26738 603 41 0 31438 0
vsize: 125916
[startup+810.019 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28119 0 0 0 80930 78 0 0 25 0 1 0 422541694 129073152 26787 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31512 26787 603 41 0 31471 0
vsize: 126048
[startup+820.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28181 0 0 0 81930 78 0 0 25 0 1 0 422541694 129605632 26849 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31642 26849 603 41 0 31601 0
vsize: 126568
[startup+830.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28300 0 0 0 82930 78 0 0 25 0 1 0 422541694 130146304 26968 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31774 26968 603 41 0 31733 0
vsize: 127096
[startup+840.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28370 0 0 0 83930 79 0 0 25 0 1 0 422541694 130408448 27038 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31838 27038 603 41 0 31797 0
vsize: 127352
[startup+850.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28429 0 0 0 84930 79 0 0 25 0 1 0 422541694 130678784 27097 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31904 27097 603 41 0 31863 0
vsize: 127616
[startup+860.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28473 0 0 0 85930 79 0 0 25 0 1 0 422541694 130809856 27141 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31936 27141 603 41 0 31895 0
vsize: 127744
[startup+870.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28556 0 0 0 86930 79 0 0 25 0 1 0 422541694 131215360 27224 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32035 27224 603 41 0 31994 0
vsize: 128140
[startup+880.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28642 0 0 0 87930 79 0 0 25 0 1 0 422541694 131485696 27310 4294967295 134512640 134672761 3221224560 3221223696 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32101 27310 603 41 0 32060 0
vsize: 128404
[startup+890.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28792 0 0 0 88930 80 0 0 25 0 1 0 422541694 132157440 27460 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32265 27460 603 41 0 32224 0
vsize: 129060
[startup+900.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 28948 0 0 0 89930 80 0 0 25 0 1 0 422541694 132698112 27616 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32397 27616 603 41 0 32356 0
vsize: 129588
[startup+910.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 29041 0 0 0 90929 81 0 0 25 0 1 0 422541694 133095424 27709 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32494 27709 603 41 0 32453 0
vsize: 129976
[startup+920.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 29159 0 0 0 91929 81 0 0 25 0 1 0 422541694 133636096 27827 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32626 27827 603 41 0 32585 0
vsize: 130504
[startup+930.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 29328 0 0 0 92929 81 0 0 25 0 1 0 422541694 134295552 27996 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32787 27996 603 41 0 32746 0
vsize: 131148
[startup+940.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 29509 0 0 0 93929 82 0 0 25 0 1 0 422541694 135098368 28177 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32983 28177 603 41 0 32942 0
vsize: 131932
[startup+950.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27501
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 29687 0 0 0 94928 83 0 0 25 0 1 0 422541694 135770112 28355 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33147 28355 603 41 0 33106 0
vsize: 132588
[startup+960.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 29847 0 0 0 95928 83 0 0 25 0 1 0 422541694 136441856 28515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33311 28516 603 41 0 33270 0
vsize: 133244
[startup+970.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 30028 0 0 0 96927 84 0 0 25 0 1 0 422541694 137109504 28696 4294967295 134512640 134672761 3221224560 3221223728 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33474 28696 603 41 0 33433 0
vsize: 133896
[startup+980.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 30231 0 0 0 97927 84 0 0 25 0 1 0 422541694 138039296 28899 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33701 28899 603 41 0 33660 0
vsize: 134804
[startup+990.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 30423 0 0 0 98927 85 0 0 25 0 1 0 422541694 138842112 29091 4294967295 134512640 134672761 3221224560 3221223728 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33897 29091 603 41 0 33856 0
vsize: 135588
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 30607 0 0 0 99926 86 0 0 25 0 1 0 422541694 139501568 29275 4294967295 134512640 134672761 3221224560 3221223760 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34058 29275 603 41 0 34017 0
vsize: 136232
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 30795 0 0 0 100926 86 0 0 25 0 1 0 422541694 140308480 29463 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34255 29463 603 41 0 34214 0
vsize: 137020
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 30999 0 0 0 101925 87 0 0 25 0 1 0 422541694 141119488 29667 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34453 29667 603 41 0 34412 0
vsize: 137812
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 31224 0 0 0 102925 88 0 0 25 0 1 0 422541694 142053376 29892 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34681 29892 603 41 0 34640 0
vsize: 138724
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 31483 0 0 0 103924 88 0 0 25 0 1 0 422541694 143126528 30151 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34943 30151 603 41 0 34902 0
vsize: 139772
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 31642 0 0 0 104924 89 0 0 25 0 1 0 422541694 143785984 30310 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35104 30310 603 41 0 35063 0
vsize: 140416
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 31836 0 0 0 105924 90 0 0 25 0 1 0 422541694 144580608 30504 4294967295 134512640 134672761 3221224560 3221223744 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35298 30504 603 41 0 35257 0
vsize: 141192
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 32019 0 0 0 106923 90 0 0 25 0 1 0 422541694 145256448 30687 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35463 30687 603 41 0 35422 0
vsize: 141852
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 32205 0 0 0 107923 91 0 0 25 0 1 0 422541694 146051072 30873 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35657 30873 603 41 0 35616 0
vsize: 142628
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 32432 0 0 0 108922 92 0 0 25 0 1 0 422541694 146993152 31100 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35887 31100 603 41 0 35846 0
vsize: 143548
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 32604 0 0 0 109921 93 0 0 25 0 1 0 422541694 147673088 31272 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36053 31272 603 41 0 36012 0
vsize: 144212
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 32669 0 0 0 110920 93 0 0 25 0 1 0 422541694 147943424 31337 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36119 31337 603 41 0 36078 0
vsize: 144476
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 32757 0 0 0 111920 93 0 0 25 0 1 0 422541694 148348928 31425 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36218 31425 603 41 0 36177 0
vsize: 144872
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 32823 0 0 0 112920 94 0 0 25 0 1 0 422541694 148619264 31491 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36284 31491 603 41 0 36243 0
vsize: 145136
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 32882 0 0 0 113919 94 0 0 25 0 1 0 422541694 148754432 31550 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36317 31550 603 41 0 36276 0
vsize: 145268
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 32945 0 0 0 114919 94 0 0 25 0 1 0 422541694 149024768 31613 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36383 31613 603 41 0 36342 0
vsize: 145532
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 33255 0 0 0 115919 95 0 0 25 0 1 0 422541694 150364160 31923 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36710 31923 603 41 0 36669 0
vsize: 146840
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 33653 0 0 0 116918 96 0 0 25 0 1 0 422541694 151973888 32321 4294967295 134512640 134672761 3221224560 3221223744 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37103 32321 603 41 0 37062 0
vsize: 148412
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 34066 0 0 0 117917 97 0 0 25 0 1 0 422541694 153579520 32734 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37495 32734 603 41 0 37454 0
vsize: 149980
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 34466 0 0 0 118916 98 0 0 25 0 1 0 422541694 155324416 33134 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37921 33134 603 41 0 37880 0
vsize: 151684
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27503
Raw data (stat): 27446 (minisat+) R 27445 22932 22931 0 -1 0 34893 0 0 0 119915 100 0 0 25 0 1 0 422541694 157081600 33561 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38350 33561 603 41 0 38309 0
vsize: 153400
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 27503
Raw data (stat): 27446 (minisat+) Z 27445 22932 22931 0 -1 12 34896 0 0 0 119916 106 0 0 25 0 1 0 422541694 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): 1199.16
CPU system time (s): 1.06984
CPU usage (%): 100.011
Max. virtual memory (Kb): 153400
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####