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/web/www.ps.uni-sb.de/~walser/benchmarks/ppp-problems/normalized-ppp:1-12,16.opb
MD5SUM	41edd2db35f2c8eb6d4b1f0a68a60338
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	10
Number of bits of the biggest number in a constraint	4
Biggest sum of numbers in a constraint	102
Number of bits of the biggest sum of numbers	7
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	6.63699
Number of variables	4662
Total number of constraints	36387
Number of constraints which are clauses	30696
Number of constraints which are cardinality constraints (but not clauses)	5613
Number of constraints which are nor clauses,nor cardinality constraints	78
Minimum length of a constraint	1
Maximum length of a constraint	29
Trace number 33799

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-05-27 16:49:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3257 boxname=wulflinc20 idbench=362 idsolver=8 numberseed=0
MD5SUM SOLVER: 4b637b3b6117f2add1a6288e91336322  /oldhome/oroussel/solvers/vallstSAT2005PB.sh
MD5SUM BENCH:  41edd2db35f2c8eb6d4b1f0a68a60338  /oldhome/oroussel/tmp/wulflinc20/normalized-ppp:1-12,16.opb
REAL COMMAND:  vallstSAT2005PB.sh /oldhome/oroussel/tmp/wulflinc20/normalized-ppp:1-12,16.opb 0
IDLAUNCH: 3257
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        723848 kB
Buffers:         34860 kB
Cached:         253412 kB
SwapCached:        728 kB
Active:          61628 kB
Inactive:       228764 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        723596 kB
SwapTotal:     2097892 kB
SwapFree:      2096304 kB
Dirty:            2076 kB
Writeback:           0 kB
Mapped:           5084 kB
Slab:            14692 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 16:53:06 (client local time) WITH STATUS 10 IN 226.022 SECONDS
stats: 3257 0 226.022 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
1:
seed: 0
Nr of vars set: 0  (#equs: 0)
Nr of vars set: 0  (#equs: 0)
#decisions: 14096054;  #end-nodes: 415763;
#proof improvement attempts: 0;  #restarts: 1531
Current batch, end-nodes: 252 / 462 (462)
#axs: 31899, #non-axs: 243
tight: meta-meta: start: 6, end: 9;  meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14;  meta: start: 30, end (keep): 50
result: model found (1)
seed: 0
Nr of vars set: 4388  (#equs: 0)
Time taken: 3 min, 44 sec
times:
0m0.019s 0m0.008s
3m15.334s 0m29.174s
v -v1 -v2 -v3 -v4 -v5 -v6 -v7 -v8 -v9  v10 -v11 -v12 -v13  v14 -v15 -v16 -v17 -v18 -v19 -v20 -v21 -v22 -v23 -v24 -v25 -v26 -v27 -v28 -v29 -v30 -v31 -v32 -v33 -v34 -v35 -v36 -v37 -v38 -v39 -v40 -v41 -v42 -v43  v44 -v45 -v46 -v47  v48 -v49 -v50 -v51 -v52 -v53 -v54 -v55 -v56 -v57 -v58 -v59 -v60 -v61  v62 -v63 -v64 -v65 -v66 -v67 -v68 -v69 -v70  v71 -v72 -v73 -v74 -v75 -v76 -v77 -v78 -v79 -v80 -v81 -v82 -v83 -v84  v85 -v86 -v87 -v88 -v89 -v90 -v91 -v92 -v93 -v94  v95 -v96 -v97 -v98 -v99 -v100 -v101 -v102 -v103 -v104 -v105 -v106 -v107 -v108 -v109 -v110 -v111 -v112 -v113 -v114 -v115  v116 -v117 -v118 -v119 -v120 -v121 -v122 -v123 -v124 -v125 -v126 -v127 -v128 -v129 -v130 -v131 -v132 -v133 -v134  v135 -v136 -v137 -v138 -v139 -v140 -v141 -v142 -v143 -v144 -v145 -v146 -v147 -v148 -v149 -v150 -v151 -v152 -v153 -v154 -v155 -v156 -v157 -v158 -v159 -v160 -v161  v162 -v163 -v164 -v165 -v166 -v167 -v168 -v169 -v170 -v171 -v172 -v173 -v174 -v175 -v176  v177 -v178 -v179 -v180 -v181 -v182 -v183 -v184 -v185 -v186 -v187 -v188 -v189 -v190 -v191 -v192 -v193 -v194 -v195 -v196 -v197 -v198 -v199 -v200 -v201  v202 -v203 -v204 -v205 -v206 -v207 -v208 -v209 -v210 -v211  v212 -v213 -v214 -v215 -v216 -v217 -v218 -v219 -v220 -v221 -v222 -v223 -v224 -v225  v226 -v227 -v228 -v229 -v230 -v231 -v232 -v233 -v234 -v235 -v236 -v237 -v238 -v239 -v240 -v241 -v242 -v243 -v244 -v245 -v246 -v247  v248 -v249 -v250 -v251 -v252 -v253 -v254 -v255 -v256 -v257 -v258 -v259 -v260 -v261 -v262  v263 -v264 -v265 -v266 -v267 -v268 -v269 -v270 -v271 -v272 -v273 -v274 -v275 -v276 -v277 -v278  v279 -v280 -v281 -v282 -v283 -v284 -v285 -v286 -v287 -v288 -v289 -v290 -v291 -v292 -v293  v294 -v295 -v296  v297 -v298 -v299 -v300 -v301 -v302 -v303 -v304 -v305 -v306 -v307 -v308 -v309 -v310 -v311 -v312 -v313 -v314 -v315 -v316 -v317 -v318 -v319 -v320 -v321 -v322 -v323 -v324  v325 -v326 -v327 -v328 -v329 -v330  v331 -v332 -v333 -v334 -v335 -v336 -v337 -v338 -v339 -v340 -v341 -v342 -v343 -v344 -v345 -v346 -v347 -v348 -v349 -v350 -v351 -v352 -v353 -v354 -v355 -v356  v357 -v358 -v359  v360 -v361 -v362 -v363 -v364 -v365 -v366 -v367 -v368 -v369 -v370 -v371 -v372  v373 -v374 -v375 -v376 -v377 -v378 -v379 -v380 -v381 -v382 -v383 -v384  v385 -v386 -v387 -v388 -v389 -v390 -v391  v392 -v393 -v394 -v395 -v396 -v397 -v398 -v399 -v400  v401 -v402 -v403 -v404 -v405 -v406 -v407 -v408 -v409 -v410 -v411 -v412  v413 -v414 -v415 -v416 -v417 -v418 -v419 -v420 -v421 -v422 -v423 -v424 -v425 -v426 -v427 -v428 -v429 -v430 -v431 -v432 -v433 -v434 -v435  v436 -v437 -v438 -v439 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 -v449 -v450 -v451  v452 -v453 -v454 -v455 -v456 -v457 -v458 -v459 -v460 -v461 -v462  v463 -v464 -v465 -v466 -v467 -v468 -v469 -v470 -v471 -v472 -v473 -v474  v475 -v476 -v477 -v478 -v479 -v480 -v481 -v482 -v483 -v484  v485 -v486 -v487 -v488 -v489 -v490 -v491 -v492 -v493 -v494 -v495 -v496 -v497 -v498 -v499 -v500 -v501 -v502 -v503 -v504 -v505 -v506 -v507 -v508 -v509 -v510 -v511 -v512  v513 -v514  v515 -v516 -v517 -v518 -v519 -v520 -v521 -v522 -v523 -v524 -v525 -v526  v527 -v528 -v529 -v530 -v531  v532 -v533 -v534 -v535 -v536 -v537 -v538 -v539  v540 -v541 -v542 -v543 -v544 -v545 -v546 -v547 -v548 -v549 -v550 -v551 -v552 -v553 -v554 -v555 -v556 -v557  v558 -v559 -v560 -v561 -v562 -v563 -v564 -v565 -v566 -v567  v568 -v569 -v570 -v571 -v572 -v573 -v574 -v575 -v576 -v577 -v578 -v579 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587  v588 -v589 -v590 -v591 -v592 -v593  v594 -v595 -v596 -v597 -v598 -v599 -v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 -v608 -v609 -v610 -v611 -v612 -v613 -v614 -v615 -v616 -v617 -v618 -v619 -v620 -v621 -v622 -v623 -v624  v625 -v626 -v627 -v628 -v629 -v630 -v631 -v632 -v633 -v634  v635 -v636 -v637  v638 -v639 -v640 -v641 -v642 -v643 -v644 -v645 -v646 -v647 -v648 -v649 -v650 -v651 -v652 -v653 -v654 -v655 -v656 -v657 -v658 -v659  v660 -v661 -v662 -v663 -v664 -v665  v666 -v667  v668 -v669 -v670 -v671 -v672 -v673 -v674 -v675 -v676 -v677 -v678 -v679 -v680 -v681 -v682 -v683 -v684 -v685 -v686 -v687 -v688 -v689 -v690 -v691 -v692 -v693  v694  v695 -v696 -v697 -v698 -v699 -v700 -v701 -v702 -v703 -v704 -v705 -v706 -v707 -v708 -v709 -v710 -v711 -v712 -v713 -v714  v715 -v716 -v717 -v718 -v719 -v720 -v721 -v722 -v723 -v724 -v725 -v726 -v727 -v728 -v729 -v730 -v731 -v732 -v733 -v734 -v735 -v736 -v737 -v738 -v739 -v740  v741 -v742 -v743 -v744 -v745 -v746 -v747 -v748 -v749  v750 -v751 -v752 -v753 -v754 -v755 -v756  v757 -v758 -v759 -v760 -v761 -v762 -v763 -v764  v765 -v766 -v767 -v768 -v769 -v770 -v771 -v772 -v773 -v774 -v775 -v776 -v777 -v778 -v779 -v780 -v781 -v782 -v783 -v784 -v785 -v786 -v787 -v788 -v789 -v790 -v791 -v792 -v793 -v794 -v795 -v796 -v797 -v798 -v799 -v800 -v801 -v802  v803 -v804 -v805  v806 -v807 -v808 -v809 -v810 -v811 -v812 -v813  v814 -v815 -v816  v817 -v818 -v819 -v820  v821 -v822 -v823 -v824 -v825 -v826 -v827 -v828 -v829 -v830 -v831 -v832 -v833 -v834 -v835 -v836 -v837 -v838 -v839 -v840 -v841 -v842 -v843 -v844 -v845 -v846 -v847 -v848 -v849 -v850 -v851 -v852 -v853 -v854 -v855 -v856 -v857 -v858  v859 -v860 -v861  v862 -v863 -v864 -v865 -v866 -v867 -v868 -v869 -v870 -v871  v872 -v873 -v874 -v875 -v876 -v877 -v878 -v879 -v880 -v881 -v882 -v883 -v884  v885 -v886 -v887 -v888 -v889 -v890 -v891  v892 -v893 -v894 -v895 -v896 -v897 -v898 -v899 -v900 -v901 -v902 -v903 -v904  v905 -v906 -v907 -v908 -v909  v910 -v911 -v912 -v913 -v914 -v915 -v916  v917 -v918 -v919 -v920 -v921 -v922 -v923 -v924 -v925 -v926 -v927 -v928 -v929 -v930 -v931 -v932 -v933 -v934 -v935 -v936 -v937 -v938 -v939 -v940 -v941 -v942 -v943 -v944  v945 -v946 -v947 -v948  v949 -v950 -v951 -v952 -v953 -v954 -v955 -v956  v957 -v958 -v959 -v960 -v961 -v962 -v963 -v964 -v965 -v966 -v967 -v968  v969 -v970 -v971 -v972 -v973 -v974 -v975 -v976 -v977 -v978 -v979 -v980 -v981 -v982 -v983 -v984 -v985 -v986 -v987 -v988 -v989 -v990 -v991 -v992 -v993  v994 -v995  v996 -v997 -v998 -v999 -v1000 -v1001 -v1002 -v1003 -v1004  v1005 -v1006 -v1007 -v1008 -v1009 -v1010 -v1011  v1012 -v1013 -v1014 -v1015 -v1016 -v1017 -v1018 -v1019 -v1020 -v1021 -v1022 -v1023 -v1024 -v1025 -v1026 -v1027 -v1028 -v1029 -v1030  v1031 -v1032 -v1033 -v1034 -v1035 -v1036 -v1037 -v1038 -v1039  v1040 -v1041 -v1042 -v1043  v1044  v1045 -v1046 -v1047 -v1048 -v1049 -v1050 -v1051 -v1052 -v1053 -v1054 -v1055 -v1056 -v1057 -v1058 -v1059 -v1060 -v1061 -v1062 -v1063 -v1064 -v1065 -v1066 -v1067 -v1068 -v1069 -v1070  v1071 -v1072 -v1073 -v1074 -v1075 -v1076 -v1077  v1078 -v1079 -v1080 -v1081 -v1082 -v1083 -v1084 -v1085 -v1086 -v1087 -v1088 -v1089 -v1090 -v1091 -v1092 -v1093 -v1094  v1095 -v1096 -v1097 -v1098 -v1099 -v1100 -v1101 -v1102 -v1103 -v1104 -v1105 -v1106 -v1107 -v1108 -v1109 -v1110 -v1111 -v1112 -v1113 -v1114 -v1115 -v1116  v1117 -v1118 -v1119 -v1120  v1121 -v1122 -v1123 -v1124 -v1125 -v1126 -v1127 -v1128 -v1129 -v1130 -v1131 -v1132 -v1133 -v1134  v1135 -v1136 -v1137 -v1138 -v1139 -v1140 -v1141 -v1142 -v1143  v1144 -v1145 -v1146 -v1147 -v1148 -v1149 -v1150 -v1151 -v1152 -v1153 -v1154 -v1155 -v1156 -v1157 -v1158 -v1159 -v1160 -v1161 -v1162 -v1163 -v1164 -v1165  v1166 -v1167 -v1168 -v1169 -v1170 -v1171 -v1172 -v1173 -v1174 -v1175 -v1176  v1177 -v1178 -v1179 -v1180 -v1181 -v1182 -v1183 -v1184 -v1185 -v1186 -v1187 -v1188 -v1189 -v1190  v1191 -v1192 -v1193 -v1194 -v1195 -v1196 -v1197 -v1198 -v1199 -v1200 -v1201 -v1202  v1203 -v1204 -v1205 -v1206 -v1207 -v1208 -v1209 -v1210 -v1211  v1212 -v1213 -v1214 -v1215 -v1216 -v1217 -v1218 -v1219 -v1220 -v1221 -v1222 -v1223 -v1224 -v1225 -v1226 -v1227 -v1228 -v1229 -v1230 -v1231  v1232 -v1233 -v1234 -v1235 -v1236 -v1237 -v1238  v1239 -v1240 -v1241 -v1242 -v1243 -v1244 -v1245 -v1246  v1247 -v1248 -v1249 -v1250  v1251 -v1252 -v1253 -v1254 -v1255 -v1256 -v1257 -v1258 -v1259 -v1260 -v1261 -v1262 -v1263 -v1264 -v1265 -v1266 -v1267 -v1268 -v1269 -v1270 -v1271 -v1272 -v1273 -v1274 -v1275 -v1276 -v1277 -v1278 -v1279 -v1280 -v1281  v1282 -v1283 -v1284 -v1285 -v1286 -v1287 -v1288 -v1289 -v1290 -v1291 -v1292 -v1293 -v1294 -v1295  v1296 -v1297 -v1298 -v1299 -v1300 -v1301  v1302 -v1303 -v1304 -v1305 -v1306 -v1307 -v1308 -v1309 -v1310 -v1311 -v1312 -v1313 -v1314  v1315  v1316 -v1317 -v1318 -v1319 -v1320 -v1321 -v1322 -v1323 -v1324 -v1325 -v1326 -v1327 -v1328 -v1329 -v1330 -v1331 -v1332 -v1333 -v1334  v1335 -v1336 -v1337 -v1338 -v1339 -v1340 -v1341 -v1342 -v1343 -v1344 -v1345  v1346 -v1347 -v1348 -v1349 -v1350 -v1351 -v1352 -v1353 -v1354 -v1355 -v1356 -v1357 -v1358 -v1359 -v1360 -v1361 -v1362 -v1363 -v1364 -v1365 -v1366 -v1367 -v1368 -v1369  v1370  v1371 -v1372 -v1373 -v1374 -v1375  v1376 -v1377 -v1378 -v1379 -v1380 -v1381 -v1382 -v1383 -v1384 -v1385 -v1386 -v1387 -v1388  v1389 -v1390 -v1391 -v1392 -v1393 -v1394 -v1395 -v1396 -v1397 -v1398 -v1399 -v1400 -v1401 -v1402 -v1403 -v1404 -v1405 -v1406 -v1407 -v1408  v1409 -v1410 -v1411 -v1412 -v1413 -v1414 -v1415 -v1416 -v1417 -v1418 -v1419 -v1420 -v1421  v1422 -v1423 -v1424 -v1425 -v1426 -v1427 -v1428 -v1429 -v1430 -v1431 -v1432 -v1433 -v1434 -v1435 -v1436 -v1437 -v1438 -v1439 -v1440  v1441 -v1442 -v1443 -v1444 -v1445 -v1446 -v1447  v1448 -v1449 -v1450 -v1451  v1452 -v1453 -v1454 -v1455 -v1456 -v1457 -v1458 -v1459 -v1460 -v1461 -v1462  v1463 -v1464 -v1465 -v1466 -v1467 -v1468 -v1469 -v1470 -v1471 -v1472 -v1473 -v1474 -v1475 -v1476 -v1477  v1478 -v1479 -v1480 -v1481 -v1482 -v1483 -v1484 -v1485 -v1486  v1487 -v1488 -v1489 -v1490 -v1491 -v1492 -v1493 -v1494 -v1495 -v1496 -v1497 -v1498 -v1499 -v1500  v1501 -v1502  v1503 -v1504 -v1505 -v1506 -v1507 -v1508 -v1509 -v1510 -v1511 -v1512 -v1513 -v1514 -v1515 -v1516 -v1517 -v1518 -v1519 -v1520 -v1521 -v1522  v1523 -v1524 -v1525 -v1526 -v1527 -v1528 -v1529 -v1530 -v1531 -v1532 -v1533 -v1534 -v1535 -v1536 -v1537 -v1538 -v1539 -v1540  v1541 -v1542 -v1543 -v1544 -v1545  v1546  v1547 -v1548 -v1549 -v1550 -v1551 -v1552 -v1553 -v1554 -v1555 -v1556 -v1557 -v1558 -v1559 -v1560 -v1561 -v1562 -v1563 -v1564 -v1565 -v1566 -v1567 -v1568 -v1569 -v1570 -v1571 -v1572  v1573 -v1574 -v1575 -v1576 -v1577 -v1578 -v1579 -v1580 -v1581  v1582 -v1583 -v1584 -v1585 -v1586 -v1587 -v1588 -v1589  v1590 -v1591 -v1592 -v1593 -v1594 -v1595 -v1596 -v1597 -v1598 -v1599 -v1600 -v1601 -v1602 -v1603 -v1604 -v1605 -v1606  v1607 -v1608 -v1609 -v1610 -v1611 -v1612 -v1613 -v1614 -v1615 -v1616 -v1617 -v1618 -v1619 -v1620 -v1621 -v1622  v1623 -v1624 -v1625 -v1626 -v1627  v1628 -v1629 -v1630 -v1631 -v1632 -v1633 -v1634 -v1635 -v1636 -v1637 -v1638 -v1639 -v1640 -v1641  v1642 -v1643 -v1644 -v1645 -v1646 -v1647 -v1648 -v1649 -v1650 -v1651 -v1652 -v1653 -v1654 -v1655 -v1656 -v1657 -v1658  v1659 -v1660 -v1661 -v1662 -v1663 -v1664 -v1665 -v1666 -v1667 -v1668 -v1669 -v1670 -v1671  v1672 -v1673  v1674 -v1675 -v1676 -v1677 -v1678 -v1679 -v1680 -v1681 -v1682 -v1683 -v1684  v1685 -v1686 -v1687 -v1688 -v1689 -v1690 -v1691 -v1692 -v1693 -v1694  v1695 -v1696 -v1697 -v1698 -v1699 -v1700 -v1701 -v1702 -v1703 -v1704  v1705 -v1706 -v1707 -v1708 -v1709 -v1710 -v1711 -v1712 -v1713 -v1714 -v1715  v1716 -v1717 -v1718 -v1719 -v1720 -v1721  v1722 -v1723 -v1724 -v1725  v1726 -v1727 -v1728 -v1729 -v1730 -v1731 -v1732 -v1733 -v1734 -v1735 -v1736 -v1737 -v1738 -v1739 -v1740 -v1741 -v1742 -v1743 -v1744 -v1745 -v1746 -v1747 -v1748 -v1749 -v1750 -v1751 -v1752  v1753 -v1754 -v1755 -v1756 -v1757 -v1758 -v1759  v1760 -v1761 -v1762 -v1763 -v1764 -v1765 -v1766 -v1767 -v1768 -v1769 -v1770  v1771  v1772 -v1773 -v1774 -v1775 -v1776 -v1777 -v1778 -v1779 -v1780 -v1781 -v1782 -v1783 -v1784 -v1785 -v1786 -v1787 -v1788 -v1789  v1790 -v1791 -v1792 -v1793 -v1794  v1795 -v1796 -v1797 -v1798 -v1799 -v1800 -v1801 -v1802 -v1803 -v1804 -v1805 -v1806 -v1807 -v1808 -v1809  v1810 -v1811 -v1812 -v1813 -v1814 -v1815 -v1816 -v1817 -v1818 -v1819 -v1820  v1821 -v1822 -v1823 -v1824 -v1825 -v1826 -v1827 -v1828 -v1829 -v1830 -v1831 -v1832 -v1833  v1834 -v1835 -v1836 -v1837 -v1838 -v1839 -v1840  v1841  v1842 -v1843 -v1844 -v1845 -v1846 -v1847 -v1848 -v1849 -v1850 -v1851  v1852 -v1853 -v1854 -v1855 -v1856 -v1857 -v1858 -v1859 -v1860 -v1861 -v1862 -v1863 -v1864 -v1865 -v1866 -v1867 -v1868 -v1869 -v1870 -v1871  v1872 -v1873 -v1874 -v1875 -v1876 -v1877 -v1878 -v1879  v1880 -v1881 -v1882  v1883 -v1884  v1885 -v1886 -v1887 -v1888 -v1889 -v1890 -v1891 -v1892 -v1893 -v1894 -v1895 -v1896 -v1897 -v1898 -v1899 -v1900 -v1901 -v1902 -v1903 -v1904 -v1905 -v1906 -v1907 -v1908  v1909 -v1910 -v1911 -v1912 -v1913 -v1914 -v1915 -v1916 -v1917 -v1918 -v1919 -v1920 -v1921 -v1922 -v1923 -v1924  v1925 -v1926 -v1927 -v1928 -v1929 -v1930 -v1931 -v1932 -v1933 -v1934 -v1935 -v1936 -v1937 -v1938  v1939 -v1940 -v1941 -v1942 -v1943 -v1944 -v1945 -v1946 -v1947 -v1948 -v1949 -v1950 -v1951 -v1952 -v1953 -v1954  v1955 -v1956 -v1957 -v1958 -v1959 -v1960 -v1961 -v1962 -v1963 -v1964 -v1965 -v1966 -v1967 -v1968 -v1969 -v1970 -v1971 -v1972 -v1973 -v1974 -v1975 -v1976 -v1977 -v1978 -v1979  v1980 -v1981 -v1982 -v1983 -v1984 -v1985 -v1986 -v1987 -v1988 -v1989 -v1990  v1991 -v1992 -v1993 -v1994 -v1995  v1996 -v1997 -v1998 -v1999 -v2000  v2001 -v2002 -v2003 -v2004 -v2005 -v2006 -v2007 -v2008 -v2009 -v2010 -v2011 -v2012 -v2013 -v2014 -v2015 -v2016 -v2017 -v2018 -v2019 -v2020 -v2021 -v2022 -v2023 -v2024 -v2025 -v2026 -v2027 -v2028 -v2029 -v2030 -v2031 -v2032 -v2033 -v2034 -v2035 -v2036 -v2037 -v2038 -v2039 -v2040 -v2041 -v2042 -v2043 -v2044  v2045 -v2046 -v2047 -v2048 -v2049  v2050 -v2051 -v2052 -v2053 -v2054 -v2055 -v2056 -v2057 -v2058 -v2059 -v2060 -v2061 -v2062 -v2063 -v2064 -v2065 -v2066 -v2067 -v2068 -v2069 -v2070 -v2071  v2072 -v2073 -v2074 -v2075 -v2076 -v2077 -v2078 -v2079 -v2080 -v2081 -v2082 -v2083 -v2084 -v2085 -v2086 -v2087  v2088 -v2089 -v2090 -v2091 -v2092 -v2093 -v2094 -v2095 -v2096 -v2097 -v2098 -v2099 -v2100  v2101 -v2102 -v2103 -v2104 -v2105 -v2106 -v2107 -v2108 -v2109 -v2110 -v2111 -v2112 -v2113 -v2114 -v2115 -v2116 -v2117 -v2118 -v2119 -v2120 -v2121 -v2122  v2123 -v2124 -v2125 -v2126 -v2127 -v2128 -v2129 -v2130 -v2131 -v2132  v2133 -v2134 -v2135 -v2136  v2137 -v2138 -v2139 -v2140 -v2141 -v2142 -v2143 -v2144 -v2145 -v2146 -v2147 -v2148 -v2149 -v2150 -v2151 -v2152  v2153 -v2154 -v2155 -v2156 -v2157 -v2158 -v2159 -v2160 -v2161 -v2162 -v2163 -v2164 -v2165  v2166 -v2167 -v2168 -v2169 -v2170 -v2171 -v2172 -v2173 -v2174 -v2175 -v2176 -v2177 -v2178 -v2179 -v2180 -v2181 -v2182 -v2183 -v2184 -v2185 -v2186 -v2187 -v2188 -v2189 -v2190 -v2191 -v2192 -v2193 -v2194  v2195 -v2196 -v2197 -v2198 -v2199 -v2200 -v2201 -v2202 -v2203 -v2204 -v2205 -v2206 -v2207 -v2208 -v2209  v2210 -v2211 -v2212 -v2213 -v2214 -v2215 -v2216 -v2217 -v2218 -v2219 -v2220 -v2221 -v2222 -v2223 -v2224 -v2225 -v2226 -v2227  v2228 -v2229 -v2230 -v2231 -v2232  v2233 -v2234 -v2235 -v2236 -v2237 -v2238 -v2239 -v2240 -v2241  v2242 -v2243 -v2244 -v2245 -v2246  v2247 -v2248 -v2249 -v2250  v2251 -v2252 -v2253 -v2254 -v2255 -v2256 -v2257 -v2258 -v2259 -v2260  v2261 -v2262 -v2263 -v2264 -v2265 -v2266  v2267 -v2268 -v2269 -v2270 -v2271 -v2272 -v2273  v2274 -v2275 -v2276 -v2277 -v2278  v2279 -v2280 -v2281 -v2282  v2283 -v2284 -v2285 -v2286 -v2287 -v2288 -v2289 -v2290 -v2291  v2292 -v2293 -v2294  v2295 -v2296 -v2297 -v2298 -v2299  v2300 -v2301 -v2302 -v2303 -v2304 -v2305 -v2306 -v2307  v2308 -v2309 -v2310 -v2311 -v2312  v2313 -v2314 -v2315 -v2316  v2317 -v2318 -v2319 -v2320 -v2321 -v2322 -v2323 -v2324  v2325 -v2326 -v2327 -v2328 -v2329 -v2330 -v2331  v2332 -v2333 -v2334 -v2335 -v2336 -v2337 -v2338  v2339 -v2340 -v2341 -v2342 -v2343 -v2344 -v2345  v2346 -v2347 -v2348 -v2349  v2350 -v2351 -v2352 -v2353 -v2354  v2355 -v2356 -v2357 -v2358 -v2359  v2360 -v2361 -v2362 -v2363 -v2364 -v2365 -v2366 -v2367  v2368 -v2369 -v2370 -v2371 -v2372  v2373 -v2374 -v2375 -v2376 -v2377 -v2378  v2379 -v2380 -v2381 -v2382  v2383 -v2384 -v2385 -v2386 -v2387 -v2388 -v2389  v2390 -v2391 -v2392 -v2393 -v2394 -v2395 -v2396 -v2397 -v2398 -v2399  v2400 -v2401  v2402 -v2403 -v2404 -v2405 -v2406 -v2407 -v2408 -v2409 -v2410 -v2411  v2412 -v2413  v2414 -v2415 -v2416 -v2417 -v2418  v2419 -v2420 -v2421 -v2422 -v2423 -v2424  v2425 -v2426 -v2427 -v2428 -v2429 -v2430 -v2431 -v2432  v2433 -v2434 -v2435 -v2436 -v2437 -v2438  v2439 -v2440 -v2441 -v2442 -v2443 -v2444  v2445 -v2446 -v2447 -v2448 -v2449 -v2450  v2451 -v2452 -v2453 -v2454 -v2455 -v2456 -v2457 -v2458  v2459 -v2460 -v2461 -v2462 -v2463  v2464 -v2465 -v2466 -v2467  v2468 -v2469 -v2470 -v2471 -v2472 -v2473 -v2474 -v2475 -v2476 -v2477  v2478 -v2479  v2480 -v2481 -v2482 -v2483 -v2484 -v2485 -v2486 -v2487 -v2488  v2489 -v2490 -v2491 -v2492  v2493 -v2494 -v2495 -v2496  v2497 -v2498 -v2499 -v2500 -v2501 -v2502 -v2503 -v2504 -v2505 -v2506  v2507 -v2508 -v2509 -v2510 -v2511 -v2512  v2513 -v2514 -v2515 -v2516 -v2517  v2518 -v2519 -v2520 -v2521  v2522 -v2523 -v2524 -v2525 -v2526 -v2527 -v2528 -v2529 -v2530  v2531 -v2532 -v2533 -v2534 -v2535 -v2536  v2537 -v2538 -v2539 -v2540 -v2541 -v2542  v2543 -v2544  v2545 -v2546 -v2547 -v2548 -v2549 -v2550 -v2551 -v2552 -v2553  v2554 -v2555 -v2556 -v2557 -v2558 -v2559 -v2560 -v2561  v2562 -v2563 -v2564  v2565 -v2566 -v2567 -v2568 -v2569 -v2570  v2571 -v2572 -v2573 -v2574  v2575 -v2576 -v2577 -v2578 -v2579 -v2580 -v2581 -v2582  v2583 -v2584 -v2585 -v2586 -v2587 -v2588 -v2589 -v2590 -v2591  v2592 -v2593 -v2594 -v2595 -v2596  v2597 -v2598 -v2599  v2600 -v2601 -v2602 -v2603 -v2604 -v2605 -v2606 -v2607  v2608 -v2609 -v2610 -v2611  v2612 -v2613 -v2614 -v2615 -v2616 -v2617 -v2618 -v2619 -v2620  v2621 -v2622 -v2623 -v2624 -v2625  v2626 -v2627 -v2628  v2629 -v2630 -v2631 -v2632 -v2633 -v2634 -v2635 -v2636 -v2637  v2638 -v2639 -v2640 -v2641  v2642 -v2643 -v2644 -v2645 -v2646 -v2647  v2648 -v2649 -v2650 -v2651 -v2652 -v2653 -v2654 -v2655 -v2656 -v2657  v2658 -v2659 -v2660 -v2661 -v2662  v2663 -v2664 -v2665 -v2666 -v2667 -v2668  v2669 -v2670 -v2671 -v2672 -v2673  v2674 -v2675 -v2676 -v2677 -v2678 -v2679  v2680 -v2681 -v2682 -v2683 -v2684 -v2685  v2686 -v2687 -v2688 -v2689 -v2690  v2691 -v2692 -v2693 -v2694 -v2695 -v2696  v2697 -v2698 -v2699 -v2700  v2701 -v2702 -v2703 -v2704 -v2705 -v2706 -v2707 -v2708 -v2709  v2710 -v2711 -v2712  v2713 -v2714 -v2715 -v2716 -v2717 -v2718 -v2719 -v2720 -v2721 -v2722  v2723 -v2724  v2725 -v2726 -v2727 -v2728 -v2729 -v2730  v2731 -v2732 -v2733 -v2734 -v2735 -v2736 -v2737 -v2738 -v2739  v2740 -v2741 -v2742 -v2743 -v2744  v2745 -v2746 -v2747 -v2748 -v2749 -v2750 -v2751 -v2752 -v2753  v2754 -v2755 -v2756  v2757 -v2758 -v2759 -v2760  v2761 -v2762 -v2763 -v2764 -v2765 -v2766 -v2767 -v2768  v2769 -v2770 -v2771 -v2772  v2773 -v2774 -v2775 -v2776 -v2777 -v2778 -v2779 -v2780 -v2781 -v2782  v2783 -v2784 -v2785  v2786 -v2787 -v2788 -v2789 -v2790 -v2791 -v2792 -v2793 -v2794  v2795 -v2796 -v2797  v2798 -v2799 -v2800 -v2801 -v2802 -v2803 -v2804 -v2805  v2806 -v2807 -v2808  v2809 -v2810 -v2811 -v2812 -v2813 -v2814 -v2815 -v2816 -v2817 -v2818 -v2819  v2820 -v2821 -v2822  v2823 -v2824 -v2825 -v2826 -v2827 -v2828 -v2829 -v2830  v2831 -v2832  v2833 -v2834 -v2835 -v2836 -v2837 -v2838 -v2839 -v2840 -v2841 -v2842  v2843 -v2844 -v2845 -v2846 -v2847 -v2848  v2849 -v2850 -v2851 -v2852  v2853 -v2854 -v2855 -v2856 -v2857 -v2858 -v2859 -v2860  v2861 -v2862 -v2863 -v2864 -v2865 -v2866 -v2867  v2868 -v2869 -v2870 -v2871 -v2872 -v2873  v2874 -v2875 -v2876 -v2877  v2878 -v2879 -v2880 -v2881 -v2882 -v2883 -v2884  v2885 -v2886 -v2887 -v2888 -v2889 -v2890 -v2891  v2892 -v2893 -v2894 -v2895 -v2896  v2897 -v2898 -v2899  v2900 -v2901 -v2902 -v2903 -v2904 -v2905 -v2906 -v2907  v2908 -v2909 -v2910  v2911 -v2912 -v2913 -v2914 -v2915 -v2916 -v2917 -v2918 -v2919  v2920 -v2921 -v2922 -v2923 -v2924 -v2925  v2926 -v2927 -v2928 -v2929  v2930 -v2931 -v2932 -v2933 -v2934 -v2935  v2936 -v2937 -v2938 -v2939 -v2940 -v2941 -v2942 -v2943  v2944 -v2945 -v2946  v2947 -v2948 -v2949 -v2950 -v2951 -v2952  v2953 -v2954 -v2955 -v2956 -v2957 -v2958 -v2959 -v2960 -v2961  v2962 -v2963 -v2964 -v2965 -v2966 -v2967 -v2968 -v2969  v2970  v2971 -v2972 -v2973 -v2974 -v2975 -v2976 -v2977 -v2978 -v2979 -v2980 -v2981  v2982 -v2983 -v2984 -v2985 -v2986  v2987 -v2988 -v2989 -v2990 -v2991 -v2992 -v2993  v2994  v2995 -v2996 -v2997 -v2998 -v2999 -v3000 -v3001 -v3002 -v3003  v3004 -v3005 -v3006 -v3007  v3008 -v3009 -v3010 -v3011 -v3012  v3013 -v3014 -v3015 -v3016 -v3017 -v3018 -v3019 -v3020 -v3021 -v3022 -v3023  v3024 -v3025 -v3026 -v3027 -v3028  v3029 -v3030  v3031 -v3032 -v3033 -v3034 -v3035 -v3036 -v3037  v3038 -v3039 -v3040 -v3041 -v3042  v3043 -v3044 -v3045 -v3046 -v3047 -v3048 -v3049 -v3050  v3051 -v3052 -v3053 -v3054 -v3055  v3056 -v3057 -v3058 -v3059 -v3060 -v3061 -v3062 -v3063  v3064 -v3065 -v3066 -v3067 -v3068 -v3069 -v3070 -v3071  v3072 -v3073  v3074 -v3075 -v3076 -v3077 -v3078 -v3079 -v3080  v3081 -v3082 -v3083 -v3084 -v3085 -v3086 -v3087 -v3088  v3089 -v3090 -v3091 -v3092 -v3093 -v3094  v3095 -v3096 -v3097 -v3098  v3099 -v3100 -v3101 -v3102 -v3103 -v3104 -v3105 -v3106 -v3107  v3108 -v3109 -v3110 -v3111  v3112 -v3113 -v3114 -v3115  v3116 -v3117 -v3118 -v3119 -v3120 -v3121 -v3122 -v3123  v3124 -v3125 -v3126 -v3127 -v3128 -v3129 -v3130  v3131 -v3132 -v3133 -v3134 -v3135 -v3136  v3137 -v3138 -v3139 -v3140 -v3141 -v3142  v3143 -v3144 -v3145 -v3146 -v3147  v3148 -v3149 -v3150 -v3151 -v3152  v3153 -v3154 -v3155 -v3156 -v3157  v3158 -v3159 -v3160 -v3161 -v3162 -v3163 -v3164 -v3165 -v3166  v3167 -v3168 -v3169 -v3170 -v3171 -v3172 -v3173  v3174 -v3175 -v3176 -v3177  v3178 -v3179 -v3180 -v3181 -v3182 -v3183 -v3184 -v3185  v3186 -v3187  v3188 -v3189 -v3190 -v3191 -v3192 -v3193 -v3194 -v3195  v3196 -v3197 -v3198 -v3199 -v3200 -v3201 -v3202  v3203 -v3204  v3205 -v3206 -v3207 -v3208 -v3209 -v3210  v3211 -v3212 -v3213 -v3214 -v3215 -v3216  v3217 -v3218 -v3219 -v3220 -v3221 -v3222  v3223 -v3224 -v3225 -v3226 -v3227 -v3228 -v3229 -v3230 -v3231 -v3232 -v3233  v3234 -v3235 -v3236 -v3237  v3238 -v3239 -v3240 -v3241  v3242 -v3243 -v3244 -v3245 -v3246 -v3247 -v3248 -v3249 -v3250 -v3251  v3252 -v3253 -v3254 -v3255 -v3256 -v3257  v3258 -v3259 -v3260  v3261 -v3262 -v3263 -v3264 -v3265  v3266 -v3267 -v3268 -v3269 -v3270 -v3271  v3272 -v3273 -v3274 -v3275 -v3276 -v3277 -v3278 -v3279  v3280 -v3281 -v3282 -v3283  v3284 -v3285 -v3286 -v3287 -v3288 -v3289 -v3290 -v3291 -v3292 -v3293  v3294 -v3295 -v3296 -v3297 -v3298 -v3299  v3300 -v3301  v3302 -v3303 -v3304 -v3305 -v3306  v3307 -v3308 -v3309 -v3310 -v3311 -v3312 -v3313  v3314 -v3315 -v3316 -v3317 -v3318 -v3319  v3320 -v3321 -v3322 -v3323 -v3324 -v3325 -v3326 -v3327  v3328 -v3329 -v3330 -v3331 -v3332 -v3333 -v3334 -v3335  v3336 -v3337 -v3338 -v3339 -v3340 -v3341  v3342 -v3343  v3344 -v3345 -v3346 -v3347 -v3348 -v3349 -v3350 -v3351 -v3352  v3353 -v3354 -v3355 -v3356 -v3357 -v3358  v3359 -v3360 -v3361  v3362 -v3363 -v3364 -v3365 -v3366 -v3367 -v3368 -v3369  v3370 -v3371 -v3372 -v3373  v3374 -v3375 -v3376 -v3377 -v3378 -v3379  v3380 -v3381 -v3382 -v3383 -v3384 -v3385 -v3386  v3387 -v3388 -v3389 -v3390 -v3391 -v3392 -v3393  v3394 -v3395 -v3396 -v3397 -v3398 -v3399 -v3400  v3401 -v3402 -v3403 -v3404 -v3405 -v3406 -v3407  v3408 -v3409 -v3410 -v3411  v3412 -v3413 -v3414 -v3415 -v3416  v3417 -v3418 -v3419 -v3420 -v3421 -v3422 -v3423 -v3424 -v3425  v3426 -v3427 -v3428 -v3429  v3430 -v3431 -v3432 -v3433 -v3434 -v3435  v3436 -v3437 -v3438  v3439 -v3440 -v3441 -v3442 -v3443 -v3444 -v3445 -v3446 -v3447 -v3448  v3449 -v3450 -v3451 -v3452  v3453 -v3454 -v3455 -v3456 -v3457 -v3458 -v3459 -v3460 -v3461  v3462 -v3463  v3464 -v3465 -v3466 -v3467 -v3468 -v3469 -v3470 -v3471 -v3472  v3473 -v3474 -v3475 -v3476 -v3477  v3478 -v3479 -v3480  v3481 -v3482 -v3483 -v3484 -v3485 -v3486 -v3487 -v3488 -v3489 -v3490 -v3491  v3492 -v3493 -v3494 -v3495 -v3496 -v3497  v3498 -v3499 -v3500 -v3501 -v3502 -v3503  v3504 -v3505 -v3506 -v3507  v3508 -v3509 -v3510 -v3511 -v3512  v3513 -v3514 -v3515 -v3516 -v3517 -v3518 -v3519  v3520 -v3521 -v3522 -v3523 -v3524 -v3525 -v3526  v3527 -v3528 -v3529 -v3530  v3531 -v3532 -v3533 -v3534  v3535 -v3536 -v3537 -v3538 -v3539 -v3540 -v3541 -v3542  v3543 -v3544 -v3545 -v3546  v3547 -v3548 -v3549 -v3550 -v3551 -v3552 -v3553 -v3554  v3555 -v3556 -v3557 -v3558 -v3559  v3560 -v3561 -v3562 -v3563 -v3564 -v3565  v3566 -v3567 -v3568 -v3569 -v3570 -v3571  v3572 -v3573 -v3574 -v3575 -v3576 -v3577 -v3578 -v3579 -v3580  v3581 -v3582 -v3583 -v3584 -v3585  v3586 -v3587 -v3588  v3589 -v3590 -v3591 -v3592 -v3593 -v3594 -v3595 -v3596 -v3597 -v3598  v3599 -v3600 -v3601 -v3602  v3603 -v3604 -v3605 -v3606 -v3607 -v3608 -v3609 -v3610 -v3611  v3612 -v3613 -v3614 -v3615  v3616 -v3617 -v3618  v3619 -v3620 -v3621 -v3622 -v3623 -v3624 -v3625 -v3626 -v3627 -v3628 -v3629  v3630  v3631 -v3632 -v3633 -v3634 -v3635 -v3636 -v3637 -v3638 -v3639 -v3640  v3641 -v3642 -v3643 -v3644 -v3645  v3646 -v3647 -v3648 -v3649 -v3650 -v3651  v3652 -v3653 -v3654 -v3655  v3656 -v3657 -v3658 -v3659 -v3660 -v3661 -v3662  v3663 -v3664 -v3665 -v3666  v3667 -v3668 -v3669 -v3670 -v3671 -v3672 -v3673  v3674 -v3675 -v3676 -v3677 -v3678 -v3679 -v3680 -v3681  v3682 -v3683 -v3684 -v3685 -v3686 -v3687 -v3688  v3689 -v3690 -v3691  v3692 -v3693 -v3694 -v3695 -v3696 -v3697 -v3698 -v3699  v3700 -v3701 -v3702 -v3703  v3704 -v3705 -v3706 -v3707 -v3708 -v3709 -v3710 -v3711 -v3712 -v3713  v3714 -v3715 -v3716 -v3717 -v3718 -v3719  v3720 -v3721 -v3722  v3723 -v3724 -v3725 -v3726 -v3727 -v3728 -v3729  v3730 -v3731 -v3732 -v3733  v3734 -v3735 -v3736 -v3737 -v3738  v3739 -v3740 -v3741 -v3742 -v3743 -v3744 -v3745 -v3746 -v3747 -v3748  v3749 -v3750 -v3751  v3752 -v3753 -v3754 -v3755 -v3756 -v3757 -v3758 -v3759  v3760 -v3761 -v3762 -v3763 -v3764  v3765 -v3766 -v3767 -v3768  v3769 -v3770 -v3771 -v3772 -v3773 -v3774 -v3775 -v3776 -v3777 -v3778 -v3779  v3780 -v3781 -v3782 -v3783 -v3784  v3785 -v3786  v3787 -v3788 -v3789 -v3790 -v3791 -v3792 -v3793 -v3794  v3795 -v3796 -v3797 -v3798  v3799 -v3800 -v3801 -v3802 -v3803 -v3804 -v3805 -v3806 -v3807 -v3808 -v3809  v3810  v3811 -v3812 -v3813 -v3814 -v3815 -v3816  v3817 -v3818 -v3819 -v3820 -v3821 -v3822 -v3823 -v3824 -v3825  v3826 -v3827 -v3828 -v3829  v3830 -v3831 -v3832 -v3833 -v3834 -v3835 -v3836 -v3837 -v3838  v3839 -v3840 -v3841 -v3842 -v3843 -v3844  v3845 -v3846 -v3847 -v3848 -v3849  v3850 -v3851 -v3852 -v3853  v3854 -v3855 -v3856 -v3857 -v3858 -v3859 -v3860  v3861 -v3862 -v3863 -v3864 -v3865 -v3866  v3867 -v3868 -v3869 -v3870 -v3871 -v3872 -v3873  v3874 -v3875 -v3876 -v3877  v3878 -v3879 -v3880 -v3881 -v3882 -v3883 -v3884 -v3885 -v3886  v3887 -v3888 -v3889 -v3890 -v3891 -v3892 -v3893  v3894 -v3895 -v3896 -v3897 -v3898 -v3899  v3900 -v3901 -v3902 -v3903 -v3904  v3905 -v3906 -v3907 -v3908 -v3909  v3910 -v3911 -v3912 -v3913 -v3914  v3915 -v3916 -v3917 -v3918 -v3919  v3920 -v3921 -v3922 -v3923 -v3924 -v3925 -v3926 -v3927 -v3928 -v3929  v3930  v3931 -v3932 -v3933 -v3934 -v3935 -v3936 -v3937 -v3938 -v3939  v3940 -v3941 -v3942 -v3943  v3944 -v3945 -v3946 -v3947 -v3948 -v3949 -v3950 -v3951 -v3952 -v3953  v3954 -v3955 -v3956 -v3957 -v3958 -v3959  v3960 -v3961 -v3962 -v3963 -v3964 -v3965  v3966  v3967 -v3968 -v3969 -v3970 -v3971 -v3972 -v3973 -v3974  v3975 -v3976 -v3977 -v3978  v3979 -v3980 -v3981 -v3982 -v3983 -v3984  v3985 -v3986 -v3987 -v3988 -v3989 -v3990 -v3991 -v3992 -v3993 -v3994 -v3995  v3996 -v3997 -v3998 -v3999  v4000 -v4001 -v4002 -v4003  v4004 -v4005 -v4006 -v4007 -v4008 -v4009 -v4010 -v4011 -v4012  v4013 -v4014 -v4015  v4016 -v4017 -v4018 -v4019 -v4020 -v4021  v4022 -v4023 -v4024 -v4025 -v4026 -v4027  v4028 -v4029 -v4030 -v4031 -v4032 -v4033 -v4034 -v4035 -v4036 -v4037  v4038 -v4039 -v4040 -v4041 -v4042  v4043 -v4044 -v4045 -v4046  v4047 -v4048 -v4049 -v4050 -v4051 -v4052  v4053 -v4054 -v4055 -v4056 -v4057 -v4058  v4059 -v4060 -v4061 -v4062 -v4063 -v4064 -v4065 -v4066 -v4067  v4068 -v4069 -v4070 -v4071  v4072 -v4073 -v4074 -v4075 -v4076 -v4077 -v4078 -v4079  v4080 -v4081 -v4082 -v4083 -v4084 -v4085  v4086 -v4087 -v4088 -v4089 -v4090  v4091 -v4092 -v4093 -v4094  v4095 -v4096 -v4097 -v4098 -v4099 -v4100  v4101 -v4102 -v4103 -v4104 -v4105 -v4106 -v4107  v4108 -v4109 -v4110 -v4111 -v4112 -v4113 -v4114  v4115 -v4116 -v4117 -v4118  v4119 -v4120 -v4121 -v4122 -v4123 -v4124  v4125 -v4126 -v4127 -v4128 -v4129 -v4130 -v4131 -v4132  v4133 -v4134  v4135 -v4136 -v4137 -v4138 -v4139 -v4140  v4141 -v4142 -v4143 -v4144 -v4145 -v4146 -v4147  v4148 -v4149 -v4150 -v4151 -v4152  v4153 -v4154 -v4155 -v4156 -v4157 -v4158 -v4159 -v4160 -v4161 -v4162  v4163 -v4164 -v4165 -v4166 -v4167  v4168 -v4169 -v4170 -v4171 -v4172 -v4173 -v4174 -v4175  v4176 -v4177 -v4178 -v4179 -v4180  v4181 -v4182 -v4183 -v4184  v4185 -v4186 -v4187 -v4188 -v4189 -v4190 -v4191 -v4192  v4193 -v4194 -v4195 -v4196 -v4197  v4198 -v4199 -v4200 -v4201  v4202 -v4203 -v4204 -v4205 -v4206 -v4207  v4208 -v4209 -v4210 -v4211 -v4212 -v4213 -v4214 -v4215 -v4216  v4217 -v4218 -v4219 -v4220 -v4221  v4222 -v4223 -v4224 -v4225 -v4226  v4227 -v4228 -v4229 -v4230 -v4231 -v4232 -v4233 -v4234  v4235 -v4236 -v4237 -v4238  v4239 -v4240 -v4241 -v4242 -v4243  v4244 -v4245 -v4246 -v4247 -v4248 -v4249 -v4250  v4251 -v4252 -v4253 -v4254  v4255 -v4256 -v4257 -v4258 -v4259 -v4260  v4261 -v4262 -v4263 -v4264 -v4265 -v4266 -v4267 -v4268 -v4269  v4270 -v4271 -v4272 -v4273  v4274 -v4275 -v4276 -v4277 -v4278 -v4279  v4280 -v4281 -v4282 -v4283 -v4284 -v4285 -v4286  v4287 -v4288 -v4289 -v4290 -v4291  v4292 -v4293 -v4294 -v4295 -v4296 -v4297 -v4298 -v4299 -v4300 -v4301  v4302 -v4303 -v4304 -v4305  v4306 -v4307 -v4308 -v4309 -v4310 -v4311 -v4312  v4313 -v4314 -v4315 -v4316  v4317 -v4318 -v4319 -v4320  v4321 -v4322 -v4323 -v4324 -v4325 -v4326 -v4327 -v4328 -v4329  v4330 -v4331 -v4332 -v4333 -v4334  v4335 -v4336 -v4337 -v4338 -v4339 -v4340 -v4341  v4342 -v4343 -v4344 -v4345 -v4346  v4347 -v4348 -v4349 -v4350 -v4351 -v4352 -v4353 -v4354  v4355 -v4356 -v4357 -v4358 -v4359  v4360 -v4361 -v4362 -v4363  v4364 -v4365 -v4366 -v4367 -v4368  v4369 -v4370 -v4371 -v4372 -v4373 -v4374 -v4375 -v4376 -v4377 -v4378 -v4379  v4380  v4381 -v4382 -v4383 -v4384 -v4385 -v4386 -v4387 -v4388 -v4389  v4390 -v4391 -v4392  v4393 -v4394 -v4395 -v4396 -v4397 -v4398 -v4399 -v4400 -v4401  v4402 -v4403 -v4404 -v4405 -v4406 -v4407 -v4408 -v4409  v4410 -v4411 -v4412 -v4413 -v4414 -v4415  v4416 -v4417 -v4418 -v4419 -v4420  v4421 -v4422  v4423 -v4424 -v4425 -v4426 -v4427 -v4428 -v4429 -v4430 -v4431 -v4432 -v4433  v4434  v4435 -v4436 -v4437 -v4438 -v4439 -v4440  v4441 -v4442 -v4443 -v4444 -v4445 -v4446 -v4447  v4448 -v4449 -v4450 -v4451 -v4452 -v4453  v4454 -v4455 -v4456 -v4457 -v4458 -v4459 -v4460 -v4461  v4462 -v4463 -v4464 -v4465  v4466 -v4467 -v4468 -v4469 -v4470 -v4471 -v4472 -v4473 -v4474 -v4475  v4476 -v4477 -v4478 -v4479  v4480 -v4481 -v4482 -v4483  v4484 -v4485 -v4486 -v4487 -v4488 -v4489 -v4490 -v4491 -v4492 -v4493  v4494 -v4495 -v4496 -v4497 -v4498  v4499 -v4500 -v4501 -v4502 -v4503 -v4504 -v4505  v4506 -v4507 -v4508  v4509 -v4510 -v4511 -v4512 -v4513 -v4514 -v4515  v4516 -v4517 -v4518  v4519 -v4520 -v4521 -v4522 -v4523 -v4524 -v4525 -v4526 -v4527 -v4528 -v4529  v4530 -v4531  v4532 -v4533 -v4534 -v4535 -v4536  v4537 -v4538 -v4539 -v4540 -v4541 -v4542 -v4543 -v4544 -v4545  v4546 -v4547 -v4548 -v4549 -v4550  v4551 -v4552 -v4553 -v4554  v4555 -v4556 -v4557 -v4558 -v4559 -v4560 -v4561 -v4562 -v4563  v4564 -v4565 -v4566 -v4567 -v4568 -v4569 -v4570 -v4571  v4572 -v4573 -v4574 -v4575 -v4576 -v4577  v4578 -v4579  v4580 -v4581 -v4582 -v4583 -v4584  v4585 -v4586 -v4587 -v4588 -v4589 -v4590 -v4591 -v4592  v4593 -v4594 -v4595 -v4596  v4597 -v4598 -v4599 -v4600 -v4601 -v4602 -v4603 -v4604 -v4605 -v4606  v4607 -v4608  v4609 -v4610 -v4611 -v4612 -v4613 -v4614 -v4615 -v4616 -v4617  v4618 -v4619 -v4620 -v4621 -v4622 -v4623 -v4624  v4625 -v4626 -v4627 -v4628 -v4629  v4630 -v4631 -v4632 -v4633 -v4634 -v4635 -v4636 -v4637  v4638 -v4639  v4640 -v4641 -v4642 -v4643 -v4644 -v4645 -v4646 -v4647 -v4648 -v4649  v4650 -v4651 -v4652 -v4653 -v4654  v4655 -v4656 -v4657  v4658 -v4659 -v4660 -v4661 -v4662 
s SATISFIABLE
#### 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
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 2871
Raw data (stat): 2871 (runsolver) R 2870 25399 25398 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 857728073 884736 94 4294967295 134512640 135332820 3221224448 3221219612 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.001 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+20.0021 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+30.0025 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+40.0029 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+50.0032 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+60.0036 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+70.0041 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+80.0041 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+90.0048 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2874
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+226.326 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 2884
Raw data (stat): 2871 (vallstSAT2005PB) S 2870 25399 25398 0 -1 0 321 232 0 0 1 0 0 0 21 0 1 0 857728073 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 0

Child status: 10
Real time (s): 226.325
CPU time (s): 226.022
CPU user time (s): 196.572
CPU system time (s): 29.4495
CPU usage (%): 99.8658
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	0
#### END VERIFIER DATA ####