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-ss97-4.opb |
| MD5SUM | 417d3abd60fd3b9eb4200ff5119a92c4 |
| Bench Category | optimization, small integers (OPTSMALLINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 813 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 1798 |
| Biggest coefficient in the objective function | 349 |
| Number of bits for the biggest coefficient in the objective function | 9 |
| Sum of the numbers in the objective function | 104116 |
| Number of bits of the sum of numbers in the objective function | 17 |
| Biggest number in a constraint | 349 |
| Number of bits of the biggest number in a constraint | 9 |
| Biggest sum of numbers in a constraint | 104116 |
| Number of bits of the biggest sum of numbers | 17 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1.05084 |
| Number of variables | 2289 |
| Total number of constraints | 3052 |
| Number of constraints which are clauses | 360 |
| Number of constraints which are cardinality constraints (but not clauses) | 2692 |
| Number of constraints which are nor clauses,nor cardinality constraints | 0 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 195 |
Trace number 33827
#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-05-27 16:45:11 (client local time)
PB2005-SCRIPT v4.0
MARKUPS: idlaunch=3194 boxname=wulflinc13 idbench=355 idsolver=8 numberseed=0
MD5SUM SOLVER: 4b637b3b6117f2add1a6288e91336322 /oldhome/oroussel/solvers/vallstSAT2005PB.sh
MD5SUM BENCH: 417d3abd60fd3b9eb4200ff5119a92c4 /oldhome/oroussel/tmp/wulflinc13/normalized-ss97-4.opb
REAL COMMAND: vallstSAT2005PB.sh /oldhome/oroussel/tmp/wulflinc13/normalized-ss97-4.opb 0
IDLAUNCH: 3194
/proc/cpuinfo:
processor : 0
vendor_id : GenuineIntel
cpu family : 6
model : 7
model name : Pentium III (Katmai)
stepping : 2
cpu MHz : 451.242
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.242
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 : 901.12
/proc/meminfo:
MemTotal: 1034660 kB
MemFree: 711944 kB
Buffers: 26608 kB
Cached: 276340 kB
SwapCached: 604 kB
Active: 24648 kB
Inactive: 280392 kB
HighTotal: 131008 kB
HighFree: 252 kB
LowTotal: 903652 kB
LowFree: 711692 kB
SwapTotal: 2097136 kB
SwapFree: 2095672 kB
Dirty: 1752 kB
Writeback: 0 kB
Mapped: 5584 kB
Slab: 12068 kB
Committed_AS: 63604 kB
PageTables: 316 kB
VmallocTotal: 114680 kB
VmallocUsed: 1364 kB
VmallocChunk: 113256 kB
JOB ENDED THE 2005-05-27 17:05:42 (client local time) WITH STATUS 10 IN 1230.7 SECONDS
stats: 3194 6 1230.7 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
1:
seed: 0
Nr of vars set: 7 (#equs: 0)
Nr of vars set: 7 (#equs: 1)
#decisions: 1628; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1141, #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: 86985 (17130:>=*);
#decisions: 1636; #end-nodes: 8;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 8 / 80 (80)
#axs: 1141, #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: 86986 (17129:>=*);
#decisions: 1637; #end-nodes: 9;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 9 / 80 (80)
#axs: 1141, #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: 87085 (17030:>=*);
#decisions: 1620; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 1141, #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: 87086 (17029:>=*);
#decisions: 1622; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 1141, #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: 87087 (17028:>=*);
#decisions: 1696; #end-nodes: 54;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 54 / 80 (80)
#axs: 1141, #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: 87088 (17027:>=*);
#decisions: 1639; #end-nodes: 12;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 12 / 80 (80)
#axs: 1141, #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: 87187 (16928:>=*);
#decisions: 1625; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 1141, #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: 87188 (16927:>=*);
#decisions: 1660; #end-nodes: 34;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 34 / 80 (80)
#axs: 1141, #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: 87189 (16926:>=*);
#decisions: 166684; #end-nodes: 4901;
#proof improvement attempts: 0; #restarts: 56
Current batch, end-nodes: 33 / 94 (94)
#axs: 1141, #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: 87190 (16925:>=*);
#decisions: 40364; #end-nodes: 1141;
#proof improvement attempts: 0; #restarts: 14
Current batch, end-nodes: 0 / 83 (83)
#axs: 1141, #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: 87192 (16923:>=*);
#decisions: 1563; #end-nodes: 11;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 11 / 80 (80)
#axs: 1141, #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: 87293 (16822:>=*);
#decisions: 1560; #end-nodes: 16;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 16 / 80 (80)
#axs: 1141, #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: 87294 (16821:>=*);
#decisions: 15092; #end-nodes: 484;
#proof improvement attempts: 0; #restarts: 6
Current batch, end-nodes: 0 / 81 (81)
#axs: 1141, #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: 87592 (16523:>=*);
#decisions: 1709; #end-nodes: 18;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 18 / 80 (80)
#axs: 1141, #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: 87693 (16422:>=*);
#decisions: 88128; #end-nodes: 2752;
#proof improvement attempts: 0; #restarts: 32
Current batch, end-nodes: 59 / 88 (88)
#axs: 1141, #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: 87783 (16332:>=*);
#decisions: 1593; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1141, #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: 87784 (16331:>=*);
#decisions: 53037; #end-nodes: 1646;
#proof improvement attempts: 0; #restarts: 20
Current batch, end-nodes: 0 / 85 (85)
#axs: 1141, #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: 87990 (16125:>=*);
#decisions: 1629; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 1141, #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: 88091 (16024:>=*);
#decisions: 1683; #end-nodes: 42;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 42 / 80 (80)
#axs: 1141, #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: 88192 (15923:>=*);
#decisions: 36386; #end-nodes: 1143;
#proof improvement attempts: 0; #restarts: 14
Current batch, end-nodes: 0 / 83 (83)
#axs: 1141, #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: 88388 (15727:>=*);
#decisions: 1642; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1141, #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: 88389 (15726:>=*);
#decisions: 1646; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 1141, #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: 88488 (15627:>=*);
#decisions: 1638; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1141, #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: 88489 (15626:>=*);
#decisions: 1643; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 1141, #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: 88490 (15625:>=*);
#decisions: 1646; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 1141, #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: 88589 (15526:>=*);
#decisions: 1637; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1141, #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: 88590 (15525:>=*);
#decisions: 1663; #end-nodes: 10;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 10 / 80 (80)
#axs: 1141, #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: 88688 (15427:>=*);
#decisions: 1632; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1141, #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: 88689 (15426:>=*);
#decisions: 1634; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 1141, #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: 88690 (15425:>=*);
#decisions: 1646; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 1141, #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: 88691 (15424:>=*);
#decisions: 1652; #end-nodes: 6;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 6 / 80 (80)
#axs: 1141, #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: 88791 (15324:>=*);
#decisions: 1628; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 1141, #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: 88792 (15323:>=*);
#decisions: 1670; #end-nodes: 21;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 21 / 80 (80)
#axs: 1141, #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: 88793 (15322:>=*);
#decisions: 1647; #end-nodes: 10;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 10 / 80 (80)
#axs: 1141, #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: 88893 (15222:>=*);
#decisions: 1771; #end-nodes: 73;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 73 / 80 (80)
#axs: 1141, #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: 88991 (15124:>=*);
#decisions: 1608; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 1141, #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: 88992 (15123:>=*);
#decisions: 1610; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 1141, #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: 88993 (15122:>=*);
#decisions: 1626; #end-nodes: 10;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 10 / 80 (80)
#axs: 1141, #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: 88994 (15121:>=*);
#decisions: 151204; #end-nodes: 5260;
#proof improvement attempts: 0; #restarts: 60
Current batch, end-nodes: 15 / 95 (95)
#axs: 1141, #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: 88995 (15120:>=*);
#decisions: 1711; #end-nodes: 31;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 31 / 80 (80)
#axs: 1141, #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: 88996 (15119:>=*);
#decisions: 47440; #end-nodes: 1796;
#proof improvement attempts: 0; #restarts: 21
Current batch, end-nodes: 64 / 85 (85)
#axs: 1141, #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: 88998 (15117:>=*);
#decisions: 1805; #end-nodes: 63;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 63 / 80 (80)
#axs: 1141, #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: 88999 (15116:>=*);
#decisions: 1716; #end-nodes: 35;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 35 / 80 (80)
#axs: 1141, #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: 89002 (15113:>=*);
#decisions: 170132; #end-nodes: 6484;
#proof improvement attempts: 0; #restarts: 73
Current batch, end-nodes: 0 / 98 (98)
#axs: 1141, #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: 89003 (15112:>=*);
#decisions: 1557; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 1141, #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: 89004 (15111:>=*);
#decisions: 1578; #end-nodes: 24;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 24 / 80 (80)
#axs: 1141, #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: 89005 (15110:>=*);
#decisions: 3462929; #end-nodes: 201228;
#proof improvement attempts: 0; #restarts: 989
Current batch, end-nodes: 0 / 327 (327)
#axs: 1141, #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: 89100 (15015:>=*);
#decisions: 1567; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 1141, #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: 89101 (15014:>=*);
#decisions: 1615; #end-nodes: 29;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 29 / 80 (80)
#axs: 1141, #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: 89201 (14914:>=*);
#decisions: 1645; #end-nodes: 41;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 41 / 80 (80)
#axs: 1141, #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: 89202 (14913:>=*);
#decisions: 1600; #end-nodes: 27;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 27 / 80 (80)
#axs: 1141, #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: 89302 (14813:>=*);
#decisions: 874903; #end-nodes: 40441;
#proof improvement attempts: 0; #restarts: 333
Current batch, end-nodes: 0 / 163 (163)
#axs: 1141, #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: 89309 (14806:>=*);
#decisions: 1537; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 1141, #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: 89310 (14805:>=*);
#decisions: 1548; #end-nodes: 6;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 6 / 80 (80)
#axs: 1141, #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: 89311 (14804:>=*);
#decisions: 1613; #end-nodes: 49;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 49 / 80 (80)
#axs: 1141, #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: 89312 (14803:>=*);
#decisions: 33374; #end-nodes: 1176;
#proof improvement attempts: 0; #restarts: 14
Current batch, end-nodes: 30 / 83 (83)
#axs: 1141, #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: 89400 (14715:>=*);
#decisions: 1545; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 1141, #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: 89401 (14714:>=*);
#decisions: 1573; #end-nodes: 30;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 30 / 80 (80)
#axs: 1141, #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: 89402 (14713:>=*);
#decisions: 1618; #end-nodes: 62;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 62 / 80 (80)
#axs: 1141, #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: 89403 (14712:>=*);
#decisions: 220901; #end-nodes: 8544;
#proof improvement attempts: 0; #restarts: 93
Current batch, end-nodes: 41 / 103 (103)
#axs: 1141, #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: 89495 (14620:>=*);
#decisions: 1594; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 1141, #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: 89496 (14619:>=*);
#decisions: 1595; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 1141, #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: 89497 (14618:>=*);
#decisions: 1643; #end-nodes: 25;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 25 / 80 (80)
#axs: 1141, #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: 89498 (14617:>=*);
#decisions: 68713; #end-nodes: 2467;
#proof improvement attempts: 0; #restarts: 29
Current batch, end-nodes: 44 / 87 (87)
#axs: 1141, #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: 89503 (14612:>=*);
#decisions: 1640; #end-nodes: 63;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 63 / 80 (80)
#axs: 1141, #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: 89504 (14611:>=*);
#decisions: 1349468; #end-nodes: 70810;
#proof improvement attempts: 0; #restarts: 498
Current batch, end-nodes: 62 / 204 (204)
#axs: 1141, #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: 89505 (14610:>=*);
#decisions: 941518; #end-nodes: 45699;
#proof improvement attempts: 0; #restarts: 364
Current batch, end-nodes: 76 / 171 (171)
#axs: 1141, #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: 89599 (14516:>=*);
#decisions: 1652; #end-nodes: 14;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 14 / 80 (80)
#axs: 1141, #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: 89600 (14515:>=*);
#decisions: 153546; #end-nodes: 5798;
#proof improvement attempts: 0; #restarts: 65
Current batch, end-nodes: 82 / 96 (96)
#axs: 1141, #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: 89700 (14415:>=*);
#decisions: 1706; #end-nodes: 41;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 41 / 80 (80)
#axs: 1141, #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: 89799 (14316:>=*);
#decisions: 1673; #end-nodes: 11;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 11 / 80 (80)
#axs: 1141, #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: 89800 (14315:>=*);
Interupt request received.
#decisions: 12441813; #end-nodes: 1093672;
#proof improvement attempts: 0; #restarts: 2655
Current batch, end-nodes: 564 / 743 (743)
#axs: 1141, #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:) 89800 (14315:>=*)
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: 1839 (#equs: 1)
Time taken: 20 min, 29 sec
times:
0m0.018s 0m0.008s
19m31.472s 0m58.387s
v v1 -v365 -v729 -v924 -v1119 v1704 -v1899 v2 -v366 -v1120 v1510 -v2095 -v3 -v367 v1121 -v1706 -v4 -v186 v368 -v1122 -v1317 -v1512 -v1707 v1902 -v5 -v187 v369 -v1123 -v1318 -v1513 v1708 -v1903 -v6 -v188 v370 -v734 -v929 -v1124 -v1319 -v1514 -v1709 v1904 v1515 -v2100 -v554 -v1711 v10 -v192 -v374 -v738 -v933 -v1128 -v1323 -v193 -v1324 -v1519 v1714 -v2104 v559 -v2106 -v14 v378 -v560 -v742 -v937 -v1132 v2107 v15 -v379 -v1133 -v2108 -v16 v380 -v1134 -v2109 -v563 -v1330 -v1525 -v2110 -v566 -v1723 v1918 -v2113 -v567 v1334 -v2114 -v204 -v1725 -v1920 v23 -v205 -v387 -v751 -v946 -v1141 -v1726 v1921 -v2116 -v570 -v1532 -v1727 -v2117 -v571 -v2118 v572 -v1339 -v1534 -v2119 -v2120 -v573 -v756 -v951 -v28 v392 -v1147 v1927 -v29 v393 -v1148 -v1343 v576 -v1344 -v1539 -v2124 -v1345 -v1346 -v32 -v396 -v1152 -v33 v397 -v1153 -v2128 -v34 -v398 -v959 v1154 -v2129 -v35 v399 -v1155 -v2130 -v36 v400 -v1156 v2131 -v37 -v401 v1157 -v2132 -v38 -v402 -v963 v1158 -v2133 -v964 -v2134 -v222 -v1550 v2135 -v41 -v405 -v771 -v966 -v1161 -v2136 -v588 -v1942 -v589 -v773 -v968 -v1358 v1748 -v226 -v774 -v969 v227 -v1555 -v1750 -v2140 -v46 v410 -v1166 -v1751 v1557 -v1752 v48 -v230 -v412 -v778 -v973 -v1168 -v1363 -v595 -v1754 -v50 v414 -v780 -v975 -v1170 -v1950 v2145 v233 v976 -v1756 -v2146 -v1757 -v2147 v52 -v416 -v1173 v1953 -v417 -v599 -v784 -v979 -v1369 -v54 -v418 -v1175 -v2150 -v55 -v419 -v1176 -v2151 -v56 -v420 -v1177 v1762 v421 -v603 -v1763 -v58 -v422 -v1179 -v2154 v241 -v605 -v1765 -v2155 -v60 v242 -v424 -v1181 -v1766 -v61 -v243 -v425 -v792 -v987 -v1182 -v608 -v1768 -v63 -v427 v609 -v1184 -v64 -v428 v1185 -v2160 v65 -v429 -v796 -v991 -v1186 -v248 -v1382 v2162 -v613 -v1383 v2163 -v2164 v251 -v2165 v252 -v616 v1386 v253 -v2167 -v2168 v254 -v1584 -v2169 v73 -v437 -v1195 -v1585 -v2170 -v75 v439 -v621 -v1197 -v2172 -v622 v1393 -v1588 -v77 -v441 -v1199 v260 -v1395 -v811 -v1006 v1786 -v443 -v625 -v1787 v626 -v813 -v1008 -v1788 -v1983 v2178 -v1789 -v2179 v627 -v815 -v1010 -v628 -v1596 -v1791 v2181 -v265 -v629 v1402 -v2182 -v84 -v448 -v630 -v818 -v1013 -v1208 -v2183 v631 -v2184 -v820 -v1015 -v2185 -v1796 v633 -v2187 -v2188 -v635 -v824 v1019 -v1799 v636 -v1800 v2190 -v91 -v455 -v826 -v1021 v1216 -v92 -v456 -v827 -v1022 -v1217 -v828 -v1023 -v94 v458 -v829 -v1024 -v1219 -v95 -v459 -v1220 v2195 -v278 -v1416 -v2196 v2197 -v461 v643 -v1028 -v2198 -v1224 -v462 v644 v835 -v1030 -v1420 -v1615 v645 -v1031 -v2201 -v100 -v464 -v837 v1032 -v1227 -v1422 -v2202 -v101 -v465 -v1228 -v2203 -v102 -v466 -v839 -v1034 -v1229 v1619 -v103 v467 -v1230 -v1620 -v1815 -v2010 v104 -v286 -v468 -v841 -v1036 -v1231 -v1426 -v105 -v469 v1232 -v1427 -v1622 -v1817 v106 -v470 v843 -v1038 -v1233 v289 -v108 -v472 v845 -v1040 -v1235 -v109 -v473 -v846 v1041 -v1236 -v292 -v111 -v293 -v475 -v848 -v1043 -v1238 -v2018 -v112 -v476 -v1239 -v1434 v659 -v114 -v478 v660 -v1241 -v1826 -v297 -v116 -v480 -v1243 -v1438 -v299 -v663 v300 -v1635 v119 -v483 -v1246 -v1831 -v2026 -v120 v484 -v1247 -v1832 v303 -v2223 -v122 -v486 -v1249 -v2224 v305 -v125 v307 -v489 -v1252 -v1837 -v2227 -v672 -v863 -v1058 -v127 v491 -v673 -v1254 -v1839 v674 v129 -v493 -v865 -v1255 -v2230 -v312 -v2231 -v131 v313 -v867 -v1452 -v1647 -v314 -v1453 v133 -v315 -v497 -v1259 -v1649 v1844 -v2039 v680 -v870 -v1065 -v135 v499 -v871 v1066 -v1261 -v1456 v136 -v318 -v500 -v872 -v1067 -v1262 -v1847 -v2042 v2237 v683 -v2238 -v320 -v874 v1069 -v139 -v503 -v1265 -v1460 -v2240 v140 -v322 -v1851 -v2241 -v877 v1072 -v2242 -v687 -v878 -v1073 -v1658 -v1853 v142 -v506 -v688 -v879 -v1074 -v1269 -v1464 -v1659 -v1854 -v2049 v2244 v143 -v325 -v507 -v689 -v1270 -v1465 -v2245 -v508 -v690 -v1856 v145 -v509 -v691 -v1272 -v2247 -v1468 -v1858 -v1469 -v1859 -v1470 v146 -v510 -v1276 -v1861 -v329 -v1862 v694 -v1668 -v2253 -v695 -v1474 -v1669 -v150 -v514 -v890 -v1085 -v1280 v151 -v515 v891 -v1086 -v1281 -v1476 -v1671 -v2061 -v892 -v1087 -v1477 -v1672 -v335 -v699 -v893 -v1088 v1478 -v1673 -v2258 v154 -v518 -v894 v1089 -v1284 -v1479 -v1674 -v1869 -v155 -v519 -v895 -v1090 -v1285 v1675 -v1676 v157 -v339 -v521 -v897 -v1092 -v1287 -v1677 v1872 v159 -v341 -v523 -v705 -v899 v1094 -v1289 -v1679 -v2069 -v342 -v2265 v161 -v525 -v1291 -v2266 -v344 -v2267 -v163 v345 -v527 v1098 -v1293 -v1683 -v1878 -v528 v710 -v904 -v1099 -v1294 -v1684 -v1879 -v2074 -v2269 -v347 -v1685 v2270 -v167 -v531 v1297 -v1882 -v168 v350 -v532 -v1298 -v2273 -v169 -v351 -v533 v715 -v909 v1104 -v1299 -v1494 -v2274 -v1300 -v1495 -v1690 -v1106 -v2276 -v171 v353 -v535 -v1302 -v1692 -v2082 -v172 -v536 v718 -v1303 -v2083 -v2278 v174 -v538 -v915 -v1110 -v1305 -v1695 -v539 -v916 -v1501 -v358 -v722 v1502 -v1697 -v1892 -v2087 -v359 -v1698 -v2283 -v178 -v360 -v542 -v919 v1114 -v1309 -v2284 v179 -v543 -v1310 -v1700 -v2285 v180 -v544 -v1311 -v1701 v2286 -v181 -v545 v727 -v1312 -v1897 -v2092 -v364 v728 -v1508 -v1703 -v2093 -v1314 -v1509 -v184 -v548 -v730 -v925 -v1315 -v1705 -v1900 -v549 -v731 -v926 -v1316 -v1511 -v2096 -v732 -v927 -v2097 -v733 -v928 -v2098 -v2099 -v553 -v735 -v930 -v1320 -v1710 -v8 -v372 -v736 -v931 v1126 -v1516 -v1906 -v9 -v191 v373 -v555 -v737 -v932 -v1127 -v1322 -v1712 -v1907 -v556 -v1518 -v1713 -v1908 v2103 -v11 v375 -v739 -v934 -v1129 -v194 -v13 -v195 -v377 -v741 -v936 v1131 -v1326 -v1521 -v1716 -v1911 -v197 -v561 -v743 -v938 -v1328 -v1523 v1718 -v1913 -v198 -v562 -v744 -v939 -v1329 v1524 -v1719 -v1914 -v17 -v199 v381 -v745 -v940 -v1135 v1720 -v1915 -v18 v382 -v1136 -v1526 -v1721 -v1916 -v747 -v942 -v1527 -v1722 -v1917 -v2112 -v20 -v202 v384 -v748 -v943 -v1138 -v1333 -v1528 v21 -v385 -v1139 v22 -v386 -v568 v750 -v945 -v1140 -v1335 -v1530 -v2115 -v1336 -v1531 -v24 -v206 v388 -v1142 v1337 -v1922 -v25 -v207 v389 -v753 -v948 -v1143 -v1338 v1728 -v1923 -v26 -v208 -v390 -v754 -v949 v1144 -v1729 -v1924 -v755 -v950 v1145 -v1340 -v1535 -v1730 -v1925 v27 -v209 -v391 -v1146 -v1341 v1536 -v1731 -v1926 -v2121 -v210 -v574 -v757 -v952 -v1342 -v1537 -v1732 -v2122 -v1928 -v30 -v212 -v394 -v759 -v954 v1149 -v1734 -v1929 -v1540 -v2125 v1541 -v578 -v762 -v957 v1542 -v1737 -v215 -v763 -v958 -v1348 -v1543 -v1738 v1933 -v216 -v1349 -v1544 -v1739 -v1934 -v217 -v581 -v765 -v960 v1350 -v1545 -v1740 -v1935 -v218 -v582 -v766 -v961 -v1351 -v1546 -v1741 -v1936 v219 -v583 -v767 -v962 -v1352 -v1547 -v220 -v1353 -v1548 -v1743 -v1938 -v223 v587 -v1356 -v1551 -v1941 -v42 -v406 -v772 -v967 -v1162 -v1357 v1552 -v43 -v407 -v1163 v44 -v408 -v590 -v1164 -v1359 -v1554 -v45 -v409 -v1165 -v1945 -v228 -v592 v776 -v971 -v1361 -v1556 -v1946 -v2141 -v229 -v1362 -v594 -v49 -v231 v413 -v779 -v974 -v1169 -v1364 v1559 -v2144 -v232 -v596 -v1365 -v1560 -v1755 -v51 -v415 -v597 -v1171 -v1366 -v1561 -v1951 -v235 v1564 -v1759 -v2149 -v236 -v785 v980 -v1370 -v1565 -v1760 -v1955 -v238 v602 -v787 -v982 -v1372 -v1567 -v1957 -v2152 -v239 -v1373 v1568 v240 -v604 -v789 -v984 -v1374 -v1569 -v59 -v423 -v790 -v985 -v1180 -v606 -v791 -v986 -v1376 -v1571 v1961 -v2156 v62 -v244 -v426 -v793 v988 -v1183 -v1963 -v1574 -v2159 v610 -v1380 -v1575 -v247 -v611 -v1381 -v1576 -v1771 v1966 -v2161 -v66 v430 -v612 -v797 -v992 -v1187 -v1577 -v1772 -v1967 -v67 v249 -v431 -v798 -v993 -v1188 -v1578 -v1773 -v1968 -v68 -v432 v799 -v994 -v1189 -v1384 -v1774 -v1969 -v69 -v433 -v615 -v800 -v995 v1190 -v1385 -v1580 -v1775 -v1970 -v70 -v434 -v801 -v996 -v1191 -v1971 -v71 -v435 -v617 -v802 -v997 -v1192 -v1387 -v1582 v1777 -v1972 -v803 -v998 -v1193 -v1388 -v1583 v1778 -v72 -v436 -v618 -v804 -v999 -v1194 -v1389 v1779 -v1974 -v255 -v619 -v805 -v1000 -v1390 -v1780 v1975 -v74 v256 -v438 -v620 -v806 -v1001 -v1196 v1391 -v1586 -v1781 -v1976 -v2171 -v257 -v807 -v1002 -v1392 -v1587 -v76 -v440 -v808 -v1003 -v1198 -v1978 -v259 -v1394 v1589 -v1979 -v78 -v442 -v624 -v810 -v1005 v1200 -v1590 -v1785 -v1980 -v2175 -v1201 -v1396 -v1591 -v1981 -v2176 -v812 -v1007 -v1592 -v80 -v262 -v444 -v1203 -v1398 -v1593 -v814 -v1009 -v1204 -v1399 -v1594 v1984 -v81 -v263 -v445 -v1205 v1400 -v1595 -v1790 -v1985 -v2180 -v264 v83 -v447 -v817 -v1012 -v1207 -v1597 -v1792 -v1987 v266 -v1403 -v1598 -v1793 v1988 -v85 -v449 v819 -v1014 -v1209 -v1794 -v1989 -v1210 -v1405 v1600 -v1795 -v1990 v86 -v450 -v632 v821 -v1016 -v1211 -v1406 -v1601 -v2186 -v87 -v269 -v451 -v822 v1017 -v1212 -v1407 -v1602 -v1797 -v1992 -v88 v270 -v452 -v634 -v823 -v1018 -v1213 -v1408 v1603 -v1798 -v1993 v89 -v271 -v453 -v1214 -v1409 -v1604 -v2189 -v90 -v272 -v454 -v825 -v1020 -v1215 -v1410 -v1605 -v1995 v273 -v637 -v1411 -v1606 -v1801 -v1996 -v2191 v274 -v638 -v1412 -v1607 -v1802 v1997 -v2192 -v276 -v640 -v1414 v1609 -v1804 -v1999 -v2194 -v277 v641 -v830 -v1025 -v1415 -v1610 -v96 -v460 v642 -v831 v1026 -v1221 -v1806 -v2001 -v832 -v1027 -v1222 -v1417 -v1612 -v1807 -v2002 -v1613 -v2003 -v834 -v1029 -v1419 -v1614 -v1809 v2004 -v2199 -v1810 -v2200 -v99 -v281 -v463 -v1226 -v2006 -v282 v646 -v1812 -v2007 -v283 -v1618 v1813 -v2008 v284 -v648 -v1424 -v2204 -v285 -v1425 -v650 -v1816 -v2011 -v2206 v287 -v651 -v842 -v1037 -v2012 -v2207 -v288 -v652 -v1428 -v1623 -v1818 -v2013 -v2208 -v107 -v471 -v653 v844 -v1039 -v1234 -v1429 -v1624 -v2014 -v2209 -v290 v654 -v1430 -v1625 -v1820 -v2015 -v2210 v291 -v655 -v1431 -v1626 -v1821 -v2016 -v2211 -v110 -v474 v656 v847 -v1042 -v1237 -v1432 -v1627 -v1822 -v2017 -v2212 v657 -v1433 -v1628 v2213 v294 -v658 v849 -v1044 -v1629 -v1824 -v2019 -v2214 -v113 -v295 -v477 -v850 -v1045 v1240 -v1435 -v1630 -v1825 -v2020 -v2215 -v296 -v1631 v115 -v479 -v661 -v852 -v1047 -v1242 v1437 -v1632 -v1827 -v2022 -v2217 v298 -v662 v853 -v1048 -v1633 -v1828 -v2023 -v2218 -v117 v481 -v854 -v1049 -v1244 v1439 -v1634 -v1829 -v2024 -v2219 -v118 -v482 -v664 -v855 -v1050 -v1245 -v1440 -v1830 v2025 -v2220 -v301 -v665 v856 -v1051 -v1441 -v1636 -v2221 -v666 -v857 -v1052 -v1637 v2222 -v121 -v485 -v667 -v858 -v1053 -v1248 -v1443 -v1638 v1833 -v2028 -v304 v668 -v1444 -v1639 -v1834 -v2029 -v671 v862 -v1057 -v1447 -v1642 -v2032 v308 -v1448 -v1643 -v1838 -v2033 -v1644 -v128 -v492 -v311 -v675 -v1450 -v1645 -v130 -v494 v676 -v866 -v1061 -v1256 -v1451 v1646 -v1841 -v2036 v132 -v496 -v678 v868 -v1063 -v1258 -v1648 -v1843 -v2038 -v2233 -v134 -v316 -v498 -v1260 -v1455 v1650 -v2235 -v317 -v681 -v1651 -v1846 -v2041 -v2236 -v137 -v319 -v501 -v873 -v1068 -v1263 -v1458 v1653 -v1848 -v2043 -v138 v502 -v684 -v1264 -v1459 -v1654 -v1849 -v2239 v321 -v685 -v875 -v1070 -v1655 -v2045 -v1267 -v2047 -v2048 -v324 -v880 v1075 -v1660 -v1855 -v2050 -v1661 -v2248 -v2249 -v1665 -v2250 -v692 v886 -v1081 v693 -v148 -v330 -v512 -v888 -v1083 -v1278 -v1863 -v2058 -v149 v331 -v513 -v889 v1084 -v1279 -v1864 -v2059 -v2254 v332 -v696 -v1475 -v1670 -v1865 -v2060 v2255 -v697 -v1866 -v2256 -v152 -v516 v698 -v1282 -v1867 -v2062 v2257 -v153 v517 -v1283 -v1868 -v2063 -v700 -v2064 -v2259 -v337 v701 -v1480 -v1870 -v2065 -v2260 -v702 -v1871 -v2261 -v703 -v1482 -v2067 -v2262 -v158 -v522 -v704 -v898 -v1093 -v1288 -v1678 -v2263 -v1484 -v1874 -v2264 -v160 -v524 v706 -v900 -v1095 -v1290 v1485 -v1680 -v1875 -v2070 -v343 -v707 -v901 -v1096 v1486 -v1876 -v2071 -v162 v526 -v708 -v902 -v1097 -v1292 -v1487 v1877 -v2072 -v709 -v1488 -v2073 -v2268 -v1881 -v349 v713 -v907 -v1102 -v1492 -v2077 -v2272 -v714 v908 -v1103 -v1493 -v1883 -v2078 -v1884 -v2079 -v716 -v717 -v912 -v1107 v1497 -v2277 -v1693 -v719 -v1889 -v2084 -v2279 -v720 -v1890 -v2085 -v2280 -v721 v176 -v540 -v917 -v1112 -v1307 -v2282 -v177 -v541 v723 v918 -v1113 -v1308 -v1893 -v2088 v724 -v1504 -v1894 -v361 -v725 v920 -v1115 -v1505 -v362 -v726 -v921 -v1116 -v1506 -v1896 -v2091 -v363 -v1507 -v1702 -v182 -v546 -v923 v1118 -v1313 -v1898 -v2288 -one -v7 v12 -v19 v31 -v39 v40 -v47 v53 -v57 -v79 v82 -v93 -v97 -v98 -v123 v124 -v126 v141 v144 -v147 v156 -v164 -v165 -v166 -v170 -v173 -v175 -v183 v185 -v189 v190 -v196 -v200 -v201 -v203 -v211 -v213 v214 v221 v224 v225 -v234 -v237 -v245 -v246 v250 v258 v261 -v267 -v268 v275 -v279 -v280 -v302 -v306 -v309 -v310 -v323 -v326 -v327 -v328 -v333 -v334 -v336 -v338 v340 -v346 v348 v352 -v354 -v355 -v356 v357 v371 -v376 v383 -v395 -v403 -v404 v411 -v446 -v457 -v487 -v488 -v490 -v495 -v504 -v505 -v511 -v520 -v529 -v530 -v534 v537 -v547 -v550 -v551 -v552 -v557 -v558 -v564 -v565 -v569 -v575 -v577 -v579 v580 v584 -v585 -v586 -v591 -v593 -v598 v600 v601 v607 -v614 v623 -v639 v647 -v649 -v669 -v670 -v677 -v679 -v682 -v686 v711 -v712 -v740 -v746 -v749 -v752 -v758 -v760 -v761 -v764 -v768 -v769 -v770 -v775 -v777 -v781 -v782 -v783 -v786 -v788 -v794 -v795 -v809 -v816 -v833 v836 -v838 -v840 -v851 v859 -v860 -v861 v864 -v869 -v876 -v881 -v882 -v883 -v884 v885 -v887 -v896 -v903 -v905 -v906 v910 -v911 -v913 -v914 v922 -v935 -v941 -v944 -v947 -v953 -v955 -v956 -v965 -v970 -v972 -v977 -v978 v981 -v983 -v989 -v990 -v1004 -v1011 -v1033 -v1035 -v1046 -v1054 -v1055 -v1056 -v1059 v1060 -v1062 -v1064 -v1071 v1076 -v1077 -v1078 v1079 -v1080 -v1082 -v1091 -v1100 -v1101 -v1105 v1108 v1109 v1111 -v1117 -v1125 -v1130 -v1137 v1150 -v1151 -v1159 -v1160 -v1167 -v1172 -v1174 -v1178 -v1202 -v1206 -v1218 -v1223 -v1225 -v1250 -v1251 v1253 -v1257 -v1266 -v1268 -v1271 v1273 -v1274 -v1275 -v1277 -v1286 -v1295 -v1296 -v1301 -v1304 -v1306 -v1321 -v1325 -v1327 -v1331 v1332 -v1347 -v1354 -v1355 v1360 -v1367 -v1368 -v1371 v1375 -v1377 -v1378 -v1379 -v1397 -v1401 -v1404 -v1413 -v1418 -v1421 -v1423 -v1436 -v1442 v1445 -v1446 -v1449 -v1454 -v1457 v1461 -v1462 v1463 -v1466 -v1467 -v1471 v1472 v1473 -v1481 v1483 v1489 -v1490 -v1491 -v1496 -v1498 -v1499 v1500 -v1503 v1517 -v1520 -v1522 -v1529 -v1533 v1538 -v1549 -v1553 -v1558 v1562 -v1563 -v1566 -v1570 -v1572 -v1573 -v1579 -v1581 -v1599 -v1608 -v1611 -v1616 -v1617 v1621 -v1640 -v1641 -v1652 -v1656 -v1657 -v1662 -v1663 -v1664 -v1666 -v1667 -v1681 -v1682 v1686 -v1687 -v1688 -v1689 v1691 -v1694 -v1696 -v1699 -v1715 -v1717 -v1724 -v1733 -v1735 -v1736 -v1742 -v1744 -v1745 v1746 -v1747 -v1749 -v1753 -v1758 -v1761 -v1764 -v1767 -v1769 -v1770 -v1776 -v1782 -v1783 -v1784 -v1803 -v1805 v1808 -v1811 -v1814 -v1819 -v1823 -v1835 -v1836 -v1840 -v1842 -v1845 v1850 -v1852 -v1857 -v1860 -v1873 -v1880 -v1885 -v1886 -v1887 -v1888 -v1891 -v1895 -v1901 -v1905 -v1909 v1910 -v1912 -v1919 -v1930 -v1931 -v1932 -v1937 v1939 -v1940 -v1943 v1944 -v1947 -v1948 -v1949 -v1952 -v1954 -v1956 -v1958 v1959 -v1960 v1962 v1964 -v1965 -v1973 v1977 -v1982 -v1986 -v1991 -v1994 v1998 -v2000 -v2005 -v2009 -v2021 -v2027 -v2030 v2031 -v2034 -v2035 -v2037 -v2040 -v2044 -v2046 -v2051 v2052 -v2053 -v2054 -v2055 -v2056 -v2057 v2066 -v2068 -v2075 -v2076 -v2080 -v2081 -v2086 -v2089 -v2090 -v2094 -v2101 -v2102 -v2105 v2111 -v2123 -v2126 -v2127 -v2137 -v2138 -v2139 -v2142 v2143 -v2148 -v2153 -v2157 -v2158 -v2166 -v2173 -v2174 v2177 -v2193 v2205 v2216 -v2225 -v2226 -v2228 -v2229 v2232 -v2234 -v2243 -v2246 -v2251 -v2252 -v2271 -v2275 -v2281 -v2287
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.97 0.92 2/54 31874
Raw data (stat): 31874 (runsolver) R 31873 1269 1268 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 799488794 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+10.0011 s]
Raw data (loadavg): 0.93 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.0022 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.0028 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.003 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.003 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.0037 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.0039 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31877
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.013 s]
Raw data (loadavg): 1.07 0.99 0.93 2/55 31930
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.014 s]
Raw data (loadavg): 1.06 0.99 0.93 2/55 31930
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.013 s]
Raw data (loadavg): 1.05 0.99 0.93 2/55 31930
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.013 s]
Raw data (loadavg): 1.04 0.99 0.93 2/55 31930
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.013 s]
Raw data (loadavg): 1.04 0.99 0.93 2/55 31930
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.03 0.99 0.93 2/55 31930
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.013 s]
Raw data (loadavg): 1.03 0.99 0.93 2/55 31930
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.02 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.02 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.01 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.01 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.01 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.01 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.01 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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): 1.00 0.99 0.93 2/55 31932
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 31934
Raw data (stat): 31874 (vallstSAT2005PB) S 31873 1269 1268 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 799488794 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.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 31940
Raw data (stat): 31874 (vallstSAT2005PB) R 31873 1269 1268 0 -1 0 430 1842 0 0 20 4 117150 5843 21 0 1 0 799488794 2179072 249 4294967295 134512640 135087896 3221224528 3221221156 1074404950 0 0 7 1132560120 0 0 0 17 0 0 0
Raw data (statm): 532 249 485 147 0 385 0
vsize: 2128
[startup+1230.87 s]
Raw data (loadavg): 1.00 0.99 0.93 1/53 31946
Raw data (stat): 31874 (vallstSAT2005PB) R 31873 1269 1268 0 -1 0 430 1842 0 0 20 4 117150 5843 21 0 1 0 799488794 2179072 249 4294967295 134512640 135087896 3221224528 3221221156 1074404950 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): 1230.87
CPU time (s): 1230.7
CPU user time (s): 1172.11
CPU system time (s): 58.5881
CPU usage (%): 99.986
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier: FAILED
ERROR: unsatisfied constraint on line 4
#### END VERIFIER DATA ####