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/routing/normalized-s4-4-3-9pb.opb
MD5SUM	7d64f372313e74de659e9e56ab2d9bab
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	68
Optimality of the best value was proved	NO
Number of terms in the objective function	840
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	840
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	840
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04684
Number of variables	840
Total number of constraints	2526
Number of constraints which are clauses	2502
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	35
Trace number 6286

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-14 04:21:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4757 boxname=wulflinc3 idbench=245 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7d64f372313e74de659e9e56ab2d9bab  /oldhome/oroussel/tmp/wulflinc3/normalized-s4-4-3-9pb.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc3/normalized-s4-4-3-9pb.opb /oldhome/oroussel/tmp/wulflinc3/normalized-s4-4-3-9pb.opb
IDLAUNCH: 4757
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        850132 kB
Buffers:         36280 kB
Cached:         125140 kB
SwapCached:       3276 kB
Active:          79568 kB
Inactive:        87980 kB
HighTotal:      131008 kB
HighFree:         7364 kB
LowTotal:       903652 kB
LowFree:        842768 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11340 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:28:45 (client local time) WITH STATUS 30 IN 425.257 SECONDS
stats: 4757 0 425.257 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2526 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2520]---> BDD-cost:    1
c ---[2503]---> BDD-cost:    1
c ---[2465]---> BDD-cost:    1
c ---[2455]---> BDD-cost:    1
c ---[2449]---> BDD-cost:    1
c ---[2431]---> BDD-cost:    1
c ---[2393]---> BDD-cost:    1
c ---[2383]---> BDD-cost:    1
c ---[2377]---> BDD-cost:    1
c ---[2359]---> BDD-cost:    1
c ---[2321]---> BDD-cost:    1
c ---[2311]---> BDD-cost:    1
c ---[2309]---> BDD-cost:    1
c ---[2283]---> BDD-cost:    1
c ---[2265]---> BDD-cost:    1
c ---[2239]---> BDD-cost:    1
c ---[2206]---> BDD-cost:    1
c ---[2180]---> BDD-cost:    1
c ---[2178]---> BDD-cost:    1
c ---[2168]---> BDD-cost:    1
c ---[2151]---> BDD-cost:    1
c ---[2129]---> BDD-cost:    1
c ---[2103]---> BDD-cost:    1
c ---[2097]---> BDD-cost:    1
c ---[2079]---> BDD-cost:    1
c ---[2057]---> BDD-cost:    1
c ---[2031]---> BDD-cost:    1
c ---[2025]---> BDD-cost:    1
c ---[2007]---> BDD-cost:    1
c ---[1985]---> BDD-cost:    1
c ---[1959]---> BDD-cost:    1
c ---[1953]---> BDD-cost:    1
c ---[1935]---> BDD-cost:    1
c ---[1913]---> BDD-cost:    1
c ---[1887]---> BDD-cost:    1
c ---[1881]---> BDD-cost:    1
c ---[1871]---> BDD-cost:    1
c ---[1861]---> BDD-cost:    1
c ---[1812]---> BDD-cost:    1
c ---[1810]---> BDD-cost:    1
c ---[1758]---> BDD-cost:    1
c ---[1748]---> BDD-cost:    1
c ---[1742]---> BDD-cost:    1
c ---[1740]---> BDD-cost:    1
c ---[1692]---> BDD-cost:    1
c ---[1682]---> BDD-cost:    1
c ---[1672]---> BDD-cost:    1
c ---[1670]---> BDD-cost:    1
c ---[1664]---> BDD-cost:    1
c ---[1646]---> BDD-cost:    1
c ---[1609]---> BDD-cost:    1
c ---[1599]---> BDD-cost:    1
c ---[1593]---> BDD-cost:    1
c ---[1575]---> BDD-cost:    1
c ---[1537]---> BDD-cost:    1
c ---[1527]---> BDD-cost:    1
c ---[1513]---> BDD-cost:    1
c ---[1487]---> BDD-cost:    1
c ---[1465]---> BDD-cost:    1
c ---[1455]---> BDD-cost:    1
c ---[1422]---> BDD-cost:    1
c ---[1396]---> BDD-cost:    1
c ---[1394]---> BDD-cost:    1
c ---[1384]---> BDD-cost:    1
c ---[1378]---> BDD-cost:    1
c ---[1360]---> BDD-cost:    1
c ---[1322]---> BDD-cost:    1
c ---[1312]---> BDD-cost:    1
c ---[1298]---> BDD-cost:    1
c ---[1272]---> BDD-cost:    1
c ---[1250]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1234]---> BDD-cost:    1
c ---[1216]---> BDD-cost:    1
c ---[1178]---> BDD-cost:    1
c ---[1168]---> BDD-cost:    1
c ---[1135]---> BDD-cost:    1
c ---[1109]---> BDD-cost:    1
c ---[1107]---> BDD-cost:    1
c ---[1097]---> BDD-cost:    1
c ---[1079]---> BDD-cost:    1
c ---[1057]---> BDD-cost:    1
c ---[1031]---> BDD-cost:    1
c ---[1025]---> BDD-cost:    1
c ---[1007]---> BDD-cost:    1
c ---[ 985]---> BDD-cost:    1
c ---[ 959]---> BDD-cost:    1
c ---[ 953]---> BDD-cost:    1
c ---[ 935]---> BDD-cost:    1
c ---[ 913]---> BDD-cost:    1
c ---[ 887]---> BDD-cost:    1
c ---[ 881]---> BDD-cost:    1
c ---[ 875]---> BDD-cost:    1
c ---[ 858]---> BDD-cost:    1
c ---[ 820]---> BDD-cost:    1
c ---[ 810]---> BDD-cost:    1
c ---[ 808]---> BDD-cost:    1
c ---[ 782]---> BDD-cost:    1
c ---[ 764]---> BDD-cost:    1
c ---[ 738]---> BDD-cost:    1
c ---[ 724]---> BDD-cost:    1
c ---[ 698]---> BDD-cost:    1
c ---[ 676]---> BDD-cost:    1
c ---[ 666]---> BDD-cost:    1
c ---[ 652]---> BDD-cost:    1
c ---[ 627]---> BDD-cost:    1
c ---[ 605]---> BDD-cost:    1
c ---[ 595]---> BDD-cost:    1
c ---[ 593]---> BDD-cost:    1
c ---[ 567]---> BDD-cost:    1
c ---[ 549]---> BDD-cost:    1
c ---[ 523]---> BDD-cost:    1
c ---[ 521]---> BDD-cost:    1
c ---[ 495]---> BDD-cost:    1
c ---[ 477]---> BDD-cost:    1
c ---[ 451]---> BDD-cost:    1
c ---[ 438]---> BDD-cost:    1
c ---[ 412]---> BDD-cost:    1
c ---[ 390]---> BDD-cost:    1
c ---[ 380]---> BDD-cost:    1
c ---[ 378]---> BDD-cost:    1
c ---[ 352]---> BDD-cost:    1
c ---[ 334]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 306]---> BDD-cost:    1
c ---[ 280]---> BDD-cost:    1
c ---[ 262]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 156]---> BDD-cost:    1
c ---[ 146]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:  127
c ---[  22]---> BDD-cost:  127
c ---[  21]---> BDD-cost:  127
c ---[  20]---> BDD-cost:  127
c ---[  19]---> BDD-cost:  127
c ---[  18]---> BDD-cost:  127
c ---[  17]---> BDD-cost:  127
c ---[  16]---> BDD-cost:  127
c ---[  15]---> BDD-cost:  127
c ---[  14]---> BDD-cost:  127
c ---[  13]---> BDD-cost:  127
c ---[  12]---> BDD-cost:  127
c ---[  11]---> BDD-cost:  127
c ---[  10]---> BDD-cost:  127
c ---[   9]---> BDD-cost:  127
c ---[   8]---> BDD-cost:  127
c ---[   7]---> BDD-cost:  127
c ---[   6]---> BDD-cost:  127
c ---[   5]---> BDD-cost:  127
c ---[   4]---> BDD-cost:  127
c ---[   3]---> BDD-cost:  127
c ---[   2]---> BDD-cost:  127
c ---[   1]---> BDD-cost:  127
c ---[   0]---> BDD-cost:  127
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   18270    53462 |    6090       0        0     nan |  0.000 % |
c |       100 |   18270    53462 |    6699     100     1788    17.9 |  4.072 % |
c |       251 |   18270    53462 |    7368     251     4496    17.9 |  4.072 % |
c |       478 |   18270    53462 |    8105     478    15328    32.1 |  4.072 % |
c |       816 |   18270    53462 |    8916     816    28103    34.4 |  4.072 % |
c |      1324 |   18270    53462 |    9808    1324    44651    33.7 |  4.072 % |
c |      2091 |   18270    53462 |   10788    2091    70496    33.7 |  4.072 % |
c |      3230 |   18270    53462 |   11867    3230   107512    33.3 |  4.072 % |
c |      4938 |   18270    53462 |   13054    4938   160636    32.5 |  4.072 % |
c |      7500 |   18270    53462 |   14359    7500   254305    33.9 |  4.072 % |
c |     11344 |   18270    53462 |   15795   11344   388350    34.2 |  4.072 % |
c |     17110 |   18270    53462 |   17375    9098   274402    30.2 |  4.072 % |
c |     25760 |   18184    53220 |   19113   17566   543701    31.0 |  4.469 % |
c |     38735 |   18166    53166 |   21024   10392   316889    30.5 |  4.518 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:38684     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45461 |  105946   258584 |   35315   17093   569644    33.3 |  4.518 % |
c |     45563 |  105946   258584 |   38846   17195   571712    33.2 |  0.729 % |
c |     45713 |  105946   258584 |   42731   17345   573850    33.1 |  0.729 % |
c |     45940 |  105946   258584 |   47004   17572   584241    33.2 |  0.729 % |
c |     46277 |  105946   258584 |   51704   17909   593972    33.2 |  0.729 % |
c |     46787 |  105599   257798 |   56875   18408   606414    32.9 |  1.028 % |
c |     47547 |  105599   257798 |   62562   19168   622583    32.5 |  1.028 % |
c |     48687 |  105599   257798 |   68818   20308   677442    33.4 |  1.028 % |
c |     50395 |  104930   256263 |   75700   21938   734014    33.5 |  1.603 % |
c |     52957 |  102506   250692 |   83270   24406   792554    32.5 |  3.675 % |
c |     56802 |  102453   250570 |   91598   28250   904374    32.0 |  3.720 % |
c |     62568 |  102398   250445 |  100757   34015  1172402    34.5 |  3.769 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:33080     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66842 |  172476   414518 |   57492   38281  1295109    33.8 |  3.769 % |
c |     66942 |  172476   414518 |   63241   38381  1300064    33.9 |  2.904 % |
c |     67092 |  172476   414518 |   69565   38531  1306410    33.9 |  2.904 % |
c |     67319 |  172476   414518 |   76521   38758  1313499    33.9 |  2.904 % |
c |     67656 |  172476   414518 |   84174   39095  1325181    33.9 |  2.904 % |
c |     68162 |  172476   414518 |   92591   39601  1342710    33.9 |  2.904 % |
c |     68921 |  172176   413828 |  101850   40352  1367132    33.9 |  3.049 % |
c |     70063 |  172125   413715 |  112035   41493  1397974    33.7 |  3.074 % |
c |     71772 |  172055   413556 |  123239   43201  1461098    33.8 |  3.109 % |
c |     74334 |  171389   412017 |  135563   45708  1565908    34.3 |  3.429 % |
c |     78178 |  167549   403210 |  149119   49224  1639648    33.3 |  5.368 % |
c |     83945 |  164724   396705 |  164031   54757  1842639    33.7 |  6.812 % |
c |     92597 |  156684   378107 |  180434   63093  2086520    33.1 | 11.013 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:34114     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102861 |  227346   543336 |   75782   73343  2376427    32.4 | 11.013 % |
c |    102963 |  227265   543148 |   83360   73440  2378070    32.4 |  9.223 % |
c |    103114 |  227265   543148 |   91696   73591  2380957    32.4 |  9.223 % |
c |    103339 |  227156   542896 |  100865   73815  2399377    32.5 |  9.264 % |
c |    103676 |  227156   542896 |  110952   74152  2411921    32.5 |  9.264 % |
c |    104182 |  227156   542896 |  122047   74658  2423465    32.5 |  9.264 % |
c |    104942 |  227156   542896 |  134252   75418  2439791    32.4 |  9.264 % |
c |    106082 |  226486   541359 |  147677   76525  2498364    32.6 |  9.502 % |
c |    107791 |  225968   540159 |  162445   78217  2558319    32.7 |  9.689 % |
c |    110353 |  225968   540159 |  178689   80779  2626791    32.5 |  9.689 % |
c |    114198 |  225432   538931 |  196558   84614  2774327    32.8 |  9.870 % |
c ==============================================================================
c [1mOptimal solution: 68[0m
s OPTIMUM FOUND
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
c _______________________________________________________________________________
c 
c restarts              : 50
c conflicts             : 119108         (280 /sec)
c decisions             : 188744         (444 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 424.863 s
c _______________________________________________________________________________
#### 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.91 0.98 0.93 2/54 19451
Raw data (stat): 19451 (runsolver) R 19450 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423446602 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 1388 0 0 0 994 4 0 0 25 0 1 0 423446602 7315456 1366 4294967295 134512640 134672761 3221224560 3221223684 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1786 1366 603 41 0 1745 0
vsize: 7144
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 1589 0 0 0 1993 5 0 0 25 0 1 0 423446602 8142848 1567 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1988 1567 603 41 0 1947 0
vsize: 7952
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 1628 0 0 0 2992 5 0 0 25 0 1 0 423446602 8290304 1606 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2024 1606 603 41 0 1983 0
vsize: 8096
[startup+40.0016 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 4263 0 0 0 3985 12 0 0 25 0 1 0 423446602 21065728 4169 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5143 4169 603 41 0 5102 0
vsize: 20572
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 4382 0 0 0 4986 12 0 0 25 0 1 0 423446602 21467136 4288 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5241 4288 603 41 0 5200 0
vsize: 20964
[startup+60.0021 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 4570 0 0 0 5984 13 0 0 25 0 1 0 423446602 22257664 4476 4294967295 134512640 134672761 3221224560 3221223664 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5434 4476 603 41 0 5393 0
vsize: 21736
[startup+70.0031 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 4781 0 0 0 6983 14 0 0 25 0 1 0 423446602 23060480 4687 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5630 4687 603 41 0 5589 0
vsize: 22520
[startup+80.0036 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 4940 0 0 0 7983 14 0 0 25 0 1 0 423446602 23879680 4846 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5830 4846 603 41 0 5789 0
vsize: 23320
[startup+90.0034 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 7074 0 0 0 8978 20 0 0 25 0 1 0 423446602 32137216 6897 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7846 6897 603 41 0 7805 0
vsize: 31384
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 7170 0 0 0 9978 20 0 0 25 0 1 0 423446602 32436224 6993 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7919 6993 603 41 0 7878 0
vsize: 31676
[startup+110.004 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 7298 0 0 0 10977 21 0 0 25 0 1 0 423446602 33005568 7121 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8058 7121 603 41 0 8017 0
vsize: 32232
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 7387 0 0 0 11977 21 0 0 25 0 1 0 423446602 33304576 7210 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8131 7210 603 41 0 8090 0
vsize: 32524
[startup+130.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 7418 0 0 0 12977 21 0 0 25 0 1 0 423446602 33439744 7241 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8164 7241 603 41 0 8123 0
vsize: 32656
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 7515 0 0 0 13977 22 0 0 25 0 1 0 423446602 33837056 7338 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7338 603 41 0 8220 0
vsize: 33044
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 7584 0 0 0 14977 22 0 0 25 0 1 0 423446602 34107392 7407 4294967295 134512640 134672761 3221224560 3221223728 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7407 603 41 0 8286 0
vsize: 33308
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 7691 0 0 0 15977 22 0 0 25 0 1 0 423446602 34508800 7514 4294967295 134512640 134672761 3221224560 3221223696 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8425 7514 603 41 0 8384 0
vsize: 33700
[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 7758 0 0 0 16977 23 0 0 25 0 1 0 423446602 34775040 7581 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8490 7581 603 41 0 8449 0
vsize: 33960
[startup+180.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 7815 0 0 0 17977 23 0 0 25 0 1 0 423446602 35094528 7638 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8568 7638 603 41 0 8527 0
vsize: 34272
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 7890 0 0 0 18976 23 0 0 25 0 1 0 423446602 35364864 7713 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8634 7713 603 41 0 8593 0
vsize: 34536
[startup+200.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 7986 0 0 0 19977 23 0 0 25 0 1 0 423446602 35762176 7809 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8731 7809 603 41 0 8690 0
vsize: 34924
[startup+210.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 8035 0 0 0 20977 23 0 0 25 0 1 0 423446602 36040704 7858 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8799 7858 603 41 0 8758 0
vsize: 35196
[startup+220.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 8065 0 0 0 21977 23 0 0 25 0 1 0 423446602 36175872 7888 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8832 7888 603 41 0 8791 0
vsize: 35328
[startup+230.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 8150 0 0 0 22977 24 0 0 25 0 1 0 423446602 36442112 7973 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8897 7973 603 41 0 8856 0
vsize: 35588
[startup+240.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 8221 0 0 0 23977 24 0 0 25 0 1 0 423446602 37113856 8044 4294967295 134512640 134672761 3221224560 3221223760 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9061 8044 603 41 0 9020 0
vsize: 36244
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 8282 0 0 0 24977 24 0 0 25 0 1 0 423446602 37253120 8105 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9095 8105 603 41 0 9054 0
vsize: 36380
[startup+260.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 8347 0 0 0 25976 24 0 0 25 0 1 0 423446602 37527552 8170 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9162 8170 603 41 0 9121 0
vsize: 36648
[startup+270.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 8421 0 0 0 26976 25 0 0 25 0 1 0 423446602 37789696 8244 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9226 8244 603 41 0 9185 0
vsize: 36904
[startup+280.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 10701 0 0 0 27972 30 0 0 25 0 1 0 423446602 47992832 10359 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11717 10359 603 41 0 11676 0
vsize: 46868
[startup+290.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 10745 0 0 0 28971 30 0 0 25 0 1 0 423446602 48123904 10403 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11749 10403 603 41 0 11708 0
vsize: 46996
[startup+300.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 10829 0 0 0 29972 30 0 0 25 0 1 0 423446602 48594944 10487 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11864 10487 603 41 0 11823 0
vsize: 47456
[startup+310.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 10852 0 0 0 30972 30 0 0 25 0 1 0 423446602 48594944 10510 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11864 10510 603 41 0 11823 0
vsize: 47456
[startup+320.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 10891 0 0 0 31972 30 0 0 25 0 1 0 423446602 48726016 10549 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11896 10549 603 41 0 11855 0
vsize: 47584
[startup+330.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 10938 0 0 0 32972 30 0 0 25 0 1 0 423446602 48988160 10596 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11960 10596 603 41 0 11919 0
vsize: 47840
[startup+340.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 10986 0 0 0 33972 30 0 0 25 0 1 0 423446602 49119232 10644 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11992 10644 603 41 0 11951 0
vsize: 47968
[startup+350.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 11038 0 0 0 34972 30 0 0 25 0 1 0 423446602 49463296 10696 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12076 10696 603 41 0 12035 0
vsize: 48304
[startup+360.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 11085 0 0 0 35972 31 0 0 25 0 1 0 423446602 49594368 10743 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12108 10743 603 41 0 12067 0
vsize: 48432
[startup+370.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 11127 0 0 0 36972 31 0 0 25 0 1 0 423446602 49729536 10785 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 10785 603 41 0 12100 0
vsize: 48564
[startup+380.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 11170 0 0 0 37972 31 0 0 25 0 1 0 423446602 49860608 10828 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12173 10828 603 41 0 12132 0
vsize: 48692
[startup+390.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 11206 0 0 0 38972 31 0 0 25 0 1 0 423446602 49995776 10864 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12206 10864 603 41 0 12165 0
vsize: 48824
[startup+400.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 11212 0 0 0 39972 31 0 0 25 0 1 0 423446602 50126848 10870 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12238 10870 603 41 0 12197 0
vsize: 48952
[startup+410.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 11212 0 0 0 40972 31 0 0 25 0 1 0 423446602 50126848 10870 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12238 10870 603 41 0 12197 0
vsize: 48952
[startup+420.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 11216 0 0 0 41973 31 0 0 25 0 1 0 423446602 50126848 10874 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12238 10874 603 41 0 12197 0
vsize: 48952
[startup+425.223 s]
Raw data (loadavg): 0.99 0.98 0.93 1/53 19451
Raw data (stat): 19451 (minisat+) R 19450 10720 10719 0 -1 0 11216 0 0 0 41973 31 0 0 25 0 1 0 423446602 50126848 10874 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12238 10874 603 41 0 12197 0
vsize: 0

Child status: 30
Real time (s): 425.223
CPU time (s): 425.257
CPU user time (s): 424.918
CPU system time (s): 0.338948
CPU usage (%): 100.008
Max. virtual memory (Kb): 48952
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	68
#### END VERIFIER DATA ####