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 6166

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        894624 kB
Buffers:         34968 kB
Cached:          83596 kB
SwapCached:       2272 kB
Active:          55752 kB
Inactive:        67940 kB
HighTotal:      131008 kB
HighFree:        43484 kB
LowTotal:       903652 kB
LowFree:        851140 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10708 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:57:00 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 4575 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 398 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     398     9563 |     132       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 173[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 9344   maxlim: 4504   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   65731   242891 |   21910       0        0     nan |  0.000 % |
c |       100 |   65671   242687 |   24101      91      346     3.8 |  0.150 % |
c |       250 |   65645   242597 |   26511     236      861     3.6 |  0.178 % |
c |       475 |   65645   242597 |   29162     461     1837     4.0 |  0.178 % |
c |       812 |   65639   242577 |   32078     797     3103     3.9 |  0.185 % |
c |      1319 |   65639   242577 |   35286    1304     5077     3.9 |  0.185 % |
c |      2078 |   65613   242480 |   38814    2059     7935     3.9 |  0.214 % |
c |      3218 |   65542   242245 |   42696    3189    13638     4.3 |  0.307 % |
c |      4928 |   65542   242245 |   46966    4899    23629     4.8 |  0.307 % |
c |      7490 |   65519   242166 |   51662    7458    88015    11.8 |  0.335 % |
c |     11338 |   65519   242166 |   56828   11306   222593    19.7 |  0.335 % |
c |     17104 |   65519   242166 |   62511   17072   828671    48.5 |  0.335 % |
c |     25755 |   65519   242166 |   68762   25723  1235386    48.0 |  0.335 % |
c |     38729 |   65519   242166 |   75639   38697  3530895    91.2 |  0.335 % |
c |     58190 |   65519   242166 |   83203   58158  5386317    92.6 |  0.335 % |
c |     87382 |   65519   242166 |   91523   21863  3690223   168.8 |  0.335 % |
c |    131174 |   65519   242166 |  100675   65655 10050762   153.1 |  0.335 % |
c |    196858 |   65519   242166 |  110743   43939 16290396   370.8 |  0.335 % |
c |    295384 |   65519   242166 |  121817   46461 13761681   296.2 |  0.335 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 -x3 -x4 x5 -x6 -x7 -x8 x9 x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 x22 -x23 -x24 -x25 -x26 x27 x28 x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 x45 x46 -x47 -x48 -x49 -x50 x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 x78 x79 x80 -x81 -x82 -x83 x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 x137 -x138 -x139 x140 -x141 x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 x241 x242 x243 -x244 x245 -x246 -x247 -x248 x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 x279 -x280 -x281 -x282 -x283 x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 x441 x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 x544 x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 x601 -x602 -x603 -x604 -x605 -x606 -x607 x608 -x609 -x610 -x611 -x612 -x613 -x614 x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 x717 -x718 x719 -x720 -x721 -x722 x723 -x724 -x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 -x765 -x766 -x767 x768 x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 x873 -x874 -x875 -x876 -x877 x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 x1028 -x1029 x1030 -x1031 -x1032 -x1033 x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 x1336 -x1337 -x1338 -x1339 -x1340 -x1341 -x1342 -x1343 -x1344 x1345 -x1346 -x1347 -x1348 -x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 -x1408 -x1409 -x1410 x1411 -x1412 -x1413 -x1414 -x1415 -x1416 -x1417 x1418 -x1419 x1420 -x1421 -x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 -x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 -x1470 -x1471 -x1472 -x1473 -x1474 -x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 -x1498 -x1499 -x1500 -x1501 -x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 -x1518 -x1519 -x1520 -x1521 -x1522 -x1523 x1524 -x1525 -x1526 -x1527 -x1528 -x1529 -x1530 -x1531 -x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 -x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 x1567 -x1568 -x1569 -x1570 -x1571 -x1572 -x1573 -x1574 x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 -x1622 -x1623 -x1624 -x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 x1633 -x1634 -x1635 x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 -x1654 -x1655 -x1656 -x1657 -x1658 -x1659 -x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 -x1676 -x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 x1709 -x1710 -x1711 -x1712 -x1713 -x1714 -x1715 -x1716 -x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 -x1743 -x1744 -x1745 -x1746 -x1747 -x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 -x1765 -x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 x1787 -x1788 -x1789 -x1790 -x1791 -x1792 -x1793 -x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 -x1801 -x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 x1818 x1819 -x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 -x1827 -x1828 -x1829 -x1830 -x1831 -x1832 x1833 -x1834 -x1835 -x1836 -x1837 -x1838 -x1839 x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 -x1848 -x1849 -x1850 x1851 -x1852 -x1853 -x1854 -x1855 x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 x1876 -x1877 -x1878 x1879 -x1880 -x1881 -x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 -x1919 -x1920 -x1921 x1922 -x1923 -x1924 -x1925 -x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 -x1943 -x1944 -x1945 -x1946 -x1947 -x1948 -x1949 -x1950 -x1951 -x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 -x1962 -x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 -x1970 -x1971 -x1972 -x1973 -x1974 -x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981 -x1982 -x1983 -x1984 -x1985 -x1986 -x1987 -x1988 -x1989 -x1990 -x1991 -x1992 -x1993 -x1994 -x1995 -x1996 -x1997 -x1998 -x1999 -x2000 -x2001 x2002 -x2003 -x2004 -x2005 -x2006 -x2007 -x2008 -x2009 -x2010 -x2011 -x2012 -x2013 -x2014 -x2015 -x2016 -x2017 -x2018 -x2019 -x2020 -x2021 -x2022 -x2023 -x2024 -x2025 -x2026 -x2027 -x2028 -x2029 -x2030 -x2031 -x2032 -x2033 -x2034 -x2035 -x2036 -x2037 -x2038 -x2039 -x2040 -x2041 -x2042 -x2043 -x2044 -x2045 -x2046 -x2047 -x2048 -x2049 -x2050 -x2051 -x2052 -x2053 -x2054 -x2055 -x2056 -x2057 -x2058 -x2059 -x2060 -x2061 -x2062 -x2063 -x2064 -x2065 -x2066 x2067 -x2068 -x2069 -x2070 -x2071 -x2072 -x2073 -x2074 x2075 x2076 -x2077 -x2078 -x2079 -x2080 -x2081 -x2082 x2083 -x2084 -x2085 -x2086 -x2087 -x2088 -x2089 -x2090 -x2091 -x2092 -x2093 -x2094 -x2095 -x2096 -x2097 -x2098 -x2099 -x2100 -x2101 -x2102 -x2103 -x2104 -x2105 -x2106 -x2107 -x2108 -x2109 -x2110 -x2111 -x2112 -x2113 -x2114 -x2115 -x2116 -x2117 -x2118 -x2119 -x2120 -x2121 -x2122 -x2123 -x2124 -x2125 x2126 -x2127 -x2128 -x2129 x2130 -x2131 -x2132 -x2133 -x2134 -x2135 -x2136 x2137 -x2138 -x2139 -x2140 -x2141 -x2142 -x2143 -x2144 -x2145 -x2146 -x2147 -x2148 -x2149 x2150 -x2151 -x2152 -x2153 -x2154 -x2155 -x2156 -x2157 -x2158 -x2159 -x2160 -x2161 -x2162 -x2163 -x2164 -x2165 -x2166 -x2167 -x2168 -x2169 -x2170 -x2171 x2172 -x2173 -x2174 -x2175 -x2176 -x2177 -x2178 -x2179 -x2180 -x2181 x2182 -x2183 -x2184 -x2185 -x2186 -x2187 -x2188 -x2189 -x2190 -x2191 -x2192 -x2193 -x2194 -x2195 -x2196 -x2197 -x2198 -x2199 -x2200 -x2201 -x2202 x2203 -x2204 -x2205 x2206 -x2207 -x2208 -x2209 -x2210 -x2211 -x2212 -x2213 -x2214 -x2215 -x2216 -x2217 -x2218 -x2219 -x2220 -x2221 -x2222 -x2223 -x2224 -x2225 -x2226 -x2227 -x2228 -x2229 -x2230 -x2231 -x2232 -x2233 -x2234 -x2235 -x2236 -x2237 -x2238 -x2239 -x2240 -x2241 -x2242 -x2243 -x2244 -x2245 -x2246 -x2247 -x2248 -x2249 -x2250 -x2251 -x2252 x2253 -x2254 -x2255 -x2256 -x2257 -x2258 -x2259 x2260 -x2261 -x2262 -x2263 -x2264 -x2265 x2266 -x2267 -x2268 -x2269 -x2270 -x2271 -x2272 -x2273 -x2274 -x2275 -x2276 -x2277 -x2278 -x2279 -x2280 x2281 -x2282 -x2283 -x2284 -x2285 -x2286 -x2287 -x2288 -x2289 -x2290 -x2291 -x2292 -x2293 -x2294 -x2295 -x2296 -x2297 -x2298 -x2299 -x2300 -x2301 -x2302 x2303 -x2304 -x2305 -x2306 -x2307 -x2308 -x2309 -x2310 -x2311 -x2312 -x2313 -x2314 -x2315 -x2316 -x2317 -x2318 -x2319 -x2320 -x2321 -x2322 -x2323 -x2324 -x2325 -x2326 -x2327 -x2328 -x2329 -x2330 -x2331 -x2332 -x2333 -x2334 -x2335 -x2336 -x2337 -x2338 -x2339 -x2340 -x2341 -x2342 -x2343 -x2344 -x2345 -x2346 -x2347 -x2348 x2349 -x2350 -x2351 -x2352 -x2353 -x2354 -x2355 -x2356 -x2357 -x2358 -x2359 -x2360 -x2361 -x2362 -x2363 -x2364 -x2365 -x2366 -x2367 -x2368 -x2369 -x2370 -x2371 -x2372 x2373 -x2374 -x2375 -x2376 -x2377 -x2378 -x2379 -x2380 -x2381 -x2382 -x2383 -x2384 -x2385 -x2386 -x2387 -x2388 -x2389 -x2390 -x2391 -x2392 -x2393 -x2394 -x2395 x2396 -x2397 -x2398 -x2399 -x2400 -x2401 -x2402 -x2403 -x2404 -x2405 -x2406 -x2407 -x2408 -x2409 -x2410 -x2411 -x2412 -x2413 -x2414 -x2415 -x2416 -x2417 -x2418 -x2419 -x2420 -x2421 -x2422 -x2423 -x2424 -x2425 -x2426 -x2427 -x2428 -x2429 -x2430 -x2431 -x2432 -x2433 -x2434 -x2435 -x2436 -x2437 -x2438 -x2439 -x2440 -x2441 -x2442 -x2443 -x2444 -x2445 -x2446 -x2447 -x2448 -x2449 -x2450 -x2451 -x2452 -x2453 -x2454 -x2455 -x2456 -x2457 -x2458 -x2459 -x2460 -x2461 -x2462 -x2463 -x2464 -x2465 -x2466 -x2467 -x2468 -x2469 -x2470 -x2471 -x2472 -x2473 -x2474 -x2475 -x2476 -x2477 -x2478 -x2479 -x2480 -x2481 -x2482 -x2483 -x2484 -x2485 -x2486 -x2487 -x2488 -x2489 -x2490 -x2491 -x2492 -x2493 -x2494 -x2495 -x2496 -x2497 -x2498 -x2499 -x2500 -x2501 -x2502 -x2503 -x2504 -x2505 -x2506 -x2507 -x2508 -x2509 -x2510 -x2511 -x2512 -x2513 -x2514 -x2515 -x2516 -x2517 -x2518 -x2519 -x2520 -x2521 -x2522 -x2523 -x2524 -x2525 -x2526 -x2527 -x2528 -x2529 -x2530 -x2531 -x2532 -x2533 -x2534 -x2535 -x2536 -x2537 -x2538 -x2539 -x2540 -x2541 -x2542 -x2543 -x2544 -x2545 -x2546 -x2547 -x2548 -x2549 -x2550 -x2551 -x2552 -x2553 -x2554 -x2555 -x2556 -x2557 -x2558 -x2559 -x2560 -x2561 x2562 -x2563 -x2564 -x2565 -x2566 -x2567 -x2568 -x2569 -x2570 -x2571 -x2572 -x2573 -x2574 -x2575 -x2576 -x2577 -x2578 -x2579 x2580 -x2581 -x2582 -x2583 -x2584 -x2585 -x2586 -x2587 -x2588 -x2589 -x2590 -x2591 -x2592 -x2593 -x2594 -x2595 -x2596 -x2597 -x2598 -x2599 -x2600 -x2601 -x2602 -x2603 -x2604 -x2605 -x2606 -x2607 -x2608 x2609 -x2610 x2611 -x2612 -x2613 -x2614 -x2615 -x2616 -x2617 -x2618 -x2619 -x2620 -x2621 -x2622 x2623 -x2624 -x2625 -x2626 -x2627 -x2628 -x2629 -x2630 -x2631 -x2632 -x2633 -x2634 -x2635 -x2636 x2637 -x2638 -x2639 -x2640 -x2641 -x2642 -x2643 -x2644 -x2645 -x2646 -x2647 -x2648 -x2649 -x2650 -x2651 -x2652 -x2653 -x2654 -x2655 -x2656 -x2657 -x2658 -x2659 -x2660 -x2661 -x2662 x2663 -x2664 -x2665 -x2666 -x2667 -x2668 x2669 -x2670 -x2671 -x2672 -x2673 -x2674 -x2675 -x2676 -x2677 -x2678 -x2679 -x2680 -x2681 -x2682 x2683 -x2684 -x2685 -x2686 -x2687 -x2688 -x2689 -x2690 -x2691 -x2692 -x2693 -x2694 -x2695 -x2696 -x2697 -x2698 -x2699 -x2700 x2701 -x2702 -x2703 -x2704 -x2705 -x2706 x2707 -x2708 -x2709 -x2710 -x2711 -x2712 -x2713 -x2714 -x2715 -x2716 -x2717 -x2718 -x2719 -x2720 -x2721 -x2722 -x2723 -x2724 -x2725 -x2726 -x2727 x2728 -x2729 -x2730 -x2731 -x2732 -x2733 -x2734 -x2735 -x2736 -x2737 -x2738 -x2739 -x2740 -x2741 -x2742 -x2743 -x2744 -x2745 -x2746 -x2747 -x2748 -x2749 -x2750 -x2751 -x2752 -x2753 -x2754 -x2755 -x2756 -x2757 -x2758 x2759 -x2760 -x2761 -x2762 -x2763 -x2764 x2765 -x2766 -x2767 -x2768 -x2769 -x2770 -x2771 -x2772 -x2773 -x2774 -x2775 -x2776 -x2777 -x2778 -x2779 -x2780 -x2781 -x2782 -x2783 -x2784 -x2785 x2786 -x2787 -x2788 -x2789 -x2790 -x2791 -x2792 -x2793 -x2794 -x2795 -x2796 -x2797 -x2798 -x2799 -x2800 -x2801 -x2802 -x2803 -x2804 -x2805 -x2806 -x2807 -x2808 -x2809 -x2810 -x2811 -x2812 -x2813 -x2814 -x2815 x2816 -x2817 -x2818 -x2819 -x2820 -x2821 -x2822 -x2823 -x2824 -x2825 -x2826 -x2827 -x2828 -x2829 -x2830 -x2831 -x2832 -x2833 -x2834 -x2835 -x2836 -x2837 -x2838 -x2839 x2840 -x2841 -x2842 -x2843 -x2844 -x2845 -x2846 -x2847 -x2848 -x2849 -x2850 -x2851 -x2852 -x2853 -x2854 -x2855 -x2856 -x2857 -x2858 -x2859 -x2860 -x2861 -x2862 -x2863 -x2864 -x2865 -x2866 -x2867 -x2868 -x2869 -x2870 -x2871 x2872 -x2873 -x2874 -x2875 -x2876 -x2877 -x2878 -x2879 -x2880 -x2881 -x2882 -x2883 -x2884 -x2885 -x2886 -x2887 -x2888 -x2889 -x2890 -x2891 -x2892 -x2893 -x2894 -x2895 -x2896 -x2897 -x2898 -x2899 -x2900 -x2901 -x2902 -x2903 -x2904 -x2905 -x2906 -x2907 -x2908 -x2909 -x2910 -x2911 -x2912 -x2913 -x2914 x2915 -x2916 -x2917 x2918 -x2919 -x2920 -x2921 -x2922 -x2923 -x2924 -x2925 -x2926 -x2927 -x2928 -x2929 -x2930 -x2931 x2932 -x2933 -x2934 -x2935 -x2936 -x2937 -x2938 -x2939 -x2940 -x2941 -x2942 -x2943 -x2944 -x2945 -x2946 -x2947 -x2948 -x2949 -x2950 -x2951 -x2952 -x2953 -x2954 -x2955 -x2956 -x2957 -x2958 -x2959 -x2960 -x2961 -x2962 -x2963 -x2964 -x2965 -x2966 -x2967 -x2968 -x2969 -x2970 -x2971 -x2972 -x2973 -x2974 -x2975 -x2976 -x2977 -x2978 -x2979 -x2980 -x2981 x2982 -x2983 -x2984 -x2985 -x2986 -x2987 -x2988 -x2989 -x2990 -x2991 -x2992 -x2993 -x2994 -x2995 -x2996 -x2997 -x2998 x2999 -x3000 -x3001 -x3002 -x3003 -x3004 -x3005 -x3006 -x3007 -x3008 -x3009 -x3010 -x3011 -x3012 -x3013 -x3014 -x3015 -x3016 -x3017 -x3018 -x3019 -x3020 -x3021 -x3022 -x3023 -x3024 -x3025 -x3026 -x3027 -x3028 -x3029 -x3030 -x3031 -x3032 -x3033 -x3034 -x3035 -x3036 -x3037 -x3038 -x3039 -x3040 -x3041 -x3042 -x3043 -x3044 -x3045 -x3046 -x3047 -x3048 -x3049 -x3050 -x3051 -x3052 -x3053 -x3054 -x3055 -x3056 -x3057 -x3058 -x3059 -x3060 -x3061 -x3062 -x3063 -x3064 -x3065 -x3066 -x3067 -x3068 -x3069 -x3070 -x3071 -x3072 -x3073 -x3074 -x3075 -x3076 -x3077 -x3078 -x3079 -x3080 -x3081 -x3082 -x3083 -x3084 -x3085 -x3086 -x3087 -x3088 -x3089 -x3090 -x3091 -x3092 -x3093 -x3094 -x3095 -x3096 -x3097 -x3098 -x3099 -x3100 -x3101 -x3102 -x3103 -x3104 -x3105 -x3106 -x3107 -x3108 -x3109 -x3110 -x3111 -x3112 -x3113 -x3114 -x3115 -x3116 -x3117 -x3118 -x3119 -x3120 -x3121 -x3122 -x3123 -x3124 -x3125 -x3126 -x3127 x3128 -x3129 -x3130 -x3131 -x3132 -x3133 -x3134 -x3135 -x3136 -x3137 -x3138 -x3139 -x3140 -x3141 -x3142 -x3143 -x3144 -x3145 -x3146 x3147 -x3148 -x3149 -x3150 -x3151 -x3152 -x3153 -x3154 -x3155 -x3156 -x3157 -x3158 -x3159 -x3160 -x3161 -x3162 -x3163 -x3164 -x3165 -x3166 -x3167 -x3168 -x3169 -x3170 -x3171 -x3172 -x3173 -x3174 -x3175 -x3176 -x3177 -x3178 -x3179 -x3180 -x3181 -x3182 -x3183 -x3184 -x3185 -x3186 -x3187 -x3188 -x3189 -x3190 -x3191 -x3192 -x3193 -x3194 -x3195 -x3196 -x3197 -x3198 -x3199 -x3200 -x3201 -x3202 -x3203 -x3204 -x3205 -x3206 -x3207 -x3208 -x3209 -x3210 -x3211 -x3212 -x3213 -x3214 -x3215 -x3216 -x3217 -x3218 -x3219 -x3220 -x3221 -x3222 -x3223 -x3224 -x3225 -x3226 -x3227 -x3228 -x3229 -x3230 -x3231 -x3232 -x3233 -x3234 -x3235 -x3236 -x3237 -x3238 -x3239 -x3240 -x3241 -x3242 -x3243 -x3244 -x3245 -x3246 -x3247 -x3248 -x3249 -x3250 -x3251 -x3252 -x3253 -x3254 -x3255 -x3256 -x3257 -x3258 -x3259 -x3260 -x3261 -x3262 -x3263 -x3264 -x3265 -x3266 -x3267 -x3268 -x3269 -x3270 -x3271 -x3272 -x3273 -x3274 -x3275 -x3276 -x3277 -x3278 -x3279 x3280 -x3281 -x3282 -x3283 -x3284 -x3285 -x3286 -x3287 -x3288 -x3289 -x3290 -x3291 -x3292 -x3293 -x3294 -x3295 -x3296 -x3297 -x3298 -x3299 -x3300 -x3301 -x3302 -x3303 -x3304 -x3305 -x3306 -x3307 -x3308 -x3309 x3310 -x3311 -x3312 -x3313 -x3314 -x3315 -x3316 x3317 -x3318 -x3319 -x3320 -x3321 -x3322 -x3323 -x3324 -x3325 -x3326 -x3327 -x3328 -x3329 -x3330 -x3331 -x3332 -x3333 -x3334 -x3335 -x3336 -x3337 -x3338 -x3339 -x3340 -x3341 -x3342 -x3343 -x3344 -x3345 -x3346 -x3347 -x3348 -x3349 -x3350 -x3351 -x3352 -x3353 -x3354 -x3355 -x3356 -x3357 -x3358 -x3359 -x3360 x3361 -x3362 -x3363 -x3364 -x3365 -x3366 -x3367 -x3368 -x3369 -x3370 -x3371 -x3372 -x3373 -x3374 -x3375 -x3376 -x3377 -x3378 -x3379 -x3380 -x3381 -x3382 -x3383 -x3384 -x3385 -x3386 -x3387 -x3388 -x3389 -x3390 -x3391 -x3392 -x3393 -x3394 -x3395 -x3396 -x3397 -x3398 -x3399 -x3400 -x3401 -x3402 -x3403 -x3404 -x3405 x3406 -x3407 -x3408 -x3409 x3410 -x3411 -x3412 -x3413 -x3414 -x3415 -x3416 -x3417 -x3418 -x3419 -x3420 -x3421 -x3422 -x3423 -x3424 -x3425 -x3426 -x3427 -x3428 -x3429 -x3430 -x3431 -x3432 -x3433 -x3434 -x3435 -x3436 -x3437 -x3438 -x3439 x3440 -x3441 -x3442 -x3443 -x3444 -x3445 -x3446 -x3447 -x3448 -x3449 -x3450 -x3451 -x3452 -x3453 -x3454 -x3455 -x3456 -x3457 -x3458 -x3459 -x3460 -x3461 -x3462 -x3463 -x3464 -x3465 -x3466 -x3467 -x3468 -x3469 -x3470 -x3471 x3472 -x3473 -x3474 -x3475 -x3476 -x3477 -x3478 -x3479 -x3480 -x3481 -x3482 -x3483 -x3484 -x3485 -x3486 -x3487 -x3488 -x3489 -x3490 -x3491 -x3492 -x3493 -x3494 -x3495 -x3496 -x3497 -x3498 -x3499 -x3500 -x3501 -x3502 -x3503 -x3504 -x3505 -x3506 -x3507 -x3508 -x3509 -x3510 -x3511 -x3512 x3513 -x3514 -x3515 -x3516 -x3517 -x3518 -x3519 -x3520 -x3521 -x3522 -x3523 -x3524 -x3525 -x3526 -x3527 -x3528 -x3529 -x3530 -x3531 -x3532 -x3533 -x3534 -x3535 -x3536 -x3537 -x3538 -x3539 -x3540 -x3541 -x3542 -x3543 -x3544 -x3545 -x3546 -x3547 -x3548 -x3549 -x3550 -x3551 -x3552 -x3553 -x3554 -x3555 -x3556 -x3557 -x3558 -x3559 -x3560 -x3561 -x3562 -x3563 -x3564 -x3565 -x3566 -x3567 -x3568 -x3569 -x3570 -x3571 -x3572 -x3573 -x3574 -x3575 -x3576 -x3577 -x3578 -x3579 -x3580 -x3581 -x3582 -x3583 -x3584 -x3585 -x3586 -x3587 -x3588 -x3589 -x3590 -x3591 -x3592 -x3593 -x3594 -x3595 -x3596 -x3597 -x3598 -x3599 -x3600 -x3601 -x3602 -x3603 -x3604 x3605 -x3606 -x3607 -x3608 -x3609 -x3610 -x3611 -x3612 -x3613 -x3614 -x3615 -x3616 -x3617 -x3618 -x3619 -x3620 -x3621 -x3622 -x3623 -x3624 -x3625 -x3626 -x3627 -x3628 -x3629 -x3630 -x3631 -x3632 -x3633 -x3634 -x3635 -x3636 -x3637 -x3638 -x3639 -x3640 -x3641 -x3642 -x3643 -x3644 -x3645 -x3646 -x3647 -x3648 -x3649 -x3650 -x3651 -x3652 -x3653 -x3654 -x3655 -x3656 -x3657 -x3658 -x3659 -x3660 -x3661 -x3662 -x3663 -x3664 -x3665 -x3666 -x3667 -x3668 -x3669 -x3670 -x3671 -x3672 -x3673 -x3674 -x3675 -x3676 -x3677 -x3678 -x3679 x3680 -x3681 -x3682 -x3683 -x3684 -x3685 -x3686 -x3687 -x3688 -x3689 -x3690 -x3691 -x3692 -x3693 -x3694 -x3695 -x3696 -x3697 -x3698 -x3699 -x3700 -x3701 -x3702 -x3703 -x3704 -x3705 -x3706 -x3707 -x3708 -x3709 -x3710 x3711 -x3712 -x3713 -x3714 -x3715 -x3716 -x3717 -x3718 -x3719 -x3720 -x3721 -x3722 -x3723 -x3724 -x3725 -x3726 -x3727 -x3728 -x3729 -x3730 -x3731 -x3732 -x3733 -x3734 -x3735 -x3736 -x3737 -x3738 -x3739 -x3740 -x3741 -x3742 -x3743 -x3744 -x3745 -x3746 -x3747 -x3748 -x3749 -x3750 -x3751 -x3752 -x3753 -x3754 -x3755 -x3756 -x3757 -x3758 -x3759 -x3760 -x3761 -x3762 -x3763 -x3764 -x3765 -x3766 -x3767 -x3768 -x3769 -x3770 -x3771 -x3772 -x3773 -x3774 -x3775 -x3776 -x3777 -x3778 -x3779 -x3780 -x3781 -x3782 x3783 -x3784 -x3785 -x3786 -x3787 -x3788 -x3789 -x3790 -x3791 -x3792 -x3793 -x3794 -x3795 -x3796 -x3797 -x3798 -x3799 -x3800 -x3801 -x3802 -x3803 -x3804 -x3805 -x3806 -x3807 -x3808 -x3809 -x3810 -x3811 -x3812 -x3813 -x3814 -x3815 -x3816 -x3817 -x3818 -x3819 -x3820 -x3821 -x3822 -x3823 -x3824 -x3825 -x3826 -x3827 -x3828 -x3829 -x3830 -x3831 -x3832 -x3833 -x3834 -x3835 -x3836 -x3837 -x3838 -x3839 -x3840 -x3841 -x3842 -x3843 -x3844 -x3845 -x3846 -x3847 -x3848 -x3849 -x3850 -x3851 -x3852 -x3853 -x3854 -x3855 -x3856 -x3857 -x3858 -x3859 -x3860 -x3861 -x3862 -x3863 x3864 -x3865 -x3866 -x3867 -x3868 -x3869 -x3870 -x3871 -x3872 -x3873 -x3874 -x3875 -x3876 -x3877 -x3878 -x3879 -x3880 -x3881 -x3882 -x3883 -x3884 -x3885 -x3886 -x3887 -x3888 -x3889 -x3890 -x3891 -x3892 -x3893 -x3894 -x3895 -x3896 -x3897 -x3898 -x3899 -x3900 -x3901 -x3902 -x3903 -x3904 -x3905 -x3906 -x3907 -x3908 -x3909 -x3910 -x3911 -x3912 -x3913 -x3914 -x3915 -x3916 -x3917 -x3918 -x3919 -x3920 -x3921 -x3922 -x3923 -x3924 -x3925 -x3926 -x3927 -x3928 -x3929 -x3930 -x3931 -x3932 -x3933 -x3934 -x3935 -x3936 -x3937 x3938 -x3939 -x3940 -x3941 -x3942 -x3943 -x3944 -x3945 -x3946 -x3947 -x3948 -x3949 -x3950 -x3951 -x3952 -x3953 -x3954 -x3955 -x3956 -x3957 -x3958 -x3959 -x3960 -x3961 -x3962 -x3963 -x3964 -x3965 -x3966 -x3967 -x3968 -x3969 -x3970 -x3971 x3972 -x3973 -x3974 -x3975 -x3976 -x3977 -x3978 -x3979 -x3980 -x3981 -x3982 -x3983 -x3984 -x3985 -x3986 -x3987 -x3988 -x3989 x3990 -x3991 -x3992 -x3993 -x3994 -x3995 -x3996 -x3997 -x3998 -x3999 -x4000 -x4001 -x4002 -x4003 -x4004 -x4005 -x4006 -x4007 -x4008 -x4009 -x4010 -x4011 -x4012 -x4013 -x4014 -x4015 -x4016 -x4017 -x4018 -x4019 -x4020 -x4021 -x4022 -x4023 -x4024 -x4025 -x4026 -x4027 -x4028 -x4029 -x4030 -x4031 -x4032 -x4033 -x4034 -x4035 x4036 -x4037 -x4038 -x4039 -x4040 -x4041 -x4042 -x4043 -x4044 -x4045 -x4046 -x4047 -x4048 -x4049 -x4050 -x4051 -x4052 -x4053 -x4054 -x4055 -x4056 -x4057 -x4058 -x4059 -x4060 -x4061 -x4062 -x4063 -x4064 -x4065 -x4066 -x4067 -x4068 -x4069 -x4070 -x4071 -x4072 -x4073 -x4074 -x4075 -x4076 -x4077 -x4078 -x4079 -x4080 -x4081 -x4082 -x4083 -x4084 -x4085 -x4086 -x4087 -x4088 -x4089 -x4090 -x4091 -x4092 -x4093 -x4094 -x4095 -x4096 -x4097 -x4098 -x4099 -x4100 -x4101 -x4102 -x4103 -x4104 -x4105 -x4106 -x4107 -x4108 -x4109 -x4110 -x4111 -x4112 -x4113 -x4114 -x4115 -x4116 -x4117 -x4118 -x4119 -x4120 -x4121 -x4122 -x4123 -x4124 -x4125 -x4126 -x4127 -x4128 -x4129 -x4130 -x4131 -x4132 -x4133 -x4134 -x4135 -x4136 -x4137 -x4138 x4139 -x4140 -x4141 -x4142 -x4143 -x4144 -x4145 -x4146 -x4147 -x4148 -x4149 -x4150 -x4151 -x4152 -x4153 -x4154 -x4155 -x4156 -x4157 -x4158 -x4159 -x4160 -x4161 -x4162 -x4163 -x4164 -x4165 -x4166 -x4167 -x4168 -x4169 -x4170 -x4171 -x4172 -x4173 -x4174 -x4175 -x4176 -x4177 -x4178 -x4179 -x4180 -x4181 -x4182 -x4183 -x4184 -x4185 -x4186 -x4187 -x4188 -x4189 -x4190 -x4191 -x4192 -x4193 -x4194 -x4195 -x4196 -x4197 -x4198 -x4199 -x4200 -x4201 -x4202 -x4203 -x4204 -x4205 -x4206 -x4207 -x4208 -x4209 -x4210 -x4211 -x4212 -x4213 -x4214 -x4215 -x4216 -x4217 -x4218 -x4219 -x4220 -x4221 -x4222 -x4223 -x4224 -x4225 -x4226 -x4227 -x4228 -x4229 -x4230 -x4231 -x4232 -x4233 -x4234 -x4235 -x4236 -x4237 -x4238 -x4239 -x4240 -x4241 -x4242 -x4243 -x4244 -x4245 -x4246 -x4247 -x4248 -x4249 -x4250 -x4251 -x4252 -x4253 -x4254 -x4255 -x4256 -x4257 -x4258 -x4259 -x4260 -x4261 -x4262 -x4263 -x4264 -x4265 -x4266 -x4267 -x4268 -x4269 -x4270 -x4271 -x4272 -x427#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 29187
Raw data (stat): 29187 (runsolver) R 29186 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423182568 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 7232 0 0 0 980 17 0 0 25 0 1 0 423182568 28012544 5886 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6839 5886 603 41 0 6798 0
vsize: 27356
[startup+20.001 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 7413 0 0 0 1979 18 0 0 25 0 1 0 423182568 28745728 6067 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7018 6067 603 41 0 6977 0
vsize: 28072
[startup+30.0014 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 8186 0 0 0 2977 21 0 0 25 0 1 0 423182568 31854592 6840 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7777 6840 603 41 0 7736 0
vsize: 31108
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 9232 0 0 0 3973 24 0 0 25 0 1 0 423182568 36159488 7886 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8828 7886 603 41 0 8787 0
vsize: 35312
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 10029 0 0 0 4970 27 0 0 25 0 1 0 423182568 39518208 8683 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9648 8683 603 41 0 9607 0
vsize: 38592
[startup+60.0027 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 11081 0 0 0 5966 30 0 0 25 0 1 0 423182568 43827200 9735 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10700 9735 603 41 0 10659 0
vsize: 42800
[startup+70.0031 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 11876 0 0 0 6963 32 0 0 25 0 1 0 423182568 47054848 10530 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11488 10530 603 41 0 11447 0
vsize: 45952
[startup+80.0035 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 12684 0 0 0 7962 34 0 0 25 0 1 0 423182568 50278400 11338 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12275 11338 603 41 0 12234 0
vsize: 49100
[startup+90.0029 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 13575 0 0 0 8959 37 0 0 25 0 1 0 423182568 53907456 12229 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13161 12229 603 41 0 13120 0
vsize: 52644
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 14553 0 0 0 9955 41 0 0 25 0 1 0 423182568 58204160 13207 4294967295 134512640 134672761 3221224560 3221223664 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14210 13208 603 41 0 14169 0
vsize: 56840
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 15662 0 0 0 10953 44 0 0 25 0 1 0 423182568 62767104 14316 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15324 14316 603 41 0 15283 0
vsize: 61296
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 16682 0 0 0 11951 46 0 0 25 0 1 0 423182568 66916352 15336 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16337 15336 603 41 0 16296 0
vsize: 65348
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 17752 0 0 0 12948 49 0 0 25 0 1 0 423182568 71217152 16406 4294967295 134512640 134672761 3221224560 3221223744 134558888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17387 16406 603 41 0 17346 0
vsize: 69548
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 18548 0 0 0 13945 52 0 0 25 0 1 0 423182568 74452992 17202 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18177 17202 603 41 0 18136 0
vsize: 72708
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 19259 0 0 0 14943 54 0 0 25 0 1 0 423182568 77410304 17913 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18899 17913 603 41 0 18858 0
vsize: 75596
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 19827 0 0 0 15942 55 0 0 25 0 1 0 423182568 79679488 18481 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19453 18481 603 41 0 19412 0
vsize: 77812
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 19827 0 0 0 16942 55 0 0 25 0 1 0 423182568 79679488 18481 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19453 18481 603 41 0 19412 0
vsize: 77812
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 19827 0 0 0 17943 55 0 0 25 0 1 0 423182568 79679488 18481 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19453 18481 603 41 0 19412 0
vsize: 77812
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 19827 0 0 0 18943 55 0 0 25 0 1 0 423182568 79679488 18481 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19453 18481 603 41 0 19412 0
vsize: 77812
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 19827 0 0 0 19943 55 0 0 25 0 1 0 423182568 79679488 18481 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19453 18481 603 41 0 19412 0
vsize: 77812
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 19827 0 0 0 20943 55 0 0 25 0 1 0 423182568 79679488 18481 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19453 18481 603 41 0 19412 0
vsize: 77812
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 19827 0 0 0 21943 55 0 0 25 0 1 0 423182568 79679488 18481 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19453 18481 603 41 0 19412 0
vsize: 77812
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 19827 0 0 0 22944 55 0 0 25 0 1 0 423182568 79679488 18481 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19453 18481 603 41 0 19412 0
vsize: 77812
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 19827 0 0 0 23944 55 0 0 25 0 1 0 423182568 79679488 18481 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19453 18481 603 41 0 19412 0
vsize: 77812
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 19827 0 0 0 24944 55 0 0 25 0 1 0 423182568 79679488 18481 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19453 18481 603 41 0 19412 0
vsize: 77812
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 20045 0 0 0 25943 56 0 0 25 0 1 0 423182568 80625664 18699 4294967295 134512640 134672761 3221224560 3221223664 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19684 18699 603 41 0 19643 0
vsize: 78736
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 20796 0 0 0 26941 58 0 0 25 0 1 0 423182568 83705856 19450 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20436 19450 603 41 0 20395 0
vsize: 81744
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 21405 0 0 0 27940 60 0 0 25 0 1 0 423182568 86257664 20059 4294967295 134512640 134672761 3221224560 3221223664 134560306 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21059 20059 603 41 0 21018 0
vsize: 84236
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 22134 0 0 0 28937 63 0 0 25 0 1 0 423182568 89227264 20788 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21784 20788 603 41 0 21743 0
vsize: 87136
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 22984 0 0 0 29934 66 0 0 25 0 1 0 423182568 92704768 21638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22633 21638 603 41 0 22592 0
vsize: 90532
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 23847 0 0 0 30932 68 0 0 25 0 1 0 423182568 96198656 22501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23486 22501 603 41 0 23445 0
vsize: 93944
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 24528 0 0 0 31930 70 0 0 25 0 1 0 423182568 99012608 23182 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24173 23182 603 41 0 24132 0
vsize: 96692
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 25561 0 0 0 32928 73 0 0 25 0 1 0 423182568 103186432 24215 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25192 24215 603 41 0 25151 0
vsize: 100768
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 26561 0 0 0 33925 76 0 0 25 0 1 0 423182568 107229184 25215 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26179 25215 603 41 0 26138 0
vsize: 104716
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 27489 0 0 0 34922 79 0 0 25 0 1 0 423182568 111124480 26143 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27130 26143 603 41 0 27089 0
vsize: 108520
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 28311 0 0 0 35921 81 0 0 25 0 1 0 423182568 114356224 26965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27919 26965 603 41 0 27878 0
vsize: 111676
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 29065 0 0 0 36919 83 0 0 25 0 1 0 423182568 117448704 27719 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28674 27719 603 41 0 28633 0
vsize: 114696
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 29766 0 0 0 37916 86 0 0 25 0 1 0 423182568 120422400 28420 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29400 28420 603 41 0 29359 0
vsize: 117600
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30044 0 0 0 38916 86 0 0 25 0 1 0 423182568 121499648 28698 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28698 603 41 0 29622 0
vsize: 118652
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30045 0 0 0 39916 86 0 0 25 0 1 0 423182568 121499648 28699 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28699 603 41 0 29622 0
vsize: 118652
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30045 0 0 0 40916 86 0 0 25 0 1 0 423182568 121499648 28699 4294967295 134512640 134672761 3221224560 3221223740 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28699 603 41 0 29622 0
vsize: 118652
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30046 0 0 0 41916 86 0 0 25 0 1 0 423182568 121499648 28700 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28700 603 41 0 29622 0
vsize: 118652
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30046 0 0 0 42916 86 0 0 25 0 1 0 423182568 121499648 28700 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28700 603 41 0 29622 0
vsize: 118652
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30046 0 0 0 43917 86 0 0 25 0 1 0 423182568 121499648 28700 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28700 603 41 0 29622 0
vsize: 118652
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30046 0 0 0 44917 86 0 0 25 0 1 0 423182568 121499648 28700 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28700 603 41 0 29622 0
vsize: 118652
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30046 0 0 0 45917 86 0 0 25 0 1 0 423182568 121499648 28700 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28700 603 41 0 29622 0
vsize: 118652
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30046 0 0 0 46917 86 0 0 25 0 1 0 423182568 121499648 28700 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28700 603 41 0 29622 0
vsize: 118652
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30046 0 0 0 47918 86 0 0 25 0 1 0 423182568 121499648 28700 4294967295 134512640 134672761 3221224560 3221223620 1075346629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28700 603 41 0 29622 0
vsize: 118652
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30046 0 0 0 48918 86 0 0 25 0 1 0 423182568 121499648 28700 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28700 603 41 0 29622 0
vsize: 118652
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30046 0 0 0 49918 86 0 0 25 0 1 0 423182568 121499648 28700 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28700 603 41 0 29622 0
vsize: 118652
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30046 0 0 0 50918 86 0 0 25 0 1 0 423182568 121499648 28700 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28700 603 41 0 29622 0
vsize: 118652
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30050 0 0 0 51918 86 0 0 25 0 1 0 423182568 121499648 28704 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28704 603 41 0 29622 0
vsize: 118652
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30050 0 0 0 52918 86 0 0 25 0 1 0 423182568 121499648 28704 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28704 603 41 0 29622 0
vsize: 118652
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30050 0 0 0 53918 86 0 0 25 0 1 0 423182568 121499648 28704 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28704 603 41 0 29622 0
vsize: 118652
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30050 0 0 0 54917 86 0 0 25 0 1 0 423182568 121499648 28704 4294967295 134512640 134672761 3221224560 3221223744 134558880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28704 603 41 0 29622 0
vsize: 118652
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30050 0 0 0 55917 86 0 0 25 0 1 0 423182568 121499648 28704 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28704 603 41 0 29622 0
vsize: 118652
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30050 0 0 0 56918 86 0 0 25 0 1 0 423182568 121499648 28704 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28704 603 41 0 29622 0
vsize: 118652
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30050 0 0 0 57918 86 0 0 25 0 1 0 423182568 121499648 28704 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 28704 603 41 0 29622 0
vsize: 118652
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 30320 0 0 0 58917 87 0 0 25 0 1 0 423182568 122576896 28974 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29926 28974 603 41 0 29885 0
vsize: 119704
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 31206 0 0 0 59914 90 0 0 25 0 1 0 423182568 126210048 29860 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30813 29860 603 41 0 30772 0
vsize: 123252
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 32000 0 0 0 60913 92 0 0 25 0 1 0 423182568 129568768 30654 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31633 30654 603 41 0 31592 0
vsize: 126532
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 32734 0 0 0 61912 93 0 0 25 0 1 0 423182568 132538368 31388 4294967295 134512640 134672761 3221224560 3221223664 134560207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32358 31388 603 41 0 32317 0
vsize: 129432
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 33723 0 0 0 62909 96 0 0 25 0 1 0 423182568 136572928 32377 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33343 32377 603 41 0 33302 0
vsize: 133372
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 34465 0 0 0 63907 98 0 0 25 0 1 0 423182568 139685888 33119 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34103 33119 603 41 0 34062 0
vsize: 136412
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 35156 0 0 0 64906 100 0 0 25 0 1 0 423182568 142520320 33810 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34795 33810 603 41 0 34754 0
vsize: 139180
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 35889 0 0 0 65904 102 0 0 25 0 1 0 423182568 145481728 34543 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35518 34543 603 41 0 35477 0
vsize: 142072
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 36690 0 0 0 66903 103 0 0 25 0 1 0 423182568 148709376 35344 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36306 35344 603 41 0 36265 0
vsize: 145224
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 37537 0 0 0 67901 106 0 0 25 0 1 0 423182568 152223744 36191 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37164 36191 603 41 0 37123 0
vsize: 148656
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 38239 0 0 0 68900 107 0 0 25 0 1 0 423182568 155222016 36893 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37896 36893 603 41 0 37855 0
vsize: 151584
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 38747 0 0 0 69898 108 0 0 25 0 1 0 423182568 157265920 37401 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38395 37401 603 41 0 38354 0
vsize: 153580
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 39299 0 0 0 70897 110 0 0 25 0 1 0 423182568 159551488 37953 4294967295 134512640 134672761 3221224560 3221223716 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38953 37953 603 41 0 38912 0
vsize: 155812
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 39895 0 0 0 71896 111 0 0 25 0 1 0 423182568 161984512 38549 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39547 38549 603 41 0 39506 0
vsize: 158188
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 40558 0 0 0 72894 113 0 0 25 0 1 0 423182568 164679680 39212 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40205 39212 603 41 0 40164 0
vsize: 160820
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 40958 0 0 0 73893 114 0 0 25 0 1 0 423182568 166301696 39612 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40601 39612 603 41 0 40560 0
vsize: 162404
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 41344 0 0 0 74892 115 0 0 25 0 1 0 423182568 167915520 39998 4294967295 134512640 134672761 3221224560 3221223664 134560474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40995 39999 603 41 0 40954 0
vsize: 163980
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 41907 0 0 0 75891 117 0 0 25 0 1 0 423182568 170213376 40561 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41556 40561 603 41 0 41515 0
vsize: 166224
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 42833 0 0 0 76888 120 0 0 25 0 1 0 423182568 174096384 41487 4294967295 134512640 134672761 3221224560 3221223748 1075346941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42504 41487 603 41 0 42463 0
vsize: 170016
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 43636 0 0 0 77887 122 0 0 25 0 1 0 423182568 177336320 42290 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43295 42290 603 41 0 43254 0
vsize: 173180
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 44385 0 0 0 78885 123 0 0 25 0 1 0 423182568 180436992 43039 4294967295 134512640 134672761 3221224560 3221223712 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44052 43039 603 41 0 44011 0
vsize: 176208
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 44918 0 0 0 79884 125 0 0 25 0 1 0 423182568 182591488 43572 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44578 43572 603 41 0 44537 0
vsize: 178312
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 45495 0 0 0 80883 126 0 0 25 0 1 0 423182568 184872960 44149 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45135 44149 603 41 0 45094 0
vsize: 180540
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46060 0 0 0 81882 127 0 0 25 0 1 0 423182568 187289600 44714 4294967295 134512640 134672761 3221224560 3221223744 134559411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45725 44714 603 41 0 45684 0
vsize: 182900
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 82881 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223664 134555222 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 83881 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+850.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 84882 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 85882 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 86882 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 87882 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 88882 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 89883 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 90883 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 91883 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 92883 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 93883 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 94883 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 95883 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 96883 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223616 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 97883 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 98883 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 99883 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 100884 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 101884 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 102884 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 103884 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223664 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 104884 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 105885 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 106885 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 107885 128 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 108884 129 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 109884 129 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 110884 129 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 111884 129 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 112885 129 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46257 0 0 0 113885 129 0 0 25 0 1 0 423182568 188096512 44911 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44911 603 41 0 45881 0
vsize: 183688
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46260 0 0 0 114885 129 0 0 25 0 1 0 423182568 188096512 44914 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44914 603 41 0 45881 0
vsize: 183688
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46264 0 0 0 115885 129 0 0 25 0 1 0 423182568 188096512 44918 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44918 603 41 0 45881 0
vsize: 183688
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46266 0 0 0 116885 129 0 0 25 0 1 0 423182568 188096512 44920 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45922 44920 603 41 0 45881 0
vsize: 183688
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46268 0 0 0 117886 129 0 0 25 0 1 0 423182568 188088320 44922 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45920 44922 603 41 0 45879 0
vsize: 183680
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46268 0 0 0 118886 129 0 0 25 0 1 0 423182568 188088320 44922 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45920 44922 603 41 0 45879 0
vsize: 183680
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29187
Raw data (stat): 29187 (minisat+) R 29186 24215 24214 0 -1 0 46268 0 0 0 119886 129 0 0 25 0 1 0 423182568 188088320 44922 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45920 44922 603 41 0 45879 0
vsize: 183680
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29187
Raw data (stat): 29187 (minisat+) Z 29186 24215 24214 0 -1 12 46271 0 0 0 119887 137 0 0 25 0 1 0 423182568 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.13
CPU time (s): 1200.25
CPU user time (s): 1198.87
CPU system time (s): 1.37579
CPU usage (%): 100.01
Max. virtual memory (Kb): 183688
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####