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/sorensson/garden/normalized-g7x7.opb
MD5SUM	0cf87a0fcd2352953842751bd4aefa7f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	12
Optimality of the best value was proved	NO
Number of terms in the objective function	49
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	49
Number of bits of the sum of numbers in the objective function	6
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	49
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.083986
Number of variables	49
Total number of constraints	49
Number of constraints which are clauses	49
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	3
Maximum length of a constraint	5

Trace number 29371

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-05-25 07:15:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20787 boxname=wulflinc7 idbench=377 idsolver=14 numberseed=0
MD5SUM SOLVER: d29da23ec752be69e0579424c0f0767e  /oldhome/oroussel/solvers/sat4jPseudoBis.jar
MD5SUM BENCH:  0cf87a0fcd2352953842751bd4aefa7f  /oldhome/oroussel/tmp/wulflinc7/normalized-g7x7.opb
REAL COMMAND:  java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudoBis.jar /oldhome/oroussel/tmp/wulflinc7/normalized-g7x7.opb
IDLAUNCH: 20787
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        764200 kB
Buffers:         22368 kB
Cached:         228560 kB
SwapCached:        740 kB
Active:          45332 kB
Inactive:       207720 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        763948 kB
SwapTotal:     2097136 kB
SwapFree:      2095584 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5124 kB
Slab:            11756 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 07:21:14 (client local time) WITH STATUS 30 IN 336.023 SECONDS
stats: 20787 0 336.023 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c SAT4J: a SATisfiability library for Java (c) 2004-2005 Daniel Le Berre
c This is free software under the GNU LGPL licence. See www.sat4j.org for details.
c version Special PB05 Second trial
c --- Begin Solver configuration ---
c org.sat4j.minisat.uip.FirstUIP@1e4cbc4
c org.sat4j.minisat.constraints.PBMinDataStructure@1fdc96c
c org.sat4j.minisat.learning.MiniSATLearning@b2fd8f
c conflictBoundIncFactor=1.5 learntBoundIncFactor=1.1 initLearntBoundConstraintFactor=0.5 initConflictBound=100 
c 
c --- End Solver configuration ---
c solving /oldhome/oroussel/tmp/wulflinc7/normalized-g7x7.opb
c reading problem ... done. Time 0.164 ms.
c #vars     49
c #constraints  49
c SATISFIABLE
c OPTIMIZING...
c CURRENT OPTIMUM=                  17 		Current CPU time: 0.20 ms
c CURRENT OPTIMUM=                  16 		Current CPU time: 0.64 ms
c CURRENT OPTIMUM=                  15 		Current CPU time: 0.67 ms
c CURRENT OPTIMUM=                  14 		Current CPU time: 0.76 ms
c CURRENT OPTIMUM=                  13 		Current CPU time: 1.05 ms
c CURRENT OPTIMUM=                  12 		Current CPU time: 12.04 ms
c starts	: 16
c conflicts	: 4491
c decisions	: 7375
c propagations	: 36984
c inspects	: 3679043
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 4490
c root simplifications	: 23
s OPTIMUM_FOUND
v -x1 -x2 x3 -x4 x5 -x6 -x7 x8 -x9 -x10 -x11 -x12 -x13 x14 -x15 -x16 -x17 x18 -x19 -x20 -x21 -x22 x23 -x24 -x25 -x26 x27 -x28 -x29 -x30 -x31 x32 -x33 -x34 -x35 x36 -x37 -x38 -x39 -x40 -x41 x42 -x43 -x44 x45 -x46 x47 -x48 -x49 
c objectif function=12
c Total CPU time (ms) : 333.235
#### 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.85 0.97 0.94 2/54 6787
Raw data (stat): 6787 (runsolver) R 6786 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 778790363 1052672 99 4294967295 134512640 135381576 3221224416 3221219636 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 1.10 1.02 0.95 2/64 6802
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18108 3 1 0 755 40 0 0 25 0 11 0 778790363 858644480 19973 4294967295 134512640 134569956 3221224384 3221214804 1130898680 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209630 19973 13086 16 0 209614 0
vsize: 838520
[startup+20.0057 s]
Raw data (loadavg): 1.09 1.02 0.95 2/64 6803
Raw data (stat): 6787 (java) S 6786 24300 24299 0 -1 0 18110 3 1 0 1723 40 0 0 25 0 11 0 778790363 858611712 20469 4294967295 134512640 134569956 3221224384 3221213400 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 20469 13086 16 0 209606 0
vsize: 838488
[startup+30.0062 s]
Raw data (loadavg): 1.07 1.01 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 2680 40 0 0 25 0 11 0 778790363 858611712 20892 4294967295 134512640 134569956 3221224384 3221214680 1131143412 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 20892 13086 16 0 209606 0
vsize: 838488
[startup+40.0074 s]
Raw data (loadavg): 1.06 1.01 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 3645 40 0 0 25 0 11 0 778790363 858611712 21167 4294967295 134512640 134569956 3221224384 3221214780 1131143392 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209622 21167 13086 16 0 209606 0
vsize: 838488
[startup+50.0075 s]
Raw data (loadavg): 1.05 1.01 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 4606 40 0 0 25 0 11 0 778790363 858611712 21408 4294967295 134512640 134569956 3221224384 3221214776 1131149924 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 21408 13086 16 0 209606 0
vsize: 838488
[startup+60.007 s]
Raw data (loadavg): 1.04 1.01 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 5559 40 0 0 25 0 11 0 778790363 858611712 21576 4294967295 134512640 134569956 3221224384 3221214672 1131163005 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 21576 13086 16 0 209606 0
vsize: 838488
[startup+70.0079 s]
Raw data (loadavg): 1.04 1.01 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 6520 41 0 0 25 0 11 0 778790363 858611712 21677 4294967295 134512640 134569956 3221224384 3221214272 1131243908 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 21677 13086 16 0 209606 0
vsize: 838488
[startup+80.0083 s]
Raw data (loadavg): 1.03 1.01 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 7480 41 0 0 25 0 11 0 778790363 858611712 21773 4294967295 134512640 134569956 3221224384 3221214672 1131162344 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 21773 13086 16 0 209606 0
vsize: 838488
[startup+90.0088 s]
Raw data (loadavg): 1.02 1.01 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 8441 41 0 0 25 0 11 0 778790363 858611712 21903 4294967295 134512640 134569956 3221224384 3221214096 1131241858 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 21903 13086 16 0 209606 0
vsize: 838488
[startup+100.009 s]
Raw data (loadavg): 1.02 1.01 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 9411 41 0 0 25 0 11 0 778790363 858611712 21986 4294967295 134512640 134569956 3221224384 3221214504 1131179187 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 21986 13086 16 0 209606 0
vsize: 838488
[startup+110.009 s]
Raw data (loadavg): 1.02 1.01 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 10382 41 0 0 25 0 11 0 778790363 858611712 22100 4294967295 134512640 134569956 3221224384 3221214320 1131241852 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 22100 13086 16 0 209606 0
vsize: 838488
[startup+120.01 s]
Raw data (loadavg): 1.01 1.01 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 11353 41 0 0 25 0 11 0 778790363 858611712 22201 4294967295 134512640 134569956 3221224384 3221214580 1130885141 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 22201 13086 16 0 209606 0
vsize: 838488
[startup+130.01 s]
Raw data (loadavg): 1.01 1.00 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 12315 41 0 0 25 0 11 0 778790363 858611712 22323 4294967295 134512640 134569956 3221224384 3221214776 1131149607 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 22323 13086 16 0 209606 0
vsize: 838488
[startup+140.01 s]
Raw data (loadavg): 1.01 1.00 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 13287 41 0 0 25 0 11 0 778790363 858611712 22410 4294967295 134512640 134569956 3221224384 3221214656 1131143523 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 22410 13086 16 0 209606 0
vsize: 838488
[startup+150.015 s]
Raw data (loadavg): 1.01 1.00 0.95 2/64 6803
Raw data (stat): 6787 (java) S 6786 24300 24299 0 -1 0 18111 3 1 0 14253 41 0 0 25 0 11 0 778790363 858611712 22496 4294967295 134512640 134569956 3221224384 3221213264 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 22496 13086 16 0 209606 0
vsize: 838488
[startup+160.015 s]
Raw data (loadavg): 1.01 1.00 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 15224 41 0 0 25 0 11 0 778790363 858611712 22591 4294967295 134512640 134569956 3221224384 3221214672 1131162125 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 22591 13086 16 0 209606 0
vsize: 838488
[startup+170.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 16197 41 0 0 25 0 11 0 778790363 858611712 22663 4294967295 134512640 134569956 3221224384 3221214672 1131162082 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 22663 13086 16 0 209606 0
vsize: 838488
[startup+180.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 17169 41 0 0 25 0 11 0 778790363 858611712 22740 4294967295 134512640 134569956 3221224384 3221214672 1131162125 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 22740 13086 16 0 209606 0
vsize: 838488
[startup+190.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 18142 41 0 0 25 0 11 0 778790363 858611712 22826 4294967295 134512640 134569956 3221224384 3221214672 1131162960 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209622 22826 13086 16 0 209606 0
vsize: 838488
[startup+200.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 19115 42 0 0 25 0 11 0 778790363 858611712 22912 4294967295 134512640 134569956 3221224384 3221214656 1131143483 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 22912 13086 16 0 209606 0
vsize: 838488
[startup+210.014 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 20088 42 0 0 25 0 11 0 778790363 858611712 22991 4294967295 134512640 134569956 3221224384 3221213688 1085679313 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 22991 13086 16 0 209606 0
vsize: 838488
[startup+220.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 21053 42 0 0 25 0 11 0 778790363 858611712 23097 4294967295 134512640 134569956 3221224384 3221214392 1078032762 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 23097 13086 16 0 209606 0
vsize: 838488
[startup+230.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 22036 42 0 0 25 0 11 0 778790363 858611712 23143 4294967295 134512640 134569956 3221224384 3221214352 1085679762 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209622 23143 13086 16 0 209606 0
vsize: 838488
[startup+240.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 23001 42 0 0 24 0 11 0 778790363 858611712 23240 4294967295 134512640 134569956 3221224384 3221214504 1131179187 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 23240 13086 16 0 209606 0
vsize: 838488
[startup+250.016 s]
Raw data (loadavg): 1.07 1.02 0.96 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 23984 42 0 0 25 0 11 0 778790363 858611712 23283 4294967295 134512640 134569956 3221224384 3221214204 1131241828 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209622 23283 13086 16 0 209606 0
vsize: 838488
[startup+260.017 s]
Raw data (loadavg): 1.06 1.02 0.96 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 24953 42 0 0 25 0 11 0 778790363 858611712 23357 4294967295 134512640 134569956 3221224384 3221214324 1131243984 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 23357 13086 16 0 209606 0
vsize: 838488
[startup+270.016 s]
Raw data (loadavg): 1.05 1.01 0.96 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 25928 42 0 0 25 0 11 0 778790363 858611712 23431 4294967295 134512640 134569956 3221224384 3221213936 1131244045 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 23431 13086 16 0 209606 0
vsize: 838488
[startup+280.017 s]
Raw data (loadavg): 1.04 1.01 0.96 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 26903 42 0 0 25 0 11 0 778790363 858611712 23504 4294967295 134512640 134569956 3221224384 3221214656 1131143412 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 23504 13086 16 0 209606 0
vsize: 838488
[startup+290.016 s]
Raw data (loadavg): 1.04 1.01 0.96 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 27879 43 0 0 25 0 11 0 778790363 858611712 23571 4294967295 134512640 134569956 3221224384 3221213768 1131241897 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 23571 13086 16 0 209606 0
vsize: 838488
[startup+300.016 s]
Raw data (loadavg): 1.03 1.01 0.96 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 28856 43 0 0 25 0 11 0 778790363 858611712 23640 4294967295 134512640 134569956 3221224384 3221213912 1085679321 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 23640 13086 16 0 209606 0
vsize: 838488
[startup+310.016 s]
Raw data (loadavg): 1.02 1.01 0.96 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 29832 43 0 0 24 0 11 0 778790363 858611712 23706 4294967295 134512640 134569956 3221224384 3221214128 1085679762 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 23706 13086 16 0 209606 0
vsize: 838488
[startup+320.016 s]
Raw data (loadavg): 1.02 1.01 0.96 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 30809 43 0 0 25 0 11 0 778790363 858611712 23778 4294967295 134512640 134569956 3221224384 3221214672 1131162870 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209622 23778 13086 16 0 209606 0
vsize: 838488
[startup+330.024 s]
Raw data (loadavg): 1.02 1.01 0.96 2/64 6803
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 31788 43 0 0 25 0 11 0 778790363 858611712 23847 4294967295 134512640 134569956 3221224384 3221214672 1131162198 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 23847 13086 16 0 209606 0
vsize: 838488
[startup+334.289 s]
Raw data (loadavg): 1.02 1.01 0.96 1/53 6804
Raw data (stat): 6787 (java) R 6786 24300 24299 0 -1 0 18111 3 1 0 31788 43 0 0 25 0 11 0 778790363 858611712 23847 4294967295 134512640 134569956 3221224384 3221214672 1131162198 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209622 23847 13086 16 0 209606 0
vsize: 0

Child status: 30
Real time (s): 334.289
CPU time (s): 336.023
CPU user time (s): 335.455
CPU system time (s): 0.567913
CPU usage (%): 100.519
Max. virtual memory (Kb): 838520
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	12
#### END VERIFIER DATA ####