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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl10_15_pb.cnf.cr.opb
MD5SUMba9cd165dfff9daff67f98334a7b589e
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 16
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.009997
Number of variables300
Total number of constraints50
Number of constraints which are clauses30
Number of constraints which are cardinality constraints (but not clauses)20
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint10
Maximum length of a constraint15

Trace number 34666 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-05-28 10:10:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23929 boxname=wulflinc10 idbench=3 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ba9cd165dfff9daff67f98334a7b589e  /oldhome/oroussel/tmp/wulflinc10/normalized-chnl10_15_pb.cnf.cr.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc10/normalized-chnl10_15_pb.cnf.cr.opb
IDLAUNCH: 23929
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        856052 kB
Buffers:         34132 kB
Cached:         123068 kB
SwapCached:         84 kB
Active:          39020 kB
Inactive:       120828 kB
HighTotal:      131008 kB
HighFree:         4200 kB
LowTotal:       903652 kB
LowFree:        851852 kB
SwapTotal:     2097136 kB
SwapFree:      2096728 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5880 kB
Slab:            13112 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 10:18:59 (client local time) WITH STATUS 20 IN 537.331 SECONDS
stats: 23929 7 537.331 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...

Decision: 280/860	Time: 11.2203/86400
Decision: 280/860	Time: 11.7952/86400
Decision: 280/860	Time: 12.3781/86400
Decision: 280/860	Time: 12.999/86400
Decision: 280/860	Time: 13.7899/86400
Decision: 280/860	Time: 14.6188/86400
Decision: 280/860	Time: 15.4806/86400
Decision: 280/860	Time: 16.2955/86400
Decision: 280/860	Time: 17.2784/86400
Decision: 280/860	Time: 18.4122/86400
Decision: 280/860	Time: 19.508/86400
Decision: 280/860	Time: 20.7528/86400
Decision: 280/860	Time: 21.9837/86400
Decision: 280/860	Time: 23.2215/86400
Decision: 280/860	Time: 24.5293/86400
Decision: 280/860	Time: 25.9351/86400
Decision: 280/860	Time: 27.3888/86400
Decision: 280/860	Time: 28.7876/86400
Decision: 280/860	Time: 30.3964/86400
Decision: 280/860	Time: 32.0521/86400
Decision: 280/860	Time: 33.8149/86400
Decision: 280/860	Time: 35.6076/86400
Decision: 280/860	Time: 37.3373/86400
Decision: 280/860	Time: 39.275/86400
Decision: 280/860	Time: 41.2197/86400
Decision: 280/860	Time: 43.5104/86400
Decision: 280/860	Time: 45.6481/86400
Decision: 280/860	Time: 47.9597/86400
Decision: 280/860	Time: 50.1424/86400
Decision: 280/860	Time: 52.512/86400
Decision: 280/860	Time: 55.0976/86400
Decision: 280/860	Time: 57.4043/86400
Decision: 280/860	Time: 59.7179/86400
Decision: 280/860	Time: 62.0586/86400
Decision: 280/860	Time: 64.9081/86400
Decision: 280/860	Time: 67.1608/86400
Decision: 280/860	Time: 69.9074/86400
Decision: 280/860	Time: 72.339/86400
Decision: 280/860	Time: 74.9496/86400
Decision: 280/860	Time: 77.1093/86400
Decision: 280/860	Time: 79.7559/86400
Decision: 280/860	Time: 82.0935/86400
Decision: 280/860	Time: 84.5551/86400
Decision: 280/860	Time: 86.8438/86400
Decision: 280/860	Time: 89.0835/86400
Decision: 280/860	Time: 91.5201/86400
Decision: 280/860	Time: 93.6778/86400
Decision: 280/860	Time: 96.3743/86400
Decision: 280/860	Time: 99.1799/86400
Decision: 280/860	Time: 101.582/86400
Decision: 280/860	Time: 104.171/86400
Decision: 280/860	Time: 106.663/86400
Decision: 280/860	Time: 109.074/86400
Decision: 280/860	Time: 111.744/86400
Decision: 280/860	Time: 114.263/86400
Decision: 280/860	Time: 117.253/86400
Decision: 280/860	Time: 120.676/86400
Decision: 280/860	Time: 123.227/86400
Decision: 280/860	Time: 125.525/86400
Decision: 280/860	Time: 128.363/86400
Decision: 280/860	Time: 130.95/86400
Decision: 280/860	Time: 133.595/86400
Decision: 280/860	Time: 135.903/86400
Decision: 280/860	Time: 138.853/86400
Decision: 280/860	Time: 141.415/86400
Decision: 280/860	Time: 144.191/86400
Decision: 280/860	Time: 146.693/86400
Decision: 280/860	Time: 149.265/86400
Decision: 280/860	Time: 152.308/86400
Decision: 280/860	Time: 154.865/86400
Decision: 280/860	Time: 157.722/86400
Decision: 280/860	Time: 160.44/86400
Decision: 280/860	Time: 163.723/86400
Decision: 280/860	Time: 166.92/86400
Decision: 280/860	Time: 170.125/86400
Decision: 280/860	Time: 173.48/86400
Decision: 280/860	Time: 177.111/86400
Decision: 280/860	Time: 179.913/86400
Decision: 280/860	Time: 183.137/86400
Decision: 280/860	Time: 186.539/86400
Decision: 280/860	Time: 190.509/86400
Decision: 280/860	Time: 193.517/86400
Decision: 280/860	Time: 197.449/86400
Decision: 280/860	Time: 201.454/86400
Decision: 280/860	Time: 205.414/86400
Decision: 280/860	Time: 209.152/86400
Decision: 280/860	Time: 212.933/86400
Decision: 280/860	Time: 216.82/86400
Decision: 280/860	Time: 220.663/86400
Decision: 280/860	Time: 224.479/86400
Decision: 280/860	Time: 228.639/86400
Decision: 280/860	Time: 232.619/86400
Decision: 280/860	Time: 235.823/86400
Decision: 280/860	Time: 239.731/86400
Decision: 280/860	Time: 244.085/86400
Decision: 280/860	Time: 247.235/86400
Decision: 280/860	Time: 251.216/86400
Decision: 280/860	Time: 255.907/86400
Decision: 280/860	Time: 260.335/86400
Decision: 280/860	Time: 264.031/86400
Decision: 280/860	Time: 269.107/86400
Decision: 280/860	Time: 273.481/86400
Decision: 280/860	Time: 278.074/86400
Decision: 280/860	Time: 283.32/86400
Decision: 280/860	Time: 287.648/86400
Decision: 280/860	Time: 292.719/86400
Decision: 280/860	Time: 298.523/86400
Decision: 280/860	Time: 303.839/86400
Decision: 280/860	Time: 308.387/86400
Decision: 280/860	Time: 315.221/86400
Decision: 280/860	Time: 321.202/86400
Decision: 280/860	Time: 327.175/86400
Decision: 281/860	Time: 339.084/86400
Decision: 281/860	Time: 344.211/86400
Decision: 281/860	Time: 348.628/86400
Decision: 283/860	Time: 360.245/86400
Decision: 283/860	Time: 364.896/86400
Decision: 283/860	Time: 370.486/86400
Decision: 283/860	Time: 374.775/86400
Decision: 283/860	Time: 380.723/86400
Decision: 283/860	Time: 387.859/86400
Decision: 286/860	Time: 404.877/86400
Decision: 287/860	Time: 417.943/86400
Decision: 287/860	Time: 423.697/86400
Decision: 292/860	Time: 449.354/86400s UNSATISFIABLE
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Enforcing Stack size limit: 67108864 bytes
Raw data (loadavg): 0.07 0.02 0.00 2/54 20812
Raw data (stat): 20812 (runsolver) R 20811 15547 15546 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 805765780 884736 93 4294967295 134512640 135332820 3221224464 3221219872 134515228 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 93 205 205 0 11 0
vsize: 864
Current StackSize limit: 67108864 bytes
[startup+10.001 s]
Raw data (loadavg): 0.21 0.05 0.01 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 1041 0 0 0 996 3 0 0 25 0 1 0 805765780 6946816 981 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1696 981 300 300 0 1396 0
vsize: 6784
[startup+20.001 s]
Raw data (loadavg): 0.33 0.08 0.02 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 1761 0 0 0 1991 8 0 0 25 0 1 0 805765780 7864320 1701 4294967295 134512640 135726644 3221224576 3221223072 134744163 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1920 1701 300 300 0 1620 0
vsize: 7680
[startup+30.0095 s]
Raw data (loadavg): 0.44 0.11 0.03 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 2311 0 0 0 2988 11 0 0 25 0 1 0 805765780 13172736 2154 4294967295 134512640 135726644 3221224576 3221223072 134744156 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3216 2154 300 300 0 2916 0
vsize: 12864
[startup+40.0133 s]
Raw data (loadavg): 0.52 0.14 0.04 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 2689 0 0 0 3986 14 0 0 25 0 1 0 805765780 13893632 2532 4294967295 134512640 135726644 3221224576 3221223072 134744182 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3392 2532 300 300 0 3092 0
vsize: 13568
[startup+50.0177 s]
Raw data (loadavg): 0.60 0.16 0.05 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 2999 0 0 0 4983 16 0 0 25 0 1 0 805765780 14286848 2842 4294967295 134512640 135726644 3221224576 3221223200 134744588 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3488 2842 300 300 0 3188 0
vsize: 13952
[startup+60.019 s]
Raw data (loadavg): 0.66 0.19 0.06 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 3246 0 0 0 5982 18 0 0 25 0 1 0 805765780 14876672 3089 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3632 3089 300 300 0 3332 0
vsize: 14528
[startup+70.0194 s]
Raw data (loadavg): 0.71 0.22 0.07 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 3671 0 0 0 6979 21 0 0 25 0 1 0 805765780 15859712 3321 4294967295 134512640 135726644 3221224576 3221223072 134743975 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3872 3321 300 300 0 3572 0
vsize: 15488
[startup+80.0204 s]
Raw data (loadavg): 0.75 0.24 0.08 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 3795 0 0 0 7978 22 0 0 25 0 1 0 805765780 16056320 3445 4294967295 134512640 135726644 3221224576 3221223072 134743982 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3920 3445 300 300 0 3620 0
vsize: 15680
[startup+90.0203 s]
Raw data (loadavg): 0.79 0.27 0.09 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 3885 0 0 0 8977 23 0 0 25 0 1 0 805765780 24641536 3535 4294967295 134512640 135726644 3221224576 3221223072 134744156 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6016 3535 300 300 0 5716 0
vsize: 24064
[startup+100.02 s]
Raw data (loadavg): 0.82 0.29 0.10 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 4017 0 0 0 9976 25 0 0 25 0 1 0 805765780 24838144 3667 4294967295 134512640 135726644 3221224576 3221223072 134743987 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6064 3667 300 300 0 5764 0
vsize: 24256
[startup+110.021 s]
Raw data (loadavg): 0.85 0.31 0.11 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 4170 0 0 0 10974 26 0 0 25 0 1 0 805765780 25034752 3820 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6112 3820 300 300 0 5812 0
vsize: 24448
[startup+120.022 s]
Raw data (loadavg): 0.87 0.34 0.12 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 4367 0 0 0 11973 28 0 0 25 0 1 0 805765780 25235456 4017 4294967295 134512640 135726644 3221224576 3221223072 134744163 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6161 4017 300 300 0 5861 0
vsize: 24644
[startup+130.024 s]
Raw data (loadavg): 0.89 0.36 0.13 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 4520 0 0 0 12972 29 0 0 25 0 1 0 805765780 25235456 4170 4294967295 134512640 135726644 3221224576 3221223168 134760154 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6161 4170 300 300 0 5861 0
vsize: 24644
[startup+140.024 s]
Raw data (loadavg): 0.91 0.38 0.14 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 4577 0 0 0 13971 30 0 0 25 0 1 0 805765780 25370624 4227 4294967295 134512640 135726644 3221224576 3221223072 134743955 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6194 4227 300 300 0 5894 0
vsize: 24776
[startup+150.025 s]
Raw data (loadavg): 0.92 0.40 0.15 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 4699 0 0 0 14970 31 0 0 25 0 1 0 805765780 26046464 4349 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6359 4349 300 300 0 6059 0
vsize: 25436
[startup+160.025 s]
Raw data (loadavg): 0.93 0.42 0.15 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 4906 0 0 0 15968 33 0 0 25 0 1 0 805765780 26722304 4556 4294967295 134512640 135726644 3221224576 3221223072 134744140 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6524 4556 300 300 0 6224 0
vsize: 26096
[startup+170.025 s]
Raw data (loadavg): 0.94 0.44 0.16 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 5089 0 0 0 16967 34 0 0 25 0 1 0 805765780 27398144 4739 4294967295 134512640 135726644 3221224576 3221223088 134742599 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6689 4739 300 300 0 6389 0
vsize: 26756
[startup+180.027 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 5206 0 0 0 17966 35 0 0 25 0 1 0 805765780 27668480 4856 4294967295 134512640 135726644 3221224576 3221223072 134743955 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6755 4856 300 300 0 6455 0
vsize: 27020
[startup+190.028 s]
Raw data (loadavg): 0.96 0.47 0.18 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 5476 0 0 0 18964 36 0 0 25 0 1 0 805765780 28073984 5126 4294967295 134512640 135726644 3221224576 3221223072 134743975 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6854 5126 300 300 0 6554 0
vsize: 27416
[startup+200.027 s]
Raw data (loadavg): 0.96 0.49 0.19 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 5981 0 0 0 19962 38 0 0 25 0 1 0 805765780 29917184 5246 4294967295 134512640 135726644 3221224576 3221223144 134736573 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7304 5246 300 300 0 7004 0
vsize: 29216
[startup+210.028 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 6193 0 0 0 20961 39 0 0 25 0 1 0 805765780 30187520 5458 4294967295 134512640 135726644 3221224576 3221223072 134743955 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7370 5458 300 300 0 7070 0
vsize: 29480
[startup+220.029 s]
Raw data (loadavg): 0.97 0.52 0.20 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 6288 0 0 0 21960 41 0 0 25 0 1 0 805765780 30187520 5553 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7370 5553 300 300 0 7070 0
vsize: 29480
[startup+230.029 s]
Raw data (loadavg): 0.98 0.54 0.21 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 6458 0 0 0 22959 41 0 0 25 0 1 0 805765780 30322688 5723 4294967295 134512640 135726644 3221224576 3221223072 134744169 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7403 5723 300 300 0 7103 0
vsize: 29612
[startup+240.029 s]
Raw data (loadavg): 0.98 0.55 0.22 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 6477 0 0 0 23959 42 0 0 25 0 1 0 805765780 30322688 5742 4294967295 134512640 135726644 3221224576 3221223072 134743955 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7403 5742 300 300 0 7103 0
vsize: 29612
[startup+250.029 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 6528 0 0 0 24958 43 0 0 25 0 1 0 805765780 30457856 5793 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7436 5793 300 300 0 7136 0
vsize: 29744
[startup+260.029 s]
Raw data (loadavg): 0.98 0.58 0.24 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 6549 0 0 0 25957 44 0 0 25 0 1 0 805765780 30457856 5814 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7436 5814 300 300 0 7136 0
vsize: 29744
[startup+270.029 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 6647 0 0 0 26957 44 0 0 25 0 1 0 805765780 30457856 5912 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7436 5912 300 300 0 7136 0
vsize: 29744
[startup+280.03 s]
Raw data (loadavg): 0.99 0.61 0.25 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 6662 0 0 0 27955 46 0 0 25 0 1 0 805765780 30457856 5927 4294967295 134512640 135726644 3221224576 3221223072 134744163 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7436 5927 300 300 0 7136 0
vsize: 29744
[startup+290.03 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 6821 0 0 0 28954 48 0 0 25 0 1 0 805765780 30728192 6086 4294967295 134512640 135726644 3221224576 3221223072 134744163 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7502 6086 300 300 0 7202 0
vsize: 30008
[startup+300.031 s]
Raw data (loadavg): 0.99 0.63 0.27 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 6945 0 0 0 29953 49 0 0 25 0 1 0 805765780 30863360 6210 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7535 6210 300 300 0 7235 0
vsize: 30140
[startup+310.031 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 7080 0 0 0 30952 50 0 0 25 0 1 0 805765780 30863360 6345 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7535 6345 300 300 0 7235 0
vsize: 30140
[startup+320.031 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 7218 0 0 0 31951 51 0 0 25 0 1 0 805765780 30863360 6483 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7535 6483 300 300 0 7235 0
vsize: 30140
[startup+330.031 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 7261 0 0 0 32950 51 0 0 25 0 1 0 805765780 30998528 6526 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7568 6526 300 300 0 7268 0
vsize: 30272
[startup+340.031 s]
Raw data (loadavg): 0.99 0.67 0.30 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 7332 0 0 0 33950 52 0 0 25 0 1 0 805765780 31268864 6597 4294967295 134512640 135726644 3221224576 3221223072 134744174 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7634 6597 300 300 0 7334 0
vsize: 30536
[startup+350.031 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 7493 0 0 0 34949 53 0 0 25 0 1 0 805765780 31268864 6758 4294967295 134512640 135726644 3221224576 3221223072 134744163 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7634 6758 300 300 0 7334 0
vsize: 30536
[startup+360.032 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 7638 0 0 0 35948 54 0 0 25 0 1 0 805765780 31404032 6903 4294967295 134512640 135726644 3221224576 3221223200 134779426 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7667 6903 300 300 0 7367 0
vsize: 30668
[startup+370.032 s]
Raw data (loadavg): 0.99 0.70 0.32 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 7651 0 0 0 36947 55 0 0 25 0 1 0 805765780 31404032 6916 4294967295 134512640 135726644 3221224576 3221223072 134744159 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7667 6916 300 300 0 7367 0
vsize: 30668
[startup+380.031 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 7665 0 0 0 37947 56 0 0 25 0 1 0 805765780 31404032 6930 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7667 6930 300 300 0 7367 0
vsize: 30668
[startup+390.031 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 7756 0 0 0 38946 56 0 0 25 0 1 0 805765780 31944704 7021 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7799 7021 300 300 0 7499 0
vsize: 31196
[startup+400.032 s]
Raw data (loadavg): 0.99 0.73 0.34 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 7774 0 0 0 39946 57 0 0 25 0 1 0 805765780 31944704 7039 4294967295 134512640 135726644 3221224576 3221223072 134744140 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7799 7039 300 300 0 7499 0
vsize: 31196
[startup+410.032 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 7870 0 0 0 40945 58 0 0 25 0 1 0 805765780 48992256 7135 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11961 7135 300 300 0 11661 0
vsize: 47844
[startup+420.032 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 7993 0 0 0 41944 59 0 0 25 0 1 0 805765780 48992256 7258 4294967295 134512640 135726644 3221224576 3221223072 134743975 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11961 7258 300 300 0 11661 0
vsize: 47844
[startup+430.033 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 8105 0 0 0 42943 60 0 0 25 0 1 0 805765780 48992256 7370 4294967295 134512640 135726644 3221224576 3221223072 134744220 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11961 7370 300 300 0 11661 0
vsize: 47844
[startup+440.033 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 8205 0 0 0 43942 62 0 0 25 0 1 0 805765780 48992256 7470 4294967295 134512640 135726644 3221224576 3221223072 134744147 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11961 7470 300 300 0 11661 0
vsize: 47844
[startup+450.033 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 8326 0 0 0 44941 63 0 0 25 0 1 0 805765780 48992256 7591 4294967295 134512640 135726644 3221224576 3221223072 134744235 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11961 7591 300 300 0 11661 0
vsize: 47844
[startup+460.033 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 8430 0 0 0 45939 64 0 0 25 0 1 0 805765780 48992256 7695 4294967295 134512640 135726644 3221224576 3221223072 134744290 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11961 7695 300 300 0 11661 0
vsize: 47844
[startup+470.033 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 8556 0 0 0 46938 65 0 0 25 0 1 0 805765780 48992256 7821 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11961 7821 300 300 0 11661 0
vsize: 47844
[startup+480.034 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 8681 0 0 0 47938 66 0 0 25 0 1 0 805765780 49127424 7946 4294967295 134512640 135726644 3221224576 3221223072 134744147 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11994 7946 300 300 0 11694 0
vsize: 47976
[startup+490.034 s]
Raw data (loadavg): 0.99 0.80 0.39 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 8789 0 0 0 48937 67 0 0 25 0 1 0 805765780 49127424 8054 4294967295 134512640 135726644 3221224576 3221223072 134744159 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11994 8054 300 300 0 11694 0
vsize: 47976
[startup+500.034 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 8909 0 0 0 49936 68 0 0 25 0 1 0 805765780 49127424 8174 4294967295 134512640 135726644 3221224576 3221223072 134743982 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11994 8174 300 300 0 11694 0
vsize: 47976
[startup+510.035 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 9030 0 0 0 50936 68 0 0 25 0 1 0 805765780 49127424 8295 4294967295 134512640 135726644 3221224576 3221223072 134744223 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11994 8295 300 300 0 11694 0
vsize: 47976
[startup+520.036 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 9132 0 0 0 51936 69 0 0 25 0 1 0 805765780 49127424 8397 4294967295 134512640 135726644 3221224576 3221223072 134743955 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11994 8397 300 300 0 11694 0
vsize: 47976
[startup+530.035 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 9250 0 0 0 52935 70 0 0 25 0 1 0 805765780 49397760 8515 4294967295 134512640 135726644 3221224576 3221223072 134743982 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12060 8515 300 300 0 11760 0
vsize: 48240
[startup+537.313 s]
Raw data (loadavg): 0.99 0.83 0.42 1/53 20812
Raw data (stat): 20812 (pb2sat) R 20811 15547 15546 0 -1 0 9250 0 0 0 52935 70 0 0 25 0 1 0 805765780 49397760 8515 4294967295 134512640 135726644 3221224576 3221223072 134743982 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12060 8515 300 300 0 11760 0
vsize: 0

Child status: 20
Real time (s): 537.312
CPU time (s): 537.331
CPU user time (s): 536.603
CPU system time (s): 0.727889
CPU usage (%): 100.004
Max. virtual memory (Kb): 48240
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####