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-2pb.opb
MD5SUM	55739635f7f3741bc4f78c540803ac21
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	64
Optimality of the best value was proved	NO
Number of terms in the objective function	648
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	648
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	648
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.03884
Number of variables	648
Total number of constraints	1952
Number of constraints which are clauses	1928
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	27
Trace number 6274

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-14 04:18:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4750 boxname=wulflinc6 idbench=238 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  55739635f7f3741bc4f78c540803ac21  /oldhome/oroussel/tmp/wulflinc6/normalized-s4-4-3-2pb.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc6/normalized-s4-4-3-2pb.opb /oldhome/oroussel/tmp/wulflinc6/normalized-s4-4-3-2pb.opb
IDLAUNCH: 4750
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        878108 kB
Buffers:         36504 kB
Cached:          97872 kB
SwapCached:       2644 kB
Active:          53432 kB
Inactive:        86452 kB
HighTotal:      131008 kB
HighFree:        29260 kB
LowTotal:       903652 kB
LowFree:        848848 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11092 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:26:08 (client local time) WITH STATUS 30 IN 457.154 SECONDS
stats: 4750 0 457.154 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1952 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1950]---> BDD-cost:    1
c ---[1924]---> BDD-cost:    1
c ---[1906]---> BDD-cost:    1
c ---[1880]---> BDD-cost:    1
c ---[1862]---> BDD-cost:    1
c ---[1840]---> BDD-cost:    1
c ---[1814]---> BDD-cost:    1
c ---[1808]---> BDD-cost:    1
c ---[1794]---> BDD-cost:    1
c ---[1768]---> BDD-cost:    1
c ---[1746]---> BDD-cost:    1
c ---[1736]---> BDD-cost:    1
c ---[1734]---> BDD-cost:    1
c ---[1708]---> BDD-cost:    1
c ---[1690]---> BDD-cost:    1
c ---[1664]---> BDD-cost:    1
c ---[1662]---> BDD-cost:    1
c ---[1636]---> BDD-cost:    1
c ---[1619]---> BDD-cost:    1
c ---[1593]---> BDD-cost:    1
c ---[1560]---> BDD-cost:    1
c ---[1534]---> BDD-cost:    1
c ---[1532]---> BDD-cost:    1
c ---[1522]---> BDD-cost:    1
c ---[1516]---> BDD-cost:    1
c ---[1498]---> BDD-cost:    1
c ---[1460]---> BDD-cost:    1
c ---[1450]---> BDD-cost:    1
c ---[1436]---> BDD-cost:    1
c ---[1410]---> BDD-cost:    1
c ---[1388]---> BDD-cost:    1
c ---[1378]---> BDD-cost:    1
c ---[1341]---> BDD-cost:    1
c ---[1319]---> BDD-cost:    1
c ---[1313]---> BDD-cost:    1
c ---[1307]---> BDD-cost:    1
c ---[1305]---> BDD-cost:    1
c ---[1279]---> BDD-cost:    1
c ---[1261]---> BDD-cost:    1
c ---[1235]---> BDD-cost:    1
c ---[1186]---> BDD-cost:    1
c ---[1176]---> BDD-cost:    1
c ---[1166]---> BDD-cost:    1
c ---[1164]---> BDD-cost:    1
c ---[1154]---> BDD-cost:    1
c ---[1144]---> BDD-cost:    1
c ---[1095]---> BDD-cost:    1
c ---[1093]---> BDD-cost:    1
c ---[1057]---> BDD-cost:    1
c ---[1035]---> BDD-cost:    1
c ---[1029]---> BDD-cost:    1
c ---[1023]---> BDD-cost:    1
c ---[1009]---> BDD-cost:    1
c ---[ 984]---> BDD-cost:    1
c ---[ 962]---> BDD-cost:    1
c ---[ 952]---> BDD-cost:    1
c ---[ 915]---> BDD-cost:    1
c ---[ 893]---> BDD-cost:    1
c ---[ 887]---> BDD-cost:    1
c ---[ 881]---> BDD-cost:    1
c ---[ 871]---> BDD-cost:    1
c ---[ 861]---> BDD-cost:    1
c ---[ 811]---> BDD-cost:    1
c ---[ 809]---> BDD-cost:    1
c ---[ 776]---> BDD-cost:    1
c ---[ 750]---> BDD-cost:    1
c ---[ 748]---> BDD-cost:    1
c ---[ 738]---> BDD-cost:    1
c ---[ 736]---> BDD-cost:    1
c ---[ 710]---> BDD-cost:    1
c ---[ 692]---> BDD-cost:    1
c ---[ 666]---> BDD-cost:    1
c ---[ 664]---> BDD-cost:    1
c ---[ 638]---> BDD-cost:    1
c ---[ 620]---> BDD-cost:    1
c ---[ 594]---> BDD-cost:    1
c ---[ 592]---> BDD-cost:    1
c ---[ 566]---> BDD-cost:    1
c ---[ 548]---> BDD-cost:    1
c ---[ 522]---> BDD-cost:    1
c ---[ 520]---> BDD-cost:    1
c ---[ 494]---> BDD-cost:    1
c ---[ 476]---> BDD-cost:    1
c ---[ 450]---> BDD-cost:    1
c ---[ 417]---> BDD-cost:    1
c ---[ 391]---> BDD-cost:    1
c ---[ 389]---> BDD-cost:    1
c ---[ 379]---> BDD-cost:    1
c ---[ 346]---> BDD-cost:    1
c ---[ 320]---> BDD-cost:    1
c ---[ 318]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 260]---> BDD-cost:    1
c ---[ 250]---> BDD-cost:    1
c ---[ 240]---> BDD-cost:    1
c ---[ 238]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 210]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[  98]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   95
c ---[  22]---> BDD-cost:   95
c ---[  21]---> BDD-cost:   95
c ---[  20]---> BDD-cost:   95
c ---[  19]---> BDD-cost:   95
c ---[  18]---> BDD-cost:   95
c ---[  17]---> BDD-cost:   95
c ---[  16]---> BDD-cost:   95
c ---[  15]---> BDD-cost:   95
c ---[  14]---> BDD-cost:   95
c ---[  13]---> BDD-cost:   95
c ---[  12]---> BDD-cost:   95
c ---[  11]---> BDD-cost:   95
c ---[  10]---> BDD-cost:   95
c ---[   9]---> BDD-cost:   95
c ---[   8]---> BDD-cost:   95
c ---[   7]---> BDD-cost:   95
c ---[   6]---> BDD-cost:   95
c ---[   5]---> BDD-cost:   95
c ---[   4]---> BDD-cost:   95
c ---[   3]---> BDD-cost:   95
c ---[   2]---> BDD-cost:   95
c ---[   1]---> BDD-cost:   95
c ---[   0]---> BDD-cost:   95
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   13664    39966 |    4554       0        0     nan |  0.000 % |
c |       102 |   13664    39966 |    5009     102     1431    14.0 |  4.348 % |
c |       252 |   13664    39966 |    5510     252     3962    15.7 |  4.348 % |
c |       477 |   13664    39966 |    6061     477     7811    16.4 |  4.348 % |
c |       816 |   13664    39966 |    6667     816    14607    17.9 |  4.348 % |
c |      1322 |   13657    39945 |    7334    1314    26979    20.5 |  4.381 % |
c |      2082 |   13657    39945 |    8067    2074    43803    21.1 |  4.381 % |
c |      3224 |   13650    39924 |    8874    3215    86686    27.0 |  4.414 % |
c |      4936 |   13650    39924 |    9761    4927   128350    26.1 |  4.414 % |
c |      7498 |   13650    39924 |   10738    7489   237984    31.8 |  4.414 % |
c |     11342 |   13650    39924 |   11811    5712   241523    42.3 |  4.414 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:29320     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11640 |   79477   194103 |   26492    6010   248861    41.4 |  4.414 % |
c |     11741 |   79477   194103 |   29141    6111   249886    40.9 |  2.558 % |
c |     11891 |   79477   194103 |   32055    6261   250982    40.1 |  2.558 % |
c |     12116 |   79477   194103 |   35260    6486   256177    39.5 |  2.558 % |
c |     12456 |   79137   193300 |   38786    6788   266316    39.2 |  2.869 % |
c |     12964 |   78595   192049 |   42665    7276   278155    38.2 |  3.663 % |
c |     13724 |   78406   191598 |   46932    8021   302581    37.7 |  3.663 % |
c |     14863 |   78209   191149 |   51625    9156   337764    36.9 |  3.872 % |
c |     16573 |   77967   190586 |   56787   10847   381524    35.2 |  4.120 % |
c |     19135 |   73173   179491 |   62466   13237   428070    32.3 |  9.610 % |
c |     22979 |   72217   177283 |   68713   17032   579963    34.1 | 10.735 % |
c |     28747 |   57135   142448 |   75584   22137   692192    31.3 | 29.191 % |
c |     37398 |   56523   140936 |   83143   30752   876283    28.5 | 29.865 % |
c |     50372 |   56220   140233 |   91457   43714  1107849    25.3 | 30.248 % |
c |     69834 |   49286   124053 |  100603   62714  1587997    25.3 | 39.377 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:26476     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85843 |  106493   257677 |   35497   78589  1997917    25.4 | 39.377 % |
c |     85945 |  103210   249990 |   39046   17938   367176    20.5 | 26.387 % |
c |     86095 |  102964   249437 |   42951   18060   368614    20.4 | 26.540 % |
c |     86320 |  102936   249372 |   47246   18281   375760    20.6 | 26.559 % |
c |     86658 |  102936   249372 |   51971   18619   385774    20.7 | 26.559 % |
c |     87164 |  102936   249372 |   57168   19125   399174    20.9 | 26.559 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87648 |  102719   248888 |   34239   19608   416317    21.2 | 26.559 % |
c |     87749 |  102719   248888 |   37662   19709   419875    21.3 | 26.730 % |
c |     87902 |  102628   248683 |   41429   19861   428151    21.6 | 26.790 % |
c |     88127 |  102628   248683 |   45572   20086   432673    21.5 | 26.790 % |
c |     88465 |  102628   248683 |   50129   20424   441806    21.6 | 26.790 % |
c |     88971 |  102628   248683 |   55142   20930   453625    21.7 | 26.790 % |
c |     89730 |  102414   248210 |   60656   21687   470144    21.7 | 26.931 % |
c |     90869 |  102414   248210 |   66722   22826   494887    21.7 | 26.931 % |
c |     92578 |  101779   246770 |   73394   24529   540404    22.0 | 27.339 % |
c |     95140 |  100877   244682 |   80733   26945   632554    23.5 | 27.948 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98157 |  100779   244451 |   33593   29955   723532    24.2 | 27.948 % |
c |     98257 |  100290   243316 |   36952   30031   723957    24.1 | 28.333 % |
c |     98407 |  100236   243191 |   40647   30177   724825    24.0 | 28.360 % |
c |     98633 |  100149   242985 |   44712   30382   727765    24.0 | 28.433 % |
c |     98972 |  100149   242985 |   49183   30721   738460    24.0 | 28.433 % |
c |     99478 |  100149   242985 |   54101   31227   756634    24.2 | 28.433 % |
c |    100237 |  100043   242742 |   59512   31984   778851    24.4 | 28.506 % |
c |    101377 |  100043   242742 |   65463   33124   817891    24.7 | 28.506 % |
c |    103086 |   99745   242049 |   72009   34814   861724    24.8 | 28.725 % |
c |    105649 |   98353   238835 |   79210   37245   924209    24.8 | 29.624 % |
c |    109495 |   98301   238711 |   87131   41088  1006352    24.5 | 29.668 % |
c |    115261 |   98301   238711 |   95844   46854  1137480    24.3 | 29.668 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:23712     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    121021 |  147944   354792 |   49314   18793   341815    18.2 | 29.668 % |
c |    121121 |  147309   353349 |   54245   18879   343347    18.2 | 22.747 % |
c |    121271 |  147309   353349 |   59669   19029   347760    18.3 | 22.747 % |
c |    121496 |  147254   353223 |   65636   19253   355117    18.4 | 22.768 % |
c |    121834 |  146522   351541 |   72200   19578   364400    18.6 | 23.141 % |
c |    122340 |  146190   350784 |   79420   20061   379045    18.9 | 23.305 % |
c |    123099 |  145325   348792 |   87362   20796   396254    19.1 | 23.701 % |
c |    124239 |  143222   343958 |   96099   21716   411685    19.0 | 24.714 % |
c |    125948 |  143222   343958 |  105708   23425   440355    18.8 | 24.714 % |
c |    128510 |  141436   339793 |  116279   13444   184678    13.7 | 25.549 % |
c ==============================================================================
c [1mOptimal solution: 64[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
c _______________________________________________________________________________
c 
c restarts              : 64
c conflicts             : 129072         (283 /sec)
c decisions             : 204022         (447 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 456.879 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.88 0.97 0.91 2/54 3029
Raw data (stat): 3029 (runsolver) R 3028 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423431072 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+9.99975 s]
Raw data (loadavg): 0.90 0.97 0.91 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 3036 0 0 0 990 7 0 0 25 0 1 0 423431072 14213120 2934 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3470 2934 603 41 0 3429 0
vsize: 13880
[startup+20.0001 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 3142 0 0 0 1990 8 0 0 25 0 1 0 423431072 14618624 3040 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3569 3040 603 41 0 3528 0
vsize: 14276
[startup+29.9999 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 3316 0 0 0 2989 8 0 0 25 0 1 0 423431072 15421440 3214 4294967295 134512640 134672761 3221224560 3221223732 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3765 3214 603 41 0 3724 0
vsize: 15060
[startup+39.999 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 3470 0 0 0 3989 9 0 0 25 0 1 0 423431072 15958016 3368 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3896 3368 603 41 0 3855 0
vsize: 15584
[startup+49.9995 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 3693 0 0 0 4988 10 0 0 25 0 1 0 423431072 16912384 3591 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3591 603 41 0 4088 0
vsize: 16516
[startup+59.9993 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 3889 0 0 0 5987 11 0 0 25 0 1 0 423431072 17850368 3787 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4358 3787 603 41 0 4317 0
vsize: 17432
[startup+69.9994 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 4089 0 0 0 6987 12 0 0 25 0 1 0 423431072 18579456 3987 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4536 3987 603 41 0 4495 0
vsize: 18144
[startup+79.9999 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 4269 0 0 0 7987 12 0 0 25 0 1 0 423431072 19378176 4167 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4731 4167 603 41 0 4690 0
vsize: 18924
[startup+89.9998 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 4367 0 0 0 8987 12 0 0 25 0 1 0 423431072 19787776 4265 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4831 4265 603 41 0 4790 0
vsize: 19324
[startup+99.9992 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 4460 0 0 0 9987 12 0 0 25 0 1 0 423431072 20054016 4358 4294967295 134512640 134672761 3221224560 3221223728 134560931 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4896 4358 603 41 0 4855 0
vsize: 19584
[startup+109.999 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 4619 0 0 0 10987 13 0 0 25 0 1 0 423431072 20725760 4517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5060 4517 603 41 0 5019 0
vsize: 20240
[startup+119.999 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 4776 0 0 0 11987 13 0 0 25 0 1 0 423431072 21401600 4674 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5225 4674 603 41 0 5184 0
vsize: 20900
[startup+129.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 4904 0 0 0 12987 14 0 0 25 0 1 0 423431072 22069248 4802 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5388 4802 603 41 0 5347 0
vsize: 21552
[startup+139.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 5008 0 0 0 13987 14 0 0 25 0 1 0 423431072 22466560 4906 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5485 4906 603 41 0 5444 0
vsize: 21940
[startup+149.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 5116 0 0 0 14987 14 0 0 25 0 1 0 423431072 22994944 5014 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5614 5014 603 41 0 5573 0
vsize: 22456
[startup+159.998 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 5209 0 0 0 15986 15 0 0 25 0 1 0 423431072 23408640 5107 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5715 5107 603 41 0 5674 0
vsize: 22860
[startup+169.998 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 6895 0 0 0 16982 20 0 0 25 0 1 0 423431072 31006720 6703 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7570 6703 603 41 0 7529 0
vsize: 30280
[startup+179.997 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 6941 0 0 0 17981 20 0 0 25 0 1 0 423431072 31006720 6749 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7570 6749 603 41 0 7529 0
vsize: 30280
[startup+189.997 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 6943 0 0 0 18982 20 0 0 25 0 1 0 423431072 31006720 6751 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7570 6751 603 41 0 7529 0
vsize: 30280
[startup+199.997 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 6948 0 0 0 19982 20 0 0 25 0 1 0 423431072 31006720 6756 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7570 6756 603 41 0 7529 0
vsize: 30280
[startup+209.997 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 6954 0 0 0 20982 20 0 0 25 0 1 0 423431072 31006720 6762 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7570 6762 603 41 0 7529 0
vsize: 30280
[startup+219.997 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 6954 0 0 0 21982 20 0 0 25 0 1 0 423431072 31006720 6762 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7570 6762 603 41 0 7529 0
vsize: 30280
[startup+229.996 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 6963 0 0 0 22983 20 0 0 25 0 1 0 423431072 31006720 6771 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7570 6771 603 41 0 7529 0
vsize: 30280
[startup+239.996 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 6968 0 0 0 23983 20 0 0 25 0 1 0 423431072 31137792 6776 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7602 6776 603 41 0 7561 0
vsize: 30408
[startup+249.995 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 6969 0 0 0 24983 20 0 0 25 0 1 0 423431072 31137792 6777 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7602 6777 603 41 0 7561 0
vsize: 30408
[startup+259.995 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 6970 0 0 0 25983 20 0 0 25 0 1 0 423431072 31137792 6778 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7602 6778 603 41 0 7561 0
vsize: 30408
[startup+269.995 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 6971 0 0 0 26984 20 0 0 25 0 1 0 423431072 31137792 6779 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7602 6779 603 41 0 7561 0
vsize: 30408
[startup+279.994 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 6974 0 0 0 27984 20 0 0 25 0 1 0 423431072 31137792 6782 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7602 6782 603 41 0 7561 0
vsize: 30408
[startup+289.994 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7003 0 0 0 28984 20 0 0 25 0 1 0 423431072 31318016 6811 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7646 6811 603 41 0 7605 0
vsize: 30584
[startup+299.994 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7030 0 0 0 29984 20 0 0 25 0 1 0 423431072 31318016 6838 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7646 6838 603 41 0 7605 0
vsize: 30584
[startup+309.993 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7040 0 0 0 30985 20 0 0 25 0 1 0 423431072 31514624 6848 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7694 6848 603 41 0 7653 0
vsize: 30776
[startup+319.993 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7042 0 0 0 31985 20 0 0 25 0 1 0 423431072 31514624 6850 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7694 6850 603 41 0 7653 0
vsize: 30776
[startup+329.992 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7045 0 0 0 32985 20 0 0 25 0 1 0 423431072 31514624 6853 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7694 6853 603 41 0 7653 0
vsize: 30776
[startup+339.992 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7047 0 0 0 33985 20 0 0 25 0 1 0 423431072 31514624 6855 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7694 6855 603 41 0 7653 0
vsize: 30776
[startup+349.991 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7071 0 0 0 34986 21 0 0 25 0 1 0 423431072 31514624 6879 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7694 6879 603 41 0 7653 0
vsize: 30776
[startup+359.991 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7074 0 0 0 35986 21 0 0 25 0 1 0 423431072 31514624 6882 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7694 6882 603 41 0 7653 0
vsize: 30776
[startup+369.991 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7075 0 0 0 36986 21 0 0 25 0 1 0 423431072 31514624 6883 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7694 6883 603 41 0 7653 0
vsize: 30776
[startup+379.99 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7075 0 0 0 37986 21 0 0 25 0 1 0 423431072 31514624 6883 4294967295 134512640 134672761 3221224560 3221223712 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7694 6883 603 41 0 7653 0
vsize: 30776
[startup+389.99 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7450 0 0 0 38985 22 0 0 25 0 1 0 423431072 33349632 7258 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8142 7258 603 41 0 8101 0
vsize: 32568
[startup+399.99 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7450 0 0 0 39986 22 0 0 25 0 1 0 423431072 33349632 7258 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8142 7258 603 41 0 8101 0
vsize: 32568
[startup+409.99 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7450 0 0 0 40986 22 0 0 25 0 1 0 423431072 33349632 7258 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8142 7258 603 41 0 8101 0
vsize: 32568
[startup+419.99 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7450 0 0 0 41986 22 0 0 25 0 1 0 423431072 33349632 7258 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8142 7258 603 41 0 8101 0
vsize: 32568
[startup+429.99 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7450 0 0 0 42987 22 0 0 25 0 1 0 423431072 33349632 7258 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8142 7258 603 41 0 8101 0
vsize: 32568
[startup+439.996 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7450 0 0 0 43988 22 0 0 25 0 1 0 423431072 33349632 7258 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8142 7258 603 41 0 8101 0
vsize: 32568
[startup+449.995 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7450 0 0 0 44988 22 0 0 25 0 1 0 423431072 33349632 7258 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8142 7258 603 41 0 8101 0
vsize: 32568
[startup+457.041 s]
Raw data (loadavg): 1.00 0.99 0.92 1/53 3029
Raw data (stat): 3029 (minisat+) R 3028 29653 29652 0 -1 0 7450 0 0 0 44988 22 0 0 25 0 1 0 423431072 33349632 7258 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8142 7258 603 41 0 8101 0
vsize: 0

Child status: 30
Real time (s): 457.041
CPU time (s): 457.154
CPU user time (s): 456.913
CPU system time (s): 0.240963
CPU usage (%): 100.025
Max. virtual memory (Kb): 32568
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	64
#### END VERIFIER DATA ####