Some explanations
A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process.
The trace of the execution of a solver is divided in four parts:
-
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
-
SOLVER DATA
This is the output of the solver (stdout and stderr).
-
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver.
The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
-
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark
| Name | normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ws97-3.opb |
| MD5SUM | 77c89bda49ebcdc0428e1292512864a9 |
| Bench Category | optimization, medium integers (OPTMEDINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 3080 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 2792 |
| Biggest coefficient in the objective function | 1000 |
| Number of bits for the biggest coefficient in the objective function | 10 |
| Sum of the numbers in the objective function | 1385986 |
| Number of bits of the sum of numbers in the objective function | 21 |
| Biggest number in a constraint | 1000 |
| Number of bits of the biggest number in a constraint | 10 |
| Biggest sum of numbers in a constraint | 1385986 |
| Number of bits of the biggest sum of numbers | 21 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1.07184 |
| Number of variables | 3300 |
| Total number of constraints | 5284 |
| Number of constraints which are clauses | 1364 |
| Number of constraints which are cardinality constraints (but not clauses) | 3920 |
| Number of constraints which are nor clauses,nor cardinality constraints | 0 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 220 |
Trace number 33829
#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-05-27 16:46:09 (client local time)
PB2005-SCRIPT v4.0
MARKUPS: idlaunch=3212 boxname=wulflinc5 idbench=357 idsolver=8 numberseed=0
MD5SUM SOLVER: 4b637b3b6117f2add1a6288e91336322 /oldhome/oroussel/solvers/vallstSAT2005PB.sh
MD5SUM BENCH: 77c89bda49ebcdc0428e1292512864a9 /oldhome/oroussel/tmp/wulflinc5/normalized-ws97-3.opb
REAL COMMAND: vallstSAT2005PB.sh /oldhome/oroussel/tmp/wulflinc5/normalized-ws97-3.opb 0
IDLAUNCH: 3212
/proc/cpuinfo:
processor : 0
vendor_id : GenuineIntel
cpu family : 6
model : 7
model name : Pentium III (Katmai)
stepping : 2
cpu MHz : 451.007
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.007
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: 691908 kB
Buffers: 28828 kB
Cached: 293568 kB
SwapCached: 672 kB
Active: 58388 kB
Inactive: 266116 kB
HighTotal: 131008 kB
HighFree: 252 kB
LowTotal: 903652 kB
LowFree: 691656 kB
SwapTotal: 2097136 kB
SwapFree: 2095608 kB
Dirty: 1772 kB
Writeback: 0 kB
Mapped: 5112 kB
Slab: 12640 kB
Committed_AS: 63604 kB
PageTables: 316 kB
VmallocTotal: 114680 kB
VmallocUsed: 1364 kB
VmallocChunk: 113256 kB
JOB ENDED THE 2005-05-27 17:06:41 (client local time) WITH STATUS 10 IN 1231.04 SECONDS
stats: 3212 6 1231.04 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
1:
seed: 0
Nr of vars set: 0 (#equs: 0)
Nr of vars set: 0 (#equs: 0)
#decisions: 11038; #end-nodes: 80;
#proof improvement attempts: 0; #restarts: 1
Current batch, end-nodes: 0 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
result: model found (1)
Model found with constant: 1159850 (226135:>=*);
#decisions: 2241; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1160850 (225135:>=*);
#decisions: 2241; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1161851 (224134:>=*);
#decisions: 2262; #end-nodes: 23;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 23 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1162850 (223135:>=*);
#decisions: 2238; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1162851 (223134:>=*);
#decisions: 2262; #end-nodes: 26;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 26 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1163851 (222134:>=*);
#decisions: 2236; #end-nodes: 7;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 7 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1163852 (222133:>=*);
#decisions: 2257; #end-nodes: 20;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 20 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1164852 (221133:>=*);
#decisions: 2228; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1164853 (221132:>=*);
#decisions: 2238; #end-nodes: 6;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 6 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1165852 (220133:>=*);
#decisions: 2227; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1165853 (220132:>=*);
#decisions: 2254; #end-nodes: 27;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 27 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1165854 (220131:>=*);
#decisions: 2285; #end-nodes: 45;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 45 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1165855 (220130:>=*);
#decisions: 5342; #end-nodes: 159;
#proof improvement attempts: 0; #restarts: 1
Current batch, end-nodes: 79 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1165858 (220127:>=*);
#decisions: 2167; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1165859 (220126:>=*);
#decisions: 23160; #end-nodes: 557;
#proof improvement attempts: 0; #restarts: 6
Current batch, end-nodes: 74 / 81 (81)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1166852 (219133:>=*);
#decisions: 2220; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1166853 (219132:>=*);
#decisions: 2561; #end-nodes: 50;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 50 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1167855 (218130:>=*);
#decisions: 7991; #end-nodes: 179;
#proof improvement attempts: 0; #restarts: 2
Current batch, end-nodes: 19 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1167861 (218124:>=*);
#decisions: 2291; #end-nodes: 72;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 72 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1168859 (217126:>=*);
#decisions: 2191; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1168860 (217125:>=*);
#decisions: 2193; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1168861 (217124:>=*);
#decisions: 20113; #end-nodes: 334;
#proof improvement attempts: 0; #restarts: 4
Current batch, end-nodes: 13 / 81 (81)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1169850 (216135:>=*);
#decisions: 2402; #end-nodes: 42;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 42 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1169851 (216134:>=*);
#decisions: 2393; #end-nodes: 38;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 38 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1169852 (216133:>=*);
#decisions: 2380; #end-nodes: 36;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 36 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1169853 (216132:>=*);
#decisions: 84736; #end-nodes: 1393;
#proof improvement attempts: 0; #restarts: 17
Current batch, end-nodes: 0 / 84 (84)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1172855 (213130:>=*);
#decisions: 2233; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1172856 (213129:>=*);
#decisions: 2232; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1172857 (213128:>=*);
#decisions: 2235; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1173857 (212128:>=*);
#decisions: 2234; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1173858 (212127:>=*);
#decisions: 2234; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1173859 (212126:>=*);
#decisions: 2273; #end-nodes: 34;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 34 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1174859 (211126:>=*);
#decisions: 2244; #end-nodes: 8;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 8 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1174860 (211125:>=*);
#decisions: 746672; #end-nodes: 14502;
#proof improvement attempts: 0; #restarts: 147
Current batch, end-nodes: 53 / 116 (116)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1175852 (210133:>=*);
#decisions: 51576; #end-nodes: 918;
#proof improvement attempts: 0; #restarts: 11
Current batch, end-nodes: 26 / 82 (82)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1175853 (210132:>=*);
#decisions: 2077; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1175854 (210131:>=*);
#decisions: 2101; #end-nodes: 19;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 19 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1175855 (210130:>=*);
#decisions: 48166; #end-nodes: 919;
#proof improvement attempts: 0; #restarts: 11
Current batch, end-nodes: 24 / 82 (82)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1175863 (210122:>=*);
#decisions: 2216; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1175864 (210121:>=*);
#decisions: 2213; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1175865 (210120:>=*);
#decisions: 2219; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1175866 (210119:>=*);
#decisions: 2293; #end-nodes: 52;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 52 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1175867 (210118:>=*);
#decisions: 104930; #end-nodes: 2074;
#proof improvement attempts: 0; #restarts: 25
Current batch, end-nodes: 0 / 86 (86)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1179859 (206126:>=*);
#decisions: 742376; #end-nodes: 14712;
#proof improvement attempts: 0; #restarts: 149
Current batch, end-nodes: 21 / 117 (117)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1179869 (206116:>=*);
#decisions: 2271; #end-nodes: 44;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 44 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1179870 (206115:>=*);
#decisions: 1297727; #end-nodes: 28126;
#proof improvement attempts: 0; #restarts: 252
Current batch, end-nodes: 57 / 143 (143)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1179871 (206114:>=*);
#decisions: 2331; #end-nodes: 52;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 52 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1179872 (206113:>=*);
#decisions: 2267; #end-nodes: 15;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 15 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1180872 (205113:>=*);
#decisions: 1898587; #end-nodes: 46553;
#proof improvement attempts: 0; #restarts: 369
Current batch, end-nodes: 51 / 172 (172)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1181858 (204127:>=*);
#decisions: 2160; #end-nodes: 10;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 10 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1181859 (204126:>=*);
#decisions: 2158; #end-nodes: 6;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 6 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1181860 (204125:>=*);
#decisions: 2194; #end-nodes: 26;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 26 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1182860 (203125:>=*);
#decisions: 2159; #end-nodes: 7;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 7 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1182861 (203124:>=*);
#decisions: 75756; #end-nodes: 1729;
#proof improvement attempts: 0; #restarts: 21
Current batch, end-nodes: 0 / 85 (85)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1183865 (202120:>=*);
#decisions: 2202; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1184866 (201119:>=*);
#decisions: 2210; #end-nodes: 9;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 9 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1184867 (201118:>=*);
#decisions: 2203; #end-nodes: 8;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 8 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1185867 (200118:>=*);
#decisions: 4075212; #end-nodes: 104483;
#proof improvement attempts: 0; #restarts: 649
Current batch, end-nodes: 5 / 242 (242)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1186864 (199121:>=*);
#decisions: 3115661; #end-nodes: 88629;
#proof improvement attempts: 0; #restarts: 581
Current batch, end-nodes: 43 / 225 (225)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1186865 (199120:>=*);
#decisions: 4942833; #end-nodes: 124914;
#proof improvement attempts: 0; #restarts: 729
Current batch, end-nodes: 257 / 262 (262)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1187862 (198123:>=*);
#decisions: 2219; #end-nodes: 10;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 10 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1187863 (198122:>=*);
#decisions: 2263; #end-nodes: 37;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 37 / 80 (80)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant: 1187864 (198121:>=*);
Interupt request received.
#decisions: 17802933; #end-nodes: 682227;
#proof improvement attempts: 0; #restarts: 2038
Current batch, end-nodes: 376 / 589 (589)
#axs: 2573, #non-axs: 0
tight: meta-meta: start: 6, end: 9; meta: start: 12, end (keep): 23
loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50
Model found with constant:
(pushed:) 1187864 (198121:>=*)
No proof was found though that an increment of the
last pushed constraint doesn't have a model.
result: an interupt signal has been received (3)
seed: 0
Nr of vars set: 3006 (#equs: 0)
Time taken: 20 min, 29 sec
times:
0m0.018s 0m0.011s
19m10.141s 1m19.748s
v -v861 -v1081 -v1741 v2994 -v2 v432 -v862 -v1082 -v1302 -v2842 v2995 -v3148 -v3 -v863 v1083 -v4 v219 -v864 -v1084 -v1524 -v2996 v3149 v5 -v865 -v1085 -v1745 v2997 -v6 v221 -v651 -v866 -v1086 -v1526 -v1746 v1966 v2998 -v3151 -v7 -v222 v652 -v867 -v1087 -v1527 -v1747 -v1967 v2999 -v3152 v8 -v223 -v868 -v1088 v1528 -v2188 -v2408 -v2628 v3000 -v3153 -v869 -v1529 -v2848 v3001 -v3154 v224 -v439 -v654 -v1310 -v1530 -v1750 v1970 v225 -v440 -v871 -v1091 v1311 -v1531 -v1751 -v2849 v3002 v226 -v441 -v1312 -v1532 -v1752 v2850 v442 -v657 -v1313 v1973 -v2851 -v13 -v228 -v874 -v1094 -v1754 -v3005 -v229 v659 v1535 -v1975 -v2635 -v446 -v877 -v1097 v1317 -v1757 -v2854 v3007 -v1758 -v17 v232 -v662 -v879 -v1099 -v1539 -v1759 -v1979 -v3008 v3161 -v233 -v663 -v880 -v1100 -v1540 -v1760 v1980 -v3009 -v19 -v881 -v1101 -v2201 -v3010 v3163 -v665 -v882 -v1102 -v1982 v21 -v451 -v883 v1103 -v1323 v2858 -v3011 -v3164 v237 -v1544 -v2424 -v23 -v2205 v24 -v239 -v454 -v886 -v1106 v1326 -v1546 -v2860 v3013 -v3166 v455 -v1327 -v1767 v456 -v1328 -v1768 -v27 v242 -v889 -v1109 -v1549 v3014 -v3167 -v28 v243 -v890 -v1110 -v1550 -v3015 v3168 v244 -v891 v1111 -v1551 -v2431 -v3016 -v30 -v245 v460 -v892 -v1112 -v1332 v1552 -v2864 -v3017 v3170 v462 -v1334 -v1774 -v248 v895 -v1115 -v1555 -v34 -v249 v464 -v896 -v1116 -v1336 v1556 -v2865 -v3018 v3171 -v35 v897 -v1117 -v36 v251 -v466 -v898 v1118 -v1338 -v1778 v2866 -v3019 -v3172 v682 -v1779 -v1999 -v38 -v900 -v1120 -v2440 -v3020 v3173 -v39 -v901 -v1121 -v2221 v2441 -v2661 v3021 -v3174 -v40 v255 -v1562 -v41 -v256 -v1563 -v2663 v3175 -v42 -v904 -v1124 -v2444 v3023 -v3176 -v43 v258 -v1565 -v259 -v906 -v1126 -v1566 -v45 -v260 -v907 -v1127 v1567 -v3024 v3177 v46 -v908 -v1128 -v47 -v909 -v1129 -v48 -v693 -v910 -v1130 v2010 -v49 v264 -v694 -v911 -v1131 -v1571 v1791 -v2011 v3025 -v3178 -v50 -v265 v695 -v912 -v1132 -v1572 -v1792 -v2012 -v3026 v3179 v266 -v913 -v1133 -v1573 -v1793 -v52 -v267 v697 -v914 -v1134 v1574 -v1794 -v2014 -v698 -v1795 -v2015 -v54 v699 v916 -v1136 -v1796 -v2016 -v3027 -v3180 -v485 -v700 -v1357 -v2017 -v2457 -v2677 v2875 v486 -v701 -v918 -v1138 -v1358 v1798 -v2018 -v2876 -v3029 v272 -v1579 -v2459 -v703 -v920 -v1140 -v2020 -v2680 v3030 v704 -v1801 -v2021 -v490 -v922 -v1142 -v1362 v1802 -v2878 -v3031 -v276 -v491 -v1363 -v1583 v1803 v2879 v277 -v492 -v707 v924 -v1144 -v1364 -v1584 -v1804 -v2024 v2880 -v3033 -v278 -v925 -v1145 -v1585 v1805 -v3034 -v64 -v926 -v1146 -v495 -v927 -v1147 -v1367 -v1807 -v2882 v3035 -v928 -v1148 -v2028 -v3036 v3189 v281 -v711 -v929 v1149 -v1589 -v2029 -v3037 v282 -v930 v1150 -v1590 -v1810 -v3038 -v713 -v931 -v1151 -v1811 v2031 -v2471 -v2691 -v3039 -v69 v932 -v1152 -v2692 -v3040 v3193 v500 -v933 -v1153 -v1373 v1813 -v2473 -v2693 -v2888 v3041 -v71 -v286 -v1154 -v1374 -v1594 -v1814 v2889 -v3042 -v3195 -v72 v935 -v1155 -v2695 -v3043 -v3196 -v73 -v503 -v936 -v1156 -v1376 v2891 -v3044 -v3197 -v719 -v937 -v1157 -v1817 -v2037 -v3045 v720 -v938 -v1158 -v2038 v2258 -v2478 -v2698 -v3046 -v291 v939 -v1159 -v1599 -v1819 -v2259 -v2479 -v2699 -v3047 -v77 -v292 -v507 v940 -v1160 -v1380 -v1600 v2895 -v3048 -v3201 -v508 -v941 -v1161 -v1381 -v2261 v2896 -v3049 -v79 -v509 v724 -v942 -v1162 -v1382 -v2042 -v2703 v3203 -v510 v725 -v944 -v1164 -v1384 -v2044 -v2898 -v3051 v81 -v296 -v945 -v1165 -v1605 -v2705 v82 -v946 -v1166 -v1386 -v3052 -v3205 -v83 v2707 v299 v948 -v1168 -v1608 -v2268 -v2488 -v3053 -v300 -v515 -v1389 -v1609 -v1829 -v2901 -v301 v516 -v950 v1170 -v1390 -v1610 -v87 -v732 -v951 -v1171 -v2051 -v3055 v3208 -v88 -v303 v518 -v952 -v1172 -v1392 -v1612 -v2712 -v89 v519 -v1393 v520 -v954 v1174 -v1394 -v306 v521 -v1395 v1615 -v1835 -v2903 -v92 -v307 v1176 -v1396 -v1616 -v1836 v2904 -v3057 -v3210 -v93 v308 -v523 -v957 -v1617 -v2057 -v2905 -v3058 -v94 -v958 -v1178 -v2498 -v3059 v3212 -v95 v310 -v740 -v959 -v1179 -v1619 v1839 -v2059 v3060 -v3213 v741 -v960 -v1180 -v2060 v3061 -v97 -v312 -v527 -v961 -v1181 -v1401 -v1621 -v2909 -v3062 v3215 v98 -v528 -v743 -v962 -v1182 -v1402 -v2062 -v314 -v529 v963 -v1183 -v1403 -v1623 -v1843 v2910 -v3063 v100 -v315 -v530 -v964 -v1404 -v1624 v2911 -v3064 -v3217 -v316 v531 -v965 -v1185 -v1405 -v1625 -v2912 -v3065 v3218 -v532 -v747 -v1406 -v2066 v2913 -v318 -v967 v1187 -v1627 -v1847 -v3067 -v319 -v534 -v749 -v1408 -v1628 -v1848 -v2068 v2915 -v535 -v750 -v1409 -v1849 -v2069 -v2729 v106 -v751 -v970 -v1190 -v1850 -v2070 -v322 -v537 -v1411 -v1631 -v1851 v2731 -v2916 v108 v972 -v1192 -v2292 -v2512 -v2732 -v109 v324 -v539 -v973 -v1193 -v1413 -v1633 -v1853 v2917 -v3070 -v3223 -v325 -v974 -v1194 -v1634 -v756 -v975 -v1195 -v1855 -v2075 -v3071 -v327 -v542 -v976 -v1196 -v1416 -v1636 v2919 -v3072 -v758 -v977 -v1197 -v2077 v114 -v329 -v544 -v978 -v1198 -v1418 -v1638 v2920 -v3073 -v3226 -v115 -v330 -v979 -v1199 -v1419 -v1639 -v2921 -v3074 v3227 -v116 -v331 -v546 -v980 -v1200 -v1420 -v1640 v2922 -v3075 -v3228 -v117 v547 -v762 -v981 -v1201 -v1421 -v2081 -v2923 -v3076 v3229 -v333 -v1642 -v119 v549 -v764 -v983 -v1203 -v1423 -v2083 -v2924 v3077 -v3230 v120 -v550 -v765 v984 -v1204 -v1424 -v2084 v2925 -v3078 -v3231 -v121 -v336 -v551 v766 -v985 -v1205 -v1425 -v1645 -v1865 -v2085 v2926 -v3079 -v3232 v122 -v552 -v767 -v986 -v1206 -v1426 -v2086 v2927 -v3080 -v3233 -v768 -v987 -v1207 -v1867 -v2087 -v3081 -v124 -v988 -v1208 v3082 -v3235 -v340 v770 -v989 -v1209 -v1649 -v1869 -v2089 -v3083 -v126 -v990 -v1210 -v1870 -v2090 -v2530 -v2750 -v3084 v3237 v557 -v991 -v1211 -v1431 -v2311 -v2932 -v3085 -v128 -v343 -v3239 v129 -v344 -v993 -v1213 -v1653 -v3087 -v3240 v130 -v345 -v560 -v1434 -v1874 v2935 -v3241 -v995 v1215 -v1875 -v2755 -v3089 -v347 -v562 -v777 v1436 -v1656 -v1876 -v2096 -v348 -v563 -v778 -v1437 -v1657 -v1877 -v2097 -v998 -v1218 -v1878 -v2758 -v3090 -v135 -v780 -v999 -v1219 v2099 -v2938 -v3091 v3244 -v136 -v566 -v1000 -v1220 -v1440 v2939 -v3092 -v3245 -v782 -v1001 -v1221 -v1881 -v2101 v3093 -v783 v1002 -v1222 -v1882 -v2102 -v2762 -v354 -v784 -v1663 -v1883 -v2103 v355 -v570 -v785 v1444 -v1664 -v1884 -v2104 -v356 -v571 -v786 -v1445 v1665 -v1885 -v2105 -v142 -v357 v787 -v1006 -v1226 -v1666 -v1886 -v2106 v3094 -v3247 -v143 -v358 v788 -v1007 -v1227 -v1667 -v1887 -v2107 -v3095 -v3248 -v359 -v1008 -v1228 -v1668 v145 -v575 -v1009 -v1229 -v1449 v2943 -v3096 -v3249 v146 -v361 -v576 -v1010 v1230 -v1450 -v1670 v2944 -v3097 -v3250 -v362 -v792 -v1011 v1231 -v1671 -v1891 -v2111 -v3098 -v148 -v2772 v3252 -v2553 -v2773 -v149 v364 -v794 -v1014 -v1234 -v1674 -v1894 -v2114 -v3100 -v3253 -v795 v2115 -v2556 -v2776 -v1017 -v1237 -v151 v366 -v581 v797 -v2118 v2558 -v368 -v1019 -v1239 -v1679 v154 -v2340 -v370 v1021 -v1241 -v1681 -v156 -v586 v1022 -v1242 -v1462 v2950 -v3103 -v3256 v372 -v587 -v802 -v1463 -v1683 -v1903 -v2123 -v2951 -v373 -v588 v803 -v1024 -v1244 -v1464 -v1684 -v1904 -v2124 -v2952 v3105 v159 -v374 -v589 v1025 -v1245 -v1465 -v1685 -v2785 -v160 -v590 v805 -v1026 v1246 -v1466 -v2126 v2953 -v3106 -v3259 -v161 v1027 -v1247 -v1907 -v3107 v3260 v162 -v592 -v1028 -v1248 -v1468 v2955 -v3108 -v3261 -v163 -v378 v808 -v1029 v1249 -v1689 -v1909 -v2129 -v3109 v3262 v164 -v1030 -v1250 -v1910 -v3110 -v3263 v810 -v1031 -v1251 -v2131 -v2571 -v3111 -v1912 -v166 -v596 -v1033 v1253 -v1473 -v2959 -v3112 v3265 -v167 -v382 v812 -v1034 -v1254 v1694 -v1914 -v2134 -v3113 v3266 v813 -v1915 -v2135 -v169 v599 -v1036 -v1256 -v1476 -v2961 v3114 -v3267 v170 -v2797 -v171 -v1038 -v1258 -v2798 v3115 -v3268 -v172 -v387 -v1039 v1259 -v1919 -v3116 -v173 -v388 -v603 v1040 -v1260 -v1480 -v1700 v2964 -v3117 -v3270 -v174 -v389 -v1041 -v1261 -v1481 -v1701 -v390 -v1702 -v1922 -v176 -v391 -v1703 v3271 -v392 -v1704 -v1924 -v1925 v178 -v393 -v608 -v1046 -v1266 -v1486 -v1706 -v1926 v2966 -v3119 -v3272 v179 -v1047 -v1267 -v2807 -v3120 -v3273 -v180 -v395 -v610 v825 -v1488 -v1708 -v2148 -v2968 -v3274 -v396 -v611 -v1049 -v1269 -v1489 v1709 v2969 -v3122 v2370 -v2810 v398 -v1051 -v1271 -v1711 v184 -v399 -v829 -v1712 -v1932 -v2152 v615 -v830 -v1493 -v2153 -v2593 v2813 -v2970 -v186 v616 -v1494 -v2594 -v2971 v3277 -v403 -v1056 -v1276 -v1716 -v1936 v3125 -v189 -v2377 -v405 -v620 -v835 -v1058 -v1278 -v1498 -v1718 -v2158 v2973 -v3126 v621 -v1059 -v1279 -v1499 -v1939 -v2974 -v3127 -v837 v3128 v408 -v1060 -v1280 -v1720 -v2600 -v2820 v3129 -v839 -v1061 -v1281 -v1941 -v2161 v2601 -v2821 v3130 v195 -v1062 -v1282 -v1503 v2163 -v196 -v1944 v197 -v627 -v842 -v1065 -v1285 -v1505 -v2165 v2978 -v3131 -v3284 v413 -v1066 -v1286 -v1726 v1946 -v2606 -v3132 -v414 -v629 -v2980 -v200 -v415 v630 -v1067 -v1287 -v1507 -v1727 -v2981 -v3134 v3287 -v201 v631 -v1068 -v1288 -v1508 -v2982 v3135 -v3288 -v202 -v1069 -v1289 -v2829 -v3136 -v3289 -v203 -v633 -v848 v1070 -v1290 -v1510 -v2170 -v2984 -v3137 v3290 -v419 -v1071 -v1291 -v1731 v1951 -v3138 -v420 -v1732 -v851 -v1073 -v1293 -v1953 -v2173 -v1074 -v1294 -v3139 -v422 -v1075 -v1295 -v1955 -v2615 -v2835 v3140 -v423 -v1076 -v1296 -v2616 -v2836 v3141 -v1517 -v2177 -v424 v1078 -v1298 -v1738 -v1958 -v3142 -v211 -v426 v3143 -v3296 -v427 -v213 v428 -v643 -v1079 -v1299 -v1519 -v1739 -v2991 -v3144 v3297 -v214 v429 -v644 -v1080 -v1300 -v1520 -v1740 -v2992 -v3145 v3298 -v645 v860 -v2993 -v216 v1521 -v2181 -v2401 -v2621 -v217 -v647 -v1522 -v1742 v1962 -v2182 -v2402 -v2622 -v2183 -v2403 -v2623 -v434 -v649 -v1304 -v1744 v1964 -v2184 -v2404 -v2624 -v2843 -v220 -v650 -v1525 -v1965 -v2185 -v2405 -v2625 -v2186 -v2406 -v2626 -v2187 -v2407 -v2627 -v438 -v653 -v1308 -v1748 -v1968 -v2847 -v2189 -v2409 -v2629 -v2190 -v2410 -v2630 -v11 -v872 -v1092 -v2192 -v2412 -v2632 -v3003 -v3156 -v12 -v227 -v873 -v1093 -v1533 -v1753 -v2193 -v2413 -v2633 v3004 -v3157 v658 -v1974 -v2194 -v2414 -v2634 -v444 -v875 -v1095 -v1315 -v1755 -v2195 -v2415 -v15 -v2196 -v2416 -v2636 -v3159 -v16 -v231 v661 -v1537 -v1977 -v2197 -v3160 -v878 -v1098 v1318 -v1538 -v1978 -v2198 -v2418 -v2638 -v447 v1319 -v2199 -v2419 -v2639 -v2855 v18 -v448 -v1320 -v2200 -v2420 -v2640 v2856 -v3162 -v234 v449 -v664 -v1321 -v1541 -v1761 v1981 -v2421 -v2641 -v2857 v20 -v235 -v450 v1322 -v1542 -v1762 -v2202 -v2422 -v2642 -v236 -v666 -v1543 -v1763 -v1983 -v2203 -v2423 -v2643 -v22 -v452 -v1324 -v2204 -v2859 -v3165 -v238 -v668 -v885 v1105 -v1545 -v1765 -v1985 -v2425 -v2645 -v669 -v1766 -v1986 -v2206 -v2426 -v2646 -v25 -v2207 -v2427 -v26 -v2208 -v2428 -v457 -v672 -v1329 v1769 -v1989 -v2209 -v2429 -v2649 -v2861 -v458 -v673 v1330 -v1770 -v1990 -v2210 -v2430 -v2650 -v2862 -v459 -v674 -v1331 -v1991 -v2863 -v675 -v1772 -v1992 -v2212 -v2432 -v2652 -v32 -v247 -v677 -v894 v1114 -v1554 -v1994 -v2214 -v2434 -v2654 -v33 -v463 v678 -v1335 -v1775 -v1995 -v2215 -v2435 -v2655 -v2216 -v2436 -v2656 -v250 -v465 v680 -v1337 -v1557 -v1777 -v1997 -v2217 -v2437 -v2657 -v681 -v1998 -v2218 -v2438 -v2658 -v37 -v252 -v467 -v899 -v1119 -v1339 -v1559 -v2219 v2439 -v2659 v253 -v468 -v683 -v1340 -v1560 -v1780 v2000 -v2220 -v2660 -v2867 -v254 -v469 v684 -v1341 -v1561 -v1781 -v2001 -v2868 -v470 -v685 -v902 -v1122 -v1342 v1782 -v2002 -v2222 -v2442 -v2662 -v257 v472 -v687 -v1344 v1564 -v1784 -v2004 -v2224 -v2664 -v2870 -v473 -v688 -v905 -v1125 v1345 -v1785 -v2005 -v2225 -v2445 -v2665 v44 -v474 -v689 -v1346 -v1786 v2006 -v2226 -v2446 -v2666 v475 -v690 -v1347 -v1787 -v2007 -v2227 -v2447 -v2667 -v2871 -v261 -v476 -v691 -v1348 v1568 -v1788 -v2008 -v2228 -v2448 -v2668 -v262 -v477 v692 -v1349 -v1569 -v1789 -v2009 -v2229 v2449 -v2669 -v263 v478 -v1350 -v1570 -v1790 -v479 -v1351 -v2231 -v2451 -v2671 -v2872 -v480 -v1352 -v2232 v2452 -v2672 -v2873 -v51 -v481 -v696 v1353 -v2013 -v2233 -v2453 -v2673 -v482 -v1354 -v2234 -v2454 -v2674 v53 -v268 -v483 -v915 -v1135 -v1355 v1575 -v2235 -v2455 -v2675 -v269 -v484 -v1356 -v1576 -v2236 -v2456 -v2676 v2874 -v55 v270 -v917 v1137 -v1577 -v1797 -v2237 -v3028 -v3181 -v56 -v271 -v1578 -v2238 -v2458 -v2678 v3182 -v57 -v487 -v702 v919 -v1139 -v1359 -v1799 -v2019 -v2239 -v2679 -v58 -v273 v488 -v1360 -v1580 v1800 -v2240 -v2460 -v2877 -v3183 -v59 -v274 -v489 -v921 -v1141 -v1361 -v1581 -v2241 v2461 -v2681 -v60 v275 -v705 -v1582 -v2022 -v2242 -v2462 -v2682 v3184 -v2243 -v2463 -v2683 -v2244 -v2464 -v2684 v63 -v493 -v708 -v1365 -v2025 -v2245 -v2465 -v2685 v2881 -v3187 v279 -v494 -v709 -v1366 -v1586 -v1806 -v2026 -v2246 v2466 -v2686 -v65 -v280 v710 -v1587 -v2027 v2247 -v2467 -v2687 -v3188 -v1368 -v1588 -v1808 -v2248 v2468 -v2688 -v2883 -v496 -v1369 -v1809 -v2249 -v2469 -v2689 -v2884 -v497 -v1370 -v2250 -v2470 -v2690 -v2885 -v68 -v498 -v1371 -v2251 v2886 -v3192 -v284 -v499 v714 -v1372 -v1592 -v1812 -v2032 -v2252 -v2472 -v2887 -v70 -v285 -v715 -v1593 -v2033 -v2253 -v3194 v287 -v502 -v717 -v1375 -v1595 -v1815 -v2035 -v2255 -v2475 v2890 -v288 v718 -v1596 v1816 -v2036 -v2256 -v2476 -v2696 -v74 -v289 v504 -v1377 -v1597 -v2257 -v2477 v2697 -v2892 v3198 -v75 -v290 -v505 -v1378 -v1598 -v2893 v3199 -v76 -v506 v721 -v1379 -v2039 v2894 -v3200 v78 -v293 -v723 -v1601 v1821 -v2041 -v2481 -v2701 -v3202 -v294 -v1602 v1822 -v2262 -v2482 -v2702 -v943 -v1163 -v1383 -v1603 -v1823 -v2043 v2263 -v2483 -v2897 -v3050 -v80 -v295 -v1604 v1824 -v2264 -v2484 -v2704 v3204 -v511 -v726 v1385 -v1825 -v2045 -v2265 -v2485 -v297 -v1606 -v1826 -v2266 v2486 -v2706 -v298 v513 -v728 -v947 -v1167 -v1387 -v1607 -v1827 -v2047 -v2267 -v84 -v514 -v729 -v1388 -v1828 -v2048 -v2708 v2900 -v3206 -v2269 -v2489 v2709 -v86 -v731 -v1830 -v2050 -v2270 -v2490 -v2710 v302 -v517 -v1391 -v1611 -v1831 v2271 -v2491 -v2711 -v2902 -v733 -v1832 -v2052 v2272 -v2492 -v304 -v734 -v953 -v1173 -v1613 -v1833 -v2053 -v2273 -v2493 v2713 -v90 -v305 -v735 -v1614 -v1834 -v2054 -v2274 -v2494 -v2714 -v2275 -v2495 -v2715 -v738 -v1837 -v2277 -v2497 -v2717 v3211 -v524 -v1398 -v2278 -v2906 -v525 -v1399 -v2279 -v2499 -v2719 -v2907 -v96 -v311 -v1620 v2280 -v2500 -v2720 -v3214 -v2281 -v2501 v2721 -v313 -v1622 v1842 -v2282 -v2502 -v2722 v99 -v744 -v2063 -v2283 -v2503 -v2723 -v3216 -v2284 -v2504 v2724 -v746 -v1845 -v2065 -v2285 v2505 -v2725 v102 -v317 -v966 -v1186 -v1626 -v1846 -v2286 v2506 -v2726 -v3066 -v3219 v104 -v968 -v1188 -v2288 -v2508 v2728 -v3068 -v3221 -v321 -v536 -v1410 -v1630 -v2290 v2510 -v2730 v107 -v752 -v971 -v1191 -v2071 -v2291 -v2511 v3069 -v3222 -v323 -v538 -v753 -v1412 -v1632 -v1852 -v2072 -v754 -v2073 -v2293 -v2513 v2733 v110 -v540 -v755 -v1414 -v1854 v2074 -v2294 -v2514 -v2734 -v111 -v326 v541 -v1415 -v1635 v2295 -v2515 -v2735 -v2918 v3224 -v112 v757 -v2076 -v2296 -v2516 v2736 -v3225 -v113 v328 -v1637 v2297 -v2517 -v2298 -v2518 -v2738 -v2299 -v2519 -v2739 -v2300 -v2520 v2740 -v332 -v1641 -v2301 v118 -v548 -v763 -v982 -v1202 -v1422 -v1862 -v2082 -v2522 v2742 -v334 v1643 -v1863 -v2303 -v2523 -v2743 -v335 -v1644 -v2305 v2525 -v2745 -v337 -v1646 -v1866 -v2306 -v338 -v1647 -v2307 -v2527 v2747 -v769 -v1868 -v2088 -v2308 -v2528 -v2748 -v555 -v1429 -v2309 -v2529 v2749 -v2930 -v556 -v1430 v2310 -v2931 -v342 -v772 -v1651 -v1871 v2091 -v2531 -v2751 -v2312 v2313 -v2533 -v2753 -v2314 -v131 -v561 -v1435 v2936 -v3242 v132 -v996 -v1216 -v2316 -v2536 -v2756 v133 -v997 -v1217 -v2317 -v2537 v2757 -v564 -v1438 -v2937 -v350 -v1659 -v1879 -v2319 -v2539 -v2759 v351 -v781 -v1660 v1880 -v2100 -v2320 -v2540 -v2760 v352 -v567 -v1441 -v1661 -v2321 v2541 -v2761 -v2940 v138 -v353 -v568 -v1442 -v1662 -v2322 -v2542 v139 -v1003 -v1223 -v2323 -v2543 v2763 -v140 -v1004 -v1224 -v2324 -v2544 -v2764 -v2325 -v2545 -v2765 -v572 v1446 -v2326 -v2546 -v2766 -v2941 -v573 -v1447 -v2327 v2547 -v2767 v2942 v574 -v789 -v1448 -v1888 -v2108 -v2328 -v2548 v2768 -v360 -v790 -v1669 -v1889 -v2109 v2329 -v2549 -v2769 v147 -v577 -v1451 v2945 -v3251 -v579 -v1454 v2334 -v2554 -v2774 v2947 -v365 -v1675 -v1016 -v1236 -v1456 -v1676 -v1896 v2116 -v2336 v1457 -v1677 -v1897 -v2337 -v2557 -v2777 -v796 -v152 -v367 -v582 -v1018 -v1238 -v1458 -v1678 -v1898 -v2338 -v2778 v2949 -v3102 -v3255 v798 -v2119 v2339 -v2559 -v2779 -v369 -v584 -v799 -v1460 -v1680 -v1900 -v2120 -v2560 -v2780 -v155 v585 -v800 -v1461 -v1901 -v2121 -v2341 -v2561 -v2781 -v371 v801 -v1682 -v1902 -v2122 -v2342 -v2562 -v2782 -v157 -v1023 -v1243 -v2343 v2563 -v2783 v3104 -v3257 -v158 v2344 -v2564 -v2784 -v3258 -v804 -v1905 -v2125 -v2345 -v2565 -v375 -v1686 -v1906 -v2346 -v2566 -v2786 -v376 v591 -v806 -v1467 -v1687 -v2127 -v2347 -v2567 -v2787 -v2954 -v377 -v807 -v1688 -v1908 -v2128 -v2348 -v2568 v2788 -v593 -v1469 -v2349 -v2569 -v2789 -v2956 -v594 -v1470 -v2350 -v2570 -v2790 v2957 -v380 -v595 -v1471 v1691 -v1911 -v2351 -v2791 -v2958 v1032 -v1252 -v1472 -v1692 -v2132 -v2352 -v2572 -v2792 -v2353 -v2573 -v2793 -v597 -v1474 -v2354 -v2960 -v168 -v383 -v598 -v1035 -v1255 -v1475 -v1695 -v2355 v2575 -v2795 -v384 -v814 -v1696 -v1916 -v2136 -v2356 -v2576 v2796 -v385 -v600 -v815 -v1037 -v1257 -v1477 -v1697 -v1917 -v2137 v2357 -v2577 v817 -v2139 -v2359 -v2579 -v2799 -v2360 -v2580 -v2800 -v2361 -v2581 v2801 v175 -v605 -v820 -v1042 -v1262 -v1482 -v2142 v2362 -v2582 -v2802 -v2363 -v2583 -v2803 v177 -v607 -v822 -v1044 -v1264 -v1484 v2144 -v2364 -v2584 -v2804 -v1045 -v1265 -v1485 -v1705 -v2145 -v2365 v2585 -v2805 -v394 -v609 -v824 -v1487 -v1707 -v1927 -v2147 -v2367 v2587 v2967 -v1048 -v1268 -v1928 -v2368 -v2588 v2808 v3121 v181 -v826 -v1929 -v2149 -v2369 -v2589 -v2809 -v3275 -v397 v612 -v827 -v1050 -v1270 -v1490 -v1710 -v1930 -v2150 -v183 -v613 -v828 -v1491 -v1931 v2151 -v2371 -v2591 -v2811 -v2372 -v2592 -v2812 -v185 -v400 -v1053 -v1273 -v1713 -v3123 v3276 -v618 -v833 -v1496 -v2156 -v2972 -v404 v619 -v834 -v1057 -v1277 -v1497 -v1717 v1937 -v2157 -v2597 -v2817 -v1938 v2378 -v2598 -v2818 -v836 -v2159 -v2379 -v2599 -v2819 -v192 v407 -v622 -v2975 -v3281 -v193 -v623 -v838 -v1500 v1940 -v2160 -v2380 -v2976 -v3282 v194 -v409 -v624 -v1501 -v1721 -v2381 -v2977 -v3283 -v410 -v625 -v840 -v1502 -v1722 -v1942 -v2162 v2382 -v2602 -v2822 -v1063 -v1283 -v1723 -v1943 -v2383 -v2603 -v2823 -v412 -v1725 v1945 -v2385 -v628 -v843 -v1506 -v2166 -v2386 -v2979 -v2387 -v2607 v2827 -v416 -v1728 -v417 -v632 v847 -v1509 -v1729 -v1949 -v2169 v2389 -v2609 v2983 v418 -v1730 -v1950 -v2390 -v2610 -v2830 v204 -v634 -v849 -v1511 -v2171 -v2391 -v2611 -v2831 v2985 -v3291 -v205 -v635 v850 -v1072 -v1292 -v1512 -v1952 -v2172 v2612 -v2832 -v636 -v1513 -v2393 v2613 -v2833 -v207 v637 -v1515 -v2987 -v3293 -v208 v638 -v1516 -v2396 -v2988 -v3294 -v1077 v1297 -v1737 -v1957 -v2397 -v2617 -v2837 -v641 v856 -v2990 -v212 -v642 v857 -v858 -v1959 -v2179 v2399 -v2619 -v2839 -v859 -v1960 v2180 -v2400 -v2620 -v2840 -v215 -v3146 v3299 -one -v1 -v9 -v10 -v14 -v29 -v31 v61 -v62 -v66 -v67 -v85 -v91 -v101 -v103 -v105 -v123 -v125 -v127 -v134 -v137 v141 -v144 v150 -v153 -v165 -v182 v187 v188 v190 -v191 -v198 -v199 v206 v209 -v210 -v218 v230 -v240 -v241 -v246 v283 -v309 v320 -v339 -v341 v346 -v349 -v363 -v379 -v381 -v386 -v401 -v402 -v406 v411 -v421 -v425 -v430 v431 v433 -v435 -v436 -v437 -v443 -v445 v453 -v461 v471 -v501 -v512 -v522 -v526 v533 -v543 v545 v553 v554 -v558 -v559 v565 -v569 -v578 -v580 -v583 -v601 -v602 v604 v606 -v614 -v617 -v626 -v639 v640 -v646 -v648 -v655 -v656 -v660 -v667 -v670 -v671 v676 -v679 -v686 -v706 -v712 v716 v722 -v727 v730 -v736 v737 v739 v742 -v745 -v748 -v759 -v760 v761 v771 v773 -v774 -v775 -v776 v779 -v791 v793 -v809 v811 v816 v818 -v819 -v821 -v823 -v831 -v832 -v841 v844 -v845 -v846 -v852 -v853 -v854 -v855 -v870 -v876 -v884 -v887 -v888 -v893 -v903 -v923 -v934 -v949 -v955 -v956 -v969 -v992 -v994 -v1005 v1012 v1013 -v1015 v1020 -v1043 -v1052 -v1054 -v1055 v1064 -v1089 -v1090 -v1096 -v1104 v1107 -v1108 -v1113 -v1123 -v1143 -v1169 -v1175 v1177 -v1184 -v1189 -v1212 v1214 -v1225 -v1232 -v1233 -v1235 -v1240 v1263 v1272 -v1274 -v1275 -v1284 -v1301 -v1303 v1305 -v1306 v1307 v1309 v1314 -v1316 -v1325 v1333 -v1343 -v1397 -v1400 -v1407 -v1417 -v1427 -v1428 -v1432 -v1433 -v1439 -v1443 -v1452 -v1453 -v1455 -v1459 -v1478 -v1479 -v1483 -v1492 -v1495 -v1504 -v1514 -v1518 -v1523 -v1534 -v1536 -v1547 -v1548 -v1553 -v1558 -v1591 -v1618 -v1629 v1648 -v1650 -v1652 -v1654 -v1655 -v1658 -v1672 -v1673 -v1690 -v1693 -v1698 -v1699 -v1714 -v1715 v1719 -v1724 -v1733 -v1734 -v1735 v1736 -v1743 -v1749 v1756 -v1764 -v1771 -v1773 -v1776 v1783 -v1818 -v1820 v1838 -v1840 -v1841 -v1844 -v1856 -v1857 -v1858 -v1859 -v1860 -v1861 -v1864 -v1872 -v1873 -v1890 -v1892 -v1893 -v1895 -v1899 -v1913 v1918 -v1920 -v1921 -v1923 -v1933 -v1934 v1935 -v1947 -v1948 -v1954 -v1956 -v1961 -v1963 -v1969 -v1971 v1972 -v1976 v1984 -v1987 v1988 -v1993 -v1996 -v2003 -v2023 -v2030 -v2034 -v2040 -v2046 -v2049 -v2055 -v2056 -v2058 -v2061 -v2064 -v2067 v2078 v2079 -v2080 -v2092 -v2093 -v2094 -v2095 -v2098 -v2110 -v2112 -v2113 -v2117 v2130 -v2133 -v2138 -v2140 -v2141 -v2143 -v2146 -v2154 -v2155 -v2164 -v2167 -v2168 -v2174 -v2175 -v2176 -v2178 -v2191 -v2211 -v2213 -v2223 -v2230 v2254 -v2260 -v2276 -v2287 v2289 -v2302 -v2304 -v2315 v2318 -v2330 -v2331 -v2332 -v2333 -v2335 -v2358 v2366 -v2373 -v2374 -v2375 -v2376 -v2384 -v2388 -v2392 -v2394 v2395 -v2398 -v2411 -v2417 -v2433 -v2443 -v2450 -v2474 -v2480 -v2487 -v2496 -v2507 -v2509 -v2521 -v2524 v2526 v2532 -v2534 -v2535 -v2538 -v2550 -v2551 -v2552 -v2555 -v2574 -v2578 -v2586 -v2590 -v2595 v2596 -v2604 -v2605 v2608 -v2614 -v2618 -v2631 -v2637 -v2644 -v2647 -v2648 -v2651 -v2653 -v2670 -v2694 -v2700 -v2716 -v2718 -v2727 -v2737 v2741 -v2744 -v2746 -v2752 -v2754 -v2770 -v2771 -v2775 -v2794 -v2806 v2814 -v2815 -v2816 -v2824 -v2825 -v2826 -v2828 v2834 -v2838 -v2841 -v2844 -v2845 -v2846 -v2852 v2853 -v2869 v2899 -v2908 -v2914 -v2928 -v2929 -v2933 v2934 -v2946 v2948 -v2962 v2963 -v2965 -v2986 v2989 -v3006 v3012 -v3022 -v3032 -v3054 v3056 v3086 -v3088 -v3099 -v3101 -v3118 -v3124 -v3133 -v3147 -v3150 -v3155 v3158 v3169 -v3185 -v3186 v3190 v3191 v3207 -v3209 v3220 v3234 v3236 v3238 v3243 -v3246 -v3254 v3264 -v3269 -v3278 -v3279 v3280 v3285 v3286 v3292 -v3295
s SATISFIABLE
Interupt; Current theory and settings are copied here:
/tmp/vallst_sh_out_theory.vnf
/tmp/vallst_sh_changing_setting.options
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.91 0.95 0.91 1/54 14226
Raw data (stat): 14226 (runsolver) R 14225 7266 7265 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 799487921 884736 94 4294967295 134512640 135332820 3221224464 3221219628 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+9.99994 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+40.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+50.0033 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+70.0031 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+680.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+770.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+790.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14229
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+840.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/59 14272
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+850.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14282
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14282
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14282
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14282
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+890.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14282
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+900.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14282
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+910.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+920.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+930.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+940.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+960.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+970.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+980.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14284
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14286
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14286
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14286
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14286
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14286
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1220.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14286
Raw data (stat): 14226 (vallstSAT2005PB) S 14225 7266 7265 0 -1 0 321 232 0 0 1 1 0 0 19 0 1 0 799487921 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 0 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1230.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14292
Raw data (stat): 14226 (vallstSAT2005PB) R 14225 7266 7265 0 -1 0 430 2125 0 0 12 2 115017 7979 19 0 1 0 799487921 2179072 249 4294967295 134512640 135087896 3221224528 3221221232 134818762 0 0 7 1132560120 0 0 0 17 0 0 0
Raw data (statm): 532 249 485 147 0 385 0
vsize: 2128
[startup+1231.27 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 14298
Raw data (stat): 14226 (vallstSAT2005PB) R 14225 7266 7265 0 -1 0 430 2125 0 0 12 2 115017 7979 19 0 1 0 799487921 2179072 249 4294967295 134512640 135087896 3221224528 3221221232 134818762 0 0 7 1132560120 0 0 0 17 0 0 0
Raw data (statm): 532 249 485 147 0 385 0
vsize: 0
Child status: 10
Real time (s): 1231.27
CPU time (s): 1231.04
CPU user time (s): 1151
CPU system time (s): 80.0488
CPU usage (%): 99.9815
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier: FAILED
ERROR: unsatisfied constraint on line 4
#### END VERIFIER DATA ####