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-5.opb |
| MD5SUM | 6049145b9f1adfd7114adf044503d587 |
| Bench Category | optimization, small integers (OPTSMALLINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 2642 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 748 |
| Biggest coefficient in the objective function | 240 |
| Number of bits for the biggest coefficient in the objective function | 8 |
| Sum of the numbers in the objective function | 33855 |
| Number of bits of the sum of numbers in the objective function | 16 |
| Biggest number in a constraint | 240 |
| Number of bits of the biggest number in a constraint | 8 |
| Biggest sum of numbers in a constraint | 33855 |
| Number of bits of the biggest sum of numbers | 16 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1.02984 |
| Number of variables | 907 |
| Total number of constraints | 1309 |
| Number of constraints which are clauses | 126 |
| Number of constraints which are cardinality constraints (but not clauses) | 1183 |
| Number of constraints which are nor clauses,nor cardinality constraints | 0 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 134 |
Trace number 33831
#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-05-27 16:46:21 (client local time)
PB2005-SCRIPT v4.0
MARKUPS: idlaunch=3221 boxname=wulflinc1 idbench=358 idsolver=8 numberseed=0
MD5SUM SOLVER: 4b637b3b6117f2add1a6288e91336322 /oldhome/oroussel/solvers/vallstSAT2005PB.sh
MD5SUM BENCH: 6049145b9f1adfd7114adf044503d587 /oldhome/oroussel/tmp/wulflinc1/normalized-ws97-5.opb
REAL COMMAND: vallstSAT2005PB.sh /oldhome/oroussel/tmp/wulflinc1/normalized-ws97-5.opb 0
IDLAUNCH: 3221
/proc/cpuinfo:
processor : 0
vendor_id : GenuineIntel
cpu family : 6
model : 7
model name : Pentium III (Katmai)
stepping : 2
cpu MHz : 451.053
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.053
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: 681448 kB
Buffers: 27104 kB
Cached: 302344 kB
SwapCached: 760 kB
Active: 29900 kB
Inactive: 301880 kB
HighTotal: 131008 kB
HighFree: 252 kB
LowTotal: 903652 kB
LowFree: 681196 kB
SwapTotal: 2097136 kB
SwapFree: 2095360 kB
Dirty: 2636 kB
Writeback: 0 kB
Mapped: 5780 kB
Slab: 15512 kB
Committed_AS: 92684 kB
PageTables: 332 kB
VmallocTotal: 114680 kB
VmallocUsed: 1388 kB
VmallocChunk: 113256 kB
JOB ENDED THE 2005-05-27 17:06:52 (client local time) WITH STATUS 10 IN 1230.27 SECONDS
stats: 3221 6 1230.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
1:
seed: 0
Nr of vars set: 4 (#equs: 0)
Nr of vars set: 7 (#equs: 0)
#decisions: 528; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 23551 (10303:>=*);
#decisions: 532; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 662, #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: 23651 (10203:>=*);
#decisions: 542; #end-nodes: 17;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 17 / 80 (80)
#axs: 662, #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: 23750 (10104:>=*);
#decisions: 550; #end-nodes: 23;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 23 / 80 (80)
#axs: 662, #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: 23752 (10102:>=*);
#decisions: 601; #end-nodes: 53;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 53 / 80 (80)
#axs: 662, #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: 23851 (10003:>=*);
#decisions: 571; #end-nodes: 26;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 26 / 80 (80)
#axs: 662, #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: 23852 (10002:>=*);
#decisions: 617; #end-nodes: 74;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 74 / 80 (80)
#axs: 662, #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: 23950 (9904:>=*);
#decisions: 547; #end-nodes: 18;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 18 / 80 (80)
#axs: 662, #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: 23951 (9903:>=*);
#decisions: 584; #end-nodes: 41;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 41 / 80 (80)
#axs: 662, #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: 23952 (9902:>=*);
#decisions: 558; #end-nodes: 28;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 28 / 80 (80)
#axs: 662, #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: 23953 (9901:>=*);
#decisions: 23584; #end-nodes: 2474;
#proof improvement attempts: 0; #restarts: 29
Current batch, end-nodes: 47 / 87 (87)
#axs: 662, #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: 23958 (9896:>=*);
#decisions: 642; #end-nodes: 19;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 19 / 80 (80)
#axs: 662, #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: 23959 (9895:>=*);
#decisions: 718; #end-nodes: 53;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 53 / 80 (80)
#axs: 662, #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: 23960 (9894:>=*);
#decisions: 582; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 662, #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: 24059 (9795:>=*);
#decisions: 94055; #end-nodes: 11509;
#proof improvement attempts: 0; #restarts: 121
Current batch, end-nodes: 0 / 110 (110)
#axs: 662, #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: 24263 (9591:>=*);
#decisions: 550; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 662, #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: 24363 (9491:>=*);
#decisions: 547; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 662, #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: 24364 (9490:>=*);
#decisions: 553; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 662, #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: 24365 (9489:>=*);
#decisions: 558; #end-nodes: 7;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 7 / 80 (80)
#axs: 662, #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: 24465 (9389:>=*);
#decisions: 546; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 662, #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: 24466 (9388:>=*);
#decisions: 563; #end-nodes: 10;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 10 / 80 (80)
#axs: 662, #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: 24564 (9290:>=*);
#decisions: 541; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 662, #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: 24565 (9289:>=*);
#decisions: 549; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 662, #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: 24566 (9288:>=*);
#decisions: 555; #end-nodes: 5;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 5 / 80 (80)
#axs: 662, #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: 24567 (9287:>=*);
#decisions: 1308; #end-nodes: 146;
#proof improvement attempts: 0; #restarts: 1
Current batch, end-nodes: 66 / 80 (80)
#axs: 662, #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: 24659 (9195:>=*);
#decisions: 523; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 24660 (9194:>=*);
#decisions: 12759; #end-nodes: 1312;
#proof improvement attempts: 0; #restarts: 16
Current batch, end-nodes: 0 / 84 (84)
#axs: 662, #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: 24662 (9192:>=*);
#decisions: 499; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 662, #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: 24663 (9191:>=*);
#decisions: 494; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 662, #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: 24664 (9190:>=*);
#decisions: 106277; #end-nodes: 12078;
#proof improvement attempts: 0; #restarts: 126
Current batch, end-nodes: 47 / 111 (111)
#axs: 662, #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: 24761 (9093:>=*);
#decisions: 603; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 662, #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: 24762 (9092:>=*);
#decisions: 662; #end-nodes: 20;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 20 / 80 (80)
#axs: 662, #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: 24763 (9091:>=*);
#decisions: 649; #end-nodes: 37;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 37 / 80 (80)
#axs: 662, #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: 24764 (9090:>=*);
#decisions: 664; #end-nodes: 33;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 33 / 80 (80)
#axs: 662, #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: 24863 (8991:>=*);
#decisions: 623; #end-nodes: 19;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 19 / 80 (80)
#axs: 662, #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: 24962 (8892:>=*);
#decisions: 574; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 662, #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: 24963 (8891:>=*);
#decisions: 577; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 662, #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: 24964 (8890:>=*);
#decisions: 580; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 662, #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: 24965 (8889:>=*);
#decisions: 581; #end-nodes: 5;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 5 / 80 (80)
#axs: 662, #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: 24966 (8888:>=*);
#decisions: 660; #end-nodes: 57;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 57 / 80 (80)
#axs: 662, #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: 25064 (8790:>=*);
#decisions: 572; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 662, #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: 25066 (8788:>=*);
#decisions: 593550; #end-nodes: 75948;
#proof improvement attempts: 0; #restarts: 523
Current batch, end-nodes: 32 / 210 (210)
#axs: 662, #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: 25068 (8786:>=*);
#decisions: 481; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25069 (8785:>=*);
#decisions: 480; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 662, #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: 25070 (8784:>=*);
#decisions: 970115; #end-nodes: 141610;
#proof improvement attempts: 0; #restarts: 792
Current batch, end-nodes: 3 / 278 (278)
#axs: 662, #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: 25160 (8694:>=*);
#decisions: 501; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25161 (8693:>=*);
#decisions: 504; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 662, #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: 25162 (8692:>=*);
#decisions: 502; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25163 (8691:>=*);
#decisions: 564; #end-nodes: 35;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 35 / 80 (80)
#axs: 662, #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: 25164 (8690:>=*);
#decisions: 617; #end-nodes: 63;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 63 / 80 (80)
#axs: 662, #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: 25165 (8689:>=*);
#decisions: 652; #end-nodes: 76;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 76 / 80 (80)
#axs: 662, #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: 25166 (8688:>=*);
#decisions: 149696; #end-nodes: 15845;
#proof improvement attempts: 0; #restarts: 159
Current batch, end-nodes: 0 / 119 (119)
#axs: 662, #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: 25167 (8687:>=*);
#decisions: 495; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25168 (8686:>=*);
#decisions: 492; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25169 (8685:>=*);
#decisions: 576; #end-nodes: 60;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 60 / 80 (80)
#axs: 662, #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: 25170 (8684:>=*);
#decisions: 510311; #end-nodes: 66305;
#proof improvement attempts: 0; #restarts: 475
Current batch, end-nodes: 180 / 198 (198)
#axs: 662, #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: 25171 (8683:>=*);
#decisions: 6575; #end-nodes: 645;
#proof improvement attempts: 0; #restarts: 8
Current batch, end-nodes: 0 / 82 (82)
#axs: 662, #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: 25259 (8595:>=*);
#decisions: 519; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25260 (8594:>=*);
#decisions: 528; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 662, #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: 25261 (8593:>=*);
#decisions: 520; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 662, #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: 25262 (8592:>=*);
#decisions: 529; #end-nodes: 5;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 5 / 80 (80)
#axs: 662, #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: 25263 (8591:>=*);
#decisions: 529; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 662, #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: 25264 (8590:>=*);
#decisions: 581; #end-nodes: 29;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 29 / 80 (80)
#axs: 662, #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: 25265 (8589:>=*);
#decisions: 12607; #end-nodes: 1227;
#proof improvement attempts: 0; #restarts: 15
Current batch, end-nodes: 0 / 83 (83)
#axs: 662, #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: 25268 (8586:>=*);
#decisions: 517; #end-nodes: 11;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 11 / 80 (80)
#axs: 662, #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: 25269 (8585:>=*);
#decisions: 598; #end-nodes: 51;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 51 / 80 (80)
#axs: 662, #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: 25270 (8584:>=*);
#decisions: 85049; #end-nodes: 8769;
#proof improvement attempts: 0; #restarts: 95
Current batch, end-nodes: 48 / 103 (103)
#axs: 662, #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: 25271 (8583:>=*);
#decisions: 2555883; #end-nodes: 403437;
#proof improvement attempts: 0; #restarts: 1505
Current batch, end-nodes: 179 / 456 (456)
#axs: 662, #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: 25360 (8494:>=*);
#decisions: 521; #end-nodes: 1;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 1 / 80 (80)
#axs: 662, #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: 25361 (8493:>=*);
#decisions: 526; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 662, #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: 25362 (8492:>=*);
#decisions: 531; #end-nodes: 4;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 4 / 80 (80)
#axs: 662, #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: 25363 (8491:>=*);
#decisions: 572; #end-nodes: 27;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 27 / 80 (80)
#axs: 662, #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: 25364 (8490:>=*);
#decisions: 655; #end-nodes: 72;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 72 / 80 (80)
#axs: 662, #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: 25365 (8489:>=*);
#decisions: 620; #end-nodes: 61;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 61 / 80 (80)
#axs: 662, #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: 25366 (8488:>=*);
#decisions: 212439; #end-nodes: 22197;
#proof improvement attempts: 0; #restarts: 209
Current batch, end-nodes: 60 / 132 (132)
#axs: 662, #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: 25367 (8487:>=*);
#decisions: 2251900; #end-nodes: 329984;
#proof improvement attempts: 0; #restarts: 1336
Current batch, end-nodes: 275 / 414 (414)
#axs: 662, #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: 25369 (8485:>=*);
#decisions: 499; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25370 (8484:>=*);
#decisions: 61317; #end-nodes: 5916;
#proof improvement attempts: 0; #restarts: 67
Current batch, end-nodes: 7 / 96 (96)
#axs: 662, #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: 25371 (8483:>=*);
#decisions: 557; #end-nodes: 30;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 30 / 80 (80)
#axs: 662, #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: 25372 (8482:>=*);
#decisions: 580; #end-nodes: 44;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 44 / 80 (80)
#axs: 662, #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: 25373 (8481:>=*);
#decisions: 553; #end-nodes: 21;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 21 / 80 (80)
#axs: 662, #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: 25374 (8480:>=*);
#decisions: 2504706; #end-nodes: 400531;
#proof improvement attempts: 0; #restarts: 1499
Current batch, end-nodes: 13 / 454 (454)
#axs: 662, #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: 25464 (8390:>=*);
#decisions: 477; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25465 (8389:>=*);
#decisions: 480; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 662, #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: 25466 (8388:>=*);
#decisions: 487; #end-nodes: 3;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 3 / 80 (80)
#axs: 662, #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: 25467 (8387:>=*);
#decisions: 514; #end-nodes: 20;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 20 / 80 (80)
#axs: 662, #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: 25468 (8386:>=*);
#decisions: 505; #end-nodes: 13;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 13 / 80 (80)
#axs: 662, #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: 25469 (8385:>=*);
#decisions: 584; #end-nodes: 46;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 46 / 80 (80)
#axs: 662, #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: 25470 (8384:>=*);
#decisions: 635; #end-nodes: 79;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 79 / 80 (80)
#axs: 662, #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: 25471 (8383:>=*);
#decisions: 222376; #end-nodes: 23759;
#proof improvement attempts: 0; #restarts: 221
Current batch, end-nodes: 8 / 135 (135)
#axs: 662, #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: 25558 (8296:>=*);
#decisions: 484; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25559 (8295:>=*);
#decisions: 483; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25560 (8294:>=*);
#decisions: 486; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 662, #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: 25561 (8293:>=*);
#decisions: 492; #end-nodes: 5;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 5 / 80 (80)
#axs: 662, #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: 25562 (8292:>=*);
#decisions: 498; #end-nodes: 8;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 8 / 80 (80)
#axs: 662, #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: 25563 (8291:>=*);
#decisions: 563; #end-nodes: 47;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 47 / 80 (80)
#axs: 662, #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: 25564 (8290:>=*);
#decisions: 558; #end-nodes: 51;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 51 / 80 (80)
#axs: 662, #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: 25565 (8289:>=*);
#decisions: 560; #end-nodes: 42;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 42 / 80 (80)
#axs: 662, #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: 25662 (8192:>=*);
#decisions: 476; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25663 (8191:>=*);
#decisions: 475; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25664 (8190:>=*);
#decisions: 497; #end-nodes: 13;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 13 / 80 (80)
#axs: 662, #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: 25665 (8189:>=*);
#decisions: 512; #end-nodes: 27;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 27 / 80 (80)
#axs: 662, #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: 25666 (8188:>=*);
#decisions: 1503662; #end-nodes: 194741;
#proof improvement attempts: 0; #restarts: 969
Current batch, end-nodes: 67 / 322 (322)
#axs: 662, #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: 25667 (8187:>=*);
#decisions: 1504; #end-nodes: 69;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 69 / 80 (80)
#axs: 662, #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: 25668 (8186:>=*);
#decisions: 140094; #end-nodes: 13615;
#proof improvement attempts: 0; #restarts: 140
Current batch, end-nodes: 0 / 115 (115)
#axs: 662, #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: 25672 (8182:>=*);
#decisions: 465; #end-nodes: 0;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 0 / 80 (80)
#axs: 662, #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: 25673 (8181:>=*);
#decisions: 475; #end-nodes: 6;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 6 / 80 (80)
#axs: 662, #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: 25674 (8180:>=*);
#decisions: 467; #end-nodes: 2;
#proof improvement attempts: 0; #restarts: 0
Current batch, end-nodes: 2 / 80 (80)
#axs: 662, #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: 25675 (8179:>=*);
Interupt request received.
#decisions: 16104941; #end-nodes: 2735132;
#proof improvement attempts: 0; #restarts: 4369
Current batch, end-nodes: 601 / 1172 (1172)
#axs: 662, #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:) 25675 (8179:>=*)
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: 745 (#equs: 0)
Time taken: 20 min, 29 sec
times:
0m0.019s 0m0.005s
18m56.653s 1m33.185s
v v1 -v127 -v505 v640 -v774 -v4 v256 -v508 -v5 -v131 v257 -v383 v509 -v6 -v132 v258 v510 -v7 -v133 v512 v8 -v134 -v513 v388 v516 -v11 -v137 v517 -v12 v138 v518 -v14 v392 v520 -v15 -v141 v267 v521 -v16 v394 v522 -v17 -v143 v523 v18 -v396 -v524 v19 -v525 v659 v20 -v146 -v526 -v21 v273 -v527 -v22 v528 -v662 -v23 -v149 v529 -v24 v150 v530 -v25 -v151 v403 v531 -v26 v152 v532 v27 -v153 -v533 -v28 v406 -v534 -v29 v407 v535 -v30 -v156 v536 -v31 v157 v537 v32 -v158 v672 -v806 v33 -v159 -v285 -v539 -v34 v160 v540 -v287 -v413 -v36 v162 v542 -v37 v163 v543 -v38 v164 -v544 v39 -v545 v679 -v813 -v40 -v166 -v546 -v41 -v419 -v547 -v42 v168 v548 -v43 -v421 v549 -v44 v170 -v550 v551 v45 -v171 -v552 v686 -v46 -v172 -v553 -v47 v173 -v425 v554 -v48 -v174 v426 v555 -v49 v175 v556 v428 v51 -v177 -v558 -v52 -v178 v559 -v431 -v694 -v828 -v54 -v180 -v432 -v561 -v55 v433 -v562 -v56 v308 -v563 -v697 v831 v57 -v435 -v564 -v58 v436 v565 -v566 -v59 v185 -v567 v568 v60 -v569 -v703 v837 -v61 v187 -v570 -v62 -v314 -v440 -v571 v705 -v839 -v63 v189 -v572 -v64 -v316 -v573 v65 -v317 -v574 -v66 v318 -v575 v67 -v193 -v576 -v710 -v68 -v194 v320 -v577 -v711 v845 v69 -v195 -v447 -v578 v70 -v196 -v579 -v71 -v580 v714 -v72 -v198 -v581 -v73 -v582 -v74 v200 -v583 -v75 -v201 -v584 -v76 -v202 v585 v78 -v204 -v330 -v456 -v587 -v79 -v457 -v588 v722 v589 -v81 -v207 -v333 v459 -v590 -v82 -v334 -v591 -v83 -v335 v461 -v592 -v726 -v727 v861 -v85 -v211 -v594 -v728 v862 -v86 -v212 v464 -v595 -v87 -v213 -v596 -v730 v864 v88 -v214 -v597 -v89 -v467 v598 -v732 -v90 -v216 -v468 -v599 -v600 -v92 v218 -v602 -v93 -v219 -v603 -v94 -v220 -v604 -v738 v872 -v96 v222 -v606 -v349 v475 -v741 -v98 v224 -v608 -v99 -v351 -v477 -v609 -v743 v877 v226 -v744 v878 -v227 -v745 v879 -v102 -v228 v354 -v480 -v612 v103 -v229 -v355 -v481 -v613 -v104 -v614 v748 -v105 -v231 -v357 v483 -v615 -v106 -v616 -v107 -v233 -v485 -v617 -v108 v234 -v618 -v109 v235 -v619 v753 v110 -v236 -v362 -v488 -v620 -v754 v888 v756 -v890 v113 -v365 -v623 -v240 -v115 v241 -v493 -v625 v759 -v116 -v242 -v626 -v627 -v761 v895 -v117 -v495 -v628 -v118 -v370 -v630 v764 -v898 -v119 -v631 -v765 v899 -v120 -v246 -v632 -v766 v900 -v121 v373 -v633 -v122 -v374 -v500 -v634 -v123 -v635 v903 v124 -v376 -v502 -v636 -v770 v904 v771 -v905 v126 -v638 v772 -v2 -v128 -v506 -v3 -v507 v641 -v130 v642 -v776 -v643 -v777 -v384 -v644 -v778 -v645 -v779 -v259 -v646 -v780 -v260 -v386 v647 -v781 -v261 -v387 -v136 -v389 -v264 -v390 -v652 -v786 -v654 -v788 -v655 -v789 -v142 -v656 -v790 -v269 -v657 -v791 -v270 v658 -v792 -v145 -v271 -v272 -v398 v660 -v794 -v147 -v399 v661 -v795 -v148 -v400 -v275 -v663 -v797 -v276 -v402 -v664 -v798 -v277 -v665 -v799 -v278 -v404 -v666 -v800 -v279 -v405 v667 -v801 -v154 -v280 v668 -v802 -v155 -v281 -v669 -v803 -v283 -v409 -v671 -v805 -v411 -v286 -v412 -v674 -v808 -v675 -v809 -v289 -v415 -v677 -v811 -v290 -v416 v678 -v812 -v165 -v291 -v417 -v292 v680 -v814 -v294 -v420 -v682 -v816 -v169 -v683 -v817 -v296 -v422 v684 -v818 -v685 -v819 -v297 -v423 -v820 -v299 -v688 -v822 -v300 -v689 -v823 -v301 -v427 -v690 -v824 -v50 -v176 -v302 -v557 v691 -v825 -v303 -v429 v692 -v826 -v304 v430 -v693 -v827 -v53 -v179 v305 v560 v306 v695 -v829 -v181 -v696 v830 -v182 -v434 -v183 -v309 -v698 v832 -v184 -v310 -v700 v834 -v311 -v437 v701 -v835 -v702 -v836 -v186 -v312 -v438 -v313 -v439 -v704 v838 v188 -v315 -v706 v840 -v190 v442 v707 -v841 -v191 -v443 -v192 -v444 -v709 v843 -v319 -v445 v844 -v446 -v321 v846 -v322 -v448 v713 -v847 v197 -v323 -v449 -v324 v450 -v715 v849 v325 -v716 v850 -v326 -v452 -v717 v851 -v327 v453 -v718 v852 -v328 v454 -v719 -v853 v721 -v855 -v205 v331 -v856 v206 -v724 v858 -v208 v460 v337 -v463 -v338 v729 -v863 -v339 v465 -v340 -v466 v731 -v865 -v215 v341 -v866 v342 -v733 v867 -v217 -v344 v736 -v870 v345 -v471 -v737 v871 v346 -v472 v347 v739 -v873 -v348 -v740 v874 -v350 -v476 -v742 v876 v225 -v352 -v478 v353 -v479 -v746 v880 -v747 v881 -v749 v883 -v484 -v750 v884 v359 -v360 -v486 -v752 v886 -v361 -v487 -v887 -v755 v889 v238 -v490 -v491 -v757 v891 -v114 -v366 v492 -v624 -v367 -v893 v368 -v494 -v760 v894 v243 -v369 -v762 v896 -v245 v497 v372 -v498 -v247 -v499 v767 -v901 -v375 -v501 -v125 -v637 -v252 -v378 -v504 -v906 -one v9 -v10 v13 -v35 -v77 -v80 -v84 -v91 -v95 -v97 -v100 -v101 -v111 -v112 -v129 -v135 -v139 -v140 -v144 v161 v167 -v199 -v203 -v209 -v210 -v221 -v223 -v230 -v232 -v237 -v239 v244 v248 v249 -v250 -v251 -v253 -v254 v255 -v262 v263 -v265 -v266 -v268 v274 -v282 -v284 -v288 -v293 v295 v298 -v307 -v329 -v332 v336 v343 -v356 v358 v363 -v364 -v371 v377 -v379 v380 -v381 -v382 v385 -v391 -v393 v395 -v397 v401 v408 -v410 -v414 v418 -v424 -v441 -v451 v455 -v458 -v462 -v469 -v470 -v473 -v474 v482 -v489 -v496 -v503 v511 -v514 v515 -v519 -v538 v541 v586 -v593 -v601 -v605 -v607 -v610 -v611 -v621 -v622 -v629 v639 v648 -v649 -v650 -v651 v653 -v670 v673 -v676 v681 v687 -v699 v708 -v712 -v720 -v723 -v725 -v734 -v735 -v751 v758 v763 v768 -v769 -v773 -v775 -v782 -v783 -v784 -v785 -v787 -v793 -v796 -v804 -v807 -v810 -v815 -v821 -v833 -v842 -v848 -v854 -v857 v859 v860 v868 v869 v875 -v882 v885 -v892 -v897 -v902
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.92 0.95 0.90 1/55 12754
Raw data (stat): 12754 (runsolver) R 12753 8378 8377 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 742632652 884736 94 4294967295 134512640 135332820 3221224464 3221219628 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.96 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+30.001 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+40.0006 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+60.0011 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+70.0009 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+80.0017 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+90.0015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+220 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+450.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+460.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+480.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+490.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+530.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+560.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+570.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+580.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+590.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+600.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+610.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+620.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+630.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+640.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+650.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+660.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+670.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+680.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+690.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+700.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+710.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+720.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+730.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+740.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+750.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+760.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+770.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+780.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+810.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 12757
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+830.004 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 12810
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+840.004 s]
Raw data (loadavg): 1.06 0.99 0.91 2/56 12810
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+850.004 s]
Raw data (loadavg): 1.05 0.99 0.91 2/56 12810
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+860.004 s]
Raw data (loadavg): 1.04 0.99 0.91 2/56 12810
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+870.004 s]
Raw data (loadavg): 1.03 0.99 0.91 2/56 12810
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+880.004 s]
Raw data (loadavg): 1.11 1.00 0.92 2/56 12812
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+890.003 s]
Raw data (loadavg): 1.09 1.00 0.92 2/56 12812
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+900.004 s]
Raw data (loadavg): 1.24 1.04 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+910.004 s]
Raw data (loadavg): 1.20 1.03 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+920.004 s]
Raw data (loadavg): 1.17 1.03 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+930.004 s]
Raw data (loadavg): 1.14 1.03 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+940.003 s]
Raw data (loadavg): 1.12 1.03 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+950.004 s]
Raw data (loadavg): 1.10 1.03 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+960.005 s]
Raw data (loadavg): 1.08 1.03 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+970.005 s]
Raw data (loadavg): 1.07 1.03 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+980.004 s]
Raw data (loadavg): 1.06 1.02 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+990.004 s]
Raw data (loadavg): 1.05 1.02 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1000 s]
Raw data (loadavg): 1.04 1.02 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1010 s]
Raw data (loadavg): 1.04 1.02 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1020 s]
Raw data (loadavg): 1.03 1.02 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1030.01 s]
Raw data (loadavg): 1.02 1.02 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1040.01 s]
Raw data (loadavg): 1.02 1.02 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1050.01 s]
Raw data (loadavg): 1.02 1.02 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1060.01 s]
Raw data (loadavg): 1.01 1.02 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1070.01 s]
Raw data (loadavg): 1.01 1.02 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1080.01 s]
Raw data (loadavg): 1.01 1.01 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1090.01 s]
Raw data (loadavg): 1.01 1.01 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1100.01 s]
Raw data (loadavg): 1.01 1.01 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.01 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.01 0.93 2/56 12814
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.01 0.93 2/56 12816
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.01 0.93 2/56 12816
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.01 0.93 2/56 12816
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.01 0.93 2/56 12816
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.01 0.93 2/56 12816
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 12816
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 12816
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 12816
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1210.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 12816
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1220.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 12816
Raw data (stat): 12754 (vallstSAT2005PB) S 12753 8378 8377 0 -1 0 321 232 0 0 1 0 0 0 20 0 1 0 742632652 2179072 242 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0
Raw data (statm): 532 242 485 147 0 385 0
vsize: 2128
[startup+1230.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 12822
Raw data (stat): 12754 (vallstSAT2005PB) R 12753 8378 8377 0 -1 0 430 1506 0 0 22 4 113666 9322 21 0 1 0 742632652 2179072 249 4294967295 134512640 135087896 3221224528 3221221464 134743553 0 0 7 1132560120 0 0 0 17 1 0 0
Raw data (statm): 532 249 485 147 0 385 0
vsize: 2128
[startup+1230.44 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 12828
Raw data (stat): 12754 (vallstSAT2005PB) R 12753 8378 8377 0 -1 0 430 1506 0 0 22 4 113666 9322 21 0 1 0 742632652 2179072 249 4294967295 134512640 135087896 3221224528 3221221464 134743553 0 0 7 1132560120 0 0 0 17 1 0 0
Raw data (statm): 532 249 485 147 0 385 0
vsize: 0
Child status: 10
Real time (s): 1230.44
CPU time (s): 1230.27
CPU user time (s): 1136.94
CPU system time (s): 93.3258
CPU usage (%): 99.9861
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier: FAILED
ERROR: unsatisfied constraint on line 4
#### END VERIFIER DATA ####